From 06146b5dc90529a6ece19d689a0c41f9d5dea4d5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Oct 2003 14:42:51 +0000
Subject: 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
---
 theories/Logic/ClassicalChoice.v | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 theories/Logic/ClassicalChoice.v

(limited to 'theories')

diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
new file mode 100644
index 0000000000..b7fb6845a0
--- /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.
-- 
cgit v1.2.3