Make dependent elimination compatible with Set Mangle Names

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' =

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

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

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 =

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
 

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

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

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.

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 :=