feat: binderNameHint

[nomeata]

This PR adds the binderNameHint gadget. It can be used in rewrite and simp rules to preserve a user-provided name where possible.

The expression binderNameHint v binder e defined to be e.

If it is used on the right-hand side of an equation that is applied by a tactic like rw or simp,
and v is a local variable, and binder is an expression that (after beta-reduction) is a binder
(so fun w => … or ∀ w, …), then it will rename v to the name used in the 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

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.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-04 12:46:57) View Log
• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-04 14:57:50) View Log
• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-04 15:48:23) View Log
• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-04 16:43:23) View Log
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-05 11:21:14)
• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-06 10:05:30) View Log
• ✅ Mathlib branch lean-pr-testing-6947 has successfully built against this PR. (2025-02-06 11:23:47) View Log

[eric-wieser]

Should this be legal on the LHS too, to allow reverse rewriting?

[nomeata]

Hmm, for that we’d have to make sure it does not get in the way of matching, so probably has to be marked as reducible? One would have to investigate if that works well first.

[eric-wieser]

I wonder if this ought to be reducible, so that defeq matching on the types of theorems (for instance, perhaps loogle and exact?) does not get tripped up by it?

More extremely, perhaps it should be a macro that produces an Expr.mdata, so that unaware tactics can easily strip it?

[nomeata]

Right, making this reducible is worth a try.

I don’t think a mdata can store other expressions, so not sure if this would work better.