The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tie Cheng wrote:
> According to the manual, an inductive definition Ind(Γ)(ΓI:=ΓC ) 
> admits r inductive parameters if each type of constructors (c:C) in ΓC 
> is such that
>
> C≡ ∀ p1:P1,…,∀ pr:Pr,∀ a1:A1, … ∀ an:An, (I p1 … pr t1… tq)
>
> with I one of the inductive definitions in ΓI. We say that q is the 
> number of real arguments of the constructor c.
>
> The following List definition has 1 parameter:
>
> Ind()(List:Set→Set:=nil:(∀ A:Set, List A), cons : (∀ A:Set, A → List A 
> → List A) )
>
> But the following definition has 0 parameter:
>
> Ind()(List:Set→Set:=nil:(∀ A:Set, List A), cons : (∀ A:Set, A → List 
> A → List (A*A)) )
>
> What puzzles me is why the second definition has 0 parameter (unlike 
> the first definition), actually I do not think I understand how to 
> represent each of their constructors in form of ≡ ∀ p1:P1,…,∀ pr:Pr,∀ 
> a1:A1, … ∀ an:An, (I p1 … pr t1… tq) to see their "r"...

Completely formal definitions of rules like this can be hard to follow.  
Here are two attempts at more intuitive explanations.

The first will only make sense if you already understand sections in 
Coq: Parameters are those arguments to the inductive family that could 
just as well have been made variables in a section, rather than binding 
them explicitly in the definition of the inductive family or its 
constructors.  (Actually, relatively recent versions of Coq support 
non-uniform parameters, which make my explanation technically 
inaccurate, but it could still be a useful starting point. :])

Alternate explanation: Parameters are arguments to the inductive family 
that are instantiated in a particular boring, uniform way in each 
constructor.  That is, in the final part of each constructor's type, the 
parameter is instantiated directly from one of the arguments to the 
constructor.  The key benefit of the use of parameters, as opposed to 
normal arguments, is that parameters are treated more simply in 
dependent pattern matching, and so they are treated more simply in the 
derived induction principles, too.  If you haven't run into these issues 
yet, then it could definitely appear that the notion of "parameter" is 
quite baroque!

For your particular example, it's pretty easy to see why the definitions 
are classified as they are: The first definition copies the single 
argument to [List] directly from an argument for each of [nil] and 
[cons].  The second definition assigns a type to [cons] that _computes_ 
the argument to [List] in a more complicated way than copying it from an 
argument to the constructor.  This computation disqualifies the single 
argument to [List] from being a parameter.

If you still don't understand how these are instances of the general 
constructor template you mentioned, I suggest simplifying the template 
knowing that r = 1 and n = 0 in the first case, and r = 0 and n = 1 in 
the second case.