Ignat Insarov (Jun 19 2021 at 09:12): 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.
* 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
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 MSets? Is it, actually, treated in a special way by Coq? How can I _«register»_ an equality for my own stuff?
Ignat Insarov (Jun 19 2021 at 12:57):[This write up makes an impression that there is an ongoing disaster about this topic…][1]
[1]: https://gist.github.com/Blaisorblade/78441b030a7c0e20ab1242c8e6662db6
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?
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).
Ignat Insarov (Jun 19 2021 at 20:32):Thanks!
Last updated: Sep 30 2023 at 06:01 UTC