coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] Positivity and Elimination Principle, AUGER Cédric
- Re: [Coq-Club] Positivity and Elimination Principle,
Adam Chlipala
- Re: [Coq-Club] Positivity and Elimination Principle,
Chung-Kil Hur
- Re: [Coq-Club] Positivity and Elimination Principle,
Adam Chlipala
- Re: [Coq-Club] Positivity and Elimination Principle, Chung-Kil Hur
- Re: [Coq-Club] Positivity and Elimination Principle, AUGER Cédric
- Re: [Coq-Club] Positivity and Elimination Principle,
Adam Chlipala
- Re: [Coq-Club] Positivity and Elimination Principle,
Jean-Francois Monin
- Re: [Coq-Club] Positivity and Elimination Principle,
AUGER Cédric
- Re: [Coq-Club] Positivity and Elimination Principle, Adam Chlipala
- Re: [Coq-Club] Positivity and Elimination Principle,
AUGER Cédric
- Re: [Coq-Club] Positivity and Elimination Principle,
Chung-Kil Hur
- Re: [Coq-Club] Positivity and Elimination Principle,
Adam Chlipala
Archive powered by MhonArc 2.6.16.