Remplacement des Grammar et des [| |] par des notations

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

1 files changed, 134 insertions, 154 deletions

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 34bc697d49..1c48c4b45c 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -12,36 +12,6 @@ Require Export Bool.
 
 Set Implicit Arguments.
 
-Grammar ring formula : constr :=
-  formula_expr [ expr($p) ] -> [$p]
-| formula_eq [ expr($p) "==" expr($c) ] -> [ (eqT A $p $c) ]
-
-with expr : constr :=
-  RIGHTA
-    expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
-  | expr_expr1 [ expr1($p) ] -> [$p]
-
-with expr1 : constr :=
-  RIGHTA
-    expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
-  | expr1_final [ final($p) ] -> [$p]
-
-with final : constr :=
-  final_var [ prim:var($id) ] -> [ $id ]
-| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ]
-| final_app [ "(" application($r) ")" ] -> [ $r ]
-| final_0 [ "0" ] -> [ Azero ]
-| final_1 [ "1" ] -> [ Aone ]
-| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ]
-
-with application : constr :=
-  LEFTA
-    app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
-  | app_tail [ expr($c1) ] -> [ $c1 ].
-
-Grammar constr constr0 :=
-  formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].
-
 Section Theory_of_semi_rings.
 
 Variable A : Type.
@@ -55,16 +25,21 @@ Variable Azero : A.
   is a good choice. The proof of A_eq_prop is in this case easy. *)
 Variable Aeq : A -> A -> bool.
 
+Infix 4 "+" Aplus.
+Infix 4 "*" Amult.
+Notation "0" := Azero.
+Notation "1" := Aone.
+
 Record Semi_Ring_Theory : Prop :=
-{ SR_plus_sym  : (n,m:A)[| n + m == m + n |];
-  SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-  SR_mult_sym : (n,m:A)[| n*m == m*n |];
-  SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
-  SR_plus_zero_left :(n:A)[| 0 + n == n|];
-  SR_mult_one_left : (n:A)[| 1*n == n |];
-  SR_mult_zero_left : (n:A)[| 0*n == 0 |];
-  SR_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
-  SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
+{ SR_plus_sym  : (n,m:A) n + m == m + n;
+  SR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
+  SR_mult_sym : (n,m:A) n*m == m*n;
+  SR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
+  SR_plus_zero_left :(n:A) 0 + n == n;
+  SR_mult_one_left : (n:A) 1*n == n;
+  SR_mult_zero_left : (n:A) 0*n == 0;
+  SR_distr_left   : (n,m,p:A) (n + m)*p == n*p + m*p;
+  SR_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p;
   SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
 }.
 
@@ -86,77 +61,77 @@ Hints Resolve  plus_sym plus_assoc mult_sym mult_assoc
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
-Lemma SR_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
-Symmetry; EAuto. Save.
+Lemma SR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
+Symmetry; EAuto. Qed.
 
-Lemma SR_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
-Symmetry; EAuto. Save.
+Lemma SR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
+Symmetry; EAuto. Qed.
 
-Lemma SR_plus_zero_left2 : (n:A)[| n == 0 + n |].
-Symmetry; EAuto. Save.
+Lemma SR_plus_zero_left2 : (n:A) n == 0 + n.
+Symmetry; EAuto. Qed.
 
-Lemma SR_mult_one_left2 : (n:A)[| n == 1*n |].
-Symmetry; EAuto. Save.
+Lemma SR_mult_one_left2 : (n:A) n == 1*n.
+Symmetry; EAuto. Qed.
 
-Lemma SR_mult_zero_left2 : (n:A)[| 0 == 0*n |].
-Symmetry; EAuto. Save.
+Lemma SR_mult_zero_left2 : (n:A) 0 == 0*n.
+Symmetry; EAuto. Qed.
 
-Lemma SR_distr_left2 : (n,m,p:A) [| n*p + m*p  == (n + m)*p |].
-Symmetry; EAuto. Save.
+Lemma SR_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
+Symmetry; EAuto. Qed.
 
-Lemma SR_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |].
+Lemma SR_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p).
 Intros.
 Rewrite -> plus_assoc.
 Elim (plus_sym m n).
 Rewrite <- plus_assoc.
 Reflexivity.
-Save.
+Qed.
 
