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, 63 insertions, 74 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 9f6217320..932db000f 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -31,62 +31,55 @@ Set Implicit Arguments.
 Section Berardis_paradox.
 
 (** Excluded middle *)
-Hypothesis EM : (P:Prop) P \/ ~P.
+Hypothesis EM : forall P:Prop, P \/ ~ P.
 
 (** Conditional on any proposition. *)
-Definition IFProp := [P,B:Prop][e1,e2:P]
-  Cases (EM B) of
-    (or_introl _) => e1
-  | (or_intror _) => e2
+Definition IFProp (P B:Prop) (e1 e2:P) :=
+  match EM B with
+  | or_introl _ => e1
+  | or_intror _ => e2
   end.
 
 (** Axiom of choice applied to disjunction.
     Provable in Coq because of dependent elimination. *)
-Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop)
-  ( B -> (Q e1))->
-  (~B -> (Q e2))->
-  (Q (IFProp B e1 e2)).
+Lemma AC_IF :
+ forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
+   (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
 Proof.
-Intros P B e1 e2 Q p1 p2.
-Unfold IFProp.
-Case (EM B); Assumption.
+intros P B e1 e2 Q p1 p2.
+unfold IFProp in |- *.
+case (EM B); assumption.
 Qed.
 
 
 (** We assume a type with two elements. They play the role of booleans.
     The main theorem under the current assumptions is that [T=F] *)
-Variable Bool: Prop.
-Variable T: Bool.
-Variable F: Bool.
+Variable Bool : Prop.
+Variable T : Bool.
+Variable F : Bool.
 
 (** The powerset operator *)
-Definition pow [P:Prop] :=P->Bool.
+Definition pow (P:Prop) := P -> Bool.
 
 
 (** A piece of theory about retracts *)
 Section Retracts.
 
-Variable A,B: Prop.
+Variables A B : Prop.
 
-Record retract : Prop := {
-    i: A->B;
-    j: B->A;
-    inv: (a:A)(j (i a))==a
-  }.
+Record retract : Prop := 
+  {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
 
-Record retract_cond : Prop := {
-    i2: A->B;
-    j2: B->A;
-    inv2: retract -> (a:A)(j2 (i2 a))==a
-  }.
+Record retract_cond : Prop := 
+  {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
 
 
 (** The dependent elimination above implies the axiom of choice: *)
-Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a.
+Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
 Proof.
-Intros r.
-Case r; Simpl.
-Trivial.
+intros r.
+case r; simpl in |- *.
+trivial.
 Qed.
 
 End Retracts.
@@ -96,75 +89,71 @@ End Retracts.
     which is provable in classical logic ( => is already provable in
     intuitionnistic logic). *)
 
-Lemma L1 : (A,B:Prop)(retract_cond (pow A) (pow B)).
+Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
 Proof.
-Intros A B.
-Elim (EM (retract (pow A) (pow B))).
-Intros (f0, g0, e).
-Exists f0 g0.
-Trivial.
-
-Intros hf.
-Exists ([x:(pow A); y:B]F) ([x:(pow B); y:A]F).
-Intros; Elim hf; Auto.
+intros A B.
+elim (EM (retract (pow A) (pow B))).
+intros [f0 g0 e].
+exists f0 g0.
+trivial.
+
+intros hf.
+exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F).
+intros; elim hf; auto.
 Qed.
 
 
 (** The paradoxical set *)
-Definition U := (P:Prop)(pow P).
+Definition U := forall P:Prop, pow P.
 
 (** Bijection between [U] and [(pow U)] *)
-Definition f : U -> (pow U) :=
-  [u](u U).
+Definition f (u:U) : pow U := u U.
 
-Definition g : (pow U) -> U :=
-  [h,X]
-    let lX = (j2 (L1 X U)) in
-    let rU = (i2 (L1 U U)) in
-    (lX (rU h)).
+Definition g (h:pow U) : U :=
+  fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).
 
 (** We deduce that the powerset of [U] is a retract of [U].
     This lemma is stated in Berardi's article, but is not used
     afterwards. *)
-Lemma retract_pow_U_U : (retract (pow U) U).
+Lemma retract_pow_U_U : retract (pow U) U.
 Proof.
-Exists g f.
-Intro a.
-Unfold f g; Simpl.
-Apply AC.
-Exists ([x:(pow U)]x) ([x:(pow U)]x).
-Trivial.
+exists g f.
+intro a.
+unfold f, g in |- *; simpl in |- *.
+apply AC.
+exists (fun x:pow U => x) (fun x:pow U => x).
+trivial.
 Qed.
 
 (** Encoding of Russel's paradox *)
 
 (** The boolean negation. *)
-Definition Not_b := [b:Bool](IFProp b==T F T).
+Definition Not_b (b:Bool) := IFProp (b = T) F T.
 
 (** the set of elements not belonging to itself *)
-Definition R : U := (g ([u:U](Not_b (u U u)))).
+Definition R : U := g (fun u:U => Not_b (u U u)).
 
 
-Lemma not_has_fixpoint : (R R)==(Not_b (R R)).
+Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
-Unfold 1 R.
-Unfold g.
-Rewrite AC with r:=(L1 U U) a:=[u:U](Not_b (u U u)).
-Trivial.
-Exists ([x:(pow U)]x) ([x:(pow U)]x); Trivial.
+unfold R at 1 in |- *.
+unfold g in |- *.
+rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
+trivial.
+exists (fun x:pow U => x) (fun x:pow U => x); trivial.
 Qed.
 
 
-Theorem classical_proof_irrelevence : T==F.
+Theorem classical_proof_irrelevence : T = F.
 Proof.
-Generalize not_has_fixpoint.
-Unfold Not_b.
-Apply AC_IF.
-Intros is_true is_false.
-Elim is_true; Elim is_false; Trivial.
-
-Intros not_true is_true.
-Elim not_true; Trivial.
+generalize not_has_fixpoint.
+unfold Not_b in |- *.
+apply AC_IF.
+intros is_true is_false.
+elim is_true; elim is_false; trivial.
+
+intros not_true is_true.
+elim not_true; trivial.
 Qed.
 
-End Berardis_paradox.
+End Berardis_paradox.
\ No newline at end of file