Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 90 insertions, 85 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 699051ec1..192603273 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -18,64 +18,66 @@
    though definite description conflicts with classical logic *)
 
 Definition RelationalChoice :=
- (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')))).
+  forall (A B:Type) (R:A -> B -> Prop),
+    (forall x:A,  exists y : B | R x y) ->
+     exists R' : A -> B -> Prop
+    | (forall x:A,
+          exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition FunctionalChoice :=
- (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))).
+  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)).
 
 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 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].
-NewDestruct (Descr A B R') as [f H1].
-Intro x.
-Elim (H0 x); Intros y [H2 [H3 H4]]; Exists y; Split; [Exact H3 | Exact H4].
-Exists f; Intro x.
-Elim (H0 x); Intros y [H2 [H3 H4]].
-Rewrite <- (H4 (f x) (H1 x)).
-Exact H2.
+  forall (A B:Type) (R:A -> B -> Prop),
+    (forall x:A,  exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) ->
+     exists f : A -> B | (forall x:A, R x (f x)).
+
+Lemma description_rel_choice_imp_funct_choice :
+ ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
+intros Descr RelCh.
+red in |- *; intros A B R H.
+destruct (RelCh A B R H) as [R' H0].
+destruct (Descr A B R') as [f H1].
+intro x.
+elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
+exists f; intro x.
+elim (H0 x); intros y [H2 [H3 H4]].
+rewrite <- (H4 (f x) (H1 x)).
+exact H2.
 Qed.
 
-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].
-Exists [x,y]y=(f x).
-Intro x; Exists (f x);
-Split; [Apply H0| Split;[Reflexivity| Intros y H1; Symmetry; Exact H1]].
+Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
+intros FunCh.
+red in |- *; intros A B R H.
+destruct (FunCh A B R H) as [f H0].
+exists (fun x y => y = f x).
+intro x; exists (f x); split;
+ [ apply H0
+ | split; [ reflexivity | intros y H1; symmetry  in |- *; exact H1 ] ].
 Qed.
 
-Lemma funct_choice_imp_description : 
-  FunctionalChoice->ParamDefiniteDescription.
-Intros FunCh.
-Red; Intros A B R H.
-NewDestruct (FunCh A B R) as [f H0].
+Lemma funct_choice_imp_description :
+ FunctionalChoice -> ParamDefiniteDescription.
+intros FunCh.
+red in |- *; intros A B R H.
+destruct (FunCh A B R) as [f H0].
 (* 1 *)
-Intro x.
-Elim (H x); Intros y [H0 H1].
-Exists y; Exact H0.
+intro x.
+elim (H x); intros y [H0 H1].
+exists y; exact H0.
 (* 2 *)
-Exists f; Exact H0.
+exists f; exact H0.
 Qed.
 
 Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
-  FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
-Split.
-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).
+ FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
+split.
+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.
 
 (* We show that the guarded relational formulation of the axiom of Choice
@@ -83,52 +85,55 @@ Qed.
    independance of premises or proof-irrelevance *)
 
 Definition GuardedRelationalChoice :=
- (A:Type;B:Type;P:A->Prop;R: A->B->Prop) 
-  ((x:A)(P x)->(EX y:B|(R x y)))
-   -> (EXT R':A->B->Prop | 
-        ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))).
+  forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
+    (forall x:A, P x ->  exists y : B | R x y) ->
+     exists R' : A -> B -> Prop
+    | (forall x:A,
+         P x ->
+          exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
-Definition ProofIrrelevance := (A:Prop)(a1,a2:A) a1==a2.
+Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
-Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : 
-  RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
+Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
+ RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
 Proof.
-Intros rel_choice proof_irrel.
-Red; Intros A B P R H.
-NewDestruct (rel_choice ? ? [x:(sigT ? P);y:B](R (projT1 ? ? x) y)) as [R' H0].
-Intros [x HPx].
-NewDestruct (H x HPx) as [y HRxy].
-Exists y; Exact HRxy.
-Pose R'':=[x:A;y:B](EXT H:(P x) | (R' (existT ? P x H) y)).
-Exists R''; Intros x HPx.
-NewDestruct (H0 (existT ? P x HPx)) as [y [HRxy [HR'xy Huniq]]].
-Exists y. Split.
-  Exact HRxy.
-  Split.
-    Red; Exists HPx; Exact HR'xy.
-    Intros y' HR''xy'.
-      Apply Huniq.
-      Unfold R'' in HR''xy'.
-      NewDestruct HR''xy' as [H'Px HR'xy'].
-      Rewrite proof_irrel with a1:=HPx a2:=H'Px.
-      Exact HR'xy'.
+intros rel_choice proof_irrel.
+red in |- *; intros A B P R H.
+destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
+intros [x HPx].
+destruct (H x HPx) as [y HRxy].
+exists y; exact HRxy.
+pose (R'' := fun (x:A) (y:B) =>  exists H : P x | R' (existT P x H) y).
+exists R''; intros x HPx.
+destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
+exists y. split.
+  exact HRxy.
+  split.
+    red in |- *; exists HPx; exact HR'xy.
+    intros y' HR''xy'.
+      apply Huniq.
+      unfold R'' in HR''xy'.
+      destruct HR''xy' as [H'Px HR'xy'].
+      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px).
+      exact HR'xy'.
 Qed.
 
 Definition IndependenceOfPremises :=
- (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)).
+  forall (A:Type) (P:A -> Prop) (Q:Prop),
+    (Q ->  exists x : _ | P x) ->  exists x : _ | Q -> P x.
 
 Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
-  RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
+ RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
 Proof.
-Intros RelCh IndPrem.
-Red; Intros A B P R H.
-NewDestruct (RelCh A B [x,y](P x)->(R x y)) as [R' H0].
-  Intro x. Apply IndPrem.
-    Apply H.
-  Exists R'.
-  Intros x HPx.
-    NewDestruct (H0 x) as [y [H1 H2]].
-    Exists y. Split. 
-      Apply (H1 HPx).
-      Exact H2.
-Qed.
+intros RelCh IndPrem.
+red in |- *; intros A B P R H.
+destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
+  intro x. apply IndPrem.
+    apply H.
+  exists R'.
+  intros x HPx.
+    destruct (H0 x) as [y [H1 H2]].
+    exists y. split. 
+      apply (H1 HPx).
+      exact H2.
+Qed.
\ No newline at end of file