From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 6 May 2009 14:26:06 +0000 (+0000)
Subject: apply and auto.equational_case call saturation.solve_narrowing
X-Git-Tag: make_still_working~4017
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git

apply and auto.equational_case call saturation.solve_narrowing
that performs goal inference and demodulation
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 15b2d848b..53120a44d 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -368,32 +368,12 @@ let init_cache_and_tables
 =
   let _, metasenv, subst, _, _, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let is_prop m s c t = 
-    let ty,_ = 
-      CicTypeChecker.type_of_aux' m ~subst:s c t CicUniv.oblivion_ugraph
-    in
-    let sort,_ = 
-      CicTypeChecker.type_of_aux' m ~subst:s c ty CicUniv.oblivion_ugraph
-    in
-    match CicReduction.whd ~subst c sort with
-    | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true
-    | _ -> false
-  in
   let add_list_to_tables metasenv subst automation_cache ct =
-    let _,_,bag = automation_cache.AutomationCache.tables in
-    let maxmeta = Equality.maxmeta bag in
-    List.fold_left
-      (fun (c,maxmeta) (t,ty) ->            
-         let head, metasenv, args, maxmeta =
-           TermUtil.saturate_term maxmeta metasenv context ty 0
-         in
-         if List.exists (is_prop metasenv subst context) args then
-           c,maxmeta
-         else
-           let st = if args = [] then t else Cic.Appl (t::args) in
-           AutomationCache.add_term_to_active 
-             c metasenv [] context st (Some head), maxmeta)
-       (automation_cache,maxmeta) ct
+    List.fold_left 
+      (fun automation_cache (t,_) -> 
+          AutomationCache.add_term_to_active automation_cache
+           metasenv subst context t None)
+      automation_cache ct
   in
   if restricted_univ = [] then
     let ct = 
@@ -406,29 +386,22 @@ let init_cache_and_tables
     in
     let cache = AutoCache.cache_empty in
     let cache = cache_add_list cache context (ct@lt) in  
-    let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct 
+    let automation_cache = 
+      add_list_to_tables metasenv subst automation_cache ct 
     in
