Ajout exists! et restructuration/extension des fichiers sur la

description et le choix


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

1 files changed, 24 insertions, 12 deletions

diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 5b347b1be..51f1b3eff 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -8,26 +8,38 @@
 
 (*i $Id$ 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.