Suppression Field

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

2 files changed, 263 insertions, 32 deletions

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 9fb11f2b5..78a29437c 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -52,7 +52,17 @@ Intros; Case (total_order R0 x); Intro; [Unfold Rsqr; Apply Rmult_lt_pos; Assump
 Save.
 
 Lemma Rsqr_div : (x,y:R) ~``y==0`` -> ``(Rsqr (x/y))==(Rsqr x)/(Rsqr y)``.
-Intros; Unfold Rsqr; Field; Repeat Apply prod_neq_R0; Assumption.
+Intros; Unfold Rsqr.
+Unfold Rdiv.
+Rewrite Rinv_Rmult.
+Repeat Rewrite Rmult_assoc.
+Apply Rmult_mult_r.
+Pattern 2 x; Rewrite Rmult_sym.
+Repeat Rewrite Rmult_assoc.
+Apply Rmult_mult_r.
+Reflexivity.
+Assumption.
+Assumption.
 Save.
 
 Lemma Rsqr_eq_0 : (x:R) ``(Rsqr x)==0`` -> ``x==0``.
@@ -267,38 +277,156 @@ Definition sol_x1 [a:nonzeroreal;b,c:R] : R := ``(-b+(sqrt (Delta a b c)))/(2*a)
 Definition sol_x2 [a:nonzeroreal;b,c:R] : R := ``(-b-(sqrt (Delta a b c)))/(2*a)``.
 
 Lemma Rsqr_inv : (x:R) ~``x==0`` -> ``(Rsqr (/x))==/(Rsqr x)``.
-Intros; Unfold Rsqr; Field; Repeat Apply prod_neq_R0; Assumption.
+Intros; Unfold Rsqr.
+Rewrite Rinv_Rmult; Try Reflexivity Orelse Assumption.
 Save.
 
 Lemma Rsqr_sol_eq_0_1 : (a:nonzeroreal;b,c,x:R) (Delta_is_pos a b c) -> (x==(sol_x1 a b c))\/(x==(sol_x2 a b c)) -> ``a*(Rsqr x)+b*x+c==0``.
-Intros.
-Elim H0; Intro.
+Intros; Elim H0; Intro.
 Unfold sol_x1 in H1; Unfold Delta in H1; Rewrite H1; Unfold Rdiv; Repeat Rewrite Rsqr_times; Rewrite Rsqr_plus; Rewrite <- Rsqr_neg; Rewrite Rsqr_sqrt.
 Rewrite Rsqr_inv.
-Unfold Rsqr; Field.
-Case a.
-Intros y H2; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; Assumption Orelse DiscrR.
+Unfold Rsqr; Repeat Rewrite Rinv_Rmult.
+Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym a).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite Rmult_Rplus_distrl.
+Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``(sqrt (b*b-4*(a*c))) `` ``(/2*/a)``).
+Rewrite Rmult_Rplus_distr; Repeat Rewrite Rplus_assoc.
+Replace ``( -b*((sqrt (b*b-4*(a*c)))*(/2*/a))+(b*( -b*(/2*/a))+(b*((sqrt (b*b-4*(a*c)))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``.
+Unfold Rminus; Repeat Rewrite <- Rplus_assoc.
+Replace ``b*b+b*b`` with ``2*(b*b)``.
+Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Replace ``2+1+1`` with ``2*2``.
+Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym a); Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite <- Ropp_mul2.
+Ring.
+Apply (cond_nonzero a).
+DiscrR.
+DiscrR.
+Ring.
+DiscrR.
+Ring.
+Repeat Rewrite Rplus_assoc; Repeat Rewrite <- (Rplus_sym c); Repeat Rewrite Rplus_assoc.
+Rewrite (Rplus_sym ``-b*((sqrt (b*b-4*(a*c)))*(/2*/a))``); Repeat Rewrite Rplus_assoc.
+Repeat Rewrite Ropp_mul1; Rewrite Rplus_Ropp_r.
+Rewrite Rplus_Or; Apply Rplus_sym.
+DiscrR.
+Apply (cond_nonzero a).
+DiscrR.
+Apply (cond_nonzero a).
+Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
+Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
 Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
-Unfold Delta_is_pos in H.
-Unfold Delta in H.
 Assumption.
 Unfold sol_x2 in H1; Unfold Delta in H1; Rewrite H1; Unfold Rdiv; Repeat Rewrite Rsqr_times; Rewrite Rsqr_minus; Rewrite <- Rsqr_neg; Rewrite Rsqr_sqrt.
 Rewrite Rsqr_inv.
-Unfold Rsqr; Field.
-Case a.
-Intros y H2; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; Assumption Orelse DiscrR.
-Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
-Unfold Delta_is_pos in H.
-Unfold Delta in H.
+Unfold Rsqr; Repeat Rewrite Rinv_Rmult; Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym a); Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Unfold Rminus; Rewrite Rmult_Rplus_distrl.
+Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``-(sqrt (b*b+ -(4*(a*c)))) `` ``(/2*/a)``).
+Rewrite Rmult_Rplus_distr; Repeat Rewrite Rplus_assoc.
+Rewrite Ropp_mul1; Rewrite Ropp_Ropp.
+Replace ``(b*((sqrt (b*b+ -(4*(a*c))))*(/2*/a))+(b*( -b*(/2*/a))+(b*( -(sqrt (b*b+ -(4*(a*c))))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``.
+Repeat Rewrite <- Rplus_assoc; Replace ``b*b+b*b`` with ``2*(b*b)``.
+Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Replace ``2+1+1`` with ``2*2``.
+Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym a); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite <- Ropp_mul2; Ring.
+Apply (cond_nonzero a).
+DiscrR.
+DiscrR.
+Ring.
+DiscrR.
+Ring.
+Ring.
+DiscrR.
+Apply (cond_nonzero a).
+DiscrR.
+Apply (cond_nonzero a).
+Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a).
+Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a).
+Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a).
 Assumption.
 Save.
 
 Lemma canonical_Rsqr : (a:nonzeroreal;b,c,x:R) ``a*(Rsqr x)+b*x+c == a* (Rsqr (x+b/(2*a))) + (4*a*c - (Rsqr b))/(4*a)``.
-Intros; Unfold Rsqr; Field; Case a; Intros y H1; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; Assumption Orelse DiscrR.
+Intros.
+Rewrite Rsqr_plus.
+Repeat Rewrite Rmult_Rplus_distr.
+Repeat Rewrite Rplus_assoc.
+Apply Rplus_plus_r.
+Unfold Rdiv Rminus.
+Rewrite (Rmult_Rplus_distrl ``4*a*c`` ``-(Rsqr b)`` ``/(4*a)``).
+Rewrite Rsqr_times.
+Repeat Rewrite Rinv_Rmult.
+Repeat Rewrite (Rmult_sym a).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite (Rmult_sym ``/4``).
+Rewrite (Rmult_sym ``4``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite (Rmult_sym a).
+Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite (Rmult_sym x).
+Repeat Rewrite Rplus_assoc.
+Rewrite (Rplus_sym ``(Rsqr b)*((Rsqr (/2*/a))*a)``).
+Repeat Rewrite Rplus_assoc.
+Apply Rplus_plus_r.
+Rewrite Ropp_mul1.
+Unfold Rsqr.
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite <- (Rmult_sym ``(/a*/2)``).
+Rewrite Rmult_assoc.
+Rewrite <- (Rinv_Rmult ``2`` ``2``).
+Replace ``2*2`` with ``4``.
+Rewrite Rplus_Ropp_l.
+Symmetry; Apply Rplus_Or.
+Ring.
+DiscrR.
+DiscrR.
+Apply (cond_nonzero a).
+Apply (cond_nonzero a).
+DiscrR.
+DiscrR.
+Apply (cond_nonzero a).
+DiscrR.
+Apply (cond_nonzero a).
+DiscrR.
+Apply (cond_nonzero a).
 Save.
 
 Lemma Rsqr_eq : (x,y:R) (Rsqr x)==(Rsqr y) -> x==y \/ x==``-y``.
-Intros; Unfold Rsqr in H; Generalize (Rplus_plus_r ``-(y*y)`` ``x*x`` ``y*y`` H); Rewrite Rplus_Ropp_l; Replace ``-(y*y)+x*x`` with ``(x-y)*(x+y)``; [Intro; Generalize (without_div_Od ``x-y`` ``x+y`` H0); Intro; Elim H1; Intros; [Left; Apply Rminus_eq; Assumption | Right; Apply Rminus_eq; Unfold Rminus; Rewrite Ropp_Ropp; Assumption] | Ring].
+Intros; Unfold Rsqr in H; Generalize (Rplus_plus_r ``-(y*y)`` ``x*x`` ``y*y`` H); Rewrite Rplus_Ropp_l; Replace ``-(y*y)+x*x`` with ``(x-y)*(x+y)``.
+Intro; Generalize (without_div_Od ``x-y`` ``x+y`` H0); Intro; Elim H1; Intros.
+Left; Apply Rminus_eq; Assumption.
+Right; Apply Rminus_eq; Unfold Rminus; Rewrite Ropp_Ropp; Assumption.
+Ring.
 Save.
 
 Lemma Rsqr_sol_eq_0_0 : (a:nonzeroreal;b,c,x:R) (Delta_is_pos a b c) -> ``a*(Rsqr x)+b*x+c==0`` -> (x==(sol_x1 a b c))\/(x==(sol_x2 a b c)).
@@ -314,11 +442,24 @@ Right; Unfold sol_x2; Generalize (Rplus_plus_r ``-(b/(2*a))`` ``x+b/(2*a)`` ``-(
 Intro; Rewrite H6; Unfold Rdiv; Ring.
 Ring.
 Rewrite Rsqr_div.
-Rewrite Rsqr_sqrt; [Unfold Rdiv Rsqr; Field; Case a; Intros y H3; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; Assumption Orelse DiscrR | Unfold Delta_is_pos in H; Assumption].
+Rewrite Rsqr_sqrt.
+Unfold Rdiv.
+Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym ``/a``).
+Rewrite Rmult_assoc.
+Rewrite <- Rinv_Rmult.
+Replace ``4*a*a`` with ``(Rsqr (2*a))``.
+Reflexivity.
+SqRing.
+Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
+Apply (cond_nonzero a).
+Assumption.
 Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)].
 Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
 Symmetry; Apply Rmult_1l.
 Apply (cond_nonzero a).
-Unfold Rdiv; Field; Case a; Intros y H3; Apply prod_neq_R0; [DiscrR | Assumption].
-Unfold Delta; Reflexivity.
+Unfold Rdiv; Rewrite <- Ropp_mul1.
+Rewrite Ropp_distr2.
+Reflexivity.
+Reflexivity.
 Save.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index f31429d4a..dfab20d09 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -20,6 +20,20 @@ Require DiscrR.
 Require Fourier.
 Require SplitAbsolu.
 
+(** Modif **)
+Lemma double : (x:R) ``2*x==x+x``.
+Intro; Ring.
+Save.
+
+Lemma aze : ``2<>0``.
+DiscrR.
+Save.
+
+Lemma double_var : (x:R) ``x == x/2 + x/2``.
+Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m.
+Apply aze.
+Save.
+
 (*******************************)
 (*      Calculus               *)
 (*******************************)
@@ -32,7 +46,10 @@ Save.
 (*********)
 Lemma eps2:(eps:R)(Rplus (Rmult eps (Rinv (Rplus R1 R1)))
                         (Rmult eps (Rinv (Rplus R1 R1))))==eps.
-Intro esp;Field;DiscrR.
+Intro esp.
+Assert H := (double_var esp).
+Unfold Rdiv in H.
+Symmetry; Exact H.
 Save.
 
 (*********)
@@ -40,19 +57,51 @@ Lemma eps4:(eps:R)
   (Rplus (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) )))
         (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) ))))==
                   (Rmult eps (Rinv (Rplus R1 R1))).
