The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,
You may also want to use functional induction if the induction you
need folows the structure of f.

The usual way is to define f using Function and then:

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

You also have functional inversion to deduce things from hypothesis of
the form (f a) = t where t contains constructors.

Hope this helps.

Pierre Courtieu

Le 11 mai 2010 08:59, Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>
 a écrit :
> 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
>
>