Stream: math-comp users

Topic: equivalence classes of fingraph

view this post on Zulip Evgeniy Moiseenko (Dec 23 2021 at 13:42):

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?

view this post on Zulip Christian Doczkal (Jan 01 2022 at 12:11):

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.

view this post on Zulip Evgeniy Moiseenko (Jan 08 2022 at 14:55):

@Christian Doczkal
looks like equivalence_partition is exactly what I need, thank you!

Last updated: Feb 02 2023 at 15:04 UTC