The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Stefan Holdermans wrote:
> > 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.
>
> That is indeed a severe restriction.

It's helpful to consider the restriction in light of how [induction] is 
implemented with proof terms.  Since [induction] looks up induction 
principles that were generated when types were defined, the relevant 
details are actually in that principle generation.  There, dependent 
[match] terms are employed, and the limitation on [induction] comes from 
the limitation of dependent [match]es that all arguments in [in] clauses 
must be variables.  This restriction is hard to relax in a non-heuristic 
way, because of the undecidability of higher-order unification.

(I've intentionally kept this explanation terse, both because some 
readers probably don't care about the details and because it is more 
instructive to poke around the formal definition of CIC based on these 
prompts than to spend time parsing a long explanation.)