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, 57 insertions, 52 deletions

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index ff94d8e3b..b03ec80e8 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -30,104 +30,109 @@ Section PredExt_GuardRelChoice_imp_EM.
 (* The axiom of extensionality for predicates *)
 
 Definition PredicateExtensionality :=
-   (P,Q:bool->Prop)((b:bool)(P b)<->(Q b))->P==Q.
+  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
 
 (* From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
-Require ClassicalFacts.
+Require Import ClassicalFacts.
 
 Variable pred_extensionality : PredicateExtensionality.
   
-Lemma prop_ext : (A,B:Prop) (A<->B) -> A==B.
+Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
 Proof.
-  Intros A B H.
-  Change ([_]A true)==([_]B true).
-  Rewrite pred_extensionality with P:=[_:bool]A Q:=[_:bool]B.
-    Reflexivity.
-    Intros _; Exact H.
+  intros A B H.
+  change ((fun _ => A) true = (fun _ => B) true) in |- *.
+  rewrite
+   pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
+    reflexivity.
+    intros _; exact H.
 Qed.
 
-Lemma proof_irrel : (A:Prop)(a1,a2:A) a1==a2.
+Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
 Proof.
-  Apply (ext_prop_dep_proof_irrel_cic prop_ext).
+  apply (ext_prop_dep_proof_irrel_cic prop_ext).
 Qed.
 
 (* From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
-Require ChoiceFacts.
+Require Import ChoiceFacts.
 
 Variable rel_choice : RelationalChoice.
 
 Lemma guarded_rel_choice :
-  (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')).
 Proof.
-  Exact
-    (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
+  exact
+   (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
 Qed.
 
 (* The form of choice we need: there is a functional relation which chooses
    an element in any non empty subset of bool *)
 
-Require Bool.
+Require Import Bool.
 
 Lemma AC :
-  (EXT R:(bool->Prop)->bool->Prop |
-     (P:bool->Prop)(EX b : bool | (P b))->
-        (EX b : bool | (P b) /\ (R P b) /\ ((b':bool)(R P b')->b=b'))).
+  exists R : (bool -> Prop) -> bool -> Prop
+ | (forall P:bool -> Prop,
+      ( exists b : bool | P b) ->
+       exists b : bool | P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
 Proof.
-  Apply guarded_rel_choice with
-    P:= [Q:bool->Prop](EX y | (Q y)) R:=[Q:bool->Prop;y:bool](Q y).
-  Exact [_;H]H.
+  apply guarded_rel_choice with
+   (P := fun Q:bool -> Prop =>  exists y : _ | Q y)
+   (R := fun (Q:bool -> Prop) (y:bool) => Q y).
+  exact (fun _ H => H).
 Qed.
 
 (* The proof of the excluded middle *)
 (* Remark: P could have been in Set or Type *)
 
-Theorem pred_ext_and_rel_choice_imp_EM : (P:Prop)P\/~P.
+Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
-Intro P.
+intro P.
 
 (* first we exhibit the choice functional relation R *)
-NewDestruct AC as [R H].
+destruct AC as [R H].
 
-Pose class_of_true := [b]b=true\/P.
-Pose class_of_false := [b]b=false\/P.
+pose (class_of_true := fun b => b = true \/ P).
+pose (class_of_false := fun b => b = false \/ P).
 
 (* the actual "decision": is (R class_of_true) = true or false? *)
-NewDestruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
-Exists true; Left; Reflexivity.
-NewDestruct H0.
+destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
+exists true; left; reflexivity.
+destruct H0.
 
 (* the actual "decision": is (R class_of_false) = true or false? *)
-NewDestruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
-Exists false; Left; Reflexivity.
-NewDestruct H1.
+destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
+exists false; left; reflexivity.
+destruct H1.
 
 (* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
-Right.
-Intro HP.
-Assert Hequiv:(b:bool)(class_of_true b)<->(class_of_false b).
-Intro b; Split.
-Unfold class_of_false; Right; Assumption.
-Unfold class_of_true; Right; Assumption.
-Assert Heq:class_of_true==class_of_false.
-Apply pred_extensionality with 1:=Hequiv.
-Apply diff_true_false.
-Rewrite <- H0.
-Rewrite <- H1.
-Rewrite <- H0''. Reflexivity.
-Rewrite Heq.
-Assumption.
+right.
+intro HP.
+assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
+intro b; split.
+unfold class_of_false in |- *; right; assumption.
+unfold class_of_true in |- *; right; assumption.
+assert (Heq : class_of_true = class_of_false).
+apply pred_extensionality with (1 := Hequiv).
+apply diff_true_false.
+rewrite <- H0.
+rewrite <- H1.
+rewrite <- H0''. reflexivity.
+rewrite Heq.
+assumption.
 
 (* cases where P is true *)
-Left; Assumption.
-Left; Assumption.
+left; assumption.
+left; assumption.
 
 Qed.
 
-End PredExt_GuardRelChoice_imp_EM.
+End PredExt_GuardRelChoice_imp_EM.
\ No newline at end of file