From 06d6dda7872607754423a5ec43e488ad59e13b18 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 20:33:07 +0200 Subject: Enforce the argument of elim functions to be a variable. --- tactics/elim.ml | 22 ++++++++-------------- tactics/elim.mli | 2 +- tactics/inv.ml | 2 +- 3 files changed, 10 insertions(+), 16 deletions(-) diff --git a/tactics/elim.ml b/tactics/elim.ml index 852ad626e1..f812cb544e 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -34,14 +34,14 @@ module NamedDecl = Context.Named.Declaration (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim - rec_flag allnames tac predicate ind (c, t) = + rec_flag allnames tac predicate ind (id, t) = let open Pp in Proofview.Goal.enter begin fun gl -> let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Proofview.Goal.enter begin fun gl -> - let indclause = mk_clenv_from gl (c, t) in + let indclause = mk_clenv_from gl (mkVar id, t) in (* applying elimination_scheme just a little modified *) let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in let indmv = @@ -116,16 +116,16 @@ let elim_on_ba tac ba = tac branches end -let elimination_then tac c = +let elimination_then tac id = let open Declarations in Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl (mkVar id)) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | NotRecord -> true,gl_make_elim | FakeRecord | PrimRecord _ -> false,gl_make_case true in - general_elim_then_using mkelim isrec None tac None ind (c, t) + general_elim_then_using mkelim isrec None tac None ind (id, t) end (* Supposed to be called without as clause *) @@ -168,14 +168,11 @@ Another example : Qed. *) -let elimHypThen tac id = - elimination_then tac (mkVar id) - let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = - elimHypThen + elimination_then (introElimAssumsThen (fun bas -> tclTHEN (clear [id]) @@ -236,9 +233,6 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c - let induction_trailer abs_i abs_j bargs = tclTHEN (tclDO (abs_j - abs_i) intro) @@ -261,7 +255,7 @@ let induction_trailer abs_i abs_j bargs = in let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST - [revert ids; simple_elimination (mkVar id)]) + [revert ids; elimination_then (fun _ -> tclIDTAC) id]) end )) @@ -279,7 +273,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) id))) end let h_double_induction = double_ind diff --git a/tactics/elim.mli b/tactics/elim.mli index 4c5cdc8a31..737bbdf728 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -16,7 +16,7 @@ open Tactypes val case_tac : bool -> or_and_intro_pattern option -> (intro_patterns -> named_context -> unit Proofview.tactic) -> - constr -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic + constr -> inductive * EInstance.t -> Id.t * types -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index f77b52b931..1bb8158e07 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -490,7 +490,7 @@ let raw_inversion inv_kind id status names = tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) - [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (c,t); + [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (id, t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) end -- cgit v1.2.3 From 950da3527f0383aba8faf79b99a11313e0e9a3fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 20:36:47 +0200 Subject: Defunctionalize the mk_elim creation in Elim. --- tactics/elim.ml | 127 ++++++++++++++++++++++++++------------------------------ 1 file changed, 60 insertions(+), 67 deletions(-) diff --git a/tactics/elim.ml b/tactics/elim.ml index f812cb544e..c2672449af 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -31,79 +31,73 @@ type branch_args = { module NamedDecl = Context.Named.Declaration +type elim_kind = Case of bool | Elim + (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim rec_flag allnames tac predicate ind (id, t) = let open Pp in Proofview.Goal.enter begin fun gl -> - let sigma, elim = mk_elim ind gl in - let ind = on_snd (fun u -> EInstance.kind sigma u) ind in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.enter begin fun gl -> - let indclause = mk_clenv_from gl (mkVar id, t) in - (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in - let indmv = - match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> CErrors.anomaly (str"elimination.") - in - let pmv = - let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in - match EConstr.kind elimclause.evd p with - | Meta p -> p - | _ -> - let name_elim = - match EConstr.kind sigma elim with - | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim - | _ -> mt () - in - CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ name_elim ++ str " is unknown.") - in - let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in - let brnames = Tacticals.compute_induction_names false branchsigns allnames in - let flags = Unification.elim_flags () in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' - in - let after_tac i = - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = List.length branchsigns.(i); - branchnum = i+1; - ity = ind; } + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ind = on_snd (fun u -> EInstance.kind sigma u) ind in + let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in + let sigma, elim = match mk_elim with + | Case dep -> + let (sigma, r) = Indrec.build_case_analysis_scheme env sigma ind dep sort in + (sigma, EConstr.of_constr r) + | Elim -> + let gr = Indrec.lookup_eliminator env (fst ind) sort in + Evd.fresh_global env sigma gr in - tac ba - in - let branchtacs = List.init (Array.length branchsigns) after_tac in - Proofview.tclTHEN - (Clenv.res_pf ~flags elimclause') - (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end + let indclause = mk_clenv_from_env env sigma None (mkVar id, t) in + (* applying elimination_scheme just a little modified *) + let elimclause = mk_clenv_from_env env sigma None (elim, Retyping.get_type_of env sigma elim) in + let indmv = + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> CErrors.anomaly (str"elimination.") + in + let pmv = + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with + | Meta p -> p + | _ -> + let name_elim = + match EConstr.kind sigma elim with + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env env sigma elim + | _ -> mt () + in + CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") + in + let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in + let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in + let brnames = Tacticals.compute_induction_names false branchsigns allnames in + let flags = Unification.elim_flags () in + let elimclause' = + match predicate with + | None -> elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' + in + let after_tac i = + let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); + nassums = List.length branchsigns.(i); + branchnum = i+1; + ity = ind; } + in + tac ba + in + let branchtacs = List.init (Array.length branchsigns) after_tac in + Proofview.tclTHEN + (Clenv.res_pf ~flags elimclause') + (Proofview.tclEXTEND [] tclIDTAC branchtacs) + end (* computing the case/elim combinators *) -let gl_make_elim ind = begin fun gl -> - let env = Proofview.Goal.env gl in - let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in - let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, c) -end - -let gl_make_case dep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind (project gl) u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) dep - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) -end - let make_elim_branch_assumptions ba hyps = let assums = try List.rev (List.firstn ba.nassums hyps) @@ -122,8 +116,8 @@ let elimination_then tac id = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl (mkVar id)) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with - | NotRecord -> true,gl_make_elim - | FakeRecord | PrimRecord _ -> false,gl_make_case true + | NotRecord -> true, Elim + | FakeRecord | PrimRecord _ -> false, Case true in general_elim_then_using mkelim isrec None tac None ind (id, t) end @@ -146,9 +140,8 @@ let introCaseAssumsThen with_evars tac ba = (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba)) let case_tac dep names tac elim ind c = - let mkcase = gl_make_case dep in let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in - general_elim_then_using mkcase false names tac (Some elim) ind c + general_elim_then_using (Case dep) false names tac (Some elim) ind c (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate -- cgit v1.2.3 From f9b5e98e7bc94f0385d1a9a62f3c3d5b9227197f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 21:11:15 +0200 Subject: Restrict a spurious call to a reduction to a quantified inductive type. Actually the callers of that function only apply it to an applied inductive type. --- tactics/elim.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/tactics/elim.ml b/tactics/elim.ml index c2672449af..0c3cada4a3 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -113,7 +113,7 @@ let elim_on_ba tac ba = let elimination_then tac id = let open Declarations in Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl (mkVar id)) in + let (ind,t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | NotRecord -> true, Elim @@ -178,7 +178,6 @@ and general_decompose_aux recognizer id = (* Best strategies but loss of compatibility *) let tmphyp_name = Id.of_string "_TmpHyp" -let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> @@ -195,11 +194,8 @@ let head_in indl t gl = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let ity,_ = - if !up_to_delta - then find_mrectype env sigma t - else extract_mrectype sigma t - in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl + let ity,_ = extract_mrectype sigma t in + List.exists (fun i -> eq_ind (fst i) (fst ity)) indl with Not_found -> false let decompose_these c l = -- cgit v1.2.3 From 146c760fb4cdfc41a3b07db1622f56a4d6a42a3b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 21:24:03 +0200 Subject: Statically enforce that elim is passed a fully applied inductive type. --- tactics/elim.ml | 24 +++++++++++------------- tactics/elim.mli | 2 +- tactics/inv.ml | 5 +++-- 3 files changed, 15 insertions(+), 16 deletions(-) diff --git a/tactics/elim.ml b/tactics/elim.ml index 0c3cada4a3..49437a2aef 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -22,7 +22,6 @@ open Tactics open Proofview.Notations type branch_args = { - ity : pinductive; (* the type we were eliminating on *) branchnum : int; (* the branch number *) nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. @@ -36,22 +35,22 @@ type elim_kind = Case of bool | Elim (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim - rec_flag allnames tac predicate ind (id, t) = + rec_flag allnames tac predicate (ind, u, args) id = let open Pp in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let ind = on_snd (fun u -> EInstance.kind sigma u) ind in let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in let sigma, elim = match mk_elim with | Case dep -> - let (sigma, r) = Indrec.build_case_analysis_scheme env sigma ind dep sort in + let u = EInstance.kind sigma u in + let (sigma, r) = Indrec.build_case_analysis_scheme env sigma (ind, u) dep sort in (sigma, EConstr.of_constr r) | Elim -> - let gr = Indrec.lookup_eliminator env (fst ind) sort in + let gr = Indrec.lookup_eliminator env ind sort in Evd.fresh_global env sigma gr in - let indclause = mk_clenv_from_env env sigma None (mkVar id, t) in + let indclause = mk_clenv_from_env env sigma None (mkVar id, mkApp (mkIndU (ind, u), args)) in (* applying elimination_scheme just a little modified *) let elimclause = mk_clenv_from_env env sigma None (elim, Retyping.get_type_of env sigma elim) in let indmv = @@ -73,7 +72,7 @@ let general_elim_then_using mk_elim (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in + let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag (ind, u) in let brnames = Tacticals.compute_induction_names false branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = @@ -85,8 +84,7 @@ let general_elim_then_using mk_elim let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = List.length branchsigns.(i); - branchnum = i+1; - ity = ind; } + branchnum = i+1; } in tac ba in @@ -113,13 +111,14 @@ let elim_on_ba tac ba = let elimination_then tac id = let open Declarations in Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in + let ((ind, u), t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in + let _, args = decompose_app_vect (Proofview.Goal.sigma gl) t in let isrec,mkelim = - match (Global.lookup_mind (fst (fst ind))).mind_record with + match (Global.lookup_mind (fst ind)).mind_record with | NotRecord -> true, Elim | FakeRecord | PrimRecord _ -> false, Case true in - general_elim_then_using mkelim isrec None tac None ind (id, t) + general_elim_then_using mkelim isrec None tac None (ind, u, args) id end (* Supposed to be called without as clause *) @@ -191,7 +190,6 @@ let general_decompose recognizer c = end let head_in indl t gl = - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try let ity,_ = extract_mrectype sigma t in diff --git a/tactics/elim.mli b/tactics/elim.mli index 737bbdf728..01053502e4 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -16,7 +16,7 @@ open Tactypes val case_tac : bool -> or_and_intro_pattern option -> (intro_patterns -> named_context -> unit Proofview.tactic) -> - constr -> inductive * EInstance.t -> Id.t * types -> unit Proofview.tactic + constr -> inductive * EInstance.t * EConstr.t array -> Id.t -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index 1bb8158e07..41899132a6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -463,7 +463,7 @@ let raw_inversion inv_kind id status names = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in - let (ind, t) = + let ((ind, u), t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in @@ -487,10 +487,11 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in + let (_, args) = decompose_app_vect sigma t in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) - [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (id, t); + [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate (ind, u, args) id; onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) end -- cgit v1.2.3