The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Neil Ghani wrote:
> 1. I've been trying to write down an induction principle for the 
> initial algebra of any functor, ie type operator with map operation. I 
> know Coq generates induction principles for some functors and I 
> wondered if it can generate an induction principle for any functor or 
> if there are limitations on the class of functors for which induction 
> principles can be generated.
>
> 2. What are the principles underlying the induction principles Coq 
> generates? I believe they are added as axioms every time an inductive  
> data type is declared. Do they just look right or are they proven to 
> be correct in a mathematical sense? If the later, could I get a 
> response with a reference please?

I hope my answer to #2 sheds light on the issues behind #1.

No, no axioms are added.  Induction principle generation is only a 
convenience; each principle is a recursive function definition in CIC.  
After writing an inductive definition for type [foo], try running [Print 
foo_ind.].  Some inductive types have useful principles that aren't 
generated automatically;  for instance, mutually-inductive types (which 
the [Scheme] command handles) and nested types (like inductive types [T] 
defined in terms of [list T], for which it's helpful to manually define 
a principle in terms of a predicate that describes when another 
predicate holds of every element of a list).

So now I guess I do get to answering #1: the limitations on induction 
come directly from the validity rules for recursive function 
definitions.  I'm not sure of the best reference to a definitive 
treatment of the formal rules.  The Coq manual tries to give an 
intuition, at least, of which definitions are accepted.