Ajout tactics Reals

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

4 files changed, 103 insertions, 73 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
new file mode 100644
index 0000000000..a5155163b9
--- /dev/null
+++ b/theories/Reals/DiscrR.v
@@ -0,0 +1,38 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Rbase.
+
+Tactic Definition Sup0 :=
+  Match Context With
+  | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1
+  | [ |- (Rgt (Rplus R1 ?1) R0) ] ->
+    Apply (Rgt_trans (Rplus R1 ?1) ?1 R0);
+    [Pattern 1 (Rplus R1 ?1);Rewrite Rplus_sym;Unfold Rgt;
+     Apply Rlt_r_r_plus_R1
+    |Sup0].
+
+Tactic Definition DiscrR :=
+  Match Context With
+  | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption
+  | [ |- ~((Rplus R1 ?1)==R0) ] -> Apply Rgt_not_eq;Sup0
+  | [ |- ~(Ropp ?1)==R0 ] -> Apply Ropp_neq; DiscrR
+  | [ |- ~(?1==?1) ] -> ElimType False
+  | [ |- ~(Rminus R0 ?1)==R0 ] -> Rewrite Rminus_Ropp; DiscrR
+  | [ |- ~(?1==?2) ] -> 
+    (Apply Rminus_not_eq; Ring (Rminus ?1 ?2); 
+      (Match Context With
+      | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> 
+        Repeat Rewrite <-Ropp_distr1; DiscrR
+      | [ |- ? ] -> DiscrR)
+     Orelse (Apply Rminus_not_eq_right; DiscrR)).
+  
+
+
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 4b4ab63514..f8b88f9c6e 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -492,12 +492,22 @@ Intro;Ring.
 Save.
 Hints Resolve minus_R0 : real.
 
+Lemma Rminus_Ropp:(r:R)``0-r==-r``.
+Intro;Ring.
+Save.
+Hints Resolve Rminus_Ropp : real.
+
 (**********)
 Lemma Ropp_distr2:(r1,r2:R)``-(r1-r2)==r2-r1``.
   Intros; Ring.
 Save.
 Hints Resolve Ropp_distr2 : real.
 
+Lemma Ropp_distr3:(r1,r2:R)``-(r2-r1)==r1-r2``.
+Intros; Ring.
+Save.
+Hints Resolve Ropp_distr3 : real. 
+
 (**********)
 Lemma eq_Rminus:(r1,r2:R)(r1==r2)->``r1-r2==0``.
   Intros; Rewrite H; Ring.
@@ -511,6 +521,11 @@ Lemma Rminus_eq:(r1,r2:R)``r1-r2==0`` -> r1==r2.
 Save.
 Hints Immediate Rminus_eq : real.
 
+Lemma Rminus_eq_right:(r1,r2:R)``r2-r1==0`` -> r1==r2.
+Intros;Generalize (Rminus_eq r2 r1 H);Clear H;Intro H;Rewrite H;Ring.
+Save.
+Hints Immediate Rminus_eq_right : real.
+
 (**********)
 Lemma Rminus_eq_contra:(r1,r2:R)``r1<>r2``->``r1-r2<>0``.
 Red; Intros r1 r2 H H0.
@@ -518,6 +533,16 @@ Apply H; Auto with real.
 Save.
 Hints Resolve Rminus_eq_contra : real.
 
+Lemma Rminus_not_eq:(r1,r2:R)``r1-r2<>0``->``r1<>r2``.
+Red; Intros; Elim H; Apply eq_Rminus; Auto.
+Save.
+Hints Resolve Rminus_not_eq : real.
+
+Lemma Rminus_not_eq_right:(r1,r2:R)``r2-r1<>0`` -> ``r1<>r2``.
+Red; Intros;Elim H;Rewrite H0; Ring.
+Save.
+Hints Resolve Rminus_not_eq_right : real. 
+
 (**********)
 Lemma Rminus_distr:  (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``.
 Intros; Ring.
@@ -752,7 +777,6 @@ Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` ->
 Intros; Apply Rlt_trans with ``r2*r3``; Auto with real.
 Save.
 
-
 (*s Order and Substractions *)
 Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``.
 Intros; Apply (Rlt_anti_compatibility ``r2``).
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 4cce53ce47..591bc22e42 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -15,6 +15,9 @@
 
 Require Export Rbasic_fun.
 Require Export Classical_Prop.
+Require DiscrR.
+Require Fourier.
+Require SplitAbsolu.
 
 (*******************************)
 (*      Calculus               *)
@@ -22,34 +25,13 @@ Require Export Classical_Prop.
 (*********)
 Lemma eps2_Rgt_R0:(eps:R)(Rgt eps R0)->
       (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0).
-Intros;Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Intro;
- Elim (Rplus_ne R1);Intros a b;Rewrite a in H0;Clear a b;
- Generalize (Rlt_Rinv (Rplus R1 R1) 
-                       (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H0));Intro;
- Unfold Rgt in H;
- Generalize (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps H1 H);Intro;
- Rewrite (Rmult_Or (Rinv (Rplus R1 R1))) in H2;
- Rewrite (Rmult_sym (Rinv (Rplus R1 R1)) eps) in H2;
- Unfold Rgt;Assumption.
+Intros;Fourier.
 Save.
 
 (*********)
 Lemma eps2:(eps:R)(Rplus (Rmult eps (Rinv (Rplus R1 R1)))
                         (Rmult eps (Rinv (Rplus R1 R1))))==eps.
-Intro;Rewrite<-(Rmult_Rplus_distr eps (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1)));
- Elim (Rmult_ne eps);Intros a b;Pattern 2 eps;Rewrite <- a;Clear a b;
- Apply Rmult_mult_r;Clear eps;Cut ~(Rplus R1 R1)==R0.
-Intro;Apply (r_Rmult_mult (Rplus R1 R1) 
-         (Rplus (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1))) R1);Auto;
-Rewrite (Rmult_Rplus_distr (Rplus R1 R1) (Rinv (Rplus R1 R1)) 
-                              (Rinv (Rplus R1 R1)));
- Rewrite (Rinv_r (Rplus R1 R1) H);Elim (Rmult_ne (Rplus R1 R1));Intros a b;
- Rewrite a;Clear a b;Reflexivity.
-Red;Intro;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H0);Intro;Elim (Rplus_ne R1);
- Intros a b;Rewrite a in H1;Clear a b;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H0 H1);Intro;
- Elim (imp_not_Req R0 (Rplus R1 R1));Auto;Left;Assumption.
+Intro esp;Field;DiscrR.
 Save.
 
 (*********)
@@ -57,50 +39,19 @@ 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;Rewrite<-(Rmult_Rplus_distr eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
-                            (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
- Apply Rmult_mult_r;Clear eps;
- Rewrite <-(let (H1,H2)=
-     (Rmult_ne (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) in H1);
- Rewrite <-(Rmult_Rplus_distr (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) R1 R1);
- Cut ~(Rplus R1 R1)==R0. 
-Intro;Apply (r_Rmult_mult (Rplus R1 R1) 
-           (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) (Rplus R1 R1)) 
-           (Rinv (Rplus R1 R1)));Auto.
-Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
-                      (Rplus R1 R1));
- Rewrite <-(Rmult_assoc (Rplus R1 R1) (Rplus R1 R1) 
-             (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
- Rewrite (Rinv_r (Rplus R1 R1) H);Rewrite (Rmult_Rplus_distr (Rplus R1 R1) R1 R1);
- Rewrite (let (H1,H2)=(Rmult_ne (Rplus R1 R1)) in H1);
- Apply (Rinv_r (Rplus (Rplus R1 R1) (Rplus R1 R1))).
-Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
- Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H0);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H0 H1);Intro;
- Clear H0 H1;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H2);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H0;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
-    H2 H0).
-Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H H0).
+Intro eps;Field;DiscrR.
 Save.
 
 (*********)
 Lemma Rlt_eps2_eps:(eps:R)(Rgt eps R0)->
         (Rlt (Rmult eps (Rinv (Rplus R1 R1))) eps).
-Intros;Unfold Rgt in H;Elim (Rmult_ne eps);Intros a b;Pattern 2 eps;
- Rewrite <- a;Clear a b;
+Intros;Unfold Rgt in H;Pattern 2 eps;Rewrite <- Rmult_1r;
  Apply (Rlt_monotony eps (Rinv (Rplus R1 R1)) R1 H);
  Apply (Rlt_anti_compatibility (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1))
-      R1);Elim (Rmult_ne (Rinv (Rplus R1 R1)));Intros a b;
- Pattern 1 2 (Rinv (Rplus R1 R1));Rewrite <-b;Clear a b;
- Rewrite (eps2 R1);Elim (Rplus_ne R1);Intros a b;Pattern 1 R1;
- Rewrite <-a;Clear a b;Rewrite (Rplus_sym (Rinv (Rplus R1 R1)) R1);
+      R1);Pattern 1 2 (Rinv (Rplus R1 R1));Rewrite <-Rmult_1l;
+ Rewrite (eps2 R1);
+ Pattern 1 R1;Rewrite <-Rplus_Or;
+ Rewrite (Rplus_sym (Rinv (Rplus R1 R1)) R1);
  Apply (Rlt_compatibility R1 R0 (Rinv (Rplus R1 R1)) 
    (Rlt_Rinv (Rplus R1 R1) (Rlt_r_plus_R1 R1 (Rlt_le R0 R1 Rlt_R0_R1)))). 
 Save.
@@ -231,24 +182,19 @@ Save.
 
 (*********)
 Lemma R_dist_sym:(x,y:R)(R_dist x y)==(R_dist y x).
-Intros; Unfold R_dist; Unfold Rabsolu;
- Case (case_Rabsolu (Rminus x y)); Case (case_Rabsolu (Rminus y x));
- Intros l l0.
-Generalize (Rlt_RoppO (Rminus y x) l); Intro;
+Unfold R_dist;Intros;SplitAbsolu;Ring.
+Generalize (Rlt_RoppO (Rminus y x) r); Intro;
  Rewrite (Ropp_distr2 y x) in H;
- Generalize (Rlt_antisym (Rminus x y) R0 l0); Intro;Unfold Rgt in H;
+ Generalize (Rlt_antisym (Rminus x y) R0 r0); Intro;Unfold Rgt in H;
  ElimType False; Auto.
-Apply (Ropp_distr2 x y).
-Apply sym_eqT;Apply (Ropp_distr2 y x). 
-Generalize (minus_Rge y x l); Intro;
- Generalize (minus_Rge x y l0); Intro;
- Generalize (Rge_ge_eq x y H0 H); Intro;Rewrite H1;Trivial.
+Generalize (minus_Rge y x r); Intro;
+ Generalize (minus_Rge x y r0); Intro;
+ Generalize (Rge_ge_eq x y H0 H); Intro;Rewrite H1;Ring.
 Save.
 
 (*********)
 Lemma R_dist_refl:(x,y:R)((R_dist x y)==R0<->x==y).
-Intros;Unfold R_dist; Unfold Rabsolu;
- Case (case_Rabsolu (Rminus x y));Intro;Split;Intro.
+Unfold R_dist;Intros;SplitAbsolu;Split;Intros.
 Rewrite (Ropp_distr2 x y) in H;Apply sym_eqT;
  Apply (Rminus_eq y x H).
 Rewrite (Ropp_distr2 x y);Generalize (sym_eqT R x y H);Intro;
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
new file mode 100644
index 0000000000..3b423aefbf
--- /dev/null
+++ b/theories/Reals/SplitAbsolu.v
@@ -0,0 +1,22 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Export Rbasic_fun.
+
+Tactic Definition SplitAbs :=
+  Match Context With
+    | [ |- [(case_Rabsolu ?1)] ] -> 
+         Case (case_Rabsolu ?1); Try SplitAbs.
+
+
+Tactic Definition SplitAbsolu :=
+  Match Context With
+    | [ id:[(Rabsolu ?)] |- ? ] -> Generalize id; Clear id;Try SplitAbsolu
+    | [ |- [(Rabsolu ?1)] ] ->  Unfold Rabsolu; Try SplitAbs;Intros.