The Coq mailing list

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

Chung-Kil Hur wrote:
> In the definition, p seems to occur in positive positions at least 
> semantically.
> I don't know why coq does not accept it.
>    

Those are positive positions, but not _strictly_ positive.  I assume 
some semantics experts found a good reason to distinguish between the 
two, in the design of CIC. :)

> But there is a way to get around this problem.
>
> ======================================
> Inductive p : Prop ->  Prop :=
> | P0 : p True
> | P1 : forall a b, (p a \/ p b) ->  p (a\/b)
> | P2 : forall a b q,
>                    (forall c, q c ->  p c) ->
>                    (forall Q, ((q a) ->  Q) ->
>                               ((q b) ->  Q) ->
>                               Q) ->
>                     p (a\/b)
> ======================================
>
> I think the above definition is equivalent to your original definition.
> But, coq accepts it.
>    

This is diabolical in a way that might be easy to miss: it only works 
for [Prop], or some other impredicative universe.  In [Set] or [Type], 
it wouldn't be possible to instantiate [q] with [p], since [p] must live 
it a universe level higher than any universe quantified in its 
constructors' types.

I tried briefly to come up with an intuitive explanation of why this 
refactoring is "OK" for [Prop] but not [Set], but I failed. :)