The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Coq users,

 I would like to prove a theorem about lambda-terms, for a given
recursive function f : term -> term. The theorem in Coq-like notation is:

  Theorem mt : forall t u : term, App(f(t),f(u)) ->^*  f(App(t,u))).

The proof on paper is done by induction on f(t), but in Coq it didn't
work because I lose the relation between f(t) (in the left of the
reduction) and t (in the right of the reduction). For the var case, for
example, the function f is defined by f(x) = x; when I apply induction
(which is not the one that comes with Coq) I need to proof that
App(x,f(u)) ->^*  f(App(t,u)) which is not true because the t on the
right of the reduction has nothing to do with the x on the left any
more. But, in fact, they are equal!

Maybe I need a stronger induction... or maybe I just don't know how to
do it in Coq...

Any help, or comments is very well welcome.

Best regards,
Flávio.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.15 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkvoxc4ACgkQJ9M3XSenoWhBTACg1wARXtYnw2AzVD/kglRmHHvV
hpwAoMw9hwXo+j+WHVKCUAZ251NP0DR2
=4BXw
-----END PGP SIGNATURE-----