The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi,

You can introduce a new object equal to [f t] and perform the
induction on this object instead. This is essentially a way of adding
(before you start the induction) the dependency you were losing :

Theorem mt : forall t u : term, App(f(t),f(u)) ->^*  f(App(t,u))).
Proof.
  intros.
  remember (f t) as h.
  induction h.
  (* now Heqh links [f t] to the destructed object *)
  ...

You will then have to perform case analysis on [t] again if you want
to deduce something about [t] itself, which means that your function
should be somewhat inversible.

Hope this helps,

S.

On Tue, May 11, 2010 at 4:49 AM, Flavio L. C. de Moura
<flaviomoura AT unb.br>
 wrote:
> -----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-----
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06