-Lemma SR_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
+Lemma SR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
 Intros.
 Rewrite -> mult_assoc.
 Elim (mult_sym m n).
 Rewrite <- mult_assoc.
 Reflexivity.
-Save.
+Qed.
 
 Hints Resolve SR_plus_permute SR_mult_permute.
 
-Lemma SR_distr_right : (n,m,p:A) [|  n*(m + p) == (n*m) + (n*p) |].
+Lemma SR_distr_right : (n,m,p:A) n*(m + p) == (n*m) + (n*p).
 Intros.
 Repeat Rewrite -> (mult_sym n).
 EAuto.
-Save.
+Qed.
 
-Lemma SR_distr_right2 : (n,m,p:A) [|  (n*m) + (n*p) == n*(m + p) |].
-Symmetry; Apply SR_distr_right. Save.
+Lemma SR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p).
+Symmetry; Apply SR_distr_right. Qed.
 
-Lemma SR_mult_zero_right : (n:A)[|  n*0 == 0|].
+Lemma SR_mult_zero_right : (n:A) n*0 == 0.
 Intro; Rewrite mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma SR_mult_zero_right2 : (n:A)[| 0 == n*0 |].
+Lemma SR_mult_zero_right2 : (n:A) 0 == n*0.
 Intro; Rewrite mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma SR_plus_zero_right :(n:A)[| n + 0 == n |].
+Lemma SR_plus_zero_right :(n:A) n + 0 == n.
 Intro; Rewrite plus_sym; EAuto.
-Save.
-Lemma SR_plus_zero_right2 :(n:A)[| n == n + 0 |].
+Qed.
+Lemma SR_plus_zero_right2 :(n:A) n == n + 0.
 Intro; Rewrite plus_sym; EAuto.
-Save.
+Qed.
 
-Lemma SR_mult_one_right : (n:A)[| n*1 == n |].
+Lemma SR_mult_one_right : (n:A) n*1 == n.
 Intro; Elim mult_sym; Auto.
-Save.
+Qed.
 
-Lemma SR_mult_one_right2 : (n:A)[| n == n*1 |].
+Lemma SR_mult_one_right2 : (n:A) n == n*1.
 Intro; Elim mult_sym; Auto.
-Save.
+Qed.
 
-Lemma SR_plus_reg_right : (n,m,p:A)[| m + n == p + n |] -> m==p.
+Lemma SR_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p.
 Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n); EAuto.
-Save.
+Qed.
 
 End Theory_of_semi_rings.
 
@@ -171,16 +146,21 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
+Infix 4 "+" Aplus.
+Infix 4 "*" Amult.
+Notation "0" := Azero.
+Notation "1" := Aone.
+Notation "- x" := (Aopp x) (at level 3).
 
 Record Ring_Theory : Prop :=
-{ Th_plus_sym  : (n,m:A)[| n + m == m + n |];
-  Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-  Th_mult_sym : (n,m:A)[| n*m == m*n |];
-  Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
-  Th_plus_zero_left :(n:A)[| 0 + n == n|];
-  Th_mult_one_left : (n:A)[| 1*n == n |];
-  Th_opp_def : (n:A) [| n + (-n) == 0 |];
-  Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
+{ Th_plus_sym  : (n,m:A) n + m == m + n;
+  Th_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
+  Th_mult_sym : (n,m:A) n*m == m*n;
+  Th_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
+  Th_plus_zero_left :(n:A) 0 + n == n;
+  Th_mult_one_left : (n:A) 1*n == n;
+  Th_opp_def : (n:A) n + (-n) == 0;
+  Th_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p;
   Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
 }.
 
@@ -200,43 +180,43 @@ Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
-Lemma Th_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
-Symmetry; EAuto. Save.
+Lemma Th_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
+Symmetry; EAuto. Qed.
 
-Lemma Th_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
-Symmetry; EAuto. Save.
+Lemma Th_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
+Symmetry; EAuto. Qed.
 
-Lemma Th_plus_zero_left2 : (n:A)[| n == 0 + n |].
-Symmetry; EAuto. Save.
+Lemma Th_plus_zero_left2 : (n:A) n == 0 + n.
+Symmetry; EAuto. Qed.
 
-Lemma Th_mult_one_left2 : (n:A)[| n == 1*n |].
-Symmetry; EAuto. Save.
+Lemma Th_mult_one_left2 : (n:A) n == 1*n.
+Symmetry; EAuto. Qed.
 
-Lemma Th_distr_left2 : (n,m,p:A) [| n*p + m*p  == (n + m)*p |].
-Symmetry; EAuto. Save.
+Lemma Th_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
+Symmetry; EAuto. Qed.
 
-Lemma Th_opp_def2 : (n:A) [| 0 == n + (-n) |].
-Symmetry; EAuto. Save.
+Lemma Th_opp_def2 : (n:A) 0 == n + (-n).
+Symmetry; EAuto. Qed.
 
-Lemma Th_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |].
+Lemma Th_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p).
 Intros.
 Rewrite -> plus_assoc.
 Elim (plus_sym m n).
 Rewrite <- plus_assoc.
 Reflexivity.
-Save.
+Qed.
 
-Lemma Th_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
+Lemma Th_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
 Intros.
 Rewrite -> mult_assoc.
 Elim (mult_sym m n).
 Rewrite <- mult_assoc.
 Reflexivity.
-Save.
+Qed.
 
 Hints Resolve Th_plus_permute Th_mult_permute.
 
-Lemma aux1 : (a:A) [| a + a == a |] -> [| a == 0 |].
+Lemma aux1 : (a:A) a + a == a -> a == 0.
 Intros.
 Generalize (opp_def a).
 Pattern 1 a.
@@ -246,21 +226,21 @@ Rewrite -> opp_def.
 Elim plus_sym.
 Rewrite plus_zero_left.
 Trivial.
-Save.
+Qed.
 
-Lemma Th_mult_zero_left :(n:A)[| 0*n == 0 |].
+Lemma Th_mult_zero_left :(n:A) 0*n == 0.
 Intros.
 Apply aux1.
 Rewrite <- distr_left.
 Rewrite plus_zero_left.
 Reflexivity.
-Save.
+Qed.
 Hints Resolve Th_mult_zero_left.
 
-Lemma Th_mult_zero_left2 : (n:A)[| 0 == 0*n |].
-Symmetry; EAuto. Save.
+Lemma Th_mult_zero_left2 : (n:A) 0 == 0*n.
+Symmetry; EAuto. Qed.
 
-Lemma aux2 : (x,y,z:A) [|x+y==0|] -> [|x+z==0|] -> y==z.
+Lemma aux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y==z.
 Intros.
 Rewrite <- (plus_zero_left y).
 Elim H0.
@@ -270,110 +250,110 @@ Rewrite -> plus_assoc.
 Rewrite -> H.
 Rewrite plus_zero_left.
 Reflexivity.
-Save.
+Qed.
 
-Lemma Th_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |].
+Lemma Th_opp_mult_left : (x,y:A) -(x*y) == (-x)*y.
 Intros.
-Apply (aux2 1![|x*y|]);
+Apply (aux2 1!x*y);
 [ Apply opp_def
 | Rewrite <- distr_left;
   Rewrite -> opp_def;
   Auto].
-Save.
+Qed.
 Hints Resolve Th_opp_mult_left.
 
-Lemma Th_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y)  |].
-Symmetry; EAuto. Save.
+Lemma Th_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y).
+Symmetry; EAuto. Qed.
 
-Lemma Th_mult_zero_right : (n:A)[| n*0 == 0|].
+Lemma Th_mult_zero_right : (n:A) n*0 == 0.
 Intro; Elim mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_mult_zero_right2 : (n:A)[| 0 == n*0 |].
+Lemma Th_mult_zero_right2 : (n:A) 0 == n*0.
 Intro; Elim mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_plus_zero_right :(n:A)[| n + 0 == n |].
+Lemma Th_plus_zero_right :(n:A) n + 0 == n.
 Intro; Rewrite plus_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_plus_zero_right2 :(n:A)[| n == n + 0 |].
+Lemma Th_plus_zero_right2 :(n:A) n == n + 0.
 Intro; Rewrite plus_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_mult_one_right : (n:A)[| n*1 == n |].
+Lemma Th_mult_one_right : (n:A) n*1 == n.
 Intro;Elim mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_mult_one_right2  : (n:A)[| n == n*1 |].
+Lemma Th_mult_one_right2  : (n:A) n == n*1.
 Intro;Elim mult_sym; EAuto.
