The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Dear Chlipala,

Thanks for your prompt reply... But it still annoys me to not be able to match the concrete examples to the formal definition - that means I do not understand the formal definition well... precisely I do not see how to fill in the "???" part here:  

The first case, r = 1 and n = 0:

C (for [cons]) ≡ (∀ A:Set, A → List A → List A) ≡ ∀ A:Set, (List A ???)                      

The second case, r = 0 and n = 1:

C (for [cons]) ≡ (∀ A:Set, A → List A → List (A*A)) ≡ ∀ List:Set→Set, (List ???)

Thank you very much and best regards

Tie 

On Thu, May 5, 2011 at 11:36 PM, Adam Chlipala <adam AT chlipala.net> wrote:

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.