The Coq mailing list

["Daniel R. Grayson" <drg AT illinois.edu>]

You seem to be right:

    Inductive even : nat -> Type :=
       | even_0 : even O
       | even_SS : forall n:nat, even n -> even (S (S n)).
    Print All.

    even_rect : 
    forall P : forall n : nat, even n -> Type,
    P 0 even_0 ->
    (forall (n : nat) (e : even n), P n e -> P (S (S n)) (even_SS n e)) ->
    forall (n : nat) (e : even n), P n e

    even_case : 
    forall P : forall n : nat, even n -> Type,
    P 0 even_0 ->
    (forall (n : nat) (e : even n),          P (S (S n)) (even_SS n e)) ->
    forall (n : nat) (e : even n), P n e


On Nov 8, 2011, at 9:23 AM, Adam Chlipala wrote:

> Daniel R. Grayson wrote:
>> The trunk generates one more inductive principle than 8.3 did, but the new 
>> one
>> (*_case) seems often to be the same as one of the old ones (*_rect).  The
>> reference manual doesn't explain its purpose.  Can anyone clarify?
>>  
> 
> I'm guessing the new principle is for case analysis, not induction, based 
> on its name.  Have you tested recursive definitions to see if the "case" 
> principles indeed omit inductive hypotheses?