From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 13:37:34 +0000 (+0000)
Subject: nauto:
X-Git-Tag: make_still_working~3269
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e16d80cc7bf9b73cf5526934b17e2ba955a522a;p=helm.git

nauto:
- fixed indexing (now always dome in the same way)
- depth=x means: tray at depth=2 ... try at depth=x
- run auto on set of goals that are linked by occurring in each others types,
  simply distribute if there is no dependency
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index d3409bcbe..8506c3adb 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -915,37 +915,50 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
 
 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 
+let keys_of_term status t =
+  let status, orig_ty = typeof status (ctx_of t) t in
+  let _, ty, _ = saturate ~delta:max_int status orig_ty in
+  let keys = [ty] in
+  let keys = 
+    let _, ty = term_of_cic_term status ty (ctx_of ty) in
+    match ty with
+    | NCic.Const (NReference.Ref (_,NReference.Def h)) 
+    | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) 
+       when h > 0 ->
+         let _,ty,_= saturate status ~delta:(h-1) orig_ty in
+         ty::keys
+    | _ -> keys
+  in
+  status, keys
+;;
+
 let mk_th_cache status gl = 
   List.fold_left 
     (fun (status, acc) g ->
        let gty = get_goalty status g in
        let ctx = ctx_of gty in
+       debug_print(lazy("th cache for: "^ppterm status gty));
+       debug_print(lazy("th cache in: "^ppcontext status ctx));
        if List.mem_assq ctx acc then status, acc else
          let idx = InvRelDiscriminationTree.empty in
          let status,_,idx = 
-           List.fold_left (fun (status, i, idx) _ -> 
-              let t = mk_cic_term ctx (NCic.Rel i) in
-              let status, orig_ty = typeof status ctx t in
-              let _, ty, _ = saturate ~delta:max_int status orig_ty in
-              let idx = InvRelDiscriminationTree.index idx ty t in
-              let idx = 
-                let _, ty = term_of_cic_term status ty (ctx_of ty) in
-                match ty with
-                | NCic.Const (NReference.Ref (_,NReference.Def h)) 
-                | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) 
-                   when h > 0 ->
-                     let _,ty,_= saturate status ~delta:(h-1) orig_ty in
-                     InvRelDiscriminationTree.index idx ty t
-                | _ -> idx
-              in
-              status, i+1, idx)
+           List.fold_left 
+             (fun (status, i, idx) _ -> 
+                let t = mk_cic_term ctx (NCic.Rel i) in
+                debug_print(lazy("indexing: "^ppterm status t));
+                let status, keys = keys_of_term status t in
+                let idx =
+                  List.fold_left (fun idx k -> 
+                    InvRelDiscriminationTree.index idx k t) idx keys
+                in
+                status, i+1, idx)
              (status, 1, idx) ctx
           in
          status, (ctx, idx) :: acc)
     (status,[]) gl
 ;;
 
-let add_to_th t ty c = 
+let add_to_th t c ty = 
   let key_c = ctx_of t in
   if not (List.mem_assq key_c c) then
       (key_c ,InvRelDiscriminationTree.index 
@@ -960,6 +973,25 @@ let add_to_th t ty c =
       replace c
 ;;
 
+let pp_idx status idx =
+   InvRelDiscriminationTree.iter idx
+      (fun k set ->
+         debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
+         Ncic_termSet.iter 
+           (fun t -> debug_print(lazy("\t"^ppterm status t))) 
+           set)
+;;
+
+let pp_th status = 
+  List.iter 
+    (fun ctx, idx ->
+       debug_print(lazy( "-----------------------------------------------"));
+       debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
+       debug_print(lazy( "||====>  "));
+       pp_idx status idx)
+;;
+
+
 let search_in_th gty th = 
   let c = ctx_of gty in
   let rec aux acc = function
@@ -975,20 +1007,6 @@ let search_in_th gty th =
   in
     aux Ncic_termSet.empty c
 ;;
-
-let pp_th status = 
-  List.iter 
-    (fun ctx, idx ->
-       prerr_endline "-----------------------------------------------";
-       prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
-       prerr_endline "||====>  ";
-       InvRelDiscriminationTree.iter idx
-          (fun k set ->
-             prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
-             Ncic_termSet.iter 
-             (fun t -> prerr_endline ("\t"^ppterm status t)) set))
-;;
-
 type cache_examination_result =
   [ `Failed_in of int
   | `UnderInspection 
@@ -1163,14 +1181,11 @@ let intro_case status gno gty depth cache name =
    let open_goals = head_goals status#stack in
    assert (List.length open_goals  = 1);
    let open_goal = List.hd open_goals in
-   let status, cache =
-     let ngty = get_goalty status open_goal in
-     let ctx = ctx_of ngty in
-     let t = mk_cic_term ctx (NCic.Rel 1) in
-     let status, ty = typeof status ctx t in
-     let _status, ty, _args = saturate status ty in
-     status, add_to_th t ty cache 
-   in
+   let ngty = get_goalty status open_goal in
+   let ctx = ctx_of ngty in
+   let t = mk_cic_term ctx (NCic.Rel 1) in
+   let status, keys = keys_of_term status t in
+   let cache = List.fold_left (add_to_th t) cache keys in
    debug_print (lazy (" intro: "^ string_of_int open_goal));
 (*    pp_th status cache; *)
    incr candidate_no;
@@ -1223,11 +1238,15 @@ let auto_main flags signature elems cache =
         aux ((s, size, don, todo, fl)::orlist, cache)
     | (s, size, don, todo, fl)::orlist 
       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
-        debug_print (lazy ("FAIL: WIDTH"));
+        debug_print (lazy ("FAIL: WIDTH: " ^ 
+         String.concat ", " 
+           (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo))));
         aux (orlist, cache)
     | (s, size, don, todo, fl)::orlist when size > flags.maxsize ->
         debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ 
-            " > " ^ string_of_int flags.maxsize ));
+            " > " ^ string_of_int flags.maxsize ^ ": " ^ 
+         String.concat ", " 
+           (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo))));
         aux (orlist, cache)
     | _ when Unix.gettimeofday () > flags.timeout ->
         debug_print (lazy ("FAIL: TIMEOUT"));
@@ -1315,28 +1334,85 @@ let int name l def =
 let auto_tac ~params:(_univ,flags) status =
   let goals = head_goals status#stack in
   let status, cache = mk_th_cache status goals in
+(*   pp_th status cache; *)
   let depth = int "depth" flags 3 in 
+  let size  = int "size" flags 10 in 
+  let width = int "width" flags (3+List.length goals) in 
   (* XXX fix sort *)
-  let goals = List.map (fun i -> D(i,depth,P)) goals in
-  let elems = [status,0,[],goals,[]] in
+  let goals depth = List.map (fun i -> D(i,depth,P)) goals in
+  let elems depth = [status,0,[],goals depth,[]] in
   let signature = () in
   let flags = { 
-          maxwidth = 3 + List.length goals; 
-          maxsize = 10; 
+          maxwidth = width;
+          maxsize = size;
           timeout = Unix.gettimeofday() +. 3000.;
           do_types = false; 
   } in
-  match auto_main flags signature elems cache with
-  | Gaveup -> raise (Error (lazy "auto gave up", None))
-  | Proved (s, (_orlist, _cache)) -> 
-      let stack = 
-        match s#stack with
-        | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
-        | _ -> assert false
-      in
-      s#set_stack stack
+  let rec up_to x =
+    if x > depth then raise (Error (lazy "auto gave up", None))
+    else
+      match auto_main flags signature (elems x) cache with
+      | Gaveup -> up_to (x+1)
+      | Proved (s, (_orlist, _cache)) -> 
+          HLog.debug ("proved at depth " ^ string_of_int x);
+          let stack = 
+            match s#stack with
+            | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+            | _ -> assert false
+          in
+          s#set_stack stack
+  in
+    up_to 2
+;;
+
+let group_by_tac eq_predicate tactic status = 
+ let goals = head_goals status#stack in
+ if List.length goals < 2 then tactic status 
+ else
+  let eq_predicate = eq_predicate status in
+  let rec aux classes = function
+    | [] -> classes
+    | g :: tl ->
+       try
+         let c = List.find (fun c -> eq_predicate c g) classes in
+         let classes = List.filter ((<>) c) classes in
+         aux ((g::c) :: classes) tl
+       with Not_found -> aux ([g] :: classes) tl
+  in
+  let classes = aux [] goals in
+  let pos_of l1 l2 = 
+    let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
+    List.map (fun x -> List.assoc x l2) l1
+  in
+  NTactics.block_tac ([ NTactics.branch_tac ]
+    @
+    HExtlib.list_concat ~sep:[NTactics.shift_tac]
+      (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
+    @
+    [ NTactics.merge_tac ]) status
+;;
+
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+
+let type_dependency status gl g =
+  let rec closure acc = function
+    | [] -> acc
+    | x::l when IntSet.mem x acc -> closure acc l
+    | x::l ->
+        let acc = IntSet.add x acc in
+        let gty = get_goalty status x in
+        let deps = metas_of_term status gty in
+        closure acc (deps @ l)
+  in
+  not (IntSet.is_empty 
+        (IntSet.inter
+          (closure IntSet.empty gl) 
+          (closure IntSet.empty [g])))
 ;;
 
+let auto_tac ~params = 
+  group_by_tac type_dependency (auto_tac ~params)
+;;
 
 (* ========================= dispatching of auto/auto_paramod ============ *)
 let auto_tac ~params:(_,flags as params) =
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 462501e66..ed583fdaf 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -407,6 +407,11 @@ let apply_subst status ctx t =
   status, (ctx, NCicUntrusted.apply_subst subst ctx t)
 ;;
 
+let metas_of_term status (context,t) =
+ let _,_,_,subst,_ = status#obj in
+ NCicUntrusted.metas_of_term subst context t
+;;
+
 (* ============= move this elsewhere ====================*)
 
 class ['stack] status =
@@ -445,6 +450,8 @@ let ppelem = function
   | Dead -> "Dead"
 ;;
 
+let string_of_path l = String.concat "." (List.map ppelem l) ;;
+
 let path_string_of (ctx,t) =
   let len_ctx = List.length ctx in
   let rec aux arity = function
@@ -463,7 +470,9 @@ let path_string_of (ctx,t) =
     | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
     | NCic.Match _ -> [Dead]
   in 
-    aux 0 t
+  let path = aux 0 t in
+(*   prerr_endline (string_of_path path); *)
+  path
 ;;
 
 let compare e1 e2 =
@@ -474,7 +483,6 @@ let compare e1 e2 =
   | e1,e2 -> Pervasives.compare e1 e2
 ;;
 
-let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
 end
 
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index fdad9f861..f3bdd5aa1 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -40,6 +40,7 @@ val analyse_indty:
   'status * (NReference.reference * int * NCic.term list * NCic.term list)
 
 val ppterm: #pstatus -> cic_term -> string
+val ppcontext: #pstatus -> NCic.context -> string
 val whd: 
  #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term -> 
   'status * cic_term 
@@ -58,6 +59,7 @@ val apply_subst:
 val fix_sorts: cic_term -> cic_term
 val saturate :
  #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
+val metas_of_term : #pstatus as 'status -> cic_term -> int list
 
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: 
diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index 6ae8d36ad..f9655f4ca 100644
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -14,11 +14,7 @@ alias symbol "covers" (instance 1) = "covers".
 alias symbol "covers" (instance 2) = "covers set".
 alias symbol "covers" (instance 3) = "covers".
 ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
-#A; #a; #U; #V; #aU; #UV;
-nelim aU;
-##[ #c; #H; nauto; 
-##| #c; #i; #HCU; #H; @2 i; nauto; 
-##]
+#A; #a; #U; #V; #aU; #UV; nelim aU; nauto depth=4;
 nqed.
 
 ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
@@ -33,11 +29,7 @@ ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
 ##[ #n; *;
-##| #b; #i_star; #IH1; #IH2;
-    ncases (EM … b i_star);
-    ##[##2: (* nauto; *) #W; @i_star; napply W;
-    ##| nauto;
-    ##]
+##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); nauto;
 ##] 
 nqed.
 
@@ -57,7 +49,8 @@ nrecord uAx : Type[1] ≝ {
 }.
 
 ndefinition uax : uAx → Ax.
-#A; @ (uax_ A) (λx.unit); #a; #_; napply (𝐂 a ?);  nlapply one; ncases (with_ A a); nauto; 
+#A; @ (uax_ A) (λx.unit); #a; #_; 
+napply (𝐂 a ?);  nlapply one; ncases (with_ A a); nauto; 
 nqed.
 
 ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
@@ -77,19 +70,17 @@ unification hint 0 ≔ ;
 
 
 ntheorem col2_4 :
-  ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
+  ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a one. 
 #A; #a; #H; nelim H;
 ##[ #n; *;
-##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); #H4; nauto;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); nauto;
 ##] 
 nqed.
 
 ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
 
 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
-#A; #a; #U; #V; #HUV; #H; nelim H;
-##[ nauto;
-##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
+#A; #a; #U; #V; #HUV; #H; nelim H; nauto depth=4; 
 nqed.
 
 ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
@@ -136,9 +127,7 @@ naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 
 nlemma replace_char:
   ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V.
-#A; #U; #V;  #a; #H1; #H2; #E; nelim E;
-##[ #b; #Hb; @; nauto;
-##| #b; #i; #H3; #H4; @2 i; #c; #Hc; nauto; ##]
+#A; #U; #V;  #UV; #VU; #a; #aU; nelim aU; nauto;
 nqed.
 
 ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index e5859f03a..06c492e86 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1168,6 +1168,7 @@ We now proceed with the proof of the infinity rule.
 
 D*)
 
+alias symbol "covers" = "new covers set".
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)