Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 17 insertions, 7 deletions

diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index bb846aa6..f99d65eb 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalUniqueChoice.v 10170 2007-10-03 14:41:25Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** This file provides classical logic and unique choice; this is
     weaker than providing iota operator and classical logic as the
@@ -15,11 +16,11 @@
     be used to build functions outside the scope of a theorem proof) *)
 
 (** Classical logic and unique choice, as shown in
-    [ChicliPottierSimpson02], implies the double-negation of
+    [[ChicliPottierSimpson02]], implies the double-negation of
     excluded-middle in [Set], hence it implies a strongly classical
     world. Especially it conflicts with the impredicativity of [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
@@ -43,13 +44,14 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The following proof comes from [ChicliPottierSimpson02] *)
+(** The following proof comes from [[ChicliPottierSimpson02]] *)
 
 Require Import Setoid.
 
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Theorem classic_set_in_prop_context :
+  forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-intro HnotEM.
+intros C HnotEM.
 set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
 assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
 apply unique_choice.
@@ -80,4 +82,12 @@ destruct (f P).
     discriminate.
     assumption.
 Qed.
- 
+
+Corollary not_not_classic_set :
+  ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+apply classic_set_in_prop_context.
+Qed.
+
+(* Compatibility *)
+Notation classic_set := not_not_classic_set (only parsing).