From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 May 2006 20:29:21 +0000 (+0000)
Subject: - proofs by subsumption now add a symmetry step if needed
X-Git-Tag: 0.4.95@7852~1401
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b75bf92c6232210cb5fcce8683a7d6c0e7a3235;p=helm.git

- proofs by subsumption now add a symmetry step if needed
- a little optimization for Equality.depend (just to aviod te exponenetial
  factor, but should be made faster)
- restored names in Lambda abstraction that give infos about the step they
  represent
---

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index b10dc818e..b5fc4543b 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -141,17 +141,26 @@ let string_of_proof ?(names=[]) p gp =
       gp)
 ;;
 
-let rec depend eq id =
+let rec depend eq id seen =
   let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
-  if id = ideq then true else  
-  match p with
-      Exact _ -> false
-    | Step (_,(_,id1,(_,id2),_)) ->
-        let eq1 = Hashtbl.find id_to_eq id1 in
-        let eq2 = Hashtbl.find id_to_eq id2 in  
-        depend eq1 id || depend eq2 id
+  if List.mem ideq seen then 
+    false,seen
+  else
+    if id = ideq then 
+      true,seen
+    else  
+      match p with
+      | Exact _ -> false,seen
+      | Step (_,(_,id1,(_,id2),_)) ->
+          let seen = ideq::seen in
+          let eq1 = Hashtbl.find id_to_eq id1 in
+          let eq2 = Hashtbl.find id_to_eq id2 in  
+          let b1,seen = depend eq1 id seen in
+          if b1 then b1,seen else depend eq2 id seen
 ;;
 
+let depend eq id = fst (depend eq id []);;
+
 let ppsubst = Subst.ppsubst ~names:[];;
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
@@ -199,6 +208,13 @@ let open_trans ens tl =
     | _ -> assert false   
 ;;
 
+let open_sym ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [ty;l;r;p] -> ty,l,r,p
+    | _ -> assert false   
+;;
+
 let open_eq_ind args =
   match args with 
   | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
@@ -321,6 +337,10 @@ let contextualize uri ty left right t =
    * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
    *)
     let rec aux uri ty left right ctx_d = function
+      | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
+        when LibraryObjects.is_sym_eq_URI uri_sym  ->
+          let ty,l,r,p = open_sym ens tl in
+          mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
       | Cic.LetIn (name,body,rest) ->
           (* we should go in body *)
           Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
@@ -512,9 +532,6 @@ let string_of_id names id =
       Not_found -> assert false
 
 let pp_proof names goalproof proof subst id initial_goal =
-  prerr_endline ("AAAAA" ^ string_of_int id);
-  prerr_endline (String.concat "+" (List.map string_of_int (wfo goalproof proof
-  id)));
   String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ 
   "\ngoal:\n   " ^ 
     (String.concat "\n   " 
@@ -544,7 +561,10 @@ let get_duplicate_step_in_wfo l p =
     match p with 
     | Exact _ -> true
     | _ -> 
-        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1);false
+        try 
+          let (pos,no) = Hashtbl.find h i in
+          Hashtbl.replace h i (pos,no+1);
+          false
         with Not_found -> Hashtbl.add h i (n,1);true
   in
   let rec aux n = function
@@ -578,9 +598,20 @@ let build_proof_term h lift proof =
   in
   let rec aux = function
      | Exact term -> CicSubstitution.lift lift term
