MAJ

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

1 files changed, 18 insertions, 13 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 2a501eca0..d0798d7a2 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -11,28 +11,29 @@
 (* We show that the functional formulation of the axiom of Choice
    (usual formulation in type theory) is equivalent to its relational
    formulation (only formulation of set theory) + the axiom of
-   (parametric) finite description (aka as axiom of unique choice) *)
+   (parametric) definite description (aka axiom of unique choice) *)
 
 (* This shows that the axiom of choice can be assumed (under its
    relational formulation) without known inconsistency with classical logic,
-   though finite description conflicts with classical logic *)
+   though definite description conflicts with classical logic *)
 
 Definition RelationalChoice :=
- (A:Type;B:Set;R: A->B->Prop) 
+ (A:Type;B:Type;R: A->B->Prop) 
   ((x:A)(EX y:B|(R x y)))
    -> (EXT R':A->B->Prop | 
          ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))).
 
 Definition FunctionalChoice :=
- (A:Type;B:Set;R: A->B->Prop)
+ (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))).
 
-Definition ParamFiniteDescription :=
- (A:Type;B:Set;R: A->B->Prop)
+Definition ParamDefiniteDescription :=
+ (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))).
 
-Lemma lem1 : ParamFiniteDescription->RelationalChoice->FunctionalChoice.
+Lemma description_rel_choice_imp_funct_choice : 
+  ParamDefiniteDescription->RelationalChoice->FunctionalChoice.
 Intros Descr RelCh.
 Red; Intros A B R H.
 NewDestruct (RelCh A B R H) as [R' H0].
@@ -45,7 +46,8 @@ Rewrite <- (H4 (f x) (H1 x)).
 Exact H2.
 Qed.
 
-Lemma lem2 : FunctionalChoice->RelationalChoice.
+Lemma funct_choice_imp_rel_choice : 
+  FunctionalChoice->RelationalChoice.
 Intros FunCh.
 Red; Intros A B R H.
 NewDestruct (FunCh A B R H) as [f H0].
@@ -54,7 +56,8 @@ Intro x; Exists (f x);
 Split; [Apply H0| Split;[Reflexivity| Intros y H1; Symmetry; Exact H1]].
 Qed.
 
-Lemma lem3 : FunctionalChoice->ParamFiniteDescription.
+Lemma funct_choice_imp_description : 
+  FunctionalChoice->ParamDefiniteDescription.
 Intros FunCh.
 Red; Intros A B R H.
 NewDestruct (FunCh A B R) as [f H0].
@@ -66,9 +69,11 @@ Exists y; Exact H0.
 Exists f; Exact H0.
 Qed.
 
-Theorem FunChoice_Equiv_RelChoice_and_ParamFinDescr :
-  FunctionalChoice <-> RelationalChoice /\ ParamFiniteDescription.
+Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
+  FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
 Split.
-Intro H; Split; [Exact (lem2 H) | Exact (lem3 H)].
-Intros [H H0]; Exact (lem1 H0 H).
+Intro H; Split; [
+  Exact (funct_choice_imp_rel_choice H)
+ | Exact (funct_choice_imp_description H)].
+Intros [H H0]; Exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.