-applicative_case has been rewritten and simplified;

 the strategy should be clear, now.
- if we have an unkown ?n goal we instantiate it with I:True:Prop.
  Due to the topological ordering of goals, ?n should not appear
  in any other open goal, so its instantiation can be arbitrary.
- paramodulation is has only an implicit knowledge of the symmetry
  of equality, hence it is in trouble to prove (a=b) = (b=a).
  A try_sym tactic has been added to smart application to cover this
  case.

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index b841f87e76f34eba283b68b9cdd5f6479eb85ecd..af30fcf9373166de3a267ad7b22ecb788ab526a6 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -582,12 +582,42 @@ let smart_apply t unit_eq status g =
           raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
 
+let compare_statuses ~past ~present =
+ let _,_,past,_,_ = past#obj in 
+ let _,_,present,_,_ = present#obj in 
+ List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
+ List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
+;;
+
+(* paramodulation has only an implicit knoweledge of the symmetry of equality;
+   hence it is in trouble in proving (a = b) = (b = a) *) 
+let try_sym tac status g =
+  (* put the right uri *)
+  let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
+  let _,_,metasenv,subst,_ = status#obj in
+  let _, context, gty = List.assoc g metasenv in
+  let is_eq = 
+    NCicParamod.is_equation status metasenv subst context gty 
+  in
+  if is_eq then
+    try tac status g
+    with Error _ ->
+      let new_status = instantiate_with_ast status g ("",0,sym_eq) in 
+      let go, _ = compare_statuses ~past:status ~present:new_status in
+      assert (List.length go  = 1);
+      let ng = List.hd go in
+      tac new_status ng
+   else tac status g
+;;
+
 let smart_apply_tac t s =
   let unit_eq = index_local_equations s#eq_cache s in   
-  NTactics.distribute_tac (smart_apply t unit_eq) s
+  NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s 
+  (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
 
 let smart_apply_auto t eq_cache =
-  NTactics.distribute_tac (smart_apply t eq_cache)
+  NTactics.distribute_tac (try_sym (smart_apply t eq_cache)) 
+  (* NTactics.distribute_tac (smart_apply t eq_cache) *)
 
 
 (****************** types **************)
@@ -1128,79 +1158,49 @@ let applicative_case depth signature status flags gty cache =
        | _ -> false, NCicParamod.is_equation status metasenv subst context t 
   in
   debug_print ~depth (lazy (string_of_bool is_eq)); 
-  (* old 
-  let candidates, smart_candidates = 
-    get_candidates ~smart:(not is_eq) depth 
-      flags status tcache signature gty in 
-    (* if the goal is an equation we avoid to apply unit equalities,
-       since superposition should take care of them; refl is an
-       exception since it prompts for convertibility *)
-  let candidates = 
-    let test x = not (is_a_fact_ast status subst metasenv context x) in
-    if is_eq then 
-      Ast.Ident("refl",None) ::List.filter test candidates 
-    else candidates in *)
   (* new *)
   let candidates, smart_candidates = 
     get_candidates ~smart:true depth 
       flags status tcache signature gty in 
+  let test = is_a_fact_ast status subst metasenv context in
+  let candidates_facts,candidates_other =
     (* if the goal is an equation we avoid to apply unit equalities,
-       since superposition should take care of them; refl is an
-       exception since it prompts for convertibility *)
-  let candidates,smart_candidates = 
-    let test x = not (is_a_fact_ast status subst metasenv context x) in
-    if is_eq then 
-      Ast.Ident("refl",`Ambiguous) ::List.filter test candidates,
-      List.filter test smart_candidates
-    else candidates,smart_candidates in 
-  debug_print ~depth
-    (lazy ("candidates: " ^ string_of_int (List.length candidates)));
-  debug_print ~depth
-    (lazy ("smart candidates: " ^ 
-             string_of_int (List.length smart_candidates)));
- (*
-  let sm = 0 in 
-  let smart_candidates = [] in *)
+     since superposition should take care of them; refl is an
+     exception since it prompts for convertibility *)
+    let l1,l2 = List.partition test candidates in
+    (* put the right uri *)
+    if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2
+  in
+  let smart_candidates_facts, smart_candidates_other =
+    let l1,l2 = List.partition test smart_candidates in
+    if is_eq then [],l2 else l1,l2
+  in
   let sm = if is_eq then 0 else 2 in
- (* wrong: we constraint maxdepth for equality goals to three *)
- (* let maxdepth = if is_eq then min flags.maxdepth 6 else flags.maxdepth in *)
+  let sm1 = if flags.last then 2 else 0 in
   let maxd = (depth + 1 = flags.maxdepth) in 
-  let only_one = flags.last && maxd in
-  debug_print  ~depth (lazy ("only_one: " ^ (string_of_bool only_one))); 
-  debug_print  ~depth (lazy ("maxd: " ^ (string_of_bool maxd)));
-  let elems =  
+  let try_candidates only_one sm acc candidates =
     List.fold_left 
       (fun elems cand ->
          if (only_one && (elems <> [])) then elems 
-         else 
-           if (maxd && not(is_prod) & 
-                not(is_a_fact_ast status subst metasenv context cand)) 
-           then (debug_print  ~depth (lazy "pruned: not a fact"); elems)
          else
            match try_candidate (~smart:sm) 
              flags depth status cache.unit_eq context cand with
                | None -> elems
                | Some x -> x::elems)
-      [] candidates
-  in
-  let more_elems = 
-    if only_one && elems <> [] then elems 
-    else
-      List.fold_left 
-        (fun elems cand ->
-         if (only_one && (elems <> [])) then elems 
-         else 
-           if (maxd && not(is_prod) &&
-                not(is_a_fact_ast status subst metasenv context cand)) 
-           then (debug_print  ~depth (lazy "pruned: not a fact"); elems)
-         else
-           match try_candidate (~smart:2) (* was smart:1 *)
-             flags depth status cache.unit_eq context cand with
-               | None -> elems
-               | Some x -> x::elems)
-        [] smart_candidates
-  in
-  elems@more_elems
+      acc candidates
+  in 
+  (* if the goal is the last one we stop at the first fact *)
+  let elems = try_candidates flags.last sm [] candidates_facts in
+  (* now we add smart_facts *)
+  let elems = try_candidates flags.last sm elems smart_candidates_facts in
+  (* if we are at maxdepth and the goal is not a product we are done 
+     similarly, if the goal is the last one and we already found a
+     solution *)
+  if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
+  else
+    let elems = try_candidates false 2 elems candidates_other in
+    debug_print ~depth (lazy ("not facts: try smart application"));
+    try_candidates false 2 elems smart_candidates_other
 ;;
 
 exception Found