From 36842ee77114d2fa896d7ffd2333c07cff22b053 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 13:44:20 +0000 Subject: [PATCH] Hypotheses patterns for elim implemented. No more need to generalize in advance. --- helm/software/components/tactics/compose.ml | 2 +- .../components/tactics/equalityTactics.ml | 10 +- .../components/tactics/primitiveTactics.ml | 205 ++++++++++++++++-- .../components/tactics/primitiveTactics.mli | 9 + .../components/tactics/proofEngineHelpers.ml | 26 +++ .../components/tactics/proofEngineHelpers.mli | 7 + helm/software/components/tactics/tactics.ml | 2 +- helm/software/components/tactics/tactics.mli | 2 +- .../components/tactics/variousTactics.ml | 127 ----------- .../components/tactics/variousTactics.mli | 8 - helm/software/matita/tests/elim_pattern.ma | 23 ++ 11 files changed, 258 insertions(+), 163 deletions(-) create mode 100644 helm/software/matita/tests/elim_pattern.ma diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml index 6bc3dd0fa..e009010a7 100644 --- a/helm/software/components/tactics/compose.ml +++ b/helm/software/components/tactics/compose.ml @@ -125,7 +125,7 @@ let compose_core t2 t1 (proof, goal) = in let proof, gl = ProofEngineTypes.apply_tactic - (VariousTactics.generalize_tac (Some (lazy_of t), [], None)) + (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None)) (proof,goal) in assert(List.length gl = 1); diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 47f422f52..82c339ae2 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -70,15 +70,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = match hyps_pat with [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty | [name,pat] -> - let rec find_hyp n = - function - [] -> assert false - | Some (Cic.Name s,Cic.Decl ty)::_ when name = s -> - Cic.Rel n, S.lift n ty - | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*) - | _::tl -> find_hyp (n+1) tl - in - let arg,gty = find_hyp 1 context in + let arg,gty = ProofEngineHelpers.find_hyp name context in let dummy = "dummy" in Some arg,false, (fun ~term typ -> diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 3822b7eac..7014a5941 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -514,20 +514,17 @@ let mk_predicate_for_elim (* FG: we find the predicate for the eliminator as in the rewrite tactic ****) let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in let argty = CicReduction.whd context argty in - let fresh_name = + let fresh_name = FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv context' C.Anonymous ~typ:argty - in + ~subst:[] metasenv context' C.Anonymous ~typ:argty in let hyp = Some (fresh_name, C.Decl argty) in let lazy_term c m u = - let distance = List.length c - List.length context in - S.lift distance arg, m, u - in + let distance = List.length c - List.length context in + S.lift distance arg, m, u in let pattern = Some lazy_term, [], Some cpattern' in let subst, metasenv, _ugraph, _conjecture, selected_terms = - ProofEngineHelpers.select - ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern - in + ProofEngineHelpers.select ~metasenv ~ugraph + ~conjecture:(0, context, pred) ~pattern in let metasenv = MS.apply_subst_metasenv subst metasenv in let map (_context_of_t, t) l = t :: l in let what = List.fold_right map selected_terms [] in @@ -607,17 +604,184 @@ let beta_after_elim_tac upto predicate = PET.apply_tactic tactic status in PET.mk_tactic beta_after_elim_tac - + +(* ANCORA DA DEBUGGARE *) + +exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;; +exception TheSelectedTermsMustLiveInTheGoalContext +exception AllSelectedTermsMustBeConvertible;; +exception GeneralizationInHypothesesNotImplementedYet;; + +let generalize_tac + ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + pattern + = + let module PET = ProofEngineTypes in + let generalize_tac mk_fresh_name_callback + ~pattern:(term,hyps_pat,concl_pat) status + = + if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet; + let (proof, goal) = status in + let module C = Cic in + let module T = Tacticals in + let uri,metasenv,_subst,pbo,pty, attrs = proof in + let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in + let subst,metasenv,u,selected_hyps,terms_with_context = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph + ~conjecture ~pattern in + let context = CicMetaSubst.apply_subst_context subst context in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let pbo = CicMetaSubst.apply_subst subst pbo in + let pty = CicMetaSubst.apply_subst subst pty in + let term = + match term with + None -> None + | Some term -> + Some (fun context metasenv ugraph -> + let term, metasenv, ugraph = term context metasenv ugraph in + CicMetaSubst.apply_subst subst term, + CicMetaSubst.apply_subst_metasenv subst metasenv, + ugraph) + in + let u,typ,term, metasenv' = + let context_of_t, (t, metasenv, u) = + match terms_with_context, term with + [], None -> + raise + UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly + | [], Some t -> context, t context metasenv u + | (context_of_t, _)::_, Some t -> + context_of_t, t context_of_t metasenv u + | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u) + in + let t,subst,metasenv' = + try + CicMetaSubst.delift_rels [] metasenv + (List.length context_of_t - List.length context) t + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise TheSelectedTermsMustLiveInTheGoalContext + in + (*CSC: I am not sure about the following two assertions; + maybe I need to propagate the new subst and metasenv *) + assert (subst = []); + assert (metasenv' = metasenv); + let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in + u,typ,t,metasenv + in + (* We need to check: + 1. whether they live in the context of the goal; + if they do they are also well-typed since they are closed subterms + of a well-typed term in the well-typed context of the well-typed + term + 2. whether they are convertible + *) + ignore ( + List.fold_left + (fun u (context_of_t,t) -> + (* 1 *) + let t,subst,metasenv'' = + try + CicMetaSubst.delift_rels [] metasenv' + (List.length context_of_t - List.length context) t + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise TheSelectedTermsMustLiveInTheGoalContext in + (*CSC: I am not sure about the following two assertions; + maybe I need to propagate the new subst and metasenv *) + assert (subst = []); + assert (metasenv'' = metasenv'); + (* 2 *) + let b,u1 = CicReduction.are_convertible ~subst context term t u in + if not b then + raise AllSelectedTermsMustBeConvertible + else + u1 + ) u terms_with_context) ; + let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in + let proof,goals = + PET.apply_tactic + (T.thens + ~start: + (cut_tac + (C.Prod( + (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), + typ, + (ProofEngineReduction.replace_lifting_csc 1 + ~equality:(==) + ~what:(List.map snd terms_with_context) + ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context) + ~where:ty) + ))) + ~continuations: + [(apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ; + T.id_tac]) + status + in + let _,metasenv'',_subst,_,_, _ = proof in + (* CSC: the following is just a bad approximation since a meta + can be closed and then re-opened! *) + (proof, + goals @ + (List.filter + (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'') + (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:metasenv'))) + in + PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) +;; + +let generalize_pattern_tac pattern = + let generalize_pattern_tac (proof,goal) = + let _,metasenv,_,_,_,_ = proof in + let conjecture = CicUtil.lookup_meta goal metasenv in + let _,context,_ = conjecture in + let generalize_hyps = + let _,hpatterns,_ = ProofEngineHelpers.sort_pattern_hyps context pattern in + List.map fst hpatterns in + let ids_and_patterns = + List.map + (fun id -> + let rel,_ = ProofEngineHelpers.find_hyp id context in + id,(Some (PET.const_lazy_term rel), [], None) + ) generalize_hyps in + let tactics = + List.map + (function (id,pattern) -> + Tacticals.then_ ~start:(generalize_tac pattern) + ~continuation:(Tacticals.try_tactic + (ProofEngineStructuralRules.clear [id])) + ) ids_and_patterns + in + PET.apply_tactic (Tacticals.seq tactics) (proof,goal) + in + PET.mk_tactic (generalize_pattern_tac) +;; + +let pattern_after_generalize_pattern_tac (tp, hpatterns, cpattern) = + let cpattern = + match cpattern with + None -> ProofEngineTypes.hole + | Some t -> t + in + let cpattern = + List.fold_left + (fun t (_,ty) -> Cic.Prod (Cic.Anonymous, ty, t)) cpattern hpatterns + in + tp, [], Some cpattern +;; + let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = - let elim_tac (proof, goal) = - let cpattern = match pattern with - | None, [], Some cpattern -> cpattern - | _ -> raise (PET.Fail (lazy "not implemented")) - in + let elim_tac pattern (proof, goal) = let ugraph = CicUniv.oblivion_ugraph in let curi, metasenv, _subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in + let pattern = pattern_after_generalize_pattern_tac pattern in + let cpattern = + match pattern with + | None, [], Some cpattern -> cpattern + | _ -> raise (PET.Fail (lazy "not implemented")) in let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in let termty = CicReduction.whd context termty in let termty, metasenv', arguments, _fresh_meta = @@ -710,7 +874,16 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation) dummy_status in - PET.mk_tactic elim_tac + let reorder_pattern ((proof, goal) as status) = + let _,metasenv,_,_,_,_ = proof in + let conjecture = CicUtil.lookup_meta goal metasenv in + let _,context,_ = conjecture in + let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in + PET.apply_tactic + (Tacticals.then_ ~start:(generalize_pattern_tac pattern) + ~continuation:(PET.mk_tactic (elim_tac pattern))) status + in + PET.mk_tactic reorder_pattern ;; let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 492fbf601..95ba654f5 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -42,6 +42,15 @@ val classify_metas : (Cic.term * Cic.context * Cic.term) list * (Cic.term * Cic.context * Cic.term) list +(* Not primitive, but useful for elim *) + +exception AllSelectedTermsMustBeConvertible;; + +val generalize_tac: + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ProofEngineTypes.lazy_pattern -> + ProofEngineTypes.tactic + (* ALB, needed by the new paramodulation... *) val apply_with_subst: term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int -> diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index 7d223a443..e45c13257 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -640,6 +640,32 @@ let lookup_type metasenv context hyp = in aux 1 context +let find_hyp name = + let rec find_hyp n = + function + [] -> assert false + | Some (Cic.Name s,Cic.Decl ty)::_ when name = s -> + Cic.Rel n, CicSubstitution.lift n ty + | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*) + | _::tl -> find_hyp (n+1) tl + in + find_hyp 1 +;; + +(* sort pattern hypotheses from the smallest to the highest Rel *) +let sort_pattern_hyps context (t,hpatterns,cpattern) = + let hpatterns = + List.sort + (fun (id1,_) (id2,_) -> + let t1,_ = find_hyp id1 context in + let t2,_ = find_hyp id2 context in + match t1,t2 with + Cic.Rel n1, Cic.Rel n2 -> compare n1 n2 + | _,_ -> assert false) hpatterns + in + t,hpatterns,cpattern +;; + (* FG: **********************************************************************) let get_name context index = diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index a51213f93..714860501 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -109,6 +109,13 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term (* orders a metasenv w.r.t. dependency among metas *) val sort_metasenv: Cic.metasenv -> Cic.metasenv +(* finds an hypothesis by name in the context *) +val find_hyp: string -> Cic.context -> Cic.term * Cic.term + +(* sort pattern hypotheses from the smallest to the highest Rel *) +val sort_pattern_hyps: + Cic.context -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_pattern + (* FG: some helper functions ************************************************) diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index b941a8752..832469ae6 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -49,7 +49,7 @@ let fail = Tacticals.fail_tac let fold = ReductionTactics.fold_tac let fourier = FourierR.fourier_tac let fwd_simpl = FwdSimplTactic.fwd_simpl_tac -let generalize = VariousTactics.generalize_tac +let generalize = PrimitiveTactics.generalize_tac let id = Tacticals.id_tac let intros = PrimitiveTactics.intros_tac let inversion = Inversion.inversion_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 3c27f52f4..c75f183e4 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 20 16:36:00 CET 2008 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Sat Jun 7 20:09:50 CEST 2008 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index 28dc4575d..4652899f0 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -56,130 +56,3 @@ let assumption_tac = in PET.mk_tactic assumption_tac ;; - -(* ANCORA DA DEBUGGARE *) - -exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;; -exception TheSelectedTermsMustLiveInTheGoalContext -exception AllSelectedTermsMustBeConvertible;; -exception GeneralizationInHypothesesNotImplementedYet;; - -let generalize_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - pattern - = - let module PET = ProofEngineTypes in - let generalize_tac mk_fresh_name_callback - ~pattern:(term,hyps_pat,concl_pat) status - = - if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet; - let (proof, goal) = status in - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - let uri,metasenv,_subst,pbo,pty, attrs = proof in - let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let subst,metasenv,u,selected_hyps,terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph - ~conjecture ~pattern in - let context = CicMetaSubst.apply_subst_context subst context in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - let pbo = CicMetaSubst.apply_subst subst pbo in - let pty = CicMetaSubst.apply_subst subst pty in - let term = - match term with - None -> None - | Some term -> - Some (fun context metasenv ugraph -> - let term, metasenv, ugraph = term context metasenv ugraph in - CicMetaSubst.apply_subst subst term, - CicMetaSubst.apply_subst_metasenv subst metasenv, - ugraph) - in - let u,typ,term, metasenv' = - let context_of_t, (t, metasenv, u) = - match terms_with_context, term with - [], None -> - raise - UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly - | [], Some t -> context, t context metasenv u - | (context_of_t, _)::_, Some t -> - context_of_t, t context_of_t metasenv u - | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u) - in - let t,subst,metasenv' = - try - CicMetaSubst.delift_rels [] metasenv - (List.length context_of_t - List.length context) t - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise TheSelectedTermsMustLiveInTheGoalContext - in - (*CSC: I am not sure about the following two assertions; - maybe I need to propagate the new subst and metasenv *) - assert (subst = []); - assert (metasenv' = metasenv); - let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in - u,typ,t,metasenv - in - (* We need to check: - 1. whether they live in the context of the goal; - if they do they are also well-typed since they are closed subterms - of a well-typed term in the well-typed context of the well-typed - term - 2. whether they are convertible - *) - ignore ( - List.fold_left - (fun u (context_of_t,t) -> - (* 1 *) - let t,subst,metasenv'' = - try - CicMetaSubst.delift_rels [] metasenv' - (List.length context_of_t - List.length context) t - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise TheSelectedTermsMustLiveInTheGoalContext in - (*CSC: I am not sure about the following two assertions; - maybe I need to propagate the new subst and metasenv *) - assert (subst = []); - assert (metasenv'' = metasenv'); - (* 2 *) - let b,u1 = CicReduction.are_convertible ~subst context term t u in - if not b then - raise AllSelectedTermsMustBeConvertible - else - u1 - ) u terms_with_context) ; - let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in - let proof,goals = - PET.apply_tactic - (T.thens - ~start: - (P.cut_tac - (C.Prod( - (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), - typ, - (ProofEngineReduction.replace_lifting_csc 1 - ~equality:(==) - ~what:(List.map snd terms_with_context) - ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context) - ~where:ty) - ))) - ~continuations: - [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ; - T.id_tac]) - status - in - let _,metasenv'',_subst,_,_, _ = proof in - (* CSC: the following is just a bad approximation since a meta - can be closed and then re-opened! *) - (proof, - goals @ - (List.filter - (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'') - (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:metasenv'))) - in - PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) -;; diff --git a/helm/software/components/tactics/variousTactics.mli b/helm/software/components/tactics/variousTactics.mli index 35576326e..3ce6c47e8 100644 --- a/helm/software/components/tactics/variousTactics.mli +++ b/helm/software/components/tactics/variousTactics.mli @@ -24,12 +24,4 @@ * http://cs.unibo.it/helm/. *) -exception AllSelectedTermsMustBeConvertible;; - val assumption_tac: ProofEngineTypes.tactic - -val generalize_tac: - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ProofEngineTypes.lazy_pattern -> - ProofEngineTypes.tactic - diff --git a/helm/software/matita/tests/elim_pattern.ma b/helm/software/matita/tests/elim_pattern.ma new file mode 100644 index 000000000..688e1d4f3 --- /dev/null +++ b/helm/software/matita/tests/elim_pattern.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/plus.ma". + +alias num (instance 0) = "natural number". +lemma ex1: ∀n:nat. n ≠ n+0 → n = O+O → (∀n1.¬¬(n≠n1+O)) → False. + intros (n U V K); + elim n in U:(? (? ? ? %)) ⊢ %; + [ apply (H V) + | apply (K ? H)] +qed. \ No newline at end of file -- 2.39.2