mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

4 files changed, 86 insertions, 47 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index f22f12a4c..47be9d236 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Export ZArith.
-Require Export ZArithRing.
+Require Export NewZArithRing.
 Require Export Setoid.
 
 (** * Definition of [Q] and basic properties *)
@@ -104,8 +104,10 @@ Proof.
 unfold Qeq in |- *; intros.
 apply Zmult_reg_l with (QDen y). 
 auto with qarith.
-ring; rewrite H; ring.
-rewrite Zmult_assoc; rewrite H0; ring.
+transitivity (Qnum x * QDen y * QDen z)%Z; try ring.
+rewrite H.
+transitivity (Qnum y * QDen z * QDen x)%Z; try ring.
+rewrite H0; ring.
 Qed.
 
 (** Furthermore, this equality is decidable: *)
@@ -167,10 +169,10 @@ Proof.
 unfold Qeq, Qplus; simpl.
 Open Scope Z_scope.
 intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
-simpl_mult; ring.
-replace (p1 * ('s2 * 'q2)) with (p1 * 'q2 * 's2) by ring.
+simpl_mult; ring_simplify.
+replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring.
 rewrite H.
-replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring.
 rewrite H0.
 ring.
 Close Scope Z_scope.
@@ -179,7 +181,11 @@ Qed.
 Add Morphism Qopp : Qopp_comp.
 Proof.
 unfold Qeq, Qopp; simpl.
-intros; ring; rewrite H; ring.
+Open Scope Z_scope.
+intros.
+replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring.
+rewrite H in |- *;  ring.
+Close Scope Z_scope.
 Qed.
 
 Add Morphism Qminus : Qminus_comp.
@@ -194,10 +200,10 @@ Proof.
 unfold Qeq; simpl.
 Open Scope Z_scope.
 intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
-intros; simpl_mult; ring.
-replace ('p2 * (q1 * s1)) with (q1 * 'p2 * s1) by ring.
+intros; simpl_mult; ring_simplify.
+replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring.
 rewrite <- H.
-replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring.
 rewrite H0.
 ring.
 Close Scope Z_scope.
@@ -579,14 +585,13 @@ unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
  simpl; simpl_mult.
 Open Scope Z_scope.
 intros.
-match goal with |- ?a <= ?b => ring a; ring b end.
+match goal with |- ?a <= ?b => ring_simplify a b end.
+rewrite Zplus_comm.
 apply Zplus_le_compat.
-replace ('t2 * ('y2 * (z1 * 'x2))) with (z1 * 't2 * ('y2 * 'x2)) by ring.
-replace ('z2 * ('x2 * (t1 * 'y2))) with (t1 * 'z2 * ('y2 * 'x2)) by ring.
-apply Zmult_le_compat_r; auto with zarith.
-replace ('t2 * ('y2 * ('z2 * x1))) with (x1 * 'y2 * ('z2 * 't2)) by ring.
-replace ('z2 * ('x2 * ('t2 * y1))) with (y1 * 'x2 * ('z2 * 't2)) by ring.
-apply Zmult_le_compat_r; auto with zarith.
+match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+auto with zarith.
+match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+auto with zarith.
 Close Scope Z_scope.
 Qed.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 026e850ea..40c310ff4 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Import NewField Field_tac.
 Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
@@ -493,6 +494,7 @@ intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto
 intros _ H; inversion H.
 Qed.
 
+(*
 Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool.
 Proof.
 constructor.
@@ -507,17 +509,41 @@ exact Qcmult_plus_distr_l.
 unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y);
  case (Qc_eq_bool x y); auto.
 Qed.
-
 Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ].
+*)
+Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)).
+Proof.
+constructor.
+ exact Qcplus_0_l.
+ exact Qcplus_comm.
+ exact Qcplus_assoc.
+ exact Qcmult_1_l.
+ exact Qcmult_comm.
+ exact Qcmult_assoc.
+ exact Qcmult_plus_distr_l.
+ reflexivity.
+ exact Qcplus_opp_r.
+Qed.
 
-(** A field tactic for rational numbers *)
+Definition Qcft :
+  field_theory _ 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).
+Proof.
+constructor.
+ exact Qcrt.
+ exact Q_apart_0_1.
+ reflexivity.
+ exact Qcmult_inv_l.
+Qed.
 
-Require Import Field.
+Add Field Qcfield : Qcft.
 
+(** A field tactic for rational numbers *)
+
+(*
 Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l
  with div:=Qcdiv.
-
-Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x.
+*)
+Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.
 intros.
 field.
 auto.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index e4b22dd56..5b4d8db03 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -52,8 +52,9 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R).
  unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
  apply IZR_eq; auto.
 clear H.
-field; auto.
-rewrite <- H0; field; auto.
+field_simplify_eq; auto.
+ring_simplify X1 Y2 (Y2 * X1)%R.
+rewrite H0 in |- *;  ring.
 Qed.
 
 Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
@@ -176,16 +177,11 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rinv_neq_0_compat; auto.
-intros; field; auto.
-do 2 rewrite <- mult_IZR.
-simpl in |- *; rewrite Pmult_comm; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply not_O_IZR; auto with qarith.
-apply Rinv_neq_0_compat; auto.
+intros; 
+  change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
+  change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
+  field; (*auto 8 with real.*)
+  repeat split; auto; auto with real.
 Qed.
 
 Lemma Q2R_div :
@@ -210,4 +206,4 @@ Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
 intros; QField.
 intro; apply H; apply eqR_Qeq.
 rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
-Abort.
\ No newline at end of file
+Abort.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 84a968475..0c4c8399c 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -8,8 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Ring.
-Require Export Setoid_ring.
+Require Export Ring.
 Require Export QArith_base.
 
 (** * A ring tactic for rational numbers *)
@@ -22,25 +21,38 @@ intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
 intros _ H; inversion H.
 Qed.
 
-Definition Qsrt : Setoid_Ring_Theory Qeq Qplus Qmult 1 0 Qopp Qeq_bool.
+Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
 Proof.
 constructor.
+exact Qplus_0_l.
 exact Qplus_comm.
 exact Qplus_assoc.
+exact Qmult_1_l.
 exact Qmult_comm.
 exact Qmult_assoc.
-exact Qplus_0_l.
-exact Qmult_1_l.
-exact Qplus_opp_r.
 exact Qmult_plus_distr_l.
-unfold Is_true; intros x y; generalize (Qeq_bool_correct x y);
- case (Qeq_bool x y); auto.
+reflexivity.
+exact Qplus_opp_r.
 Qed.
 
-Add Setoid Ring Q Qeq Q_Setoid Qplus Qmult 1 0 Qopp Qeq_bool
- Qplus_comp Qmult_comp Qopp_comp Qsrt
- [ Qmake (*inject_Z*)  Zpos 0%Z Zneg xI xO 1%positive ].
-
+Ltac isQcst t :=
+  let t := eval hnf in t in
+  match t with
+    Qmake ?n ?d =>
+      match isZcst n with
+        true => isZcst d
+      | _ => false
+      end
+  | _ => false
+  end.
+
+Ltac Qcst t :=
+  match isQcst t with
+    true => t
+  | _ => NotConstant
+  end.
+
+Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
 (** Exemple of use: *)
 
 Section Examples.