X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Finversion.ml;h=fa4b71178a7886ba20c3ded480c323c0e4ea3b50;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=3b4000ea4fb6fa1da810db0d300da3455a401ff3;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index 3b4000ea4..fa4b71178 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -49,22 +49,25 @@ let rec baseuri_of_term = function | _ -> raise (Invalid_argument "baseuri_of_term") (* returns DX1 = DX1 -> ... DXn=DXn -> GOALTY *) -let rec foo_cut nleft parameters parameters_ty body uri_of_eq = +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 + uri_of_eq selections else - match parameters with - | hd::tl -> + 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 ) - | [] -> body + (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 *) @@ -106,10 +109,15 @@ let foo_appl nleft nright_consno term uri = ;; +(* 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 = - match right_param_tys with - | hd::tl -> Cic.Prod ( + 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 rightparameters); @@ -121,21 +129,32 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty 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 + 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_ ) ) + then rightparameters_ @ [term] + else rightparameters_ ) ~with_what: (List.map (CicSubstitution.lift (-1)) l2) ~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!*) ;; +(* 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 = + termty isSetType term selections = match right_param_tys with | hd::tl -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), @@ -148,7 +167,7 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ base_rel (CicSubstitution.lift 1 goalty) uri_of_eq (List.map (CicSubstitution.lift 1) rightparameters_) (CicSubstitution.lift 1 termty) isSetType - (CicSubstitution.lift 1 term)) + (CicSubstitution.lift 1 term)) selections | [] when isSetType -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), (ProofEngineReduction.replace_lifting @@ -163,10 +182,10 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ (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)) + (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 + base_rel goalty uri_of_eq rightparameters_ + termty isSetType term selections selections ;; let isSetType paramty = ((Pervasives.compare @@ -174,7 +193,7 @@ let isSetType paramty = ((Pervasives.compare (Cic.Sort Cic.Prop)) != 0) exception EqualityNotDefinedYet -let private_inversion_tac ~term = +let private_inversion_tac ~term selections = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in @@ -223,7 +242,7 @@ let private_inversion_tac ~term = 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 + 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 ))); @@ -242,14 +261,16 @@ let private_inversion_tac ~term = (* apply (ledx_ind( lambda x. lambda y, ...)) *) let t1,metasenv,_subst,t3,t4, attrs = proof2 in let goal2 = List.hd (List.tl gl1) in - let (_,context,_) = CicUtil.lookup_meta goal2 metasenv 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 in + 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)));