Changement dans ring et field, beaucoup de correction d'erreurs,

maintenant les differentes tactics marchent mieux mais le code
est moche ...



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

14 files changed, 47 insertions, 36 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index c0087bd30..5465bc692 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Compare_dec.
 Require Import Sumbool.
 Require Import Div2.
@@ -174,4 +174,4 @@ Proof.
   pattern n at 1; rewrite <- (nat_of_N_of_nat n).
   pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
   symmetry; apply nat_of_Ncompare.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 060de9a44..51ed8a4c0 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -92,9 +92,9 @@ Proof.
     replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
       with (Un (S (S (2 * S N)))); [ idtac | ring ].
   apply H.
-  ring_nat.
+  ring.
   apply HrecN.
-  ring_nat.
+  ring.
 Qed.
 
 (** A more general inequality *)
@@ -300,7 +300,7 @@ Proof.
   do 2 rewrite Rmult_1_r; apply le_INR.
   replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
   apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
-  ring_nat.
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
     [ discriminate | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index eab47da8e..a5c5ddaf8 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -75,7 +75,7 @@ Proof.
   apply H3; assumption.
   right.
   apply H4; assumption.
-  unfold double in |- *; ring.
+  unfold double in |- *;ring.
 Qed.
 
   (* 2m <= 2n => m<=n *)
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 82b0a3949..1ef4f1ec4 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -486,7 +486,7 @@ Proof.
   apply le_trans with (pred N).
   assumption.
   apply le_pred_n.
-  ring_nat.
+  ring.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
   apply le_trans with (2 * S (S (n0 + n)))%nat.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   omega.
   right.
   unfold Rdiv in |- *; rewrite Rmult_comm.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 23d24bdf2..a79b74d7b 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -87,7 +87,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
   apply le_trans with (pred N).
   apply H0.
   apply le_pred_n.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   cut (S N = (2 * S N0)%nat).
   intro.
   replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   unfold C, Rdiv in |- *.
   rewrite (Rmult_comm (INR (fact (S N)))).
   rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
   simpl in |- *.
   pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
     apply Rlt_0_1.
-  ring_nat.
+  ring.
   unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
   unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
   assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
   replace (S (S (2 * N0))) with (2 * S N0)%nat.
   do 2 rewrite div2_double.
   reflexivity.
-  ring_nat.
+  ring.
   apply S_pred with 0%nat; apply H.
 Qed.
 
@@ -585,8 +585,8 @@ Proof.
   apply (fun m n p:nat => mult_le_compat_l p n m).
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
   replace (2 * N1)%nat with (S (S (2 * pred N1))).
   reflexivity.
   pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-  ring_nat.
+  ring.
   symmetry  in |- *; apply S_pred with 0%nat; apply H8.
   apply INR_lt.
   apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
   rewrite div2_double.
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   reflexivity.
   apply le_trans with (max (2 * S N0) 2).
   apply le_max_l.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 72b9aee32..6692fd8c7 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -278,7 +278,7 @@ Proof.
   rewrite (tech5 An (2 * S N)).
   rewrite <- HrecN.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index daebd9178..5d1327528 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,6 +13,8 @@
 (***************************************************************************)
 
 Require Export Raxioms.
+Require Import Rpow_def.
+Require Import Zpower.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
@@ -1528,6 +1530,16 @@ Proof.
   rewrite Rmult_opp_opp; auto with real.
 Qed.
 
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
+Proof.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
+Qed.
+
 (**********)
 Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index ba7396ed6..54bc50e0a 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -15,7 +15,6 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export LegacyArithRing. (* for ring_nat... *)
 Require Export ArithRing.
 
 Require Import Rbase.
@@ -378,7 +377,7 @@ Proof.
   replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
   rewrite Hrecn; reflexivity.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -425,7 +424,7 @@ Proof.
   rewrite Hrecn2.
   simpl in |- *.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 6af991673..917592702 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -53,7 +53,7 @@ Section Sigma.
     apply lt_minus_O_lt; assumption.
     apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
     omega.
@@ -71,7 +71,7 @@ Section Sigma.
     apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
     apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     omega.
     inversion H; [ right; reflexivity | left; assumption ].
   Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 70fb3e6d0..14359574f 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -522,7 +522,7 @@ Proof.
   intro; assumption.
   intro; reflexivity.
   split.
-  intro; elim diff_false_true; assumption.
+  intro feqt;discriminate feqt.
   intro.
   elim n0; assumption.
   unfold Vn in |- *.
@@ -540,7 +540,7 @@ Proof.
   unfold cond_positivity in |- *.
   case (Rle_dec 0 z); intro.
   split.
-  intro; elim diff_true_false; assumption.
+  intro feqt; discriminate feqt.
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
   split.
   intro; auto with real.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 2adac468b..2f69fb761 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -466,10 +466,10 @@ Proof.
   unfold x in |- *; replace 0 with (INR 0);
     [ apply le_INR; apply le_O_n | reflexivity ].
   prove_sup0.
-  ring_nat.
+  ring.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 57878b61f..d6ab9a4ce 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -121,7 +121,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H3 := cv_speed_pow_fact a); unfold Un in |- *; unfold Un_cv in H3;
     unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H3 eps H4); intros N H5.
@@ -316,7 +316,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H4 := cv_speed_pow_fact a0); unfold Un in |- *; unfold Un_cv in H4;
     unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H4 eps H5); intros N H6; exists N; intros.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index ba1716506..9b5111ff9 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -99,7 +99,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 28415ab61..092df1feb 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1265,8 +1265,8 @@ Proof.
   apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
   apply INR_fact_neq_0.
   apply not_O_INR; discriminate.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   unfold Vn in |- *; rewrite Rmult_assoc; unfold Rdiv in |- *;
     rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)).
   repeat apply Rmult_le_compat_l.
@@ -1293,8 +1293,8 @@ Proof.
   apply le_INR; omega.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   intro; unfold Un in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
   apply pow_lt; assumption.
   apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;