The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Edsko de Vries 
<devriese AT cs.tcd.ie>
 writes:
> 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'.

You might find Add Relation, Setoid, and Ring helpful.

  Require Import Setoid.
  Require Import Ring.
  Require Import Ring_tac.

Your definition makes it easy to convince Coq that equiv is in fact an
equivalence relation:

  Add Relation trm equiv
    reflexivity  proved by refl
    symmetry     proved by sym
    transitivity proved by trans
    as equiv_relation.

Assuming you are able to show that or/and/not are equiv-respecting
morphisms:

  Add Morphism or with signature equiv ==> equiv ==> equiv as or_morphism.
    Admitted.
  Add Morphism and with signature equiv ==> equiv ==> equiv as and_morphism.
    Admitted.
  Add Morphism not with signature equiv ==> equiv as not_morphism.
    Admitted.

you'll be able to use rewrite on terms consisting of equiv and those
morphisms:

  Lemma complement_unique : (* ... *)
    intros.
    assert(equiv a'' (or a'' a')).
    rewrite <- (id_or a'').
    rewrite <- H0.
    rewrite distr_or.
    (* ... *)

You may also benefit from the fact that boolean algebras are rings,
starting like this (although I didn't go very far with it).

  (* symmetric difference *)
  Definition plus := fun a b => or (and a (not b)) (and (not a) b).

  Add Morphism plus with signature equiv ==> equiv ==> equiv as plus_morphism.
    Admitted.

  Theorem GoodsteinRingTheory :
    ring_theory false true plus and (fun x y => plus x (not y)) not equiv.
    Admitted.
  Add Ring AR : GoodsteinRingTheory.

This should let you use the ring_simplify tactic on values of type trm.

  - a