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.

- are my definitions correct or is there another way to structure things?
- 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.
Admitted.
Lemma equiv_class_impl_lexord: forall l l',
{l}≃ ⪯/≃ {l'}≃ -> l ⪯ l'.
Proof.
intros.
Admitted.
```

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

`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.
}
apply lexord_cons in bad.
destruct bad as [bad _].
apply le_S_n in bad.
inversion bad.
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]`

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

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

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

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`

)

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.

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

```
```

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`

does ` {l}≃ ⪯/≃ {l'}≃`

mean "lift `⪯`

to equivalence classes, and apply it to the classes for `l`

and `l'`

"?

this suggests that `⪯`

respects `≃`

, and then this lemma would disappear entirely

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.

you probably do have to encode " ⪯ respects ≃" by saying that `⪯`

is proper over `≃`

— sth like `Proper (≃ ==> ≃ ==> iff) ⪯)`

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

instance

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