The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Fri, 20 Jan 2012 09:18:51 -0500,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

> 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. :)


I tried to do the proof of equivalence;
it is interesting to note that the version using the elimination
has a friendlier generated induction principle, since in the "a∨b"
using version, I had to force things using "fix".
------------------------------------------------------------------

Inductive r : Prop -> Prop :=
| P0 : r True
| P2 : forall a b q,
                  (forall c, q c -> r c) ->
                  (forall Q, ((q a) -> Q) ->
                             ((q b) -> Q) ->
                             Q) ->
                   r (a\/b)
.

Inductive p : Prop ->  Prop :=
| R0 : p True
| R1 : forall a b, (p a \/ p b) ->  p (a\/b).

Goal forall Q, r Q <-> p Q.
split; intros.
induction H; [left|right].
apply X; firstorder.
revert Q H.
refine (fix proof (Q:Prop) (pq:p Q) : r Q :=
        match pq in p q return r q with
        | R0 => P0
        | R1 a b (or_introl H) => _ (proof _ H)
        | R1 a b (or_intror H) => _ (proof _ H)
        end);
clear proof.
right with r; auto.
right with r; auto.
Qed.

=======================================================
Now for the impredicative stuff that Adam said,
I succeed in doing:
-------------------------------------------------------
Definition X:=Type.
Definition Y:X := Type.

Inductive ors (A B:Y) : Y :=
| or_introls : A -> ors A B
| or_intrors : B -> ors A B
.

Inductive ps : Y ->  Y :=
| Rs0 : ps (unit:Set)
| Rs1 : forall (a b: Set), (ors (ps a) (ps b)) ->  ps (ors a b).

Inductive rs : Y -> Y :=
| Ps0 : rs (unit:Set)
| Ps2 : forall (a b: Set) (q:Set->Set),
                          (forall (c:Set), q c -> rs c) ->
                          (forall (Q:Set), ((q a) -> Q) ->
                                           ((q b) -> Q) ->
                                           Q) ->
                          rs (ors a b)
.
======================================================
I know it is not impredicative, but when I try to turn
things impredicative, it fails (of course), but even
for the one using "a∨b"; so we cannot say that this
trick is "diabolical", since we couldn't produce the
instance we want to remove the inductive from…
------------------------------------------------------

Inductive ors (A B:Set) : Set :=
| or_introls : A -> ors A B
| or_intrors : B -> ors A B
.

Inductive ps : Set ->  Set :=
| Rs0 : ps (unit:Set)
| Rs1 : forall (a b: Set), (ors (ps a) (ps b)) ->  ps (ors a b).

Inductive rs : Set -> Set :=
| Ps0 : rs (unit:Set)
| Ps2 : forall (a b: Set) (q:Set->Set),
                          (forall (c:Set), q c -> rs c) ->
                          (forall (Q:Set), ((q a) -> Q) ->
                                           ((q b) -> Q) ->
                                           Q) ->
                          rs (ors a b)
.