-     | Step (subst,(_, id1, (pos,id2), pred)) ->
+     | Step (subst,(rule, id1, (pos,id2), pred)) ->
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
+         let varname = 
+           match rule with
+           | SuperpositionRight -> Cic.Name ("SupR" ^ Utils.string_of_pos pos) 
+           | Demodulation -> Cic.Name ("DemEq"^ Utils.string_of_pos pos)
+           | _ -> assert false
+         in
+         let pred = 
+           match pred with
+           | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+           | _ -> assert false
+         in
          let p =   build_proof_step lift subst p1 p2 pos l r pred in
 (*	 let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
 	   if not cond then
@@ -617,20 +648,19 @@ let build_goal_proof l initial ty se =
           let p,l,r = proof_of_id id in
            let p = build_proof_term h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
-           let sym,pred = 
-             match rule with 
-             | SuperpositionLeft when pos = Utils.Left -> 
-                 let pred = 
-                   match pred with 
-                   | Cic.Lambda (name,ty,Cic.Appl[eq;ty1;l;r]) ->
-                       Cic.Lambda (name,ty,Cic.Appl[eq;ty1;r;l])
-                   | _ -> assert false
-                 in
-                 true, pred
-             | _ -> false,pred 
-           in    
+         let varname = 
+           match rule with
+           | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) 
+           | Demodulation -> Cic.Name ("DemG"^ Utils.string_of_pos pos)
+           | _ -> assert false
+         in
+         let pred = 
+           match pred with
+           | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+           | _ -> assert false
+         in
            let proof = 
-             build_proof_step ~sym letsno subst current_proof p pos l r pred
+             build_proof_step letsno subst current_proof p pos l r pred
            in
            let proof,se = aux se proof tl in
            Subst.apply_subst_lift letsno subst proof,
diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 524c06eff..da76559e8 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -386,7 +386,7 @@ let subsumption_aux use_unification env table target =
         find_all_matches ~unif_fun
           metasenv context ugraph 0 left ty leftc
   in
-  let rec ok what = function
+  let rec ok what leftorright = function
     | [] -> None
     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
@@ -398,13 +398,13 @@ let subsumption_aux use_unification env table target =
             unif_fun metasenv m context what' other' ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
-          | None -> ok what tl
-          | Some s -> Some (s, equation))
+          | None -> ok what leftorright tl
+          | Some s -> Some (s, equation, leftorright))
         with 
         | Inference.MatchingFailure 
-        | CicUnification.UnificationFailure _ -> ok what tl
+        | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
-  match ok right leftr with
+  match ok right Utils.Left  leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
@@ -415,7 +415,7 @@ let subsumption_aux use_unification env table target =
                 find_all_matches ~unif_fun
                   metasenv context ugraph 0 right ty rightc
       in
-        ok left rightr
+        ok left Utils.Right rightr 
 ;;
 
 let subsumption x y z =
diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index fe8582e92..8fd618702 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -45,12 +45,12 @@ val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality) option
+  (Subst.substitution * Equality.equality * Utils.pos) option
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality) option
+  (Subst.substitution * Equality.equality * Utils.pos) option
 val superposition_left :
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t ->
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b71f5e5b6..faae7b15f 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -404,34 +404,12 @@ let check_for_deep_subsumption env active_table eq =
       Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
     match Indexing.subsumption env active_table eqtmp with
     | None -> false
-    | Some (s,eq') -> 
-(*
-        prerr_endline 
-          ("\n\n " ^ Equality.string_of_equality ~env eq ^ 
-          "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ 
-          Equality.string_of_equality ~env eq' ^ "\n\n");
-*)
-        true        
+    | Some _ -> true        
   in 
   let rec aux b (ok_so_far, subsumption_used) t1 t2  = 
     match t1,t2 with
       | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
       | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
-(* VERSIONE ERRATA 
-      | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
-          let rc = check_subsumed b t1 t1 in 
-            if rc then 
-              true, true
-            else if h1 = h2 then
-              (try 
-                 List.fold_left2 
-                   (fun (ok_so_far, subsumption_used) t t' -> 
-                      aux true (ok_so_far, subsumption_used) t t')
-                   (ok_so_far, subsumption_used) l l'
-               with Invalid_argument _ -> false,subsumption_used)
-            else
-              false, subsumption_used
-      | _ -> false, subsumption_used *)
       | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
           let rc = check_subsumed b t1 t2 in 
             if rc then 
@@ -450,20 +428,6 @@ let check_for_deep_subsumption env active_table eq =
   fst (aux false (true,false) left right)
 ;;
 
-(*
-let check_for_deep env active_table eq =
-  match Indexing.subsumption env active_table eq with
-  | None -> false
-  | Some _ -> true
-;;
-*)
-
-let profiler = HExtlib.profile "check_for_deep";;
-
-let check_for_deep_subsumption env active_table eq = 
-  profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq
-;;
-
 (* buttare via sign *)
 
 (** simplifies current using active and passive *)
@@ -479,17 +443,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if Equality.is_identity env newcurrent then
-(*         debug_print  *)
-(*           (lazy *)
-(*              (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
-(*                 (string_of_equality current) *)
-(*                 (string_of_equality newcurrent))); *)
-(*         debug_print *)
-(*           (lazy *)
-(*              (Printf.sprintf "active is: %s" *)
-(*                 (String.concat "\n"  *)
-(*                    (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
-        None
+      None
     else
       Some newcurrent
   in
@@ -541,7 +495,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 (*              if Indexing.subsumption env active_table c = None then*)
                 (match Indexing.subsumption env passive_table c with
                 | None -> res
-                | Some (_,c') -> 
+                | Some (_,c',_) -> 
                     None
                     (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
                     Some c'*))
@@ -551,15 +505,6 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 *)
 ;;
 
-type fs_time_info_t = {
-  mutable build_all: float;
-  mutable demodulate: float;
-  mutable subsumption: float;
-};;
-
-let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
-
-
 (** simplifies new using active and passive *)
 let forward_simplify_new env new_pos ?passive active =
   if Utils.debug_metas then
@@ -589,8 +534,7 @@ let forward_simplify_new env new_pos ?passive active =
     List.fold_left
       (fun s e ->
          if not (Equality.is_identity env e) then
-(*            if EqualitySet.mem e s then s *)
-           (*else*) EqualitySet.add e s
+           EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
   in
@@ -604,9 +548,6 @@ let forward_simplify_new env new_pos ?passive active =
         (fun e -> ((Indexing.subsumption env active_table e = None) &&
                          (Indexing.subsumption env passive_table e = None)))
   in
-(*   let t1 = Unix.gettimeofday () in *)
-(*   let t2 = Unix.gettimeofday () in *)
-(*   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *)
   let is_duplicate =
     match passive_table with
     | None ->
@@ -940,12 +881,35 @@ let print_goals goals =
            in
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
+              
+(* adds a symmetry step *)
+let symmetric pred eq eq_ty l id uri m =
+  let pred = 
+    Cic.Lambda (Cic.Name "Sym",eq_ty,
+     Cic.Appl [CicSubstitution.lift 1 eq ;
+               CicSubstitution.lift 1 eq_ty;
+               Cic.Rel 1;CicSubstitution.lift 1 l]) 
+  in
+  let prefl = 
+    Equality.Exact (Cic.Appl
+      [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
+  in
+  let id1 = 
+    let eq = Equality.mk_equality (0,prefl,(eq_ty,l,l,Eq),m) in
+    let (_,_,_,_,id) = Equality.open_equality eq in
+    id
+  in
+  Equality.Step(Subst.empty_subst,
+    (Equality.Demodulation,id1,(Utils.Left,id),pred))
+;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
+(*
   let names = names_of_context ctx in
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
+*)
   match ty with
-  | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
+  | Cic.Appl[Cic.MutInd(uri,_,_) as eq;eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
@@ -953,12 +917,18 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
       in
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
-        | Some (subst, equality ) ->
+        | Some (subst, equality, pos ) ->
             prerr_endline 
               ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
             prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+            let p =
+              if pos = Utils.Left then
+                symmetric pred eq eq_ty l id uri m
+              else
+                p
+            in
             Some (goalproof, p, id, subst, cicmenv)
         | None -> None)
   | _ -> None
@@ -1749,7 +1719,7 @@ let saturate
       given_clause_fullred dbd env goals theorems passive active
 *)
       let goals = make_goal_set goal in
-      let max_iterations = 1000 in
+      let max_iterations = 10000 in
       let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in