feat: binderNameHint in congr (#7053)

This PR makes `simp` heed the `binderNameHint` also in the assumptions
of congruence rules. Fixes #7052.

src/Init/BinderNameHint.lean

@@ -31,8 +31,12 @@ example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name)
 If `binder` is not a binder, then the name of `v` attains a macro scope. This only matters when the
 resulting term is used in a non-hygienic way, e.g. in termination proofs for well-founded recursion.
 
-This gadget is supported by `simp`, `dsimp` and `rw` in the right-hand-side of an equation, but not
-in hypotheses or by other tactics.
+This gadget is supported by
+* `simp`, `dsimp` and `rw` in the right-hand-side of an equation
+* `simp` in the assumptions of congruence rules
+
+It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
+(e.g. `apply`).
 -/
 @[simp ↓]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Lean/Meta/BinderNameHint.lean

@@ -52,7 +52,7 @@ and the innermost binder is at the end. We update the binder names therein when
 -/
   go (e : Expr) : MonadCacheT ExprStructEq Expr (StateT (Array Name) CoreM) Expr := do
     checkCache { val := e : ExprStructEq } fun _ => do
-      if e.isAppOfArity `binderNameHint 6 then
+      if e.isAppOfArity ``binderNameHint 6 then
         let v := e.appFn!.appFn!.appArg!
         let b := e.appFn!.appArg!
         let e := e.appArg!

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -483,8 +483,8 @@ def congrDefault (e : Expr) : SimpM Result := do
       congrArgs (← simp f) args
 
 /-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/
-def processCongrHypothesis (h : Expr) : SimpM Bool := do
-  forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
+def processCongrHypothesis (h : Expr) (hType : Expr) : SimpM Bool := do
+  forallTelescopeReducing hType fun xs hType => withNewLemmas xs do
     let lhs ← instantiateMVars hType.appFn!.appArg!
     let r ← simp lhs
     let rhs := hType.appArg!
@@ -521,7 +521,9 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
   recordCongrTheorem c.theoremName
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
-  let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
+  let thmType ← inferType thm
+  let thmHasBinderNameHint := thmType.hasBinderNameHint
+  let (xs, bis, type) ← forallMetaTelescopeReducing thmType
   if c.hypothesesPos.any (· ≥ xs.size) then
     return none
   let isIff := type.isAppOf ``Iff
@@ -537,12 +539,14 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
   if (← withSimpMetaConfig <| isDefEq lhs e) then
     let mut modified := false
     for i in c.hypothesesPos do
-      let x := xs[i]!
+      let h := xs[i]!
+      let hType ← instantiateMVars (← inferType h)
+      let hType ← if thmHasBinderNameHint then hType.resolveBinderNameHint else pure hType
       try
-        if (← processCongrHypothesis x) then
+        if (← processCongrHypothesis h hType) then
           modified := true
       catch _ =>
-        trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
+        trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {hType}"
         -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..`
         -- does not catch runtime exceptions by default.
         return none

tests/lean/run/binderNameHint_congr.lean

@@ -0,0 +1,61 @@
+section no_congr
+/--
+error: tactic 'fail' failed
+xs : List Nat
+⊢ xs = List.map (fun y => 1 + y) xs
+-/
+#guard_msgs in
+example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
+  simp
+  fail
+
+end no_congr
+
+section with_congr
+
+/--
+info: List.map_congr_left.{u_1, u_2} {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹}
+  (h : ∀ (a : α✝), a ∈ l → f a = g a) : List.map f l = List.map g l
+-/
+#guard_msgs in
+#check List.map_congr_left
+
+attribute [local congr] List.map_congr_left
+
+/--
+error: tactic 'fail' failed
+xs : List Nat
+⊢ xs = List.map (fun a => 1 + a) xs
+-/
+#guard_msgs in
+example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
+  simp -- NB: Changes variable name!
+  fail
+
+end with_congr
+
+section with_congr_hint
+
+-- Trying to use the binderNameHint on a congruence rule
+
+theorem List.map_congr_left'' {f g : α → β}
+  (h : ∀ (a : α), a ∈ l → binderNameHint a f (f a) = g a) :
+  List.map f l = List.map g l  := List.map_congr_left h
+
+attribute [local congr] List.map_congr_left''
+
+-- set_option trace.Debug.Meta.Tactic.simp true
+-- set_option pp.instantiateMVars false
+-- set_option trace.Debug.Meta.Tactic.simp.congr true
+
+/--
+error: tactic 'fail' failed
+xs : List Nat
+⊢ xs = List.map (fun y => 1 + y) xs
+-/
+#guard_msgs in
+example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
+  simp
+  fail
+
+end with_congr_hint