The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Note that this restriction is only for the occurrences of the inductive
type in the *conclusion* of the type of each constructor. A parameter
can still vary in the type of the arguments (so called non-uniform
parameters).

A usual example:

Inductive powlist (A : Type) :=
| pownil
| powcons (a : A) (l : powlist (A * A)) : powlist A.

Maxime.

On 01/22/2015 05:53 PM, Pierre Courtieu wrote:
> Hi,
>
> Note that if you put n as a non-parameter argument of ge, the
> definition is accepted.
>
> Inductive ge: nat -> nat -> Prop :=
> | ge_n : forall n, ge n n
> | ge_S : forall n m:nat, ge n m -> ge (S n) m.
>
> This is explained in section "Parametrized inductive types" of section
> 1.3.3 of reference manual. Putting n as a parameter as you did
> (putting it before the ":") forces it to be "rigid", i.e.:
> "Parameters differ from inductive type annotations in the fact that
> the conclusion of each type of constructor termi invoke the inductive
> type with the *same values* of parameters as its specification."
>
> You may want to rigidify the second argument, but it is not possible
> without changing the order of the arguments, which explains why it is
> "le" that is defined by an inductive in the standard library, ge being
> defined as its symmetric.
>
> Best regards,
> Pierre
>
>
> 2015-01-22 17:06 GMT+01:00 Matej Kosik
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com>:
>> Hello,
>>
>> While reading Section 4.5.3 of the Reference Manual (Well-formed inductive 
>> definitions)
>> and while going through the standard library, I have try to define this:
>>
>>   (* a superfluous definition of "ge" predicate *)
>>   Inductive ge (n:nat) : nat -> Prop :=
>>     | ge_n : ge n n
>>     | ge_S : forall m:nat, ge n m -> ge (S n) m.
>>
>> Coq rejects that definition with a message:
>>
>>   Error: Last occurrence of "ge" must have "n" as 1st argument in
>>   "forall m : nat, ge n m -> ge (S n) m".
>>
>> That is somewhat surprising because the definition (despite being 
>> superfluous in practise) seems plausible to me.
>>
>> If I may, I would like to ask:
>> - which side-condition of the W-Ind rule (?) the definition above breaks?
>> - why that kind of restriction must be enforced?