diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 71 |
1 files changed, 50 insertions, 21 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb98ec18..c863a453 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 9605 2007-02-07 12:19:19Z notin $ *) +(* $Id: tactics.ml 9853 2007-05-23 14:25:47Z letouzey $ *) open Pp open Util @@ -503,6 +503,20 @@ let cut_in_parallel l = in prec (List.rev l) +let error_uninstantiated_metas t clenv = + let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in + let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" + in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id) + +let clenv_refine_in id clenv gl = + let new_hyp_typ = clenv_type clenv in + if occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; + let new_hyp_prf = clenv_value clenv in + tclTHEN + (tclEVARS (evars_of clenv.env)) + (cut_replacing id new_hyp_typ + (fun x gl -> refine_no_check new_hyp_prf gl)) gl + (****************************************************) (* Resolution tactics *) (****************************************************) @@ -575,12 +589,7 @@ let apply_in id lemmas gls = let t' = pf_get_hyp_typ gls id in let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in - let new_hyp_prf = clenv_value clause in - let new_hyp_typ = clenv_type clause in - tclTHEN - (tclEVARS (evars_of clause.env)) - (cut_replacing id new_hyp_typ - (fun x gls -> refine_no_check new_hyp_prf gls)) gls + clenv_refine_in id clause gls (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -839,15 +848,11 @@ let elimination_in_clause_scheme id elimclause indclause gl = let hyp_typ = pf_type_of gl hyp in let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in let elimclause'' = clenv_fchain hypmv elimclause' hypclause in - let new_hyp_prf = clenv_value elimclause'' in let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" (str "Nothing to rewrite in " ++ pr_id id); - tclTHEN - (tclEVARS (evars_of elimclause''.env)) - (cut_replacing id new_hyp_typ - (fun x gls -> refine_no_check new_hyp_prf gls)) gl + clenv_refine_in id elimclause'' gl let general_elim_in id = general_elim_clause (elimination_in_clause_scheme id) @@ -2328,10 +2333,18 @@ let dImp cls = let setoid_reflexivity = ref (fun _ -> assert false) let register_setoid_reflexivity f = setoid_reflexivity := f -let reflexivity gl = - match match_with_equation (pf_concl gl) with +let reflexivity_red allowred gl = + (* PL: usual reflexivity don't perform any reduction when searching + for an equality, but we may need to do some when called back from + inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let concl = if not allowred then pf_concl gl + else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) + in + match match_with_equation concl with | None -> !setoid_reflexivity gl - | Some (hdcncl,args) -> one_constructor 1 NoBindings gl + | Some _ -> one_constructor 1 NoBindings gl + +let reflexivity gl = reflexivity_red false gl let intros_reflexivity = (tclTHEN intros reflexivity) @@ -2345,8 +2358,14 @@ let intros_reflexivity = (tclTHEN intros reflexivity) let setoid_symmetry = ref (fun _ -> assert false) let register_setoid_symmetry f = setoid_symmetry := f -let symmetry gl = - match match_with_equation (pf_concl gl) with +let symmetry_red allowred gl = + (* PL: usual symmetry don't perform any reduction when searching + for an equality, but we may need to do some when called back from + inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let concl = if not allowred then pf_concl gl + else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) + in + match match_with_equation concl with | None -> !setoid_symmetry gl | Some (hdcncl,args) -> let hdcncls = string_of_inductive hdcncl in @@ -2360,7 +2379,7 @@ let symmetry gl = | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) | _ -> assert false in - tclTHENLAST (cut symc) + tclTHENFIRST (cut symc) (tclTHENLIST [ intro; tclLAST_HYP simplest_case; @@ -2368,6 +2387,8 @@ let symmetry gl = gl end +let symmetry gl = symmetry_red false gl + let setoid_symmetry_in = ref (fun _ _ -> assert false) let register_setoid_symmetry_in f = setoid_symmetry_in := f @@ -2408,8 +2429,14 @@ let intros_symmetry = let setoid_transitivity = ref (fun _ _ -> assert false) let register_setoid_transitivity f = setoid_transitivity := f -let transitivity t gl = - match match_with_equation (pf_concl gl) with +let transitivity_red allowred t gl = + (* PL: usual transitivity don't perform any reduction when searching + for an equality, but we may need to do some when called back from + inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let concl = if not allowred then pf_concl gl + else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) + in + match match_with_equation concl with | None -> !setoid_transitivity t gl | Some (hdcncl,args) -> let hdcncls = string_of_inductive hdcncl in @@ -2436,7 +2463,9 @@ let transitivity t gl = tclLAST_HYP simplest_case; assumption ])) gl end - + +let transitivity t gl = transitivity_red false t gl + let intros_transitivity n = tclTHEN intros (transitivity n) (* tactical to save as name a subproof such that the generalisation of |