huge commit in automation:

[helm.git] / helm / software / matita / library / R / root.ma

diff --git a/helm/software/matita/library/R/root.ma b/helm/software/matita/library/R/root.ma
index 574483be7af69191278538323f10e532c5f6741f..1205fc92b94071bc3bd168d7e70fd8f0e463b37d 100644 (file)
--- a/helm/software/matita/library/R/root.ma
+++ b/helm/software/matita/library/R/root.ma
@@ -109,7 +109,7 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
    rewrite < sym_Rplus;apply Rle_minus_r_to_l;
    apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1)))
    [apply pos_times_pos_pos
-    [lapply (nat_lt_to_R_lt ?? H1);autobatch
+    [apply (nat_lt_to_R_lt ?? H1);
     |elim daemon]
    |rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l;
     rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?));
@@ -127,14 +127,21 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      rewrite < distr_Rtimes_Rplus_l;
      apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n)) 
      [apply Rle_plus_l;left;autobatch
-     |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
+     | 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; ]]
+      (*  
+      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
-     [lapply (nat_lt_to_R_lt ?? H1);autobatch
+     [apply (nat_lt_to_R_lt ?? H1);
      |elim daemon]]]]
 |elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1)))) 
  [|autobatch]
@@ -155,13 +162,13 @@ letin bound ≝ (λy:R.R0 < y ∧ Rexp_nat y n < x);
      assumption
     |apply lt_R0_Rinv;apply pos_times_pos_pos
      [apply pos_times_pos_pos
-      [lapply (nat_lt_to_R_lt ?? H1);autobatch
+      [apply (nat_lt_to_R_lt ?? H1);
       |elim daemon]
      |apply (trans_Rlt ???? H8);apply pos_times_pos_pos
       [apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
        assumption
       |apply lt_R0_Rinv;apply pos_times_pos_pos
-       [lapply (nat_lt_to_R_lt ?? H1);autobatch
+       [apply (nat_lt_to_R_lt ?? H1);
        |elim daemon]]]]]
   |split
    [(* show that h > R0, also useful in previous parts of the proof *)
@@ -366,7 +373,8 @@ qed.
 lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
                           root (m*n) x ? H1.
 [cases (root_sound n x H H1);assumption
-|autobatch
+| change in match O with (O*O); apply lt_times; assumption; 
+  (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *) 
 |intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
  [cases (root_sound n x H H1);assumption
  |cases (root_sound m (root n x H H1))