Fichier offrant l'axiome du choix en presence de logique classique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4723 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 35 insertions, 0 deletions

diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
new file mode 100644
index 000000000..b7fb6845a
--- /dev/null
+++ b/theories/Logic/ClassicalChoice.v
@@ -0,0 +1,35 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i logic: "-strongly-classical" i*)
+
+(*i $Id$ i*)
+
+(** This file provides classical logic and functional choice *)
+
+(** This file extends ClassicalDescription.v with the axiom of choice.
+    As ClassicalDescription.v, it implies the double-negation of
+    excluded-middle in Set and implies a strongly classical
+    world. Especially it conflicts with impredicativity of Set, knowing
+    that true<>false in Set.
+
+    This file and all files depending on it require option -strongly-classical
+*)
+
+Require Export ClassicalDescription.
+Require Export RelationalChoice.
+Require ChoiceFacts.
+
+Theorem choice : 
+ (A:Type;B:Type;R: A->B->Prop)
+  ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))).
+Proof.
+Apply description_rel_choice_imp_funct_choice.
+Exact description.
+Exact relational_choice.
+Qed.