1 files changed, 25 insertions, 13 deletions
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 5a633f84..bb8186ae 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -6,28 +6,40 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalChoice.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
+(*i $Id: ClassicalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
-(** This file provides classical logic and functional choice *)
+(** 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 extends ClassicalUniqueChoice.v with the axiom of choice.
+    As ClassicalUniqueChoice.v, it implies the double-negation of
+    excluded-middle in [Set] and leads to a classical world populated
+    with non computable functions. Especially it conflicts with the
+    impredicativity of [Set], knowing that [true<>false] in [Set].  *)
 
-Require Export ClassicalDescription.
+Require Export ClassicalUniqueChoice.
 Require Export RelationalChoice.
 Require Import ChoiceFacts.
 
+Set Implicit Arguments.
+
+Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.
+
+Theorem singleton_choice :
+  forall (A : Type) (P : A->Prop),
+  (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x.
+Proof.
+intros A P H.
+destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')).
+exists (R' tt); firstorder.
+Qed.
+
 Theorem choice :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A, exists y : B, R x y) ->
-    exists f : A -> B, (forall x:A, R x (f x)).
+ forall (A B : Type) (R : A->B->Prop),
+   (forall x : A, exists y : B, R x y) ->
+    exists f : A->B, (forall x : A, R x (f x)).
 Proof.
 intros A B.
 apply description_rel_choice_imp_funct_choice.
-exact (description A B).
+exact (unique_choice A B).
 exact (relational_choice A B).
 Qed.