The Coq mailing list

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

Edsko de Vries a écrit :

On Mon, Jan 21, 2008 at 02:40:40PM +0100, Pierre Casteran wrote:
  

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.
    

Thanks very much--nice and easy solution! Much appreciated.

Can you explain (intuitively) why a direct solution is not possible (or
more difficult?)
  

Well I didn't find another solution.  Defining some help function (as "value") for proving
some proposition is quite common in Coq (for instance tactics like discriminate were (still are?)
built on such argument). Another way of thinking is to consider what could be an invariant
of equiv : the simplest one I found was "having the same boolean value".

Perhaps there is some simpler one, but I think it must consider a notion of "value" or
"normal form". I tried to prove by induction that if equiv a b and a and b are in normal form
(i.e. equal to true or false) then a and b are equal, butI got lost very quickly :-( .

Pierre

Edsko