The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

I dont't know if it helps, but if you add some notion of "value" and 
computation,


Function value (a:trm):bool :=
match a with true => Datatypes.true
| false => Datatypes.false
| or b c => Bool.orb (value b) (value c)
| and b c => Bool.andb (value b) (value c)
| not b => Bool.negb (value b)
end.

You can prove by induction the following lemma:

Lemma L1 : forall a b, equiv a b -> value a = value b.
induction 1;simpl; auto.
...
Qed.

then by discrimination, prove that ~ equiv true false.

Pierre




Edsko de Vries a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>