Tactics destroying binder names

Stream: lean4

[Arend Mellendijk]

When working with sums, I am always very careful to keep the names of variables that I'm summing over consistent. This is in line with what I would do on paper, to make it clear how the summands in two different sums are supposed to line up.

Yet lots of tactics (particularly simp and rw) destroy the names of bound variables, and use the names in the rewrite lemma instead. This can make it much harder to read the intermediate goal state.

import Mathlib

example (f : ℕ → ℕ → ℕ) (s : Finset ℕ) :
    ∑ i ∈ s, ∑ j ∈ s, f i j = ∑ j ∈ s, ∑ i ∈ s, f i j := by
  rewrite [Finset.sum_comm]
  /-
  f : ℕ → ℕ → ℕ
  s : Finset ℕ
  ⊢ ∑ y ∈ s, ∑ x ∈ s, f x y = ∑ j ∈ s, ∑ i ∈ s, f i j
  -/
  rfl

example (f g : ℕ → ℕ) (s : Finset ℕ) : ∑ i ∈ s, (f i + g i) = 37 := by
  simp_rw [Finset.sum_add_distrib]
  /-
  f g : ℕ → ℕ
  s : Finset ℕ
  ⊢ ∑ x ∈ s, f x + ∑ x ∈ s, g x = 37
  -/
  sorry

This has me thinking: What would it take to make simp or rw respect binder names? There is probably not one "right" way to do this (what if the same binder name shows up twice on the LHS), but there ought to be something better than the current behaviour.

As a proof-of-concept I made a quick simproc for Finset.sum_add_distrib that respects binder names, but this isn't quite enough. The congruence lemma used by simp still destroys the binder name.

ugly meta code

import Mathlib

open Lean Elab Tactic Term Meta

/- Create a simproc that applies `Finset.sum_add_distrib` while keeping the binder names consistent. -/
simproc_decl test (∑ _ ∈ _, (_ + _)) :=
  fun e => do
    match e.getAppFn with
    | Expr.const ``Finset.sum levels => do
      let args := e.getAppArgs
      let fn := args[4]!
      match fn with
      | .lam binderName binderType expr binderInfo => do
        match expr.getAppFn with
        | Expr.const ``HAdd.hAdd _ =>
          let addArgs := expr.getAppArgs
          let largs := args.set! 4 (.lam binderName binderType addArgs[4]! binderInfo)
          let rargs := args.set! 4 (.lam binderName binderType addArgs[5]! binderInfo)
          let e1 : Expr := mkAppN (.const ``Finset.sum levels) largs
          let e2 : Expr := mkAppN (.const ``Finset.sum levels) rargs
          let e_new := mkAppN expr.getAppFn (addArgs.set! 4 e1 |>.set! 5 e2)
          let proof ← Lean.Meta.mkAppOptM ``Finset.sum_add_distrib #[.none , args[1]!, args[3]!, largs[4]!, rargs[4]!, .none]
          return .continue ({expr := e_new, proof? := proof} : Simp.Result)
        | _ =>
          return .continue
      | _ => return .continue
    | _ => do
      return .continue

/- This works! The binder keeps its name. -/
example (s : Finset ℕ) (f g : ℕ → ℝ) :
    ∑ j ∈ s, (f j + g j) = 9 := by
  simp only [test]
  /-
  i : ℕ
  s : Finset ℕ
  f g : ℕ → ℝ
  ⊢ ∑ j ∈ s, f j + ∑ j ∈ s, g j = 9
  -/
  sorry

/- This does not work! The `i` gets renamed to `x` by (I think) a congruence lemma. -/
example (s : Finset ℕ) (f g : ℕ → ℝ) :
    ∑ i ∈ s, ∑ j ∈ s, (f j + g i) = 37 := by
  simp_rw[test]
  /-
  s : Finset ℕ
  f g : ℕ → ℝ
  ⊢ ∑ x ∈ s, ∑ j ∈ s, f j + ∑ x ∈ s, ∑ j ∈ s, g x = 37
  -/
  sorry

[Yaël Dillies]

Thank you for bringing this up! @Kyle Miller and I spoke about it a year ago. I don't remember whether anything came of it

[Kyle Miller]

It'd be nice having a self-contained issue tracking these examples in the Lean repository.

My only ideas for this involve making isDefEq more complex and introducing a concept of binder name metavariables. Rewrite and simp would need to go through the type of a theorem and replace matching binder names with fresh binder name metavariables. Then, the pretty printer would need to be aware of these.

[Arend Mellendijk]

I wonder if there's something smaller in scope we could do in mathlib. There's been some demand about a version of rw that can rewrite underneath binders, so this is an opportunity to develop a more ergonomic rw that also tries to respect binder names.

Note further down in the linked thread that this sort of idea has been explored before, and I don't know how this would interact with that previous work.