coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <devriese AT cs.tcd.ie>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Dealing with equivalence classes
- Date: Tue, 5 Feb 2008 15:38:35 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
This is a rather general request for advice. In my formalization, I deal
with terms in a boolean algebra, and I have an inductive "equivalence"
relation across pairs of these terms (I asked about that before, trying
to prove that it shouldn't be proven that False was equivalent to True;
the current formalization of the boolean algebra can be found at
http://www.cs.tcd.ie/~devriese/coq/). Obviously, it is not true that
forall (a b : trm), equiv a b -> a = b
(for example, 'true' is not the same term as 'or true true'). This
however complicates the rest of the formalization; where I want to say
something like
f u ... -> g u ...
I have to say
f u ... -> equiv u v -> g v ...
It would be far nicer if I could have the property (*), above. One way
to do this would be to deal with equivalence classes instead; so the
equivalence class for 'true' is the same as the equivalence class for
'or true true'.
However, I have no experience with this at all (not to mention in a
constructive logic such as Coq) so I'm wondering how difficult this
would be, and what the best way would be to deal with this.
Any hints would be appreciated,
Thanks,
Edsko
- [Coq-Club] Dealing with equivalence classes, Edsko de Vries
- [Coq-Club] Re: Dealing with equivalence classes,
Adam Megacz
- Re: [Coq-Club] Re: Dealing with equivalence classes,
Edsko de Vries
- Re: [Coq-Club] Re: Dealing with equivalence classes, Arnaud Spiwack
- [Coq-Club] Re: Dealing with equivalence classes, Adam Megacz
- Re: [Coq-Club] Re: Dealing with equivalence classes, Edsko de Vries
- Re: [Coq-Club] Re: Dealing with equivalence classes,
Edsko de Vries
- [Coq-Club] Re: Dealing with equivalence classes,
Adam Megacz
Archive powered by MhonArc 2.6.16.