feat: binderNameHint

src/Init.lean

@@ -39,3 +39,4 @@ import Init.While
 import Init.Syntax
 import Init.Internal
 import Init.Try
+import Init.BinderNameHint

src/Init/BinderNameHint.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Init.Prelude
+import Init.Tactics
+
+set_option linter.unusedVariables false in
+/--
+The expression `binderNameHint v binder e` defined to be `e`.
+
+If it is used on the right-hand side of an equation that is used for rewriting by `rw` or `simp`,
+and `v` is a local variable, and `binder` is an expression that (after beta-reduction) is a binder
+(`fun w => …` or `∀ w, …`), then it will rename `v` to the name used in that binder, and remove
+the `binderNameHint`.
+
+A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local
+variable is still `name`, and not `x`:
+```
+theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
+    l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry
+
+example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
+  rw [all_eq_not_any_not]
+  -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
+```
+
+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.
+-/
+@[simp ↓]
+def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Lean/Meta.lean

@@ -51,3 +51,4 @@ import Lean.Meta.LitValues
 import Lean.Meta.CheckTactic
 import Lean.Meta.Canonicalizer
 import Lean.Meta.Diagnostics
+import Lean.Meta.BinderNameHint

src/Lean/Meta/BinderNameHint.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+
+import Lean.Util.FindExpr
+import Lean.Meta.Basic
+import Init.BinderNameHint
+
+namespace Lean
+
+
+/-- Does `e` have a binder name hint? (quick check) -/
+def Expr.hasBinderNameHint (e : Expr) : Bool :=
+  Option.isSome <| e.find? fun e => e.isConstOf `binderNameHint
+
+private def  enterScope (name : Name) (xs : Array Name) : Array Name :=
+    xs.push name
+
+private def exitScope (xs : Array Name) : Name × Array Name :=
+    assert! xs.size > 0
+    (xs.back!, xs.pop)
+
+private def rememberName (bidx : Nat) (name : Name) (xs : Array Name) : Array Name :=
+    assert! xs.size > bidx
+    xs.set! (xs.size - bidx - 1) name
+
+private def makeFresh (bidx : Nat) (xs : Array Name) : CoreM (Array Name) := do
+    assert! xs.size > bidx
+    let name := xs[xs.size - bidx - 1]!
+    let name' ← Core.mkFreshUserName name
+    return xs.set! (xs.size - bidx - 1) name'
+
+/--
+Resovles occurrences of `binderNameHint` in `e`. See docstring of `binderNameHint` for more
+information.
+-/
+partial def Expr.resolveBinderNameHint (e : Expr) : CoreM Expr :=
+  (go e).run.run' #[]
+where
+/-
+Implementation note:
+
+We traverse the expression as an open term; we do not need a local context here.
+
+The state is the array of binder names. The length of the array is always the binder nesting depth,
+and the innermost binder is at the end. We update the binder names therein when encountering a
+`binderNameHint`, and update the binder when exiting the scope.
+-/
+  go (e : Expr) : MonadCacheT ExprStructEq Expr (StateT (Array Name) CoreM) Expr := do
+    checkCache { val := e : ExprStructEq } fun _ => do
+      if e.isAppOfArity `binderNameHint 6 then
+        let v := e.appFn!.appFn!.appArg!
+        let b := e.appFn!.appArg!
+        let e := e.appArg!
+        let e' ← go e
+        match v, b.headBeta with
+        | .bvar bidx, .lam n _ _ _
+        | .bvar bidx, .forallE n _ _ _ =>
+          modify (rememberName bidx n)
+        | .bvar bidx, _ =>
+          -- If we do not have a binder to use, ensure that name has macro scope.
+          -- This is used by the auto-attach lemmas so that the new binder `fun h =>`
+          -- has a macro-scope, and is inaccessible in the termination proof.
+          -- (Using `fun _ =>` causes `property†` to appear, which is bad UX)
+          let xs ← get
+          assert! xs.size > bidx
+          let n := xs[xs.size - bidx - 1]!
+          let n' ← mkFreshUserName n
+          modify (rememberName bidx n')
+        | _, _ =>
+          pure ()
+        pure e'
+      else
+        match e with
+        | .forallE n d b bi =>
+          let d' ← go d
+          modify (enterScope n)
+          let b' ← go b
+          let n' ← modifyGet exitScope
+          return .forallE n' d' b' bi
+        | .lam n d b bi =>
+          let d' ← go d
+          modify (enterScope n)
+          let b' ← go b
+          let n' ← modifyGet exitScope
+          return .lam n' d' b' bi
+        | .letE n t v b nd  =>
+          let t' ← go t
+          let v' ← go v
+          modify (enterScope n)
+          let b' ← go b
+          let n' ← modifyGet exitScope
+          return .letE n' t' v' b' nd
+        | .app f a         => return e.updateApp! (← go f) (← go a)
+        | .mdata _ b       => return e.updateMData! (← go b)
+        | .proj _ _ b      => return e.updateProj! (← go b)
+        | _                => return e
+
+end Lean

src/Lean/Meta/Tactic/Rewrite.lean

@@ -10,6 +10,7 @@ import Lean.Meta.KAbstract
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Apply
+import Lean.Meta.BinderNameHint
 
 namespace Lean.Meta
 
@@ -43,6 +44,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs
           let eNew ← instantiateMVars eNew
+          let eNew ← if rhs.hasBinderNameHint then eNew.resolveBinderNameHint else pure eNew
           let eType ← inferType e
           let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
           try

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.BinderNameHint
 
 namespace Lean.Meta.Simp
 
@@ -147,6 +148,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {e} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}:{indentExpr e}\n==>{indentExpr rhs}"
+      let rhs ← if type.hasBinderNameHint then rhs.resolveBinderNameHint else pure rhs
       recordSimpTheorem thm.origin
       return some { expr := rhs, proof? }
     else