-    (* AutomationCache.pp_cache automation_cache; *)
+(*     AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache
   else
-    let metasenv, t_ty, s_t_ty, _ = 
-      List.fold_left
-        (fun (metasenv as orig,acc, sacc, maxmeta) t ->
-           let ty, _ = 
-             CicTypeChecker.type_of_aux' 
-               metasenv ~subst:[] context t CicUniv.oblivion_ugraph 
-           in
-           let head, metasenv, args, maxmeta =
-             TermUtil.saturate_term maxmeta metasenv context ty 0
-           in
-           if List.exists (is_prop metasenv subst context) args then
-             orig, (t,ty)::acc, sacc, maxmeta
-           else
-             let st = if args = [] then t else Cic.Appl (t::args) in
-             metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
-        (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ
+    let t_ty = 
+      List.map
+        (fun  t ->
+          let ty, _ = CicTypeChecker.type_of_aux' 
+            metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+          in
+            t, ty)
+        restricted_univ
     in
     (* let automation_cache = AutomationCache.empty () in *) 
     let automation_cache = 
@@ -439,74 +412,21 @@ let init_cache_and_tables
       { automation_cache with AutomationCache.univ = universe }
     in
     let ct = 
-      if use_context then find_context_theorems context metasenv else [] 
-    in
-    let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct
+     if use_context then find_context_theorems context metasenv else t_ty
     in
-    (* proviamo a tenere tutte le equazioni 
     let automation_cache = 
-     List.fold_left
-      (fun c (t,ty) ->            
-         AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
-       automation_cache s_t_ty
-    in *)
+      add_list_to_tables metasenv subst automation_cache ct
+    in
     (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
-    (* cache_add_list cache_empty context t_ty *)
     cache_empty
 ;;
-  (*
-(*   let signature = MetadataQuery.signature_of metasenv goal in *)
-(*   let newmeta = CicMkImplicit.new_meta metasenv [] in *)
-  let equations = 
-    retrieve_equations dont_filter (* true *) signature universe cache context metasenv 
-  in
-  debug_print 
-    (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
-  let eqs_and_types =
-    HExtlib.filter_map 
-      (fun t -> 
-         let ty,_ =
-           CicTypeChecker.type_of_aux' 
-             metasenv context t CicUniv.oblivion_ugraph
-         in
-         (* retrieve_equations could also return flexible terms *)
-         if is_an_equality ty then Some(t,ty) 
-         else
-           try
-             let ty' = unfold context ty in
-             if is_an_equality ty' then Some(t,ty') else None
-           with ProofEngineTypes.Fail _ -> None) 
-      equations
-  in
-  let bag = Equality.mk_equality_bag () in
-  let units, other_equalities, newmeta = 
-    partition_unit_equalities context metasenv newmeta bag eqs_and_types 
-  in
-  (* SIMPLIFICATION STEP 
-  let equalities = 
-    let env = (metasenv, context, CicUniv.oblivion_ugraph) in 
-    let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
-    Saturation.simplify_equalities bag eq_uri env units 
-  in 
-  *)
-  let passive = Saturation.make_passive units in
-  let no = List.length units in
-  let active = Saturation.make_active [] in
-  let active,passive,newmeta = 
-    if paramod then active,passive,newmeta
-    else
-      Saturation.pump_actives 
-        context bag newmeta active passive (no+1) infinity
-  in 
-    (active,passive,bag),cache,newmeta
-*)
 
-let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast = 
+let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast = 
   let actives, passives, bag = tables in 
   let bag, head, metasenv, args = 
-    Equality.saturate_term bag metasenv context term 
+    Equality.saturate_term bag metasenv subst context term 
   in
   let tables = actives, passives, bag in 
   let propositional_args = 
@@ -568,14 +488,14 @@ let fill_hypothesis context metasenv term tables (universe:Universe.universe) ca
   results,cache,tables
 ;;
 
-let build_equalities auto context metasenv tables universe cache equations =
+let build_equalities auto context metasenv subst tables universe cache equations =
   List.fold_left 
     (fun (tables,facts,cache) (t,ty) ->
        (* in any case we add the equation to the cache *)
        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
        try
          let saturated, cache, tables = 
-           fill_hypothesis context metasenv ty tables universe cache auto true
+           fill_hypothesis context metasenv subst ty tables universe cache auto true
          in
          let eqs, tables = 
            List.fold_left 
@@ -598,7 +518,7 @@ let build_equalities auto context metasenv tables universe cache equations =
 
 let close_more tables context status auto universe cache =
   let proof, goalno = status in
-  let _, metasenv,_subst,_,_, _ = proof in  
+  let _, metasenv,subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = 
     retrieve_equations false signature universe cache context metasenv 
@@ -613,7 +533,7 @@ let close_more tables context status auto universe cache =
            if is_an_equality ty then Some(t,ty) else None)
       equations in
   let tables, units, cache = 
-    build_equalities auto context metasenv tables universe cache eqs_and_types 
+    build_equalities auto context metasenv subst tables universe cache eqs_and_types 
   in
   let active,passive,bag = tables in
   let passive = Saturation.add_to_passive units passive in
@@ -629,7 +549,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _,metasenv,_subst,_,_, _ = proof in
+  let _,metasenv,subst,_,_, _ = proof in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
   let rec aux tables cache index = function
@@ -644,7 +564,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe
               (try 
                 let term = S.lift index term in
                 let saturated, cache, tables = 
-                  fill_hypothesis context metasenv term 
+                  fill_hypothesis context metasenv subst term 
                     tables universe cache default_auto false
                 in
                 let actives, passives, bag = tables in 
@@ -1115,8 +1035,8 @@ let apply_smart_aux
            automation_cache univ (proof'''',newmeta)
         in
         match
-          Saturation.given_clause bag (proof'''',newmeta) active passive 
-            1 0 infinity
+          Saturation.solve_narrowing bag (proof'''',newmeta) active passive 
+            1 (*0 infinity*)
         with 
           | None, active, passive, bag -> 
               raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
@@ -1619,8 +1539,7 @@ let equational_case
           1,0,flags.timeout 
         in
         match
-          Saturation.given_clause bag status active passive 
-            goal_steps saturation_steps timeout
+          Saturation.solve_narrowing bag status active passive goal_steps 
         with 
           | None, active, passive, bag -> 
               [], (active,passive,bag), cache, flags
diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml
index 7d8e7d129..34bb3efdf 100644
--- a/helm/software/components/tactics/automationCache.ml
+++ b/helm/software/components/tactics/automationCache.ml
@@ -67,7 +67,7 @@ let add_term_to_active cache metasenv subst context t ty_opt =
             ~subst metasenv context t CicUniv.oblivion_ugraph
         in
         let bag, head, metasenv, args =
-          Equality.saturate_term bag metasenv context ty
+          Equality.saturate_term bag metasenv subst context ty
         in
         let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
         let t = if args = [] then t else Cic.Appl (t:: args) in
diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 428e858c5..139dcb1f8 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -29,7 +29,7 @@ let mk_just ~dbd ~automation_cache =
  function
     `Auto (l,params) -> 
        Tactics.auto ~dbd 
-       ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~automation_cache
+       ~params:(l,("skip_trie_filtering","1")::(*("skip_context","1")::*)params) ~automation_cache
   | `Term t -> Tactics.apply t
 ;;
 
diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 5888019e4..cb12f7a77 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -1365,7 +1365,8 @@ let draw_proof bag names goal_proof proof id =
   ignore(Unix.system "gv /tmp/matita_paramod.eps");
 ;;
 
-let saturate_term (id_to_eq, maxmeta) metasenv context term = 
+let saturate_term (id_to_eq, maxmeta) metasenv subst context term = 
+  let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
   let head, metasenv, args, newmeta =
     TermUtil.saturate_term maxmeta metasenv context term 0
   in
diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index b4aa66d29..d60164689 100644
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -123,7 +123,8 @@ val equality_of_term:
 val term_of_equality: UriManager.uri -> equality -> Cic.term
 val term_is_equality: Cic.term -> bool
 
-val saturate_term : equality_bag -> Cic.metasenv -> Cic.context -> Cic.term ->
+val saturate_term : 
+     equality_bag -> Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term ->
          equality_bag * Cic.term * Cic.metasenv * Cic.term list
 
 val push_maxmeta : equality_bag -> int -> equality_bag 
diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index b759427e3..cf4bcd555 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -1249,6 +1249,7 @@ let rec demodulation_goal bag env table goal =
 (* returns all the 1 step demodulations *)
 module C = Cic;; 
 module S = CicSubstitution;;
+
 let rec demodulation_all_aux 
   metasenv context ugraph table lift_amount term 
 =
@@ -1266,17 +1267,22 @@ let rec demodulation_all_aux
       in
       match term with
       | C.Appl l ->
-         let res, _, _ = 
+         let res, _, _, _ = 
            List.fold_left
-            (fun (res,l,r) t ->
-               res @ 
-               List.map 
-                 (fun (rel, s, m, ug, c) -> 
-                   (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
-                 (demodulation_all_aux 
-                   metasenv context ugraph table lift_amount t),
-               l@[List.hd r], List.tl r)
-            (res, [], List.map (S.lift 1) l) l
+            (fun (res,b,l,r) t ->
+               if not b then res,b,l,r
+               else
+                 let demods_for_t = 
+                   demodulation_all_aux 
+                     metasenv context ugraph table lift_amount t
+                 in
+                 let b = demods_for_t = [] in
+                 res @  
+                   List.map 
+                    (fun (rel, s, m, ug, c) -> 
+                      (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+                   demods_for_t, b, l@[List.hd r], List.tl r)
+            (res, true, [], List.map (S.lift 1) l) l
          in
          res
       | t -> res
@@ -1287,10 +1293,10 @@ let demod_all steps bag env table goal =
   let is_visited l (_,_,t) = 
     List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l 
   in
-  let rec aux steps visited bag = function
-    | _ when steps = 0 -> visited, bag, []
-    | [] -> visited, bag, []
-    | goal :: rest when is_visited visited goal -> aux steps visited bag rest
+  let rec aux steps visited nf bag = function
+    | _ when steps = 0 -> visited, bag, nf
+    | [] -> visited, bag, nf
+    | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
     | goal :: rest ->
         let visited = goal :: visited in
         let _,menv,t = goal in
@@ -1299,12 +1305,57 @@ let demod_all steps bag env table goal =
         let new_goals = 
           List.map (build_newg bag context goal Equality.Demodulation) res 
         in
-        let visited, bag, res = aux steps visited bag (new_goals @ rest) in
-        visited, bag, goal :: res
+        let nf = if new_goals = [] then goal :: nf else nf in
+        aux steps visited nf bag (new_goals @ rest)
   in
-   aux steps [] bag [goal]
+  aux steps [] [] bag [goal] 
 ;;
 
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+  let proof,m,eq,ty,left,right = open_goal goal in
+  let pl = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+          | _ -> assert false                 
+        in
+        rule,pos,id,subst,pred)
+      pl
+  in
+  let pr = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+          | _ -> assert false                 
+        in
+        rule,pos,id,subst,pred)
+      pr
+  in
+  (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+  let proof,menv,eq,ty,left,right = open_goal goal in
+  let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+  let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+  let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+  let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+  List.fold_left
+    (fun acc (_,_,l as ld) -> 
+       List.fold_left 
+           (fun acc (_,_,r as rd) ->
+                combine_demodulation_proofs bag env goal ld rd :: acc)
+         acc r_demod)
+    [] l_demod
+;;
 
 let solve_demodulating bag env table initgoal steps =
   let proof,menv,eq,ty,left,right = open_goal initgoal in
diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 8370d9da3..e36cfba49 100644
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -94,6 +94,12 @@ val demodulation_goal :
   Index.t ->
   Equality.goal ->
   bool * Equality.goal
+val demodulation_all_goal :
+  Equality.equality_bag ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.goal -> int ->
+    Equality.goal list
 val demodulation_theorem :
   Equality.equality_bag ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 96b4d515b..be3d21aa1 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -298,7 +298,7 @@ let add_to_passive passive new_pos preferred =
       pos 
   in
   pos_head @ pos_list @ pos_tail, add pos_set pos,
-   List.fold_left Indexing.index pos_table new_pos
+   List.fold_left Indexing.index pos_table pos
 ;;
 
 (* TODO *)
@@ -902,7 +902,6 @@ let check_if_goals_set_is_solved bag env active passive goals =
             (fun bag -> check_if_goal_is_subsumed bag env (snd active));
             (fun bag -> check_if_goal_is_subsumed bag env (last passive))
              ])
-(* provare active and passive?*)
     (bag,None) (active_goals @ passive_goals)
 ;;
 
@@ -1654,6 +1653,77 @@ let given_clause
     Some (subst, proof,gl),a,p, b
 ;;
 
+let solve_narrowing bag status active passive goal_steps =
+  let proof, goalno = status in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
+  let canonical_menv,other_menv = 
+    List.partition (fun (_,c,_) -> c = context)  metasenv in
+  let canonical_menv = 
+    List.map 
+     (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv 
+  in
+  let metasenv' = 
+    List.filter 
+      (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal) 
+      canonical_menv 
+  in
+  let goal = [], metasenv', cleaned_goal in
+  let env = metasenv,context,CicUniv.empty_ugraph in
+  let goals = 
+    let table = List.fold_left Indexing.index (last passive) (fst active) in
+    goal :: Indexing.demodulation_all_goal bag env table goal 4
+  in
+  let rec aux newactives newpassives bag = function
+    | [] -> bag, (newactives, newpassives)
+    | hd::tl ->
+        let selected = hd in
+        let (_,m1,t1) = selected in
+        let already_in = 
+          List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
+              newactives
+        in
+        if already_in then 
+             aux newactives newpassives bag tl 
+          else
+            let bag, newpassives =
+              if Utils.metas_of_term t1 = [] then 
+                bag, newpassives
+              else 
+                let bag, new' = 
+                   Indexing.superposition_left bag env (snd active) selected
+                in
+                let new' = 
+                  List.map 
+                    (fun x -> let b, x = simplify_goal bag env x active in x)
+                    new'
+                in
+                bag, newpassives @ new'
+            in
+            aux (selected::newactives) newpassives bag tl
+  in 
+  let rec do_n bag ag pg = function
+    | 0 -> None, active, passive, bag
+    | n -> 
+        let bag, (ag, pg) = aux [] [] bag (ag @ pg) in
+        match check_if_goals_set_is_solved bag env active passive (ag,pg) with
+        | bag, None -> do_n bag ag pg (n-1)
+        | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)->
+            let subst, proof, gl =
+              build_proof bag
+                status gproof newproof subsumption_id subsumption_subst pmenv
+            in
+            let uri,metasenv,subst,meta_proof,term_to_prove,attrs = proof in
+            let proof = 
+              uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs
+            in
+            Some (subst, proof,gl),active,passive, bag
+  in
+   do_n bag [] goals goal_steps
+;;
+
 
 let add_to_passive eql passives = 
   add_to_passive passives eql eql
diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 71764cddd..d890a719d 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -74,3 +74,13 @@ val given_clause:
      ProofEngineTypes.goal list) option * 
     active_table * passive_table * Equality.equality_bag
 
+val solve_narrowing: 
+  Equality.equality_bag ->
+  ProofEngineTypes.status ->
+  active_table ->
+  passive_table -> 
+  int -> 
+    (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) option * 
+    active_table * passive_table * Equality.equality_bag
diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma
index 43c213c9b..88e2602b8 100644
--- a/helm/software/matita/library/Q/nat_fact/times.ma
+++ b/helm/software/matita/library/Q/nat_fact/times.ma
@@ -30,7 +30,7 @@ let rec times_f h g \def
 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
 =defactorize_aux g m*defactorize_aux h m.
 intro.elim g
-  [elim h;simplify;autobatch
+  [elim h;simplify;autobatch;
   |elim h
     [simplify;autobatch
     |simplify.rewrite > (H n3 (S m)).autobatch
diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index 9e7ba97f5..f2bca131f 100644
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -362,12 +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; autobatch depth=4;
+intros;
+autobatch by H, (Rlt_plus_l (-b) (a+b) c);
 (*
 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;
 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
-apply Rlt_plus_l;assumption;
+apply (Rlt_plus_l (-b) (a+b) c);assumption;
 *)
 qed.
 
diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma
index 28e254f94..2862883c5 100644
--- a/helm/software/matita/library/didactic/exercises/duality.ma
+++ b/helm/software/matita/library/didactic/exercises/duality.ma
@@ -164,6 +164,7 @@ sono necessari i seguenti lemmi:
 * lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v`
 * lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v`
 * lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3`
+* lemma `equiv_sym` : `∀F1,F2. F1 ≡ F2 → F2 ≡ F1`
 
 DOCEND*)
 
@@ -221,6 +222,7 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associat
 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
+lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed.
 
 (* Esercizio 3
    ===========
@@ -625,7 +627,7 @@ theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
  the thesis becomes (dualize F1 ≡ dualize F2).
  by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1).
  by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
- by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
+ by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2, equiv_sym we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
  by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).
  by H4 done.
 qed.
diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index aa512566e..dcdbc7b7a 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -757,7 +757,8 @@ cut (n \divides p \lor n \ndivides p)
        [elim Hcut1.elim H3.elim H4
          [rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
-          elim H1. autobatch by witness, divides_minus.
+          elim H1.
+          autobatch by witness; 
          (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
@@ -772,7 +773,7 @@ cut (n \divides p \lor n \ndivides p)
          |(* second case *)
           rewrite > (times_n_SO q).rewrite < H5.
           rewrite > distr_times_minus.
-          elim H1. autobatch by witness, divides_minus.
+          elim H1. autobatch by witness; 
           (*
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
@@ -921,10 +922,13 @@ rewrite > H4 in H2.
 elim (divides_times_to_divides ? ? ? H H2)
   [apply False_ind.apply H1.assumption
   |elim H5.
-   (* applyS (witness ? ? n2 (refl_eq ? ?)).*)
+   autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+   (*
    apply (witness ? ? n2).
    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
    rewrite > assoc_times.
-   rewrite < H6.assumption
+   autobatch.
+   (*rewrite < H6.assumption*)
+   *)
   ]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index cd53cc056..7dd4fb362 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -299,7 +299,7 @@ cut (S O < p)
          apply (lt_to_not_eq O ? H).
          rewrite > H7.
          rewrite < H10.
-         autobatch
+         autobatch;assumption;
         ]
       |elim c
         [rewrite > sym_gcd.