X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=7c5df0d82eafbbf9bfc7da73ddf573e405e72b12;hb=c9efb92560230e52522266417f6c5b75f6e8d8aa;hp=4c7f5148d1cb5a1ff225c676c7f4ea9931011b01;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 4c7f5148d..7c5df0d82 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -27,7 +27,7 @@ let debug_print = fun _ -> () -let rec injection_tac ~term = +let rec injection_tac ~first_time ~term ~liftno ~continuation = let injection_tac ~term status = let (proof, goal) = status in let module C = Cic in @@ -36,53 +36,100 @@ let rec injection_tac ~term = let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term = CicSubstitution.lift liftno term in let termty,_ = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in ProofEngineTypes.apply_tactic - (match termty with - (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when LibraryObjects.is_eq_URI equri -> ( + (match termty with + (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) + when LibraryObjects.is_eq_URI equri -> + begin match tty with (C.MutInd (turi,typeno,exp_named_subst)) - | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( - match t1,t2 with - ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), - (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) - when (uri1 = uri2) && (typeno1 = typeno2) && - (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> - (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac - | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), - (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) - when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> - let rec traverse_list i l1 l2 = - match l1,l2 with - [],[] -> T.id_tac - | hd1::tl1,hd2::tl2 -> - T.then_ - ~start:(injection1_tac ~i ~term) - ~continuation:(traverse_list (i+1) tl1 tl2) - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) - in traverse_list 1 applist1 applist2 - | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), - (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) - | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), - (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) - | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)), - (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) - | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)), - (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) - when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) -> - (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac - | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac - ) - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) - ) - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation")) - ) status + | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> + begin + match t1,t2 with + ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), + (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) + when (uri1 = uri2) && (typeno1 = typeno2) && + (consno1 = consno2) && + (exp_named_subst1 = exp_named_subst2) + -> + if first_time then + raise + (ProofEngineTypes.Fail (lazy "Injection: nothing to do")) + else + continuation ~liftno + | C.Appl + ((C.MutConstruct + (uri1,typeno1,consno1,exp_named_subst1))::applist1), + C.Appl + ((C.MutConstruct + (uri2,typeno2,consno2,exp_named_subst2))::applist2) + when (uri1 = uri2) && (typeno1 = typeno2) && + (consno1 = consno2) && + (exp_named_subst1 = exp_named_subst2) + -> + let rec traverse_list i l1 l2 = + match l1,l2 with + [],[] -> + if first_time then + continuation + else + (match term with + C.Rel n -> + (match List.nth context (n-1) with + Some (C.Name id,_) -> + fun ~liftno -> + T.then_ + ~start: + (ProofEngineStructuralRules.clear + ~hyps:[id]) + ~continuation:(continuation ~liftno) + | _ -> assert false) + | _ -> assert false) + | hd1::tl1,hd2::tl2 -> + if + fst + (CicReduction.are_convertible ~metasenv + context hd1 hd2 CicUniv.empty_ugraph) + then + traverse_list (i+1) tl1 tl2 + else + injection1_tac ~i ~term + ~continuation:(traverse_list (i+1) tl1 tl2) + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) + in + traverse_list 1 applist1 applist2 ~liftno + | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), + (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) + | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), + (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) + | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)), + (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) + | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)), + (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) + when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) -> + raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one")) + | _ -> + if first_time then + raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) + else + continuation ~liftno + end + | _ -> + if first_time then + raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) + else + continuation ~liftno + end + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation")) + ) status in ProofEngineTypes.mk_tactic (injection_tac ~term) -and injection1_tac ~term ~i = +and injection1_tac ~term ~i ~liftno ~continuation = let injection1_tac ~term ~i status = let (proof, goal) = status in (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *) @@ -91,10 +138,12 @@ and injection1_tac ~term ~i = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in + let term = CicSubstitution.lift liftno term in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) when LibraryObjects.is_eq_URI equri -> ( @@ -112,90 +161,151 @@ and injection1_tac ~term ~i = let tty',_ = CicTypeChecker.type_of_aux' metasenv context t1' CicUniv.empty_ugraph in - let pattern = - match fst(CicEnvironment.get_obj - CicUniv.empty_ugraph turi ) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx,_) -> - let _,_,_,constructor_list = (List.nth ind_type_list typeno) in - let i_constr_id,_ = List.nth constructor_list (consno - 1) in - List.map - (function (id,cty) -> - let reduced_cty = CicReduction.whd context cty in - let rec aux t k = - match t with - C.Prod (_,_,target) when (k <= nr_ind_params_dx) -> - aux target (k+1) - | C.Prod (binder,source,target) when (k > nr_ind_params_dx) -> - let binder' = - match binder with - C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" - in - C.Lambda (binder',source,(aux target (k+1))) - | _ -> - let nr_param_constr = k - 1 - nr_ind_params_dx in - if (id = i_constr_id) - then C.Rel (nr_param_constr - i + 1) - else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *) - in aux reduced_cty 1 - ) - constructor_list - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) + let patterns,outtype = + match + fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) + with + C.InductiveDefinition (ind_type_list,_,paramsno,_)-> + let _,_,_,constructor_list = + List.nth ind_type_list typeno in + let i_constr_id,_ = + List.nth constructor_list (consno - 1) in + let seed = ref 0 in + let patterns = + List.map + (function (id,cty) -> + let reduced_cty = CicReduction.whd context cty in + let rec aux t k = + match t with + C.Prod (_,_,target) when k <= paramsno -> + aux target (k+1) + | C.Prod (binder,source,target) when k > paramsno -> + let binder' = + match binder with + C.Name _ -> binder + | C.Anonymous -> + C.Name + (incr seed; "y" ^ string_of_int !seed) + in + C.Lambda (binder',source,(aux target (k+1))) + | _ -> + let nr_param_constr = k - 1 - paramsno in + if id = i_constr_id + then C.Rel (k - i) + else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *) + in aux reduced_cty 1 + ) constructor_list in + let outtype = + let seed = ref 0 in + let rec to_lambdas te head = + match CicReduction.whd context te with + | C.Prod (binder,so,ta) -> + let binder' = + match binder with + C.Name _ -> binder + | C.Anonymous -> + C.Name (incr seed; "d" ^ string_of_int !seed) + in + C.Lambda (binder',so,to_lambdas ta head) + | _ -> head in + let rec skip_prods n te = + match n, CicReduction.whd context te with + 0, _ -> te + | n, C.Prod (_,_,ta) -> skip_prods (n - 1) ta + | _, _ -> assert false + in + let abstracted_tty = + match CicSubstitution.lift (paramsno + 1) tty with + C.MutInd _ as tty' -> tty' + | C.Appl l -> + let keep,abstract = + HExtlib.split_nth (paramsno +1) l in + let rec mk_rels = + function + 0 -> [] + | n -> C.Rel n :: (mk_rels (n - 1)) + in + C.Appl (keep@mk_rels (List.length abstract)) + | _ -> assert false + in + match ind_type_list with + [] -> assert false + | (_,_,ty,_)::_ -> + to_lambdas (skip_prods paramsno ty) + (C.Lambda (C.Name "x", abstracted_tty, + S.lift (2+paramsno) tty')) + in + patterns,outtype + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) in ProofEngineTypes.apply_tactic (T.thens - ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) - ~continuations:[ - T.then_ - ~start:(injection_tac ~term:(C.Rel 1)) - ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) - ; - T.then_ - ~start:(ProofEngineTypes.mk_tactic - (fun status -> - let (proof, goal) = status in - let _,metasenv,_,_ = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in - let new_t1' = - match gty with - (C.Appl (C.MutInd (_,_,_)::arglist)) -> - List.nth arglist 1 - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct")) - in - ProofEngineTypes.apply_tactic - (ReductionTactics.change_tac - ~pattern:(ProofEngineTypes.conclusion_pattern - (Some new_t1')) - (fun _ m u -> - C.Appl [ C.Lambda (C.Name "x", tty, - C.MutCase (turi, typeno, - (C.Lambda ((C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1], m, u)) - status - )) - ~continuation: - (T.then_ - ~start: - (EqualityTactics.rewrite_simpl_tac - ~direction:`LeftToRight - ~pattern:(ProofEngineTypes.conclusion_pattern None) - term) - ~continuation:EqualityTactics.reflexivity_tac - ) + ~start: + (P.cut_tac + (C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'])) + ~continuations: + [ injection_tac ~first_time:false ~liftno:0 + ~term:(C.Rel 1) + (* here I need to lift all the continuations by 1; + since I am setting back liftno to 0, I actually + need to lift all the continuations by liftno + 1 *) + ~continuation: + (fun ~liftno:x -> + continuation ~liftno:(liftno + 1 + x)) ; + T.then_ + ~start:(ProofEngineTypes.mk_tactic + (fun status -> + let (proof, goal) = status in + let _,metasenv,_,_ = proof in + let _,context,gty = + CicUtil.lookup_meta goal metasenv + in + let new_t1' = + match gty with + (C.Appl (C.MutInd (_,_,_)::arglist)) -> + List.nth arglist 1 + | _ -> + raise + (ProofEngineTypes.Fail + (lazy + "Injection: goal after cut is not correct")) + in + ProofEngineTypes.apply_tactic + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern + (Some new_t1')) + (fun _ m u -> + C.Appl [ + C.Lambda + (C.Name "x", + tty, + C.MutCase + (turi,typeno,outtype,C.Rel 1,patterns)) ; + t1], + m, u)) + status + )) + ~continuation: + (T.then_ + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) + ~continuation:EqualityTactics.reflexivity_tac) ]) status - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality")) + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type")) ) - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality")) + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality")) in ProofEngineTypes.mk_tactic (injection1_tac ~term ~i) ;; +let injection_tac = + injection_tac ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac) +;; + exception TwoDifferentSubtermsFound of int (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori