The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

AUGER Cédric wrote:
> Consider the following "inductive".
>
> Inductive p : Prop ->  Prop :=
> | P0 : p True
> | P1 : forall a b, (p a \/ p b) ->  p (a\/b)
> | P2 : forall a b, (forall Q, ((p a) ->  Q) ->
>                                ((p b) ->  Q) ->
>                                Q) ->
>                     p (a\/b)
> .
>
> (It won't compile for positivity reasons)
>
> For me, either P1 and P2 should be both accepted, or they should be
> both refused, since P2 use the elimination principle of \/.
>
> In fact P1 is accepted, but not P2.
>
> I would be very surprised to learn that P2 is trully "unsound" whereas
> P1 is "sound". Is there some particular reasons not to be compatible
> with an elimination principle?
>    

A key fact here is that [\/] is desugared to a use of another inductive 
family [or], while [->] is a built-in operation associated with the 
positivity condition.  Your definition of [p] makes it a _nested_ 
inductive type, where, in the definition of [p], you refer to family 
[or] with at least one occurrence of [p] in its parameters.  Here the 
checking rule is to make a specialized copy of [or] and consider it 
declared as mutually inductive with [p].  At that point, you apply the 
normal rules, where it is easy to see that omitting constructor [P2] 
gives a strictly positive definition.

In contrast, [P2] clearly violates the positivity rule.  I'm not sure 
what is your basis for deciding that [P2] can't break consistency, but 
it's far from obvious to me.  It's easy to see how allowing 
non-strictly-positive occurrences can break consistency for considerably 
simpler examples; I give such an example somewhere in CPDT.