The Coq mailing list

[Ezra Cooper <e.e.k.cooper AT sms.ed.ac.uk>]

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


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.