diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 17:37:31 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 17:37:31 +0000 |
commit | fdd84089a127e7f12f43a5dd02547594effd0964 (patch) | |
tree | 4070d8a969e6287a0094540d91bd24a1dc195eb6 /test-suite/failure | |
parent | ea4180b729f90630941b5501ef83f94b6c8ecd6b (diff) |
Uminus.v : prepare this test file for the use of Fail
- Highlight the fact that the line defining "up" is the one which
should fail.
- Factor code with stdlib's Hurkens.v
- This way, this test could become a "shouldnotfail" test by placing
two final "Fail" (before the definitions of "up" and "paradox").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/Uminus.v | 69 |
1 files changed, 14 insertions, 55 deletions
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v index 3c3bf3753..d96c1e8f9 100644 --- a/test-suite/failure/Uminus.v +++ b/test-suite/failure/Uminus.v @@ -1,62 +1,21 @@ (* Check that the encoding of system U- fails *) -Inductive prop : Prop := down : Prop -> prop. - -Definition up (p:prop) : Prop := let (A) := p in A. - -Lemma p2p1 : forall A:Prop, up (down A) -> A. -Proof. -exact (fun A x => x). -Qed. +Require Hurkens. -Lemma p2p2 : forall A:Prop, A -> up (down A). -Proof. -exact (fun A x => x). -Qed. - -(** Hurkens' paradox *) - -Definition V := forall A:Prop, ((A -> prop) -> A -> prop) -> A -> prop. -Definition U := V -> prop. -Definition sb (z:V) : V := fun A r a => r (z A r) a. -Definition le (i:U -> prop) (x:U) : prop := - x (fun A r a => i (fun v => sb v A r a)). -Definition induct (i:U -> prop) : Prop := - forall x:U, up (le i x) -> up (i x). -Definition WF : U := fun z => down (induct (z U le)). -Definition I (x:U) : Prop := - (forall i:U -> prop, up (le i x) -> up (i (fun v => sb v U le x))) -> False. +Inductive prop : Prop := down : Prop -> prop. -Lemma Omega : forall i:U -> prop, induct i -> up (i WF). -Proof. -intros i y. -apply y. -unfold le, WF, induct. -intros x H0. -apply y. -exact H0. -Qed. +(* Coq should reject the following access of a Prop buried inside + a prop. *) -Lemma lemma1 : induct (fun u => down (I u)). -Proof. -unfold induct. -intros x p. -intro q. -apply (q (fun u => down (I u)) p). -intro i. -apply q with (i := fun y => i (fun v:V => sb v U le y)). -Qed. +Definition up (p:prop) : Prop := let (A) := p in A. -Lemma lemma2 : (forall i:U -> prop, induct i -> up (i WF)) -> False. -Proof. -intro x. -apply (x (fun u => down (I u)) lemma1). -intros i H0. -apply (x (fun y => i (fun v => sb v U le y))). -apply H0. -Qed. +(* Otherwise, we would have a proof of False via Hurkens' paradox *) -Theorem paradox : False. -Proof. -exact (lemma2 Omega). -Qed. +Definition paradox : False := + Hurkens.NoRetractFromSmallPropositionToProp.paradox + prop + down + up + (fun (A:Prop) (x:up (down A)) => (x:A)) + (fun (A:Prop) (x:A) => (x:up (down A))) + False. |