more transitivity on proofs

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 953635dbd8e65df346c11dbc45c0f683f4c3d42f..7ad20206a448a9f2a5fce4ab45d49e02b6c58afc 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -309,8 +309,8 @@ let rec string_of_proof_old ?(names=[]) = function
 
 let proof_of_id id =
   try
-    let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
-      p,m,l,r
+    let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+      p,l,r
   with
       Not_found -> assert false
 
@@ -325,7 +325,7 @@ let string_of_proof_new ?(names=[]) p gp =
     | Utils.Left -> "left"
     | Utils.Right -> "right"
   in
-  let fst4 (x,_,_,_) = x in
+  let fst3 (x,_,_) = x in
   let rec aux margin name = 
     let prefix = String.make margin ' ' ^ name ^ ": " in function 
     | Exact t -> 
@@ -335,8 +335,8 @@ let string_of_proof_new ?(names=[]) p gp =
         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
           prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
           (CicPp.pp pred names)^ 
-        aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^ 
-        aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2)) 
+        aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
+        aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
   in
   aux 0 "" p ^ 
   String.concat "\n" 
@@ -345,15 +345,15 @@ let string_of_proof_new ?(names=[]) p gp =
         (Printf.sprintf 
           "GOAL: %s %d %s %s\n" 
             (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ 
-        aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
+        aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
       gp)
 ;;
 
 let ppsubst = ppsubst ~names:[]
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
-let build_ens_for_sym_eq sym_eq_URI termlist =
-  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+let build_ens uri termlist =
+  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
       assert (List.length uris <= List.length termlist);
@@ -380,7 +380,7 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
         do_build_goal_proof proofbit proof
     | ProofSymBlock (termlist, proof) ->
         let proof = do_build_proof proof in
-        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
+        let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
         let t' = Cic.Lambda (name, ty, bo) in
@@ -423,66 +423,273 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
   do_build_proof proof 
 ;;
 
+let mk_sym uri ty t1 t2 p =
+  let ens, args =  build_ens uri [ty;t1;t2;p] in
+    Cic.Appl (Cic.Const(uri, ens) :: args)
+;;
+
+let mk_trans uri ty t1 t2 t3 p12 p23 =
+  let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
+    Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+let mk_eq_ind uri ty what pred p1 other p2 =
+ Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+;;
+
+let p_of_sym ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [_;_;_;p] -> p 
+    | _ -> assert false 
+;;
+
+let open_trans ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
+    | _ -> assert false   
+;;
+
+let canonical t = 
+  let rec remove_refl t =
+    match t with
+    | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
+          when LibraryObjects.is_trans_eq_URI uri_trans ->
+          let ty,l,m,r,p1,p2 = open_trans ens tl in
+            (match p1,p2 with
+              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 -> 
+                  remove_refl p2
+              | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] -> 
+                  remove_refl p1
+              | _ -> Cic.Appl (List.map remove_refl args))
+    | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+    | _ -> t
+  in
+  let rec canonical t =
+    match t with
+      | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
+          when LibraryObjects.is_sym_eq_URI uri_sym ->
+          (match p_of_sym ens tl with
+             | Cic.Appl ((Cic.Const(uri,ens))::tl)
+                 when LibraryObjects.is_sym_eq_URI uri -> 
+                   canonical (p_of_sym ens tl)
+             | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+                 when LibraryObjects.is_trans_eq_URI uri_trans ->
+                 let ty,l,m,r,p1,p2 = open_trans ens tl in
+                   mk_trans uri_trans ty r m l 
+                     (canonical (mk_sym uri_sym ty m r p2)) 
+                     (canonical (mk_sym uri_sym ty l m p1))
+             | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
+                 when LibraryObjects.is_eq_ind_URI uri_ind || 
+                      LibraryObjects.is_eq_ind_r_URI uri_ind ->
+                 let ty, what, pred, p1, other, p2 =
+                   match tl with
+                   | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
+                   | _ -> assert false
+                 in
+                 let pred,l,r = 
+                   match pred with
+                   | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
+                       when LibraryObjects.is_eq_URI uri ->
+                         Cic.Lambda 
+                           (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
+                   | _ -> 
+                       prerr_endline (CicPp.ppterm pred);
+                       assert false
+                 in
+                 let l = CicSubstitution.subst what l in
+                 let r = CicSubstitution.subst what r in
+                 Cic.Appl 
+                   [he;ty;what;pred;
+                    canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+             | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+                 when LibraryObjects.is_eq_URI uri -> t
+             | _ -> Cic.Appl (List.map canonical args))
+      | Cic.Appl l -> Cic.Appl (List.map canonical l)
+      | _ -> t
+  in
+  remove_refl (canonical t)  
+;;
+
+let build_proof_step subst p1 p2 pos l r pred =
+  let p1 = apply_subst subst p1 in
+  let p2 = apply_subst subst p2 in
+  let l = apply_subst subst l in
+  let r = apply_subst subst r in
+  let pred = apply_subst subst pred in
+  let ty,body = (* Cic.Implicit None *) 
+    match pred with
+      | Cic.Lambda (_,ty,body) -> ty,body 
+      | _ -> assert false
+  in
+  let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+    if pos = Utils.Left then l,r else r,l
+  in
+  let is_not_fixed t =
+   CicSubstitution.subst (Cic.Implicit None) t <>
+   CicSubstitution.subst (Cic.Rel 1) t
+  in
+    match body,pos with
+      |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
+         let third = CicSubstitution.subst (Cic.Implicit None) third in
+         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+         let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+           mk_trans uri_trans ty other what third
+            (mk_sym uri_sym ty what other p2) p1
+      |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
+         let third = CicSubstitution.subst (Cic.Implicit None) third in
+         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+           mk_trans uri_trans ty other what third p2 p1
+      |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left -> 
+         let third = CicSubstitution.subst (Cic.Implicit None) third in
+         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+           mk_trans uri_trans ty third what other p1 p2  
+      |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right -> 
+         let third = CicSubstitution.subst (Cic.Implicit None) third in
+         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+         let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+           mk_trans uri_trans ty third what other p1
+            (mk_sym uri_sym ty other what p2)
+      | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
+        ->
+          let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+          let pred_of t = CicSubstitution.subst t lhs in
+          let pred_of_what = pred_of what in
+          let pred_of_other = pred_of other in
+          (*           p2 : what = other
+           * ====================================
+           *  inject p2:  P(what) = P(other)
+           *)
+          let inject ty lhs what other p2 =
+           let liftedty = CicSubstitution.lift 1 ty in
+           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+           let refl_eq_part =
+            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+           in
+            mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+             (Cic.Lambda (Cic.Name "foo",ty,
+               (Cic.Appl
+                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+                refl_eq_part what p2
+          in
+           mk_trans uri_trans ty pred_of_other pred_of_what rhs
+            (mk_sym uri_sym ty pred_of_what pred_of_other
+             (inject ty lhs what other p2)
+            ) p1
+      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
+        ->
+          let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+          let pred_of t = CicSubstitution.subst t lhs in
+          let pred_of_what = pred_of what in
+          let pred_of_other = pred_of other in
+          (*           p2 : what = other
+           * ====================================
+           *  inject p2:  P(what) = P(other)
+           *)
+          let inject ty lhs what other p2 =
+           let liftedty = CicSubstitution.lift 1 ty in
+           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+           let refl_eq_part =
+            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+           in
+            mk_eq_ind (Utils.eq_ind_URI ()) ty other
+             (Cic.Lambda (Cic.Name "foo",ty,
+               (Cic.Appl
+                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+                refl_eq_part what p2
+          in
+           mk_trans uri_trans ty pred_of_other pred_of_what rhs
+            (mk_sym uri_sym ty pred_of_other pred_of_what
+             (inject ty lhs what other p2)
+            ) p1
+      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
+        ->
+          let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+          let pred_of t = CicSubstitution.subst t rhs in
+          let pred_of_what = pred_of what in
+          let pred_of_other = pred_of other in
+          (*           p2 : what = other
+           * ====================================
+           *  inject p2:  P(what) = P(other)
+           *)
+          let inject ty lhs what other p2 =
+           let liftedty = CicSubstitution.lift 1 ty in
+           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+           let refl_eq_part =
+            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+           in
+            mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+             (Cic.Lambda (Cic.Name "foo",ty,
+               (Cic.Appl
+                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+                refl_eq_part what p2
+          in
+           mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
+            (mk_sym uri_sym ty pred_of_what pred_of_other
+             (inject ty rhs other what p2))
+      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
+        ->
+          let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+          let pred_of t = CicSubstitution.subst t rhs in
+          let pred_of_what = pred_of what in
+          let pred_of_other = pred_of other in
+          (*           p2 : what = other
+           * ====================================
+           *  inject p2:  P(what) = P(other)
+           *)
+          let inject ty lhs what other p2 =
+           let liftedty = CicSubstitution.lift 1 ty in
+           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+           let refl_eq_part =
+            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+           in
+            mk_eq_ind (Utils.eq_ind_URI ()) ty other
+             (Cic.Lambda (Cic.Name "foo",ty,
+               (Cic.Appl
+                 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+                refl_eq_part what p2
+          in
+           mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
+            (mk_sym uri_sym ty pred_of_other pred_of_what
+             (inject ty rhs other what p2))
+      | _, Utils.Left ->
+        mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+      | _, Utils.Right ->
+        mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+;;
+
 let build_proof_term_new proof =
-  let rec aux extra = function
+  let rec aux = function
      | Exact term -> term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
-         let p,m1,_,_ = proof_of_id id1 in
-         let p1 = aux [] p in
-         let p,m3,l,r = proof_of_id id2 in 
-         let p2 = aux [] p in
-         let p1 = apply_subst subst p1 in
-         let p2 = apply_subst subst p2 in
-         let l = apply_subst subst l in
-         let r = apply_subst subst r in
-         let pred = apply_subst subst pred in
-         let ty = (* Cic.Implicit None *) 
-           match pred with
-           | Cic.Lambda (_,ty,_) -> ty 
-           | _ -> assert false
-         in
-         let what, other = (* Cic.Implicit None, Cic.Implicit None *)
-           if pos = Utils.Left then l,r else r,l
-         in
-         let eq_URI =
-           match pos with 
-           | Utils.Left -> Utils.eq_ind_URI () 
-           | Utils.Right ->  Utils.eq_ind_r_URI ()
-         in 
-         (Cic.Appl [
-           Cic.Const (eq_URI, []); 
-           ty; what; pred; p1; other; p2]) 
+         let p,_,_ = proof_of_id id1 in
+         let p1 = aux p in
+         let p,l,r = proof_of_id id2 in
+         let p2 = aux p in
+           build_proof_step subst p1 p2 pos l r pred
   in
-   aux [] proof
+   aux proof
 
-let build_goal_proof l refl=
-  let proof, subst = 
+let build_goal_proof l initial =
+  let proof = 
    List.fold_left 
-   (fun  (current_proof,current_subst) (pos,id,subst,pred) -> 
-      let p,m,l,r = proof_of_id id in
+   (fun  current_proof (pos,id,subst,pred) -> 
+      let p,l,r = proof_of_id id in
       let p = build_proof_term_new p in
-      let p = apply_subst subst p in
-      let l = apply_subst subst l in
-      let r = apply_subst subst r in
-      let pred = apply_subst subst pred in
-      let ty = (* Cic.Implicit None *) 
-        match pred with
-        | Cic.Lambda (_,ty,_) -> ty 
-        | _ -> assert false
-      in
-      let what, other = (* Cic.Implicit None, Cic.Implicit None *)
-        if pos = Utils.Right then l,r else r,l
-      in
-      let eq_URI =
-        match pos with
-          | Utils.Left -> Utils.eq_ind_r_URI ()
-          | Utils.Right ->  Utils.eq_ind_URI () 
-      in
-        ((Cic.Appl [Cic.Const (eq_URI, []);
-          ty; what; pred; current_proof; other; p]), subst @ current_subst))
-   (refl,[]) l
+      let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+        build_proof_step subst current_proof p pos l r pred)
+   initial l
   in
-  proof
+  canonical proof
 ;;
 
 let refl_proof ty term = 

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index f3314bfa022d461b81c63de3f9921db6d6a8fa04..584bf5c60950c684eeda9e250d00c2c9487c5994 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -593,15 +593,15 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, ((proof_new, proof_old) as proof), 
+  let w, ((proof_new, proof_old) (*as proof*)), 
      (eq_ty, left, right, order), metas, id = 
     Equality.open_equality target in
   (* first, we simplify *)
-  let right = U.guarded_simpl context right in
-  let left = U.guarded_simpl context left in
-  let order = !Utils.compare_terms left right in
-  let stat = (eq_ty, left, right, order) in 
-  let w = Utils.compute_equality_weight stat in
+(*   let right = U.guarded_simpl context right in *)
+(*   let left = U.guarded_simpl context left in *)
+(*   let order = !Utils.compare_terms left right in *)
+(*   let stat = (eq_ty, left, right, order) in  *)
+(*  let w = Utils.compute_equality_weight stat in*)
   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");