The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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