The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello,

The first line of your definition has n as a fixed given nat:
it is the expected to define what is, for any other nat i,
to be such that ge n i.
But your last line relates (S n) to some nat instead of n.
Tehrefore n should not be fixed from the beginning and 
you should try a definition starting with
Inductive ge : nat -> nat -> Prop :=

Jean-Francois

On Thu, Jan 22, 2015 at 04:06:02PM +0000, Matej Kosik wrote:
> 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?