The Coq mailing list

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

Dear Ezra,

Thank you for the help! In fact, your suggestion to *generalize* gave me 
the light that was missing to finish the proof!

Cheers,

Flávio.

Ezra Cooper escreveu:
> Flavio L. C. de Moura wrote:
> > Hello,
> >
> >    This is probably a simple question, but I didn't manage to solve 
> > it...
> >    I have a binary predicate, say my_pred n t. The first argument is 
> > a natural and the second is an term of inductive type. In the 
> > induction step I get an expression of the form my_pred (n+1) t' where 
> > t' is simpler than t, and hence I can apply the induction hypothesis, 
> > but the induction hypothesis refers to the expression my_pred n t'. 
> > In a paper and pencil proof this step is trivial, but how can I 
> > instruct Coq to apply the induction hypothesis correctly?
> > Thank you in advance! 
>
>
> Presumably you are doing induction on t, so that the induction 
> hypothesis already refers to a simpler term t'. So the problem is just 
> to *generalize* for the argument n--is that right?
>
> The typical solution to this is to reorder the quantifiers in your 
> goal. If you start with
>
>  Goal
>    forall n t, my_pred n t.
>  induction t.
>
> then Coq will implicitly introduce all the quantified variables 
> preceding t, in this case just "intro n", and thus the inductive 
> hypotheses are working with some *particular*, unknown n. If you 
> reorder them like so:
>
>  Goal
>    forall t n, my_pred n t.
>  induction t.
>
> then Coq will not need to introduce n and it will remain quantified 
> (i.e. general) in the inductive hypothesis.
>
> HTH,
> Ezra