Consider this example:

```
From Coq Require Import ZArith.
From Coq Require Import MSets.MSets.
Import MSetProperties.
Open Scope Z_scope.
Module SetOfℤ := Make (Z_as_OT). Import SetOfℤ.
Module PropertiesOfSetOfℤ := WPropertiesOn Z_as_OT SetOfℤ. Import PropertiesOfSetOfℤ.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )).
Theorem theorem₁: {1; 1} = {1; 1; 1}.
cut (In 1 {1; 1}).
* intro. apply add_equal in H. symmetry.
(* H : Equal {1; 1; 1} {1; 1} *)
(* ============================ *)
(* {1; 1; 1} = {1; 1} *)
give_up.
* apply add_spec. left. reflexivity.
Admitted.
```

As you see, I am having a difficulty proving something that looks like it should prove itself. Should I accept that my sets are `Equal`

, but not `Logic.eq`

, and reformulate my theorem with the former kind of equality? What is going on here, overall? [I am trying to read this section of the reference, but it is not helping.][1]

[1]: https://coq.inria.fr/refman/proofs/writing-proofs/rewriting.html

Should I accept that my sets are Equal, but not Logic.eq, and reformulate my theorem with the former kind of equality?

Yes.

MSets are internally represented as balanced trees, and multiple trees can represent the same set. The `eq`

relation differentiates between those trees, so it's not what you want to use to reason about MSets, and that's why you need to rely on a different equivalence relation.

In this particular case though, they are singletons, so they are unique, but MSets also contain a well-formedness proof, which is opaque. You can (1) prove that they are equal, (2) reimplement everything without opaque proofs, (3) admit the proof irrelevance axiom; but it's all a lot of work for a corner case that doesn't generalize to other sets.

Thanks! So is it right to say that for every setoid I should use its own notion of equivalence to formulate my results?

yes, it's a good general rule

So if you could elucidate for me what is a _«registered setoid equality»_, as mentioned in the link above? In this case, how can I find out that `Equal`

is a special entity with respect to `MSet`

s? Is it, actually, treated in a special way by Coq? How can I _«register»_ an equality for my own stuff?

[This write up makes an impression that there is an ongoing disaster about this topic…][1]

[1]: https://gist.github.com/Blaisorblade/78441b030a7c0e20ab1242c8e6662db6

It's not so much a disaster, but a known limitation of intensional type theories, and one of the motivations for developing theories with a more flexible equality, like HoTT.

what is a «registered setoid equality»

I'm not sure of the internal details but in practice it means there are instances of certain classes available, a sufficient condition being an instance of `Equivalence`

.

Is this documented somewhere?

This looks like the thing, but the comments are brief: <https://coq.github.io/doc/v8.13/stdlib/Coq.Classes.Equivalence.html>.

I gather this equivalence is hard wired into `rewrite`

and other tactics?

Is this documented somewhere?

There is a chapter about setoid rewriting to start from: https://coq.inria.fr/refman/addendum/generalized-rewriting.html

But it presents a bespoke set of commands which I found quite unwieldly compared to manipulating type classes directly (but that presumes being familiar with type classes already).

Thanks!

Last updated: Jun 18 2024 at 21:01 UTC