simp? lists let variables unnecessarily

Stream: lean4

[Michael Stoll]

I have noticed that simp? tends to include variables from let bindings in the list it suggests even though they are not necessary (e.g., because they do not even occur in the expression to be simplified). This seems to be triggered by an earlier simp or simp only using such a variable. Here is a Mathlib-free #mwe:

example (a b : Int) : a + b - b = a := by
  let p := 1
  have h : p = 1 := by
    simp only [p] -- no `p` below without the `simp only [p]` here
  simp?-- Try this: simp only [Int.add_sub_cancel, p]

Clearly, p should not be mentioned (and simp only [Int.add_sub_cancel] of course works). Replacing simp only [p] in the line above by sorry makes the p go away.

[Kyle Miller]

It looks like the zetaDeltaFVarIds set isn't being reset by simp, and simp uses this to keep track of which local variables have been reduced. Could you report a Lean 4 issue with this example?

[Jovan Gerbscheid]

I have made lean4#7539 to fix this. I think the relevant issue is lean4#6655

[Kyle Miller]

Good to know, I was considering making a similar change for other reasons.

[Michael Stoll]

I've added the example to lean4#6655 .