X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion.ml;h=fa4b71178a7886ba20c3ded480c323c0e4ea3b50;hb=806ecbdd749ecf2a1cabff52b41cf748fe022401;hp=5e442657d26c52578e7f32b67d5f1e79acb184d8;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index 5e442657d..fa4b71178 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -34,60 +34,66 @@ 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 selections = + if nleft > 0 + then + foo_cut (nleft-1) (List.tl parameters) (List.tl parameters_ty) body + uri_of_eq selections + else + match parameters,selections with + | hd::tl, x::xs when x -> + 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 xs) + | hd::tl,x::xs -> + foo_cut nleft tl (List.tl parameters_ty) body uri_of_eq xs + | [],[] -> body + | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type") +;; + +(* 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 +104,114 @@ 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 - | hd::tl -> Cic.Prod ( +(* induction/inversion, abbastanza semplicemente, consiste nel generare i prod + * delle uguaglianze corrispondenti ai soli parametri destri appartenenti all'insieme S. + * Attenzione al caso base: cos'e` replace_lifting? + * S = {} e` il principio di induzione + * S = insieme_dei_destri e` il principio di inversione *) +let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty + uri_of_eq rightparameters_ termty isSetType term selections selections_ = + match right_param_tys, selections with + | hd::tl, x::xs when x -> 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) - 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) ) ) + base_rel (CicSubstitution.lift 1 goalty) uri_of_eq + (List.map (CicSubstitution.lift 1) rightparameters_) + (CicSubstitution.lift 1 termty) + isSetType (CicSubstitution.lift 1 term)) xs selections_ + | hd::tl, x::xs -> + foo_prod (nright-1) tl (List.tl rightparameters) l2 + (base_rel-1) goalty uri_of_eq rightparameters_ termty + isSetType term xs selections_ + | [],[] -> + ProofEngineReduction.replace_lifting + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:[] + ~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 + | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type") +(* 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 ( +(* induction/inversion, abbastanza semplicemente, consiste nel generare i lambda + * soltanto per i parametri destri appartenenti all'insieme S. + * Warning: non ne sono piu` cosi` sicuro... + * S = {} e` il principio di induzione + * S = insieme_dei_destri e` il principio di inversione *) +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 selections = + 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 - (CicSubstitution.lift 1 term)) + 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)) selections | [] 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 + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:[] + ~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 - termty isSetType term + (CicSubstitution.lift 1 term)) selections selections + | [] -> foo_prod nright_ right_param_tys_ rightparameters created_vars + base_rel goalty uri_of_eq rightparameters_ + termty isSetType term selections selections ;; -let inversion_tac ~term = +let isSetType paramty = ((Pervasives.compare + (get_sort_type paramty) + (Cic.Sort Cic.Prop)) != 0) + +exception EqualityNotDefinedYet +let private_inversion_tac ~term selections = 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 (_,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 termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let private_inversion_tac ~term (proof, goal) = + + (*DEBUG*) debug_print (lazy ("private inversion begins")); + let _,metasenv,_subst,_,_, _ = proof in + let uri_of_eq = + match LibraryObjects.eq_URI () with + None -> raise EqualityNotDefinedYet + | Some uri -> uri + in + let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_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 o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let (_,_,typeno,_) = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -183,70 +219,164 @@ 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 - (* 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 parameters = (List.tl (term_to_list termty)) in + let parameters_tys = + (List.map + (fun t -> ( + match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with + (term,graph) -> term)) + parameters) + 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 selections in + (*DEBUG*) debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term)); + debug_print (lazy ("CONTEXT before apply HCUT: " ^ + (CicMetaSubst.ppcontext ~metasenv [] 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 t1,metasenv,_subst,t3,t4, attrs = 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,g2ty) = 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 + debug_print + (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters)))); + let lambda_t = foo_lambda nright rightparam_ty_l nright rightparam_ty_l + rightparameters [] nright goalty uri_of_eq rightparameters termty isSetType + term selections 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 ~metasenv [] 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 + CicUniv.oblivion_ugraph in - 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'' + (*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: " + ^ CicPp.ppterm ref_t)); + let proof2 = (t1,metasenv'',_subst,t3,t4, attrs) in + 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''',_subst,_,_, _) = 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,_subst,_,_, _ = proof in + let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in + let uri, typeno = + match termty with + | Cic.MutInd (uri,typeno,_) + | Cic.Appl(Cic.MutInd (uri,typeno,_)::_) -> uri,typeno + | _ -> assert false + in + (* let uri = baseuri_of_term termty in *) + let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + let name,nleft,arity,cons_list = + match obj with + Cic.InductiveDefinition (tys,_,nleft,_) -> + 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 @ [term]) + in + let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in + let (t1,metasenv,_subst,t3,t4, attrs) = proof in + let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t + CicUniv.oblivion_ugraph + in + let proof = (t1,metasenv'',_subst,t3,t4, attrs) in + let proof3,gl3 = + ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in + let patched_new_goals = + let (_,metasenv''',_subst,_,_, _) = 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) ;;