-Save.
+Qed.
 
-Lemma Th_opp_mult_right : (x,y:A)[| -(x*y) == x*(-y) |].
+Lemma Th_opp_mult_right : (x,y:A) -(x*y) == x*(-y).
 Intros; Do 2 Rewrite -> (mult_sym x); Auto.
-Save.
+Qed.
 
-Lemma Th_opp_mult_right2 : (x,y:A)[| x*(-y) == -(x*y) |].
+Lemma Th_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y).
 Intros; Do 2 Rewrite -> (mult_sym x); Auto.
-Save.
+Qed.
 
-Lemma Th_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |].
+Lemma Th_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y).
 Intros.
-Apply (aux2 1![| x + y |]);
+Apply (aux2 1! x + y);
 [ Elim plus_assoc;
-  Rewrite -> (Th_plus_permute y [| -x |]); Rewrite -> plus_assoc;
+  Rewrite -> (Th_plus_permute y -x); Rewrite -> plus_assoc;
   Rewrite -> opp_def;  Rewrite plus_zero_left; Auto
 | Auto ].
-Save.
+Qed.
 
-Lemma Th_plus_permute_opp: (n,m,p:A)[| (-m)+(n+p) == n+((-m)+p) |].
-EAuto. Save.
+Lemma Th_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p).
+EAuto. Qed.
 
-Lemma Th_opp_opp : (n:A)[| -(-n) == n |].
-Intro; Apply (aux2 1![| -n |]); 
+Lemma Th_opp_opp : (n:A) -(-n) == n.
+Intro; Apply (aux2 1! -n); 
   [ Auto | Elim plus_sym; Auto ].
-Save.
+Qed.
 Hints Resolve Th_opp_opp.
 
-Lemma Th_opp_opp2 : (n:A)[| n == -(-n) |].
-Symmetry; EAuto. Save.
+Lemma Th_opp_opp2 : (n:A) n == -(-n).
+Symmetry; EAuto. Qed.
 
-Lemma Th_mult_opp_opp : (x,y:A)[| (-x)*(-y) == x*y |].
+Lemma Th_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y.
 Intros; Rewrite <- Th_opp_mult_left; Rewrite <- Th_opp_mult_right; Auto.
-Save.
+Qed.
 
-Lemma Th_mult_opp_opp2 : (x,y:A)[| x*y == (-x)*(-y) |].
-Symmetry; Apply Th_mult_opp_opp. Save.
+Lemma Th_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y).
+Symmetry; Apply Th_mult_opp_opp. Qed.
 
-Lemma Th_opp_zero : [| -0 == 0 |].
-Rewrite <- (plus_zero_left [| -0 |]).
-Auto. Save.
+Lemma Th_opp_zero : -0 == 0.
+Rewrite <- (plus_zero_left -0).
+Auto. Qed.
 
-Lemma Th_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p.
-Intros; Generalize (congr_eqT ? ? [z][| (-n)+z |] ? ? H).
+Lemma Th_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p.
+Intros; Generalize (congr_eqT ? ? [z] (-n)+z ? ? H).
 Repeat Rewrite plus_assoc.
-Rewrite (plus_sym [| -n |] n).
+Rewrite (plus_sym -n n).
 Rewrite opp_def.
 Repeat Rewrite Th_plus_zero_left; EAuto.
-Save.
+Qed.
 
-Lemma Th_plus_reg_right : (n,m,p:A)[| m + n == p + n |] -> m==p.
+Lemma Th_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p.
 Intros.
 EApply Th_plus_reg_left with n. 
 Rewrite (plus_sym n m).
 Rewrite (plus_sym n p).
 Auto.
-Save.
+Qed.
 
-Lemma Th_distr_right : (n,m,p:A) [|  n*(m + p) == (n*m) + (n*p) |].
+Lemma Th_distr_right : (n,m,p:A)  n*(m + p) == (n*m) + (n*p).
 Intros.
 Repeat Rewrite -> (mult_sym n).
 EAuto.
-Save.
+Qed.
 
-Lemma Th_distr_right2  : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p)  |].
+Lemma Th_distr_right2  : (n,m,p:A) (n*m) + (n*p) == n*(m + p).
 Symmetry; Apply Th_distr_right.
-Save.
+Qed.
 
 End Theory_of_rings.