The Coq mailing list

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

Hi,

I have formalized Huntington's postulates (commutativity,
distributivity, identity, complement, and the closure and structural
rules) and proven the most common derived properties; the full
development can be found at

  http://www.cs.tcd.ie/~devriese/coq

Unfortunately, I need the following axiom:

  Axiom true_false_distinct : ~ equiv true false.

(where 'equiv' is the equivalence relation resulting from Huntington's
postulates). Now, Huntington actually needs this axiom too, but that is
because he needs to stipulate that 'true' and 'false' are two distinct
elements in the boolean algebra. Since 'true' and 'false' in my
formalization are two constructors for the 'trm' inductive datatype (and
therefore provably distinct), I feel that I should be able to *prove*
true_false_distinct from the postulates--but all my attempts so far have
failed. I think I need to strengthen the lemma to be able to prove
true_false_distinct, but I'm not sure how. Any advice would be
appreciated!

Thanks,

Edsko