-Intro eps;Field;DiscrR.
+Intro eps.
+Replace ``2+2`` with ``2*2``.
+Pattern 3 eps; Rewrite double_var.
+Rewrite (Rmult_Rplus_distrl ``eps/2`` ``eps/2`` ``/2``).
+Unfold Rdiv.
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_Rmult.
+Reflexivity.
+Apply aze.
+Apply aze.
+Ring.
 Save.
 
 (*********)
 Lemma Rlt_eps2_eps:(eps:R)(Rgt eps R0)->
         (Rlt (Rmult eps (Rinv (Rplus R1 R1))) eps).
-Intros;Fourier.
+Intros.
+Pattern 2 eps; Rewrite <- Rmult_1r.
+Repeat Rewrite (Rmult_sym eps).
+Apply Rlt_monotony_r.
+Exact H.
+Apply Rlt_monotony_contra with ``2``.
+Fourier.
+Rewrite Rmult_1r; Rewrite <- Rinv_r_sym.
+Fourier.
+DiscrR.
 Save.
 
 (*********)
 Lemma Rlt_eps4_eps:(eps:R)(Rgt eps R0)->
         (Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps).
-Intros;Fourier.
+Intros.
+Replace ``2+2`` with ``4``.
+Pattern 2 eps; Rewrite <- Rmult_1r.
+Repeat Rewrite (Rmult_sym eps).
+Apply Rlt_monotony_r.
+Exact H.
+Apply Rlt_monotony_contra with ``4``.
+Replace ``4`` with ``2*2``.
+Apply Rmult_lt_pos; Fourier.
+Ring.
+Rewrite Rmult_1r; Rewrite <- Rinv_r_sym.
+Fourier.
+DiscrR.
+Ring.
 Save. 
 
 (*********)
@@ -601,10 +650,22 @@ Intro; Rewrite Rabsolu_minus_sym in H5; Cut ``0<=/(Rabsolu (l*(f x)))``.
 Intro; Generalize (Rmult_lt2 ``(Rabsolu (l-(f x)))`` ``eps*(Rsqr l)/2`` ``/(Rabsolu (l*(f x)))`` ``2/(Rsqr l)`` (Rabsolu_pos ``l-(f x)``) H18 H5 H17); Replace ``eps*(Rsqr l)/2*2/(Rsqr l)`` with ``eps``.
 Intro; Assumption.
 Unfold Rdiv; Unfold Rsqr; Rewrite Rinv_Rmult.
-Field.
-Repeat Apply prod_neq_R0; [DiscrR | Assumption | Assumption].
-Assumption.
-Assumption.
+Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym l).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite (Rmult_sym l).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Reflexivity.
+Apply aze.
+Exact H0.
+Exact H0.
+Exact H0.
+Exact H0.
 Left; Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply prod_neq_R0; Assumption.
 Rewrite Rmult_sym; Rewrite Rabsolu_mult; Rewrite Rinv_Rmult.
 Rewrite (Rsqr_abs l); Unfold Rsqr; Unfold Rdiv; Rewrite Rinv_Rmult.
@@ -618,20 +679,49 @@ Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2)
 Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*/(Rabsolu (f x))`` with ``(Rabsolu l)/2``.
 Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*(2*/(Rabsolu l))`` with ``(Rabsolu (f x))``.
 Assumption.
-Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]].
-Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]].
+Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym (Rabsolu l)).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Reflexivity.
+Apply aze.
+Apply Rabsolu_no_R0.
+Assumption.
+Unfold Rdiv.
+Repeat Rewrite Rmult_assoc.
+Rewrite (Rmult_sym (Rabsolu (f x))).
+Repeat Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Reflexivity.
+Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
 Apply prod_neq_R0; Assumption.
-Field; Repeat Apply prod_neq_R0; Assumption.
+Rewrite (Rinv_Rmult ? ? H0 H16).
+Unfold Rminus; Rewrite Rmult_Rplus_distrl.
+Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l.
+Rewrite Ropp_mul1.
+Rewrite (Rmult_sym (f x)).
+Rewrite Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Reflexivity.
+Assumption.
+Assumption.
 Red; Intro; Rewrite H16 in H15; Rewrite Rabsolu_R0 in H15; Cut ``0<(Rabsolu l)/2``.
 Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rabsolu l)/2`` ``0`` H17 H15)).
 Unfold Rdiv; Apply Rmult_lt_pos.
 Apply Rabsolu_pos_lt; Assumption.
 Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro; Assumption | Discriminate].
-Field; DiscrR.
+Pattern 3 (Rabsolu l); Rewrite double_var.
+Ring.
 Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_r]].
 Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_l]].
 Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos.