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: Apr 14 2024 at 11:02 UTC