1 files changed, 76 insertions, 0 deletions
diff --git a/theories7/Logic/ClassicalDescription.v b/theories7/Logic/ClassicalDescription.v
new file mode 100644
index 00000000..85700c22
--- /dev/null
+++ b/theories7/Logic/ClassicalDescription.v
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: ClassicalDescription.v,v 1.2.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
+
+(** This file provides classical logic and definite description *)
+
+(** Classical logic and definite description, as shown in [1],
+    implies the double-negation of excluded-middle in Set, hence it
+    implies a strongly classical world. Especially it conflicts with
+    impredicativity of Set, knowing that true<>false in Set.
+
+    [1] 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.
+*)
+
+Require Export Classical.
+
+Axiom dependent_description :
+  (A:Type;B:A->Type;R: (x:A)(B x)->Prop)
+  ((x:A)(EX y:(B x)|(R x y)/\ ((y':(B x))(R x y') -> y=y')))
+   -> (EX f:(x:A)(B x) | (x:A)(R x (f x))).
+
+(** Principle of definite descriptions (aka axiom of unique choice) *)
+
+Theorem description :
+  (A:Type;B:Type;R: A->B->Prop)
+  ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y')))
+   -> (EX f:A->B | (x:A)(R x (f x))).
+Proof.
+Intros A B.
+Apply (dependent_description A [_]B).
+Qed.
+
+(** The followig proof comes from [1] *)
+
+Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False.
+Proof.
+Intro HnotEM.
+Pose R:=[A,b]A/\true=b \/ ~A/\false=b.
+Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))).
+Apply description.
+Intro A.
+NewDestruct (classic A) as [Ha|Hnota].
+  Exists true; Split.
+    Left; Split; [Assumption|Reflexivity].
+    Intros y [[_ Hy]|[Hna _]].
+      Assumption.
+      Contradiction.
+  Exists false; Split.
+    Right; Split; [Assumption|Reflexivity].
+    Intros y [[Ha _]|[_ Hy]].
+      Contradiction.
+      Assumption.
+NewDestruct H as [f Hf].
+Apply HnotEM.
+Intro P.
+Assert HfP := (Hf P).
+(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
+NewDestruct (f P).
+  Left.
+  NewDestruct HfP as [[Ha _]|[_ Hfalse]].
+    Assumption.
+    Discriminate.
+  Right.
+  NewDestruct HfP as [[_ Hfalse]|[Hna _]].
+    Discriminate.
+    Assumption.
+Qed.
+