The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Stefan Holdermans wrote:
> Finally, I'd like to establish the following theorem:
>
> Theorem T : forall a n, Q a (S n) -> Q a (S (S n)).
>
> I would have guessed that, given the lemma L, the proof of T would 
> amount to a routine induction on a derivation of Q a (S n) for 
> arbitrary a and n. However, brazenly starting with
>
> Proof.
> intros a n Hq. induction Hq.
>
> Coq gives me the following hypotheses and subgoal for the case for 
> q_base:
>
> n : nat
> m : nat
> n0 : nat
> H : P m n0
> ============================
> Q (base m) (S n0)
>
> And so I'm stuck! I would have expected some evidence of n0 = S n or 
> perhaps just H : P m (S n) and the goal Q (base m) (S (S n)).
>
> Could someone explain the experienced behaviour? Am I missing 
> something obvious and is there a straightforward workaround?

This is one of the most common problems in getting started with Coq. 
[induction] only works over predicates applied to arguments that are all 
variables. In your case, one of the arguments is [S n]. I would prefer 
that Coq signal an error in this case. Instead, the current [induction] 
implementation replaces each complex term with a fresh variable, 
forgetting structural details.

My usual tack is to restate the theorem as a lemma where all the 
arguments to the predicate to be inducted over really are variables. You 
usually achieve this by introducing new auxiliary variables and relating 
these to the predicate arguments using new equality hypotheses.