From: Claudio Sacerdoti Coen Date: Fri, 18 Jun 2004 11:29:22 +0000 (+0000) Subject: elim_tac rewritten almost entirely. It is now based on refinement + X-Git-Tag: pre_subst_in_kernel~20 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2697b6b76d4a2449ac9ad6657128c0cc3d90ac65;p=helm.git elim_tac rewritten almost entirely. It is now based on refinement + one invocation of the (now more powerful than before) apply_tac. --- diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index d26de4447..2d741f1d1 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -453,7 +453,7 @@ let elim_tac ~term = let module U = UriManager in let module R = CicReduction in let module C = Cic in - let (curi,metasenv,_,_) = proof in + let (curi,metasenv,proofbo,proofty) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty = T.type_of_aux' metasenv context term in let uri,exp_named_subst,typeno,args = @@ -484,95 +484,43 @@ let elim_tac ~term = in let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in let ety = T.type_of_aux' metasenv context eliminator_ref in - let newmeta = new_meta_of_proof ~proof in - let (econclusion,newmetas,arguments,lastmeta) = - new_metasenv_for_apply newmeta proof context ety + let rec find_args_no = + function + C.Prod (_,_,t) -> 1 + find_args_no t + | C.Cast (s,_) -> find_args_no s + | C.LetIn (_,_,t) -> 0 + find_args_no t + | _ -> 0 in - (* Here we assume that we have only one inductive hypothesis to *) - (* eliminate and that it is the last hypothesis of the theorem. *) - (* A better approach would be fingering the hypotheses in some *) - (* way. *) - let meta_of_corpse = - let (_,canonical_context,_) = - CicUtil.lookup_meta (lastmeta - 1) newmetas + let args_no = find_args_no ety in + let term_to_refine = + let rec make_tl base_case = + function + 0 -> [base_case] + | n -> (C.Implicit None)::(make_tl base_case (n - 1)) in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable - canonical_context - in - Cic.Meta (lastmeta - 1, irl) - in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse + C.Appl (eliminator_ref :: make_tl term (args_no - 1)) in - let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in - (* The conclusion of our elimination principle is *) - (* (?i farg1 ... fargn) *) - (* The conclusion of our goal is ty. So, we can *) - (* eta-expand ty w.r.t. farg1 .... fargn to get *) - (* a new ty equal to (P farg1 ... fargn). Now *) - (* ?i can be instantiated with P and we are ready *) - (* to refine the term. *) - let emeta, fargs = - match ueconclusion with - C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs - | C.Meta (emeta,_) -> emeta,[] - | _ -> raise NotTheRightEliminatorShape + let metasenv', term_to_refine' = + CicMkImplicit.expand_implicits metasenv context term_to_refine in + let refined_term,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context term_to_refine' + in + let new_goals = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let ty' = CicMetaSubst.apply_subst subst1 ty in - let eta_expanded_ty = - (*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs + let proof' = curi,metasenv'',proofbo,proofty in + let proof'', new_goals' = + apply_tactic (apply_tac ~term:refined_term) (proof',goal) in - let subst2,newmetasenv'' = - (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite - da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty + (* The apply_tactic can have closed some of the new_goals *) + let patched_new_goals = + let (_,metasenv''',_,_) = proof'' in + List.filter + (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' + ) new_goals @ new_goals' in - let in_subst_domain i = - let eq_to_i = function (j,_) -> i=j in - List.exists eq_to_i subst1 || - List.exists eq_to_i subst2 - in - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - let apply_subst _ t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) subst2 t' - in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let (newproof, newmetasenv'''') = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) - let apply_subst' t = - let t' = CicMetaSubst.apply_subst subst1 t in - CicMetaSubst.apply_subst_reducing - (Some (emeta,List.length fargs)) - ((metano,bo')::subst2) t' - in - subst_meta_and_metasenv_in_proof - proof metano apply_subst' newmetasenv''' - in - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + proof'', patched_new_goals in mk_tactic (elim_tac ~term) ;;