From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 30 Apr 2009 13:04:28 +0000 (+0000)
Subject: Minor changes pro-automation
X-Git-Tag: make_still_working~4028
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=018f85bcede6c969602d8764ed2327045d8bd551;p=helm.git

Minor changes pro-automation
---

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index 785ea12d4..ce79a875b 100644
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -59,6 +59,7 @@ axiom Rtimes_x_R1 : ∀x.x * R1 = x.
 axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
 
 (*pump 200.*)
+pump 40.
 
 lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
 intros; autobatch; 
@@ -85,34 +86,20 @@ intros;cases H
 |rewrite > H2;assumption]*)
 qed.
 
-axiom Rlt_plus_l : ∀x,y,z:R.x < y → z + x < z + y.
-axiom Rlt_times_l : ∀x,y,z:R.x < y → R0 < z → z*x < z*y.
+axiom Rlt_plus_l : ∀z,x,y:R.x < y → z + x < z + y.
+axiom Rlt_times_l : ∀z,x,y:R.x < y → R0 < z → z*x < z*y.
 
 (* FIXME: these should be lemmata *)
-axiom Rle_plus_l : ∀x,y,z:R.x ≤ y → z + x ≤ z + y.
-axiom Rle_times_l : ∀x,y,z:R.x ≤ y → R0 < z → z*x ≤ z*y.
+axiom Rle_plus_l : ∀z,x,y:R.x ≤ y → z + x ≤ z + y.
+axiom Rle_times_l : ∀z,x,y:R.x ≤ y → R0 < z → z*x ≤ z*y.
 
-lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z.
-intros;
-applyS Rle_plus_l;
-autobatch;
-(*rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);*)
-(*applyS Rle_plus_l;
-applyS*) 
-cut ((x+z ≤ y+z) = (λx.(x+?≤ x+?)) ?);[5:simplify;
-  demodulate all;
-  autobatch paramodulation by sym_Rplus;
-
-applyS Rle_plus_l by sym_Rplus;
-
-cut ((x ≤ y) = (x+z ≤ y+z)); [2:
-  lapply (Rle_plus_l ?? z H); 
-  autobatch paramodulation by sym_Rplus,Hletin;
+lemma Rle_plus_r : ∀z,x,y:R.x ≤ y → x + z ≤ y + z.
+intros; autobatch.
 qed.
 
-lemma Rle_times_r : ∀x,y,z:R.x ≤ y → R0 < z → x*z ≤ y*z.
+lemma Rle_times_r : ∀z,x,y:R.x ≤ y → R0 < z → x*z ≤ y*z.
 intros;
-rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
+(* rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); *)
 autobatch;
 qed.
 
@@ -217,7 +204,7 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; demodulate all.
+intro; autobatch paramodulation. 
 (*
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
@@ -227,7 +214,7 @@ apply eq_f2;autobatch paramodulation;
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. demodulate all. (*
+intro. autobatch paramodulation. (*
 auto paramodulation.
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
@@ -355,11 +342,11 @@ qed.
 
 lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x.
 intros;
-lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
+lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
 [ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
   lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
-  cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:
-    demodulate all;]
+  cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:autobatch
+(* end auto($Revision: 9716 $) proof: TIME=2.24 SIZE=100 DEPTH=100 *) ;]
   rewrite < Hcut; assumption;
  (*
  rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
@@ -375,13 +362,16 @@ lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
 qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros; lapply (Rlt_plus_l ?? (-b) H); applyS Hletin;
-(*
+intros;
+(* cut (∀x,y.x+(-x+y) = y);[2:
+intros.demodulate all.]
+applyS (Rlt_plus_l c (-?+a) (-b) ?) by (Hcut c a);
+ [2: applyS Hletin;
+lapply (Rlt_plus_l (-b) ?? H); autobatch; applyS Hletin; *)
 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;
 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
 apply Rlt_plus_l;assumption;
-*)
 qed.
 
 lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.
diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma
index 1205fc92b..50f98d9a9 100644
--- a/helm/software/matita/library/R/root.ma
+++ b/helm/software/matita/library/R/root.ma
@@ -128,17 +128,12 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) 
      [apply Rle_plus_l;left;autobatch
      | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
-       applyS Rexp_nat_tech;
-       [ unfold lt; change in H1 with (O < n);
-         autobatch; (*applyS H1;*)
-       | assumption;
-       | elim daemon; ]]
-      (*  
+       (* applyS Rexp_nat_tech by sym_Rtimes, assoc_Rtimes;*)
       rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
       rewrite < assoc_Rtimes;apply Rexp_nat_tech
       [autobatch
       |assumption
-      |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]*)
+      |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]
     |intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
      rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
      [apply (nat_lt_to_R_lt ?? H1);
@@ -254,7 +249,7 @@ intro;elim f;simplify
  |simplify;cases z;simplify
   [1,3:autobatch
   |rewrite < plus_n_O;rewrite > plus_n_O in ⊢ (?%?);
-   apply lt_plus;autobatch]
+   apply lt_plus;autobatch depth=2]
  |simplify;cases z;simplify;
   [1,3:autobatch
   |rewrite < plus_n_O;rewrite > (times_n_O O) in ⊢ (?%?);