From 7803bba7862a492252d520d670614738b866ae1e Mon Sep 17 00:00:00 2001 From: marangon Date: Fri, 10 Mar 2006 12:20:41 +0000 Subject: [PATCH] Inversion code cleaning. --- components/tactics/.depend | 16 +- components/tactics/Makefile | 3 +- components/tactics/inversion.ml | 354 ++++++++++++++++++++----------- components/tactics/inversion.mli | 2 + 4 files changed, 241 insertions(+), 134 deletions(-) diff --git a/components/tactics/.depend b/components/tactics/.depend index 4769431a4..10862a5b0 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -120,12 +120,16 @@ discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi -inversion.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ - inversion.cmi -inversion.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ - inversion.cmi +inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + equalityTactics.cmi inversion.cmi +inversion.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + equalityTactics.cmx inversion.cmi +inversion_principle.cmo: tacticals.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi inversion.cmi inversion_principle.cmi +inversion_principle.cmx: tacticals.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx inversion.cmx inversion_principle.cmi ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 0b8f4fb69..91d011d3d 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -13,7 +13,8 @@ INTERFACE_FILES = \ paramodulation/saturation.mli \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ - equalityTactics.mli discriminationTactics.mli inversion.mli ring.mli \ + equalityTactics.mli discriminationTactics.mli inversion.mli \ + inversion_principle.mli ring.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index 5e442657d..0ff369a9a 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -34,60 +34,63 @@ let debug_print = let inside_obj = function - | Cic.InductiveDefinition (l,params, nleft, _) -> - (l,params,nleft) - | _ -> raise (Invalid_argument "Errore in inside_obj") + | Cic.InductiveDefinition (type_list,params, nleft, _) -> + (type_list,params,nleft) + | _ -> raise (Invalid_argument "Errore in inside_obj") let term_to_list = function - | Cic.Appl l -> l - | _ -> raise (Invalid_argument "Errore in term_to_list") + | Cic.Appl l -> l + | _ -> raise (Invalid_argument "Errore in term_to_list") let rec baseuri_of_term = function - | Cic.Appl l -> baseuri_of_term (List.hd l) - | Cic.MutInd (baseuri, tyno, []) -> baseuri - | _ -> raise (Invalid_argument "baseuri_of_term") - - -(* prende il numero dei parametri sinistri, la lista dei parametri, la lista -dei tipi dei parametri, il tipo del GOAL e costruisce il termine per la cut -ossia DX1 = DX1 -> ... DXn=DXn -> GOALTY *) - -let rec foo_cut nleft l param_ty_l body uri_of_eq = - if nleft > 0 then foo_cut (nleft-1) (List.tl l) (List.tl param_ty_l) body - uri_of_eq - else match l with - | hd::tl -> Cic.Prod (Cic.Anonymous, Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); - (List.hd param_ty_l) ; hd; hd], foo_cut nleft - (List.map (CicSubstitution.lift 1) tl) (List.tl param_ty_l) - (CicSubstitution.lift 1 body) uri_of_eq ) - | [] -> body - ;; - -(* da una catena di prod costruisce una lista dei termini che lo compongono.*) -let rec list_of_prod term = -match term with - | Cic.Prod (Cic.Anonymous,src,tgt) -> [src] @ (list_of_prod tgt) - | _ -> [term] + | Cic.Appl l -> baseuri_of_term (List.hd l) + | Cic.MutInd (baseuri, tyno, []) -> baseuri + | _ -> raise (Invalid_argument "baseuri_of_term") + +(* returns DX1 = DX1 -> ... DXn=DXn -> GOALTY *) +let rec foo_cut nleft parameters parameters_ty body uri_of_eq = + if nleft > 0 + then + foo_cut (nleft-1) (List.tl parameters) (List.tl parameters_ty) body + uri_of_eq + else + match parameters with + | hd::tl -> + Cic.Prod ( + Cic.Anonymous, + Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); + (List.hd parameters_ty) ; hd; hd], + foo_cut nleft (List.map (CicSubstitution.lift 1) tl) + (List.map (CicSubstitution.lift 1) (List.tl parameters_ty)) + (CicSubstitution.lift 1 body) uri_of_eq ) + | [] -> body +;; + +(* from a complex Cic.Prod term, return the list of its components *) +let rec get_sort_type term = + match term with + | Cic.Prod (_,src,tgt) -> (get_sort_type tgt) + | _ -> term ;; let rec cut_first n l = if n>0 then match l with - | hd::tl -> cut_first (n-1) tl - | [] -> [] - else l + | hd::tl -> cut_first (n-1) tl + | [] -> [] + else l ;; let rec cut_last l = -match l with - | hd::tl when tl != [] -> hd:: (cut_last tl) - | _ -> [] + match l with + | hd::tl when tl != [] -> hd:: (cut_last tl) + | _ -> [] ;; - +(* returns the term to apply*) let foo_appl nleft nright_consno term uri = let l = [] in let a = ref l in @@ -98,84 +101,91 @@ let foo_appl nleft nright_consno term uri = for n = 1 to nright_consno do a := !a @ [(Cic.Implicit None)] done; - Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) (*L'ipotesi e' sempre Rel 1. (?) *) + (* apply i_ind ? ... ? H *) + Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) ;; -let rec foo_prod nright param_ty_l l l2 base_rel body uri_of_eq nleft termty - isSetType term = - match param_ty_l with +let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty + uri_of_eq rightparameters_ termty isSetType term = + match right_param_tys with | hd::tl -> Cic.Prod ( Cic.Anonymous, - Cic.Appl[Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd l); Cic.Rel base_rel], - foo_prod (nright-1) tl (List.map (CicSubstitution.lift 1) (List.tl l)) + Cic.Appl + [Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd rightparameters); + Cic.Rel base_rel], + foo_prod (nright-1) + (List.map (CicSubstitution.lift 1) tl) + (List.map (CicSubstitution.lift 1) (List.tl rightparameters)) (List.map (CicSubstitution.lift 1) l2) - base_rel (CicSubstitution.lift 1 body) - uri_of_eq nleft (CicSubstitution.lift 1 termty) + base_rel (CicSubstitution.lift 1 goalty) uri_of_eq + (List.map (CicSubstitution.lift 1) rightparameters_) + (CicSubstitution.lift 1 termty) isSetType (CicSubstitution.lift 1 term)) | [] -> ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) - ~what: (if isSetType - then ((cut_first (1+nleft) (term_to_list termty) ) @ [term] ) - else (cut_first (1+nleft) (term_to_list termty) ) ) + ~what: (if isSetType + then (rightparameters_ @ [term] ) + else (rightparameters_ ) ) ~with_what: (List.map (CicSubstitution.lift (-1)) l2) - ~where:body -(*TODO lo stesso sottotermine di body puo' essere sia sx che dx!*) + ~where:goalty +(* the same subterm of goalty could be simultaneously sx and dx!*) ;; -let rec foo_lambda nright param_ty_l nright_ param_ty_l_ l l2 base_rel body - uri_of_eq nleft termty isSetType ty_indty term = - (*assert nright >0 *) - match param_ty_l with - | hd::tl ->Cic.Lambda ( +let rec foo_lambda nright right_param_tys nright_ right_param_tys_ + rightparameters created_vars base_rel goalty uri_of_eq rightparameters_ + termty isSetType term = + match right_param_tys with + | hd::tl -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), - hd, (* typ *) - foo_lambda (nright-1) tl nright_ param_ty_l_ - (List.map (CicSubstitution.lift 1) l) - (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) - base_rel (CicSubstitution.lift 1 body) - uri_of_eq nleft - (CicSubstitution.lift 1 termty) - isSetType ty_indty + hd, (* type *) + foo_lambda (nright-1) + (List.map (CicSubstitution.lift 1) tl) nright_ + (List.map (CicSubstitution.lift 1) right_param_tys_) + (List.map (CicSubstitution.lift 1) rightparameters) + (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1])) + base_rel (CicSubstitution.lift 1 goalty) uri_of_eq + (List.map (CicSubstitution.lift 1) rightparameters_) + (CicSubstitution.lift 1 termty) isSetType (CicSubstitution.lift 1 term)) | [] when isSetType -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), (ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) - ~what: (cut_first (1+nleft) (term_to_list termty) ) - ~with_what: (List.map (CicSubstitution.lift (-1)) l2) - ~where:termty), (* tipo di H con i parametri destri sostituiti *) - foo_prod nright_ param_ty_l_ (List.map (CicSubstitution.lift 1) l) - (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) - (base_rel+1) (CicSubstitution.lift 1 body) - uri_of_eq nleft + ~what: (rightparameters_ ) + ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars) + ~where:termty), (* type of H with replaced right parameters *) + foo_prod nright_ (List.map (CicSubstitution.lift 1) right_param_tys_) + (List.map (CicSubstitution.lift 1) rightparameters) + (List.map (CicSubstitution.lift 1) (created_vars @ [Cic.Rel 1])) + (base_rel+1) (CicSubstitution.lift 1 goalty) uri_of_eq + (List.map (CicSubstitution.lift 1) rightparameters_) (CicSubstitution.lift 1 termty) isSetType (CicSubstitution.lift 1 term)) - | [] -> foo_prod nright_ param_ty_l_ l l2 base_rel body uri_of_eq nleft + | [] -> foo_prod nright_ right_param_tys_ rightparameters created_vars + base_rel goalty uri_of_eq rightparameters_ termty isSetType term ;; -let inversion_tac ~term = +let isSetType paramty = ((Pervasives.compare + (get_sort_type paramty) + (Cic.Sort Cic.Prop)) != 0) + +let private_inversion_tac ~term = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let module P = PrimitiveTactics in let module PET = ProofEngineTypes in - let module PEH = ProofEngineHelpers in - let inversion_tac ~term (proof, goal) = + let private_inversion_tac ~term (proof, goal) = + + (*DEBUG*) debug_print (lazy ("private inversion begins")); let (_,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in - - (* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che - e' la terza componente della relativa congettura *) - let (_,_,body) = CicUtil.lookup_meta goal metasenv in - (* estrae il tipo del termine(ipotesi) oggetto di inversion, - di solito un Cic.Appl *) + let uri_of_eq = LibraryObjects.eq_URI () in + let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let uri = baseuri_of_term termty in let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let l,params,nleft = inside_obj o in let (_,_,typeno,_) = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -183,70 +193,160 @@ let inversion_tac ~term = (uri,exp_named_subst,typeno,args) | _ -> raise NotAnInductiveTypeToEliminate in - let eliminator_uri = - let buri = UriManager.buri_of_uri uri in - let name = - match o with - C.InductiveDefinition (tys,_,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - |_ -> assert false - in - let ext = "_ind" in - UriManager.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + let buri = UriManager.buri_of_uri uri in + let name,nleft,paramty,cons_list = + match o with + C.InductiveDefinition (tys,_,nleft,_) -> + let (name,_,paramty,cons_list) = List.nth tys typeno in + (name,nleft,paramty,cons_list) + |_ -> assert false in - (* il tipo del tipo induttivo da cui viene l'ipotesi oggetto di inversione *) - let (_,_,ty_indty,cons_list) = (List.hd l) in - (*la lista di Cic.term ricavata dal tipo del tipo induttivo. *) - let param_ty_l = list_of_prod ty_indty in - let consno = List.length cons_list in - let nright= (List.length param_ty_l)- (nleft+1) in - let isSetType = ((Pervasives.compare - (List.nth param_ty_l ((List.length param_ty_l)-1)) - (Cic.Sort Cic.Prop)) != 0) + let eliminator_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_ind" ^ ".con") + in + let parameters = (List.tl (term_to_list termty)) in + let parameters_tys = + (List.map + (fun t -> ( + match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with + (term,graph) -> term + |_ -> assert false)) + parameters) in - (* eliminiamo la testa di termty, in quanto e' il nome del predicato e non un parametro.*) - let cut_term = foo_cut nleft (List.tl (term_to_list termty)) - (list_of_prod ty_indty) body uri_of_eq in + let consno = List.length cons_list in + let nright= ((List.length parameters)- nleft) in + let isSetType = isSetType paramty in + let cut_term = foo_cut nleft parameters + parameters_tys goalty uri_of_eq in + (*DEBUG*) debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term)); + debug_print (lazy ("CONTEXT before apply HCUT: " ^ + (CicMetaSubst.ppcontext [] context ))); + debug_print (lazy ("termty " ^ CicPp.ppterm termty)); (* cut DXn=DXn \to GOAL *) let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in - (* apply Hcut ; reflexivity (su tutti i goals aperti da apply_tac) *) + (* apply Hcut ; reflexivity *) let proof2, gl2 = PET.apply_tactic (Tacticals.then_ ~start: (P.apply_tac (C.Rel 1)) (* apply Hcut *) ~continuation: (EqualityTactics.reflexivity_tac) ) (proof1, (List.hd gl1)) - in + in + (*DEBUG*) debug_print (lazy ("after apply HCUT;reflexivity + in private inversion")); (* apply (ledx_ind( lambda x. lambda y, ...)) *) let (t1,metasenv,t3,t4) = proof2 in let goal2 = List.hd (List.tl gl1) in - let (metano,context,_) = CicUtil.lookup_meta goal2 metasenv in - let cut_param_ty_l = (cut_first nleft (cut_last param_ty_l)) in - (* la lista dei soli parametri destri *) - let l= cut_first (1+nleft) (term_to_list termty) in - let lambda_t = foo_lambda nright cut_param_ty_l nright cut_param_ty_l l [] - nright body uri_of_eq nleft termty isSetType ty_indty term in - let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in + let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in + (* rightparameters type list *) + let rightparam_ty_l = (cut_first nleft parameters_tys) in + (* rightparameters list *) + let rightparameters= cut_first nleft parameters in + let lambda_t = foo_lambda nright rightparam_ty_l nright rightparam_ty_l + rightparameters [] nright goalty uri_of_eq rightparameters termty isSetType + term in + let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t))); debug_print (lazy ("Term: " ^ (CicPp.ppterm termty))); - debug_print (lazy ("Body: " ^ (CicPp.ppterm body))); - debug_print (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl l)))); - + debug_print (lazy ("Body: " ^ (CicPp.ppterm goalty))); + debug_print + (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters)))); + debug_print (lazy ("CONTEXT before refinement: " ^ + (CicMetaSubst.ppcontext [] context ))); + (*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^ + CicPp.ppterm t)); let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t CicUniv.empty_ugraph in + (*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: " + ^ CicPp.ppterm ref_t)); let proof2 = (t1,metasenv'',t3,t4) in - let proof3,gl3 = PET.apply_tactic (P.apply_tac ref_t) (proof2, goal2) in - let new_goals = ProofEngineHelpers.compare_metasenvs - ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + let my_apply_tac = + let my_apply_tac status = + let proof,goals = + ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in + let patched_new_goals = + let (_,metasenv''',_,_) = proof in + let new_goals = ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + List.filter (function i -> List.exists (function (j,_,_) -> j=i) + metasenv''') new_goals @ goals + in + proof,patched_new_goals + in + ProofEngineTypes.mk_tactic my_apply_tac in - let patched_new_goals = - let (_,metasenv''',_,_) = proof3 in - List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') - new_goals @ gl3 + let proof3,gl3 = + PET.apply_tactic + (Tacticals.then_ + ~start:my_apply_tac + ~continuation: + (ReductionTactics.simpl_tac (ProofEngineTypes.conclusion_pattern(None)))) + (proof2,goal2) in - (*prerr_endline ("METASENV: " ^ CicMetaSubst.ppmetasenv metasenv []); DEBUG*) - (proof3, patched_new_goals) + + (proof3, gl3) in +ProofEngineTypes.mk_tactic (private_inversion_tac ~term) +;; + + +let inversion_tac ~term = + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic in + let module P = PrimitiveTactics in + let module PET = ProofEngineTypes in + let inversion_tac ~term (proof, goal) = + (*DEBUG*) debug_print (lazy ("inversion begins")); + let (_,metasenv,_,_) = proof in + let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let uri = baseuri_of_term termty in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let name,nleft,arity,cons_list = + match obj with + Cic.InductiveDefinition (tys,_,nleft,_) -> + (*we suppose there is only one inductiveType in the definition, + so typeno=0 identically *) + let typeno = 0 in + let (name,_,arity,cons_list) = List.nth tys typeno in + (name,nleft,arity,cons_list) + |_ -> assert false + in + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in + (* arity length = number of parameters plus 1 *) + let arity_length = (List.length (term_to_list termty)) in + (* Check the existence of any right parameter. *) + assert (arity_length > (nleft + 1)); + let appl_term arity_consno uri = + let l = [] in + let a = ref l in + for n = 1 to arity_consno do + a := (Cic.Implicit None)::(!a) + done; + (* apply i_inv ? ...? H). *) + Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) + in + let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in + let (t1,metasenv,t3,t4) = proof in + let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t + CicUniv.empty_ugraph + in + let proof = (t1,metasenv'',t3,t4) in + let proof3,gl3 = + ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in + let patched_new_goals = + let (_,metasenv''',_,_) = proof3 in + let new_goals = ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + List.filter (function i -> List.exists (function (j,_,_) -> j=i) + metasenv''') new_goals @ gl3 + in + (proof3, patched_new_goals) + in ProofEngineTypes.mk_tactic (inversion_tac ~term) ;; diff --git a/components/tactics/inversion.mli b/components/tactics/inversion.mli index 50bdf58f2..1471f5dbc 100644 --- a/components/tactics/inversion.mli +++ b/components/tactics/inversion.mli @@ -23,4 +23,6 @@ * http://cs.unibo.it/helm/. *) +val isSetType: Cic.term -> bool +val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic -- 2.39.2