## Stream: Coq users

### Topic: What do I do with Setoid equality?

#### Ignat Insarov (Jun 19 2021 at 09:12):

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.
``````

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]

#### Li-yao (Jun 19 2021 at 11:30):

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.

#### Li-yao (Jun 19 2021 at 11:34):

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.

#### Ignat Insarov (Jun 19 2021 at 11:50):

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

#### Li-yao (Jun 19 2021 at 12:37):

yes, it's a good general rule

#### Ignat Insarov (Jun 19 2021 at 12:54):

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?

#### Alexander Gryzlov (Jun 19 2021 at 17:08):

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.

#### Li-yao (Jun 19 2021 at 18:00):

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`.

#### Ignat Insarov (Jun 19 2021 at 19:35):

Is this documented somewhere?

#### Ignat Insarov (Jun 19 2021 at 19:37):

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

#### Ignat Insarov (Jun 19 2021 at 19:37):

I gather this equivalence is hard wired into `rewrite` and other tactics?

#### Li-yao (Jun 19 2021 at 20:04):

Is this documented somewhere?