## Stream: Coq users

### Topic: Working with equivalence classes/quotients

#### Lef Ioannidis (Jul 22 2023 at 16:21):

Although I often work with quotients of an equivalence class in pen-and-paper, I have never used this proof technique in Coq.
A little googling brings up a lot of literature about Quotient types, but what I really want is much simpler I think.

I wrote some simple definitions of lexicographic ordering over lists, set equivalence of lists (ignore repetition) and then trying to take the quotient of list ordering over sets. I am stuck on even the simple example though.

1. are my definitions correct or is there another way to structure things?
2. is there any support in the standard (or non-standard) Coq library for this common idiom?

How would you go about these proofs, or maybe you have done something similar already and can share your experience?

``````From Coq Require Import List RelationClasses.
Import ListNotations.
Local Open Scope list_scope.

Reserved Notation "a ⪯ b" (at level 82, left associativity).
Inductive lexord: list nat -> list nat -> Prop :=
| PreRec: forall h h' ts ts',
h <= h' ->
ts ⪯ ts' ->
h :: ts ⪯ h' :: ts'
| PreBase: forall l,
[] ⪯ l
where "a ⪯ b" := (lexord a b).

Goal [1;2] ⪯ [1;3;3].
repeat apply PreRec; auto.
apply PreBase.
Qed.

Definition seteq: list nat -> list nat -> Prop :=
fun l1 l2 => forall x, In x l1 <-> In x l2.

Instance Equiv_seteq: Equivalence seteq.
Proof.
constructor; constructor; eauto; edestruct H.
- eauto.
- eauto.
- edestruct H0; eauto with trans.
- edestruct H0; eauto with trans.
Qed.

Notation "a ≃ b" := (seteq a b) (at level 82, left associativity).

Notation ListClass := (list nat -> Prop).
Definition seteq_class: list nat -> ListClass :=
fun l l' => l ≃ l'.

Notation "{ a }≃" := (seteq_class a) (at level 81).

Definition quotient_lexord_seteq : ListClass -> ListClass -> Prop :=
fun a b => forall l l', a l -> b l' -> l ⪯ l'.
Notation "a ⪯/≃ b" := (quotient_lexord_seteq a b) (at level 83, left associativity).

Goal {[1;2]}≃ ⪯/≃ {[1;3]}≃.
Proof.
intros.
unfold quotient_lexord_seteq, seteq_class, seteq.
intros.

Lemma equiv_class_impl_lexord: forall l l',
{l}≃ ⪯/≃ {l'}≃ -> l ⪯ l'.
Proof.
intros.
``````

#### Gaëtan Gilbert (Jul 22 2023 at 17:05):

what coq version is this supposed to be? I get error ` No such Hint database: trans.`

#### Gaëtan Gilbert (Jul 22 2023 at 17:14):

``````Goal {[1;2]}≃ ⪯/≃ {[1;3]}≃.
``````

this is false:

``````Goal {[1;2]}≃ ⪯/≃ {[1;3]}≃ -> False.
Proof.
intros.
red in H. unfold seteq_class in H;simpl in H.
assert (bad : [2;1] ⪯ [1;3]).
{ apply H.
-  intros n;split;simpl;tauto.
- reflexivity.
}
Qed.
``````

also note that ListClass is not the type of quotients of seteq (how could it be, it doesn't mention seteq or anything related to it), for instance it contains `fun l => l = [1;2]`

#### Paolo Giarrusso (Jul 22 2023 at 19:10):

The usual approach in Coq is to use setoids — you never build quotient types or equivalence classes, you just build relations, and prove functions respect them

#### Julien Puydt (Jul 22 2023 at 21:45):

A canonical simple example of such an approach would be nice, as I think this question turns up quite often.

#### Pierre Castéran (Jul 23 2023 at 06:27):

There is a small example on abelian monoids, where an exponentiation fonction is proved to
respect the property of commutativity.
The repo is on Coq-community. It was made to illustrate the tutorial written in 2012 by Matthieu and me.
May be pdf should be updated, and moved to Coq-community ?

The example of proper exponentiation algorithms is developed further in pages 275-329 of this tutorial

#### Karl Palmskog (Jul 23 2023 at 08:19):

if Matthieu agrees, I suggest moving the LaTeX sources of the tutorial from 2012 to Coq-community, and we could set up CI so it's built as a PDF and deployed to GitHub Pages (e.g., `https://coq-community.org/coq-art/typeclassestut.pdf`)

#### Pierre Castéran (Jul 23 2023 at 08:27):

We could also replace the `alltt`blocks with Alectryon snippets as in the Hydra Battles doc.
I hope I can try do do it within a week.

#### Lef Ioannidis (Jul 26 2023 at 16:01):

Thank you for the answers, @Gaëtan Gilbert thanks for the clever counter-example.

With regards to Setoids, I have used them in terms of generalized rewriting but it never clicked to me they are equivalence classes.
Would it be possible to translate some of the terms from equiv classes to setoids, for example even if I write the setoid instance for ListClass
I don't know what the lemma

``````
``````

#### Paolo Giarrusso (Jul 26 2023 at 17:32):

the essential change is that instead of using `=` on the quotient set `your_carrier / your_equivalence_relation`, you never define anything corresponding to `your_carrier / your_equivalence_relation`, and just use `your_equivalence_relation` on elements of `your_carrier`

#### Paolo Giarrusso (Jul 26 2023 at 17:34):

does ` {l}≃ ⪯/≃ {l'}≃` mean "lift `⪯` to equivalence classes, and apply it to the classes for `l` and `l'`"?

#### Paolo Giarrusso (Jul 26 2023 at 17:34):

this suggests that `⪯` respects `≃`, and then this lemma would disappear entirely

#### Paolo Giarrusso (Jul 26 2023 at 17:35):

if `⪯` didn't respect `≃`, then you might need to define a variant that does by hand on the original carrier — but again, your statement suggests it's not the case here.

#### Paolo Giarrusso (Jul 26 2023 at 17:36):

you probably do have to encode " ⪯ respects ≃" by saying that `⪯` is proper over `≃` — sth like `Proper (≃ ==> ≃ ==> iff) ⪯)`

#### Paolo Giarrusso (Jul 26 2023 at 17:37):

I forget, but it might be better to phrase that using a `subrelation` instance

#### Lef Ioannidis (Jul 27 2023 at 13:23):

This explanation is very helpful, thank you @Paolo Giarrusso for taking the time to write it. Perhaps this kind of compare-and-contrast between quotients and setoids should be in the tutorial.

Last updated: Jun 23 2024 at 04:03 UTC