The Coq mailing list

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

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?)

Edsko