Ajout d'une syntaxe pour Reals.

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

1 files changed, 18 insertions, 47 deletions

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 2297e7d7b..21ab28be8 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -7,31 +7,9 @@
 (*********************************************************)
 
 Require Export ZArith.
+Require Export Rsyntax.
 Require Export TypeSyntax.
 
-Parameter R:Type.
-Parameter R0:R.
-Parameter R1:R.
-Parameter Rplus:R->R->R.
-Parameter Rmult:R->R->R.
-Parameter Ropp:R->R.
-Parameter Rinv:R->R. 
-Parameter Rlt:R->R->Prop.    
-Parameter up:R->Z.
-(*********************************************************)
-
-(**********)
-Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
-
-(**********)
-Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
-
 (*********************************************************)
 (*       Field axioms                                   *)
 (*********************************************************)
@@ -40,18 +18,17 @@ Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
 (*********************************************************)
 
 (**********)
-Axiom Rplus_sym:(r1,r2:R)((Rplus r1 r2)==(Rplus r2 r1)).
+Axiom Rplus_sym:(r1,r2:R)``r1+r2==r2+r1``.
 
 (**********)
-Axiom Rplus_assoc:(r1,r2,r3:R)
-  ((Rplus (Rplus r1 r2) r3)==(Rplus r1 (Rplus r2 r3))).
+Axiom Rplus_assoc:(r1,r2,r3:R)``(r1+r2)+r3==r1+(r2+r3)``.
 
 (**********)
-Axiom Rplus_Ropp_r:(r:R)((Rplus r (Ropp r))==R0).
+Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``.
 Hints Resolve Rplus_Ropp_r : real v62.
 
 (**********)
-Axiom Rplus_ne:(r:R)(((Rplus r R0)==r)/\((Rplus R0 r)==r)).
+Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``.
 Hints Resolve Rplus_ne : real v62.
 
 (***********************************************************)       
@@ -59,19 +36,18 @@ Hints Resolve Rplus_ne : real v62.
 (***********************************************************)
 
 (**********)
-Axiom Rmult_sym:(r1,r2:R)((Rmult r1 r2)==(Rmult r2 r1)).
+Axiom Rmult_sym:(r1,r2:R)``r1*r2==r2*r1``.
 Hints Resolve Rmult_sym : real v62. 
 
 (**********)
-Axiom Rmult_assoc:(r1,r2,r3:R)
-  ((Rmult (Rmult r1 r2) r3)==(Rmult r1 (Rmult r2 r3))).
+Axiom Rmult_assoc:(r1,r2,r3:R)``(r1*r2)*r3==r1*(r2*r3)``.
 Hints Resolve Rmult_assoc : real v62.
 
 (**********)
-Axiom Rinv_l:(r:R)(~(r==R0))->((Rmult (Rinv r) r)==R1).
+Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``.
 
 (**********)
-Axiom Rmult_ne:(r:R)(((Rmult r R1)==r)/\((Rmult R1 r)==r)).
+Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``.
 Hints Resolve Rmult_ne : real v62.
 
 (**********)
@@ -82,8 +58,7 @@ Axiom R1_neq_R0:(~R1==R0).
 (*********************************************************)
 
 (**********)
-Axiom Rmult_Rplus_distr:(r1,r2,r3:R)
-  ((Rmult r1 (Rplus r2 r3))==(Rplus (Rmult r1 r2) (Rmult r1 r3))).
+Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``.
 Hints Resolve Rmult_Rplus_distr : real v62.
 
 (*********************************************************)
@@ -94,27 +69,24 @@ Hints Resolve Rmult_Rplus_distr : real v62.
 (*********************************************************)
 
 (**********)
-Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT (Rlt r1 r2) (r1==r2)) 
-                                   (Rgt r1 r2)).
+Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``).
 
 (*********************************************************)
 (*       Lower                                           *)
 (*********************************************************)
 
 (**********)
-Axiom Rlt_antisym:(r1,r2:R)(Rlt r1 r2) -> ~(Rlt r2 r1).
+Axiom Rlt_antisym:(r1,r2:R)``r1<r2`` -> ~ ``r2<r1``.
 
 (**********)
 Axiom Rlt_trans:(r1,r2,r3:R)
-  (Rlt r1 r2)->(Rlt r2 r3)->(Rlt r1 r3).
+  ``r1<r2``->``r2<r3``->``r1<r3``.
 
 (**********)
-Axiom Rlt_compatibility:(r,r1,r2:R)(Rlt r1 r2)->
-      (Rlt (Rplus r r1) (Rplus r r2)).
+Axiom Rlt_compatibility:(r,r1,r2:R)``r1<r2``->``r+r1<r+r2``.
 
 (**********)
-Axiom Rlt_monotony:(r,r1,r2:R)(Rlt R0 r)->(Rlt r1 r2)->
-      (Rlt (Rmult r r1) (Rmult r r2)).
+Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``.
 
 (**********************************************************) 
 (*       Injection from N to R                            *)
@@ -143,22 +115,21 @@ Definition IZR:Z->R:=[z:Z](Cases z of
 (**********************************************************)
 
 (**********)
-Axiom archimed:(r:R)(Rgt (IZR (up r)) r)/\
-                    (Rle (Rminus (IZR (up r)) r) R1).
+Axiom archimed:(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)->(Rle x m).
+Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->``x <= m``.
 
 (**********)
 Definition bound:=[E:R->Prop](ExT [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)->(Rle m b).
+    (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->``m <= b``.
 
 (**********)
 Axiom complet:(E:R->Prop)(bound E)->