From fdd84089a127e7f12f43a5dd02547594effd0964 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 19 Sep 2013 17:37:31 +0000
Subject: 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
---
 test-suite/failure/Uminus.v | 69 +++++++++------------------------------------
 1 file changed, 14 insertions(+), 55 deletions(-)

(limited to 'test-suite/failure')

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.
-- 
cgit v1.2.3