The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Le 21 janv. 08 à 15:13, 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,
> > [...]
>
> Thanks very much--nice and easy solution! Much appreciated.
>
> Can you explain (intuitively) why a direct solution is not possible  
> (or
> more difficult?)

You can try o prove the property directly, but you will get stuck on  
the case
of transitivity.

forall a b c, ...

You then have a = true, b = false, but you do not know anything else
about c. So you would need a stronger induction hypothesis to go on.

Knowing there exists a normal form probably can be understood as
some way to strengthen the IH.

Actually, using normal forms to reason about algebraic equalities is
quite common and quite a lot of work has been devoted to this topic.

Cheers,


Benjamin