The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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?