tests/lean/run/binderNameHint.lean

@@ -0,0 +1,95 @@
+theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
+    l.all p = !l.any fun x => binderNameHint x p (!p x)
+  := List.all_eq_not_any_not l p
+
+/--
+error: tactic 'fail' failed
+names : List String
+⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
+-/
+#guard_msgs in
+example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
+  rw [all_eq_not_any_not]
+  fail
+
+
+/--
+error: tactic 'fail' failed
+names : List String
+⊢ (names.any fun name => !"Waldo".isPrefixOf name) = false
+-/
+#guard_msgs in
+example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
+  simp [all_eq_not_any_not, -List.any_eq_false]
+  fail
+
+
+def List.myAll (p : α → Bool) (xs : List α) : Bool := !(xs.any fun x => !p x)
+
+theorem myAll_eq_not_any_not (l : List α) (p : α → Bool) :
+    l.myAll p = !l.any fun x => binderNameHint x p (!p x)
+  := rfl
+
+/--
+error: tactic 'fail' failed
+names : List String
+⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
+-/
+#guard_msgs in
+example (names : List String) : names.myAll (fun name => "Waldo".isPrefixOf name) = true := by
+  dsimp [myAll_eq_not_any_not]
+  fail
+
+-- Check if we can pick the second binder by providing arguments to `f` in `binderNameHint`
+-- (It will beta-reduce it)
+
+
+-- Why this not in standard lib (maybe with the more complex form of recognizing lambdas that
+-- ignore arguments?)
+@[simp]
+theorem List.mapIdx_eq_map (l : List α) (f : α → β) : (l.mapIdx fun _ x => f x) = l.map f := by
+  induction l <;> simp_all
+
+set_option linter.unusedVariables false in
+theorem zipWith_eq_map_idx_zipWith (l1 : List α) (l2 : List β) (f : α → β → γ) :
+    List.zipWith f l1 l2 = (List.zip l1 l2).mapIdx
+      (fun i ⟨a, b⟩ => binderNameHint a f <| binderNameHint b (f a) <| f a b)
+  := by simp [List.zip_eq_zipWith, List.map_zipWith]
+
+/--
+error: tactic 'fail' failed
+l1 l2 : List Nat
+⊢ (List.mapIdx
+        (fun i x =>
+          match x with
+          | (x, y) => x + y)
+        (l1.zip l2)).isEmpty =
+    true
+-/
+#guard_msgs in
+example (l1 l2 : List Nat) :
+  (List.zipWith  (fun x y => x + y) l1 l2).isEmpty := by
+  rw [zipWith_eq_map_idx_zipWith]
+  fail
+
+-- For now, binder name hints do not work in other tactics, like `apply`
+-- (but at least `simp` or `dsimp` removes them)
+
+theorem myAll_eq_not_any_not_iff {l : List α} {p : α → Bool} :
+    l.myAll p ↔ !l.any fun x => binderNameHint x p (!p x)
+  := by simp [myAll_eq_not_any_not]
+
+/--
+error: unsolved goals
+names : List String
+⊢ (!names.any fun x => !"Waldo".isPrefixOf x) = true
+---
+info: names : List String
+⊢ (!names.any fun x => binderNameHint x (fun name => "Waldo".isPrefixOf name) !"Waldo".isPrefixOf x) = true
+-/
+#guard_msgs in
+example (names : List String) : names.myAll (fun name => "Waldo".isPrefixOf name) = true := by
+  apply myAll_eq_not_any_not_iff.mpr
+  trace_state
+  dsimp
+  done

