Hello!
How can I construct a list of equivalence classes of finite equivalence relation using fingraph.v
library?
Context (T : finType) (e : rel T).
Hypothesis (erefl : reflexive e).
Hypothesis (esym : symmetric e).
Hypothesis (etrans : transitive e).
Definition eqv_clss : seq (pred E) (* or : seq (seq E) *) :=
... (* what should I write here? *)
I can see the definition of roots
which should give me a list of representatives for each class.
Using it I came up to the following definition:
Definition eqv_clss : seq (pred E) :=
[seq (e r) | r <- enum (roots e) ].
Is there a simpler definition? Or, perhaps, the fingraph.v
already has some tools to handle this problem and I just overlooked it?
It depends on whether you added any axioms to Coq or not. If you have functional or predicate extensionality, then your list of equivalence classes is probably fine. Otherwise, you will not be able to check (in the boolean sense) membership in this list.
Depending on your use case, I would recommend using partitions (i.e., sets of sets) rather than lists of predicates. This way you get extensionality for free. Look for the partition
predicate and the equivalence_partition
construction.
@Christian Doczkal
looks like equivalence_partition
is exactly what I need, thank you!
Last updated: Mar 28 2024 at 21:01 UTC