From 765eb07cafb8a06a5027f4569ad06d805aba2488 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Apr 2009 14:53:46 +0000
Subject: [PATCH] run check_if_goal_is_solved on all goals (active+passive)

---
 .../tactics/paramodulation/saturation.ml      |  2 +-
 helm/software/matita/library/R/r.ma           | 21 ++++++++-----------
 .../matita/library/demo/power_derivative.ma   |  7 +++++--
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index fb6017839..96b4d515b 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -903,7 +903,7 @@ let check_if_goals_set_is_solved bag env active passive goals =
             (fun bag -> check_if_goal_is_subsumed bag env (last passive))
              ])
 (* provare active and passive?*)
-    (bag,None) active_goals
+    (bag,None) (active_goals @ passive_goals)
 ;;
 
 let infer_goal_set bag env active goals = 
diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index ce79a875b..9e7ba97f5 100644
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -204,18 +204,18 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; autobatch paramodulation. 
-(*
+(*intro; autobatch paramodulation.*)  
+intros;
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 rewrite < assoc_Rplus;
 apply eq_f2;autobatch paramodulation;
-*)
+
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. autobatch paramodulation. (*
-auto paramodulation.
+intro. (*autobatch paramodulation.*) 
+
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
@@ -225,7 +225,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 apply eq_f2 [reflexivity]
 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
-*)
+
 qed.
 
 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
@@ -362,16 +362,13 @@ 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;
-(* 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; *)
+intros; autobatch depth=4;
+(*
 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/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 8e7483e96..a425dfcc3 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -259,10 +259,13 @@ theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n).
      (D[X \sup (1+m)])
    = (D[X · X \sup m]).
    = (D[X] · X \sup m + X · D[X \sup m]).
-   = (X \sup m + X · (m · X \sup (pred m))) timeout=30.
+   = (X \sup m + X · (m · X \sup (pred m))). 
+   lapply depth=0 Fmult_associative;
+   lapply depth=0 Fmult_commutative;
+   = (X \sup m + m · (X · X \sup (pred m))) by Fmult_associative, Fmult_commutative.
    = (X \sup m + m · (X \sup (1 + pred m))).
    = (X \sup m + m · X \sup m).
-   = ((1+m) · X \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
+   = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
   done.
 qed.
 
-- 
2.39.2