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, 50 insertions, 62 deletions

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 4516a206f..a047c78c0 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -13,23 +13,8 @@
 (*********************************************************)
 
 Require Export ZArith_base.
-Require Export Rsyntax.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Require Export Rsyntax. Open Local Scope R_scope.
 
-V7only [
-(*********************************************************)
-(*   Compatibility                                       *)
-(*********************************************************)
-Notation sumboolT := Specif.sumbool.
-Notation leftT := Specif.left.
-Notation rightT := Specif.right.
-Notation sumorT := Specif.sumor.
-Notation inleftT := Specif.inleft.
-Notation inrightT := Specif.inright.
-Notation sigTT := Specif.sigT.
-Notation existTT := Specif.existT.
-Notation SigT := Specif.sigT.
-].
 
 (*********************************************************)
 (*               Field axioms                            *)
@@ -40,52 +25,53 @@ Notation SigT := Specif.sigT.
 (*********************************************************)
 
 (**********)
-Axiom Rplus_sym:(r1,r2:R)``r1+r2==r2+r1``.
-Hints Resolve Rplus_sym : real.
+Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
+Hint Resolve Rplus_comm: real.
 
 (**********)
-Axiom Rplus_assoc:(r1,r2,r3:R)``(r1+r2)+r3==r1+(r2+r3)``.
-Hints Resolve Rplus_assoc : real.
+Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
+Hint Resolve Rplus_assoc: real.
 
 (**********)
-Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``.
-Hints Resolve Rplus_Ropp_r : real v62.
+Axiom Rplus_opp_r : forall r:R, r + - r = 0.
+Hint Resolve Rplus_opp_r: real v62.
 
 (**********)
-Axiom Rplus_Ol:(r:R)``0+r==r``.
-Hints Resolve Rplus_Ol : real.
+Axiom Rplus_0_l : forall r:R, 0 + r = r.
+Hint Resolve Rplus_0_l: real.
 
 (***********************************************************)       
 (**       Multiplication                                   *)
 (***********************************************************)
 
 (**********)
-Axiom Rmult_sym:(r1,r2:R)``r1*r2==r2*r1``.
-Hints Resolve Rmult_sym : real v62. 
+Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
+Hint Resolve Rmult_comm: real v62. 
 
 (**********)
-Axiom Rmult_assoc:(r1,r2,r3:R)``(r1*r2)*r3==r1*(r2*r3)``.
-Hints Resolve Rmult_assoc : real v62.
+Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
+Hint Resolve Rmult_assoc: real v62.
 
 (**********)
-Axiom Rinv_l:(r:R)``r<>0``->``(/r)*r==1``.
-Hints Resolve Rinv_l : real.
+Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
+Hint Resolve Rinv_l: real.
 
 (**********)
-Axiom Rmult_1l:(r:R)``1*r==r``.
-Hints Resolve Rmult_1l : real.
+Axiom Rmult_1_l : forall r:R, 1 * r = r.
+Hint Resolve Rmult_1_l: real.
 
 (**********)
-Axiom R1_neq_R0:``1<>0``.
-Hints Resolve R1_neq_R0 : real.
+Axiom R1_neq_R0 : 1 <> 0.
+Hint Resolve R1_neq_R0: real.
 
 (*********************************************************)
 (**      Distributivity                                  *)
 (*********************************************************)
 
 (**********)
-Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``.
-Hints Resolve Rmult_Rplus_distr : real v62.
+Axiom
+  Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
+Hint Resolve Rmult_plus_distr_l: real v62.
 
 (*********************************************************)
 (**      Order axioms                                    *)
@@ -95,37 +81,38 @@ Hints Resolve Rmult_Rplus_distr : real v62.
 (*********************************************************)
 
 (**********)
-Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``).
+Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
 
 (*********************************************************)
 (**      Lower                                           *)
 (*********************************************************)
 
 (**********)
-Axiom Rlt_antisym:(r1,r2:R)``r1<r2`` -> ~ ``r2<r1``.
+Axiom Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
 
 (**********)
-Axiom Rlt_trans:(r1,r2,r3:R)
-  ``r1<r2``->``r2<r3``->``r1<r3``.
+Axiom Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
 
 (**********)
-Axiom Rlt_compatibility:(r,r1,r2:R)``r1<r2``->``r+r1<r+r2``.
+Axiom Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
 
 (**********)
-Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``.
+Axiom
+  Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
 
-Hints Resolve Rlt_antisym Rlt_compatibility Rlt_monotony : real.
+Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
 
 (**********************************************************) 
 (**      Injection from N to R                            *)
 (**********************************************************)
 
 (**********)
-Fixpoint INR [n:nat]:R:=(Cases n of
-                          O      => ``0``
-                         |(S O)  => ``1``
-                         |(S n)  => ``(INR n)+1``
-                        end).  
+Fixpoint INR (n:nat) : R :=
+  match n with
+  | O => 0
+  | S O => 1
+  | S n => INR n + 1
+  end.  
 Arguments Scope INR [nat_scope].
 
 
@@ -134,11 +121,12 @@ Arguments Scope INR [nat_scope].
 (**********************************************************)
 
 (**********)
-Definition IZR:Z->R:=[z:Z](Cases z of
-                         ZERO      => ``0``
-                        |(POS n) => (INR (convert n))
-                        |(NEG n) => ``-(INR (convert n))``
-                           end).  
+Definition IZR (z:Z) : R :=
+  match z with
+  | Z0 => 0
+  | Zpos n => INR (nat_of_P n)
+  | Zneg n => - INR (nat_of_P n)
+  end.  
 Arguments Scope IZR [Z_scope].
 
 (**********************************************************)
@@ -146,24 +134,24 @@ Arguments Scope IZR [Z_scope].
 (**********************************************************)
 
 (**********)
-Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``.
+Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
 
 (**********************************************************)
 (**      [R] Complete                                     *)
 (**********************************************************)
 
 (**********)
-Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->``x <= m``.
+Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
 
 (**********)
-Definition bound:=[E:R->Prop](ExT [m:R](is_upper_bound E m)).
+Definition bound (E:R -> Prop) :=  exists m : R | is_upper_bound E m.
 
 (**********)
-Definition is_lub:=[E:R->Prop][m:R]
-    (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->``m <= b``.
+Definition is_lub (E:R -> Prop) (m:R) :=
+  is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
 
 (**********)
-Axiom complet:(E:R->Prop)(bound E)->
-              (ExT [x:R] (E x))->
-              (sigTT R [m:R](is_lub E m)).
-
+Axiom
+  completeness :
+    forall E:R -> Prop,
+      bound E -> ( exists x : R | E x) -> sigT (fun m:R => is_lub E m).