tests/lean/run/binderNameHintScope.lean

@@ -0,0 +1,28 @@
+import Lean
+
+-- This checks that binderNameHint freshens up a variable.:
+
+axiom allPairs (l : List α) (p : α → α → Bool) : Bool
+
+#guard_msgs (drop warning) in
+theorem all_eq_allPairs (l : List α) (p : α → Bool) :
+    l.all p ↔ ∀ x y z, binderNameHint x p <| binderNameHint y () <| p x && p y && p z:= sorry
+
+-- below we should get `a` from the user (no dagger), `y` with dagger (binderNameHint added a macro
+-- scope) and `z` without dagger (because intro1P is not hygienic)
+
+/--
+error: tactic 'fail' failed
+f : String → Bool
+names : List String
+a y✝ z : String
+⊢ (f a && f y✝ && f z) = true
+-/
+#guard_msgs in
+open Lean Elab Tactic in
+example {f : String → Bool} (names : List String) : names.all (fun a => f a) = true := by
+  rw [all_eq_allPairs]
+  run_tac liftMetaTactic1 ((some ·.2) <$> ·.intro1P)
+  run_tac liftMetaTactic1 ((some ·.2) <$> ·.intro1P)
+  run_tac liftMetaTactic1 ((some ·.2) <$> ·.intro1P)
+  fail

tests/lean/run/binderNameHintSimp.lean

@@ -0,0 +1,35 @@
+/-!
+Checks that `simp` removes the `binderNameHint` in the pre-phase, and does not spend time looking
+at its arguments.
+
+The following traces should show no rewriting of `x` or `y`, only `z`.
+-/
+
+def x : Nat := 0
+def y : Nat := 0
+def z : Nat := 0
+
+set_option trace.Meta.Tactic.simp.rewrite true
+
+/--
+info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
+      binderNameHint x y z
+    ==>
+      z
+[Meta.Tactic.simp.rewrite] unfold z, z ==> 0
+[Meta.Tactic.simp.rewrite] eq_self:1000: 0 = 0 ==> True
+-/
+#guard_msgs in
+example : binderNameHint x y z = 0 := by
+  simp [x, y, z]
+
+/--
+info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
+      binderNameHint x y z
+    ==>
+      z
+[Meta.Tactic.simp.rewrite] unfold z, z ==> 0
+-/
+#guard_msgs in
+example : binderNameHint x y z = 0 := by
+  dsimp [x, y, z]