Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Positivity and Elimination Principle

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Positivity and Elimination Principle


chronological Thread 
  • From: AUGER Cédric <Cedric.Auger AT lri.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Positivity and Elimination Principle
  • Date: Fri, 20 Jan 2012 12:26:58 +0100

Hi all, I encountered something that I found strange at first glance.

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?



Archive powered by MhonArc 2.6.16.

Top of Page