diff --git a/src/context_map.ml b/src/context_map.ml index 25b833b3..140bef38 100644 --- a/src/context_map.ml +++ b/src/context_map.ml @@ -115,13 +115,21 @@ and pat_of_constr env sigma c = | _ -> PInac c -let rec pat_to_user_pat ?(avoid = ref Id.Set.empty) ?loc ctx = function +let rec pat_to_user_pat ?(avoid = ref Id.Set.empty) ?(keep_names = false) ?loc ctx = function | PRel i -> let decl = List.nth ctx (pred i) in let name = Context.Rel.Declaration.get_name decl in - let id = Namegen.next_name_away name !avoid in + (* In [keep_names] mode, a variable pattern reuses the context binder name + verbatim (with [Implicit] provenance), so that names of pre-existing + hypotheses survive freshening, in particular the mangling done by + [Mangle Names]. *) + let id, prov = + match name with + | Name id when keep_names && not (Id.Set.mem id !avoid) -> id, Syntax.Implicit + | _ -> Namegen.next_name_away name !avoid, Syntax.User + in avoid := Id.Set.add id !avoid; - Some (DAst.make ?loc (Syntax.(PUVar (id, User)))) + Some (DAst.make ?loc (Syntax.PUVar (id, prov))) | PCstr (((ind, _ as cstr), _), pats) -> let n = Inductiveops.inductive_nparams (Global.env()) ind in let _, pats = List.chop n pats in @@ -131,12 +139,12 @@ let rec pat_to_user_pat ?(avoid = ref Id.Set.empty) ?loc ctx = function avoid := Id.Set.add id !avoid; Some (DAst.make ?loc (Syntax.(PUVar (id, Generated)))) | PHide i -> None -and pats_to_lhs ?(avoid = ref Id.Set.empty) ?loc ctx pats = - List.map_filter (pat_to_user_pat ~avoid ?loc ctx) pats +and pats_to_lhs ?(avoid = ref Id.Set.empty) ?(keep_names = false) ?loc ctx pats = + List.map_filter (pat_to_user_pat ~avoid ~keep_names ?loc ctx) pats -let context_map_to_lhs ?(avoid = Id.Set.empty) ?loc map = +let context_map_to_lhs ?(avoid = Id.Set.empty) ?(keep_names = false) ?loc map = let avoid = ref avoid in - List.rev (pats_to_lhs ~avoid ?loc map.src_ctx map.map_inst) + List.rev (pats_to_lhs ~avoid ~keep_names ?loc map.src_ctx map.map_inst) let do_renamings env sigma ctx = let avoid, ctx' = diff --git a/src/context_map.mli b/src/context_map.mli index da4f1ede..84292e37 100644 --- a/src/context_map.mli +++ b/src/context_map.mli @@ -52,8 +52,11 @@ val inaccs_of_constrs : constr list -> pat list val pats_of_constrs : Environ.env -> Evd.evar_map -> constr list -> pat list val pat_of_constr : Environ.env -> Evd.evar_map -> constr -> pat -(** Translating back to user patterns. *) -val context_map_to_lhs : ?avoid:Id.Set.t -> ?loc:Loc.t -> context_map -> Syntax.lhs +(** Translating back to user patterns. When [keep_names] is set, variable + patterns reuse the context binder names verbatim (with [Implicit] + provenance) instead of going through name generation, so that names of + pre-existing hypotheses survive [Mangle Names]. *) +val context_map_to_lhs : ?avoid:Id.Set.t -> ?keep_names:bool -> ?loc:Loc.t -> context_map -> Syntax.lhs (** Pretty-printing *) val pr_constr_pat : env -> Evd.evar_map -> constr -> Pp.t diff --git a/src/covering.ml b/src/covering.ml index 9519f112..ee9a2072 100644 --- a/src/covering.ml +++ b/src/covering.ml @@ -1028,6 +1028,24 @@ exception UnfaithfulSplit of (Loc.t option * Pp.t) let rename_domain env sigma bindings map = let open Context.Rel.Declaration in let { src_ctx = ctx; map_inst = p; tgt_ctx = ctx' } = map in + (* Implicitly named variables (e.g. preexisting hypothesis names) may be + shadowed by explicit pattern names or other implicit names: drop their + bindings instead of producing two hypotheses with the same name. *) + let bindings = + let taken = + Int.Map.fold + (fun _ (id, _, gen) acc -> if gen == User then Id.Set.add id acc else acc) + bindings Id.Set.empty + in + let taken = ref taken in + Int.Map.filter (fun _ (id, _, gen) -> + match gen with + | Implicit -> + if Id.Set.mem id !taken then false + else (taken := Id.Set.add id !taken; true) + | _ -> true) + bindings + in let avoid = Int.Map.fold (fun i (id, inacc, generated) acc -> if generated != Generated then Id.Set.add id acc else acc) @@ -1082,18 +1100,23 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) if !Equations_common.debug then Feedback.msg_debug (str "succeeded with substitution: " ++ prlist_with_sep spc (fun ((loc, x, prov), pat) -> hov 2 (pr_provenance ~with_gen:true (Id.print x) prov ++ str" = " ++ pr_pat env !evars pat ++ spc ())) s); - let _check_aliases = + let _check_aliases = let check acc ((loc, x, gen), pat) = match Id.Map.find x acc with | exception Not_found -> Id.Map.add x (loc, gen, pat) acc | (loc', gen', pat') -> - if eq_pat_mod_inacc env !evars pat pat' then + if eq_pat_mod_inacc env !evars pat pat' then if gen == Generated then Id.Map.add x (loc', gen', pat') acc else Id.Map.add x (loc, gen, pat) acc else if data.flags.allow_aliases then acc - else + (* An implicitly named variable (e.g. a preexisting hypothesis + name in [dependent elimination]) may be shadowed by an + explicit pattern name: keep the explicit one. *) + else if gen == Implicit then acc + else if gen' == Implicit then Id.Map.add x (loc, gen, pat) acc + else let env = push_rel_context prob.src_ctx env in - let loc, pat, pat' = + let loc, pat, pat' = if loc_before loc loc' then loc', pat, pat' else loc, pat', pat in @@ -1121,7 +1144,11 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) | Generated, (User | Implicit) -> (Int.Map.add i (x', inacc && inacc', gen') bindings, s) | Generated, Generated -> (Int.Map.add i (x, inacc && inacc', gen) bindings, s) | _, Generated -> (Int.Map.add i (x, inacc && inacc', gen) bindings, s) - | _, _ -> + (* An explicit pattern name takes priority over an implicit one + (e.g. a preexisting hypothesis name in [dependent elimination]). *) + | User, Implicit -> (Int.Map.add i (x, inacc && inacc', gen) bindings, s) + | Implicit, User -> (Int.Map.add i (x', inacc && inacc', gen') bindings, s) + | _, _ -> if not (Id.equal x x') then (* We allow aliasing of implicit variable names resulting from forcing a pattern *) if not data.flags.allow_aliases && (gen == User && gen' == User) then diff --git a/src/depelim.ml b/src/depelim.ml index 56f1cc19..b554b4c2 100644 --- a/src/depelim.ml +++ b/src/depelim.ml @@ -372,6 +372,77 @@ let specialize_eqs ?with_block id = end end +(* When the covering term is refined, the subgoals are evars living in the + rel contexts computed by covering. Turning these rel contexts into the + named contexts of the subgoals ([Evarutil.push_rel_context_to_named_context]) + generates fresh names for all the binders, which under [Mangle Names] + mangles every hypothesis name, including the user-given [as]-pattern names + and the names of pre-existing hypotheses. The covering contexts however + carry the intended names: user-given names verbatim, generated names + already freshened (and mangled) by [Covering.rename_domain]. We collect, + for each subgoal evar, its covering context and instance, and rename the + subgoal hypotheses back to the corresponding binder names after refining. *) +let subgoals_of_splitting sigma split = + let rec aux acc split = + match split with + | Splitting.Compute (lhs, _, _, Splitting.RProgram c) -> + (match kind sigma c with + | Evar (ev, _ as evi) -> + if !Equations_common.debug then + Feedback.msg_debug Pp.(str "subgoal evar " ++ Evar.print ev ++ + str " ctx: " ++ Context_map.pr_context (Global.env ()) sigma lhs.Context_map.src_ctx ++ + str " inst: " ++ prlist_with_sep spc (Printer.pr_econstr_env (Global.env ()) sigma) + (Evd.expand_existential sigma evi)); + (ev, lhs.Context_map.src_ctx, Evd.expand_existential sigma evi) :: acc + | _ -> acc) + | Splitting.Compute (_, _, _, Splitting.REmpty _) -> acc + | Splitting.Split (_, _, _, brs) -> + Array.fold_left (fun acc s -> + match s with Some s -> aux acc s | None -> acc) acc brs + | Splitting.Mapping (_, s) -> aux acc s + | Splitting.Refined (_, _, s) -> aux acc s + in aux [] split + +let rename_hyps_to_subgoal_binders rsubgoals = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let ev = Proofview.Goal.goal gl in + let subgoal = List.find_opt (fun (ev', _, _) -> + match Evarutil.advance sigma ev' with + | Some ev' -> Evar.equal ev' ev + | None -> false) !rsubgoals + in + match subgoal with + | None -> Proofview.tclUNIT () + | Some (_, ctx, inst) -> + let hyps = Proofview.Goal.hyps gl in + if not (Int.equal (List.length hyps) (List.length inst)) then + Proofview.tclUNIT () + else + let len = List.length ctx in + let hyp_ids = List.fold_left (fun ids decl -> + Id.Set.add (Context.Named.Declaration.get_id decl) ids) + Id.Set.empty hyps + in + (* The named context of the subgoal and the evar instance are aligned: + an instance argument [Rel i] means the hypothesis stands for the + [i]-th declaration of the covering context. Rename it back to that + binder name, unless the name is already used in the goal. *) + let renames, _taken = List.fold_left2 (fun (renames, taken) decl arg -> + let cur = Context.Named.Declaration.get_id decl in + match kind sigma arg with + | Rel i when i <= len -> + (match Context.Rel.Declaration.get_name (List.nth ctx (pred i)) with + | Name id when not (Id.equal id cur) && not (Id.Set.mem id taken) -> + ((cur, id) :: renames, Id.Set.add id taken) + | _ -> (renames, taken)) + | _ -> (renames, taken)) + ([], hyp_ids) hyps inst + in + if List.is_empty renames then Proofview.tclUNIT () + else rename_hyp renames + end + (* Dependent elimination using Equations. *) let dependent_elim_tac ?patterns id : unit Proofview.tactic = enter_goal begin fun env sigma concl -> @@ -418,7 +489,7 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic = Tacticals.tclZEROMSG (str "Could not eliminate variable " ++ Id.print id) | Some (Covering.Splitted (_, newctx, brs)) -> let brs = Option.List.flatten (Array.to_list brs) in - let clauses_lhs = List.map Context_map.context_map_to_lhs brs in + let clauses_lhs = List.map (Context_map.context_map_to_lhs ~keep_names:true) brs in let clauses = List.map (fun lhs -> Syntax.Pre_clause (default_loc, lhs, Some rhs)) clauses_lhs in Proofview.tclUNIT clauses end @@ -430,7 +501,11 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic = List.rev_map (fun decl -> let decl_id = Context.Named.Declaration.get_id decl in if Names.Id.equal decl_id id then DAst.make ?loc pat - else DAst.make Syntax.(PUVar (decl_id, Generated))) loc_hyps + (* [Implicit] rather than [Generated]: the names of the + surrounding hypotheses are user-visible and should be + preserved (in particular under [Mangle Names]), while + still allowing aliasing with the given patterns. *) + else DAst.make Syntax.(PUVar (decl_id, Implicit))) loc_hyps in Syntax.Pre_clause (loc, lhs, Some rhs)) in Proofview.tclUNIT (List.map make_clause patterns) @@ -465,6 +540,7 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic = let prob = Context_map.id_subst ctx in let args = Context.Rel.instance_list mkRel 0 ctx in + let subgoals = ref [] in Refine.refine ~typecheck:true begin fun evars -> let evd = ref evars in (* Produce a splitting tree. *) @@ -479,8 +555,9 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic = let c = Vars.substl (List.rev rev_subst) c in if !Equations_common.debug then Feedback.msg_debug (str "refining with" ++ Printer.pr_econstr_env env !evd c); - (!evd, c) - end + subgoals := subgoals_of_splitting !evd split; + (!evd, c) + end <*> rename_hyps_to_subgoal_binders subgoals end let dependent_elim_tac_expr ?patterns id : unit Proofview.tactic = diff --git a/src/extra_tactics.ml b/src/extra_tactics.ml index 6cc5b3fe..03b2a58a 100644 --- a/src/extra_tactics.ml +++ b/src/extra_tactics.ml @@ -23,6 +23,34 @@ let autounfold_ref gr = in Eauto.autounfold ["core";db] Locusops.onConcl +(** [intro_binder_name] introduces the next hypothesis reusing the binder + name verbatim (only appending subscripts in case of clash), instead of + going through fresh name generation which would mangle it under + [Mangle Names]. It is meant to reintroduce hypotheses whose binder names + are user-given, e.g. after [revert]. Falls back to [intro] on anonymous + binders. *) +let intro_binder_name = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let name = + match kind sigma concl with + | Prod (na, _, _) | LetIn (na, _, _, _) -> na.Context.binder_name + | _ -> Anonymous + in + match name with + | Anonymous -> Tactics.intro + | Name id -> + let avoid = List.fold_left (fun avoid decl -> + Id.Set.add (Context.Named.Declaration.get_id decl) avoid) + Id.Set.empty (Proofview.Goal.hyps gl) + in + let rec freshen id = + if Id.Set.mem id avoid then freshen (Nameops.increment_subscript id) else id + in + Tactics.intro_mustbe_force (freshen id) + end + open Proofview.Goal open Proofview.Notations diff --git a/src/extra_tactics.mli b/src/extra_tactics.mli index 626a87bf..76af6054 100644 --- a/src/extra_tactics.mli +++ b/src/extra_tactics.mli @@ -19,3 +19,8 @@ val autounfold_ref : Names.GlobRef.t -> unit Proofview.tactic [ctx |- ?P args = ty] and then refines the goal with [c]. *) val refine_ho : EConstr.t -> unit Proofview.tactic + +(** Introduce the next hypothesis reusing the binder name verbatim (modulo + freshening by subscripts), bypassing name mangling ([Mangle Names]). + Falls back to [intro] on anonymous binders. *) +val intro_binder_name : unit Proofview.tactic diff --git a/src/g_equations.mlg b/src/g_equations.mlg index cef9ab54..cab35d85 100644 --- a/src/g_equations.mlg +++ b/src/g_equations.mlg @@ -509,6 +509,10 @@ TACTIC EXTEND refine_ho | [ "refine_ho" open_constr(c) ] -> { Extra_tactics.refine_ho c } END +TACTIC EXTEND intro_binder_name +| [ "intro_binder_name" ] -> { Extra_tactics.intro_binder_name } +END + TACTIC EXTEND eqns_specialize_eqs | [ "eqns_specialize_eqs" ident(i) ] -> { Depelim.specialize_eqs i diff --git a/test-suite/issue733.v b/test-suite/issue733.v new file mode 100644 index 00000000..1951864f --- /dev/null +++ b/test-suite/issue733.v @@ -0,0 +1,61 @@ +(* Test for issue #733: [dependent elimination] and [depelim] should be + compatible with [Set Mangle Names]: user-given [as]-pattern names and + pre-existing hypothesis names must be preserved, while generated names + are mangled. *) +From Equations Require Import Equations. + +Inductive vec : nat -> Type := +| vnil : vec 0 +| vcons : forall n, nat -> vec n -> vec (S n). +Derive Signature for vec. + +(** Without [Mangle Names], the [as]-pattern names are honored, as + documented. *) +Lemma dependent_elimination_ok n (v : vec (S n)) : nat. +Proof. + dependent elimination v as [@vcons k x tl]. + exact (x + k). +Qed. + +Set Mangle Names. + +(** The [as]-pattern names must be bound under [Mangle Names]. *) +Lemma dependent_elimination_mangle n (v : vec (S n)) : nat. +Proof. + dependent elimination v as [@vcons k x tl]. + exact (x + k). +Qed. + +(** Hypotheses unrelated to the eliminated variable keep their names. *) +Lemma dependent_elimination_telescope n (v : vec (S n)) (m : nat) : nat. +Proof. + dependent elimination v as [@vcons k x tl]. + exact (m + k + x). +Qed. + +(** Same without a pattern: the telescope is preserved, while the names of + the new hypotheses are generated and hence mangled. *) +Lemma dependent_elimination_nopat n (v : vec (S n)) (m : nat) : m = m. +Proof. + dependent elimination v. + exact (@eq_refl nat m). +Qed. + +(** [depelim] preserves the names of unrelated hypotheses too. *) +Lemma depelim_telescope n (v : vec (S n)) (m : nat) : m = m. +Proof. + depelim v. + exact (@eq_refl nat m). +Qed. + +(** [noconf] goes through the same block/reintroduction machinery: the names + of the hypotheses it reverts must be preserved as well. *) +Inductive tree := Leaf : nat -> tree | Node : tree -> tree -> tree. +Derive NoConfusion for tree. + +Lemma noconf_telescope (a b : nat) (H : Leaf a = Leaf b) (k : nat) : a = b. +Proof. + noconf H. + clear k. + exact (@eq_refl nat a). +Qed. diff --git a/theories/core/CoreTactics.v b/theories/core/CoreTactics.v index cc0bf988..b7628278 100644 --- a/theories/core/CoreTactics.v +++ b/theories/core/CoreTactics.v @@ -20,10 +20,13 @@ Local Open Scope equations_scope. Definition block := the_equations_tag. +(** We use [intro_binder_name] rather than [intro] so that the names of the + reverted hypotheses are reused verbatim, in particular under + [Mangle Names] which would otherwise mangle them. *) Ltac intros_until_block := match goal with |- let _ := block in _ => intros _ - | |- _ => try (intro; intros_until_block) + | |- _ => try (intro_binder_name; intros_until_block) end. Ltac block_goal :=