From 80a0de7252db131efb4d0058cb8bfdad8221d71f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 May 2006 11:25:45 +0000 Subject: [PATCH] more transitivity on proofs --- components/tactics/paramodulation/equality.ml | 329 ++++++++++++++---- components/tactics/paramodulation/indexing.ml | 12 +- 2 files changed, 274 insertions(+), 67 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 953635dbd..7ad20206a 100644 --- 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 f3314bfa0..584bf5c60 100644 --- 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"); -- 2.39.2