fix: refine how simp tracks unfolded local definitions (leanprover#8753)

This PR fixes a bug in `simp` where it was not resetting the set of
zeta-delta reduced let definitions between `simp` calls. It also fixes a
bug where `simp` would report zeta-delta reduced let definitions that
weren't given as simp arguments (these extraneous let definitions appear
due to certain processes temporarily setting `zetaDelta := true`). This
PR also modifies the metaprogramming interface for the zeta-delta
tracking functions to be re-entrant and to prevent this kind of no-reset
bug from occurring again. Closes leanprover#6655.

Re-entrance of this metaprogramming interface is not needed to fix
leanprover#6655, but it is needed for some future PRs.

The `tests/lean/run/6655.lean` file has an example of a deficiency of
`simp?`, where `simp?` still over-reports unfolded let declarations.
This is likely due to `withInferTypeConfig` setting `zetaDelta := true`
from within `isDefEq`, but I did not verify this.

This PR supersedes leanprover#7539. The difference is that this PR has
`withResetZetaDeltaFVarIds` save and restore `zetaDeltaFVarIds`, but
that PR saves and then extends `zetaDeltaFVarIds` to persist unfolded
fvars. The behavior in this PR lets metaprograms control whether they
want to persist any of the unfolded fvars in this context themselves. In
practice, metaprograms that use `withResetZetaDeltaFVarIds` are creating
many temporary fvars and are doing dependence computations. These
temporary fvars shouldn't be persisted, and also dependence shouldn't be
inferred from the fact that a dependence calculation was done. (Concrete
example: the let-to-have transformation in an upcoming PR can be run
from within simp. Just because let-to-have unfolds an fvar while
calculating dependencies of lets doesn't mean that this fvar should be
included by `simp?`.)

Author: kmill

src/Lean/Elab/MutualDef.lean

@@ -1014,7 +1014,6 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
   let letRecsToLift := letRecsToLift.toArray
   let mainFVarIds := mainFVars.map Expr.fvarId!
   let recFVarIds  := (letRecsToLift.map fun toLift => toLift.fvarId) ++ mainFVarIds
-  resetZetaDeltaFVarIds
   withTrackingZetaDelta do
     -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`.
     let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do

src/Lean/Meta/Basic.lean

@@ -687,12 +687,6 @@ def getConfig : MetaM Config :=
 def getConfigWithKey : MetaM ConfigWithKey :=
   return (← getConfig).toConfigWithKey
 
-def resetZetaDeltaFVarIds : MetaM Unit :=
-  modify fun s => { s with zetaDeltaFVarIds := {} }
-
-def getZetaDeltaFVarIds : MetaM FVarIdSet :=
-  return (← get).zetaDeltaFVarIds
-
 /-- Return the array of postponed universe level constraints. -/
 def getPostponed : MetaM (PersistentArray PostponedEntry) :=
   return (← get).postponed
@@ -1120,15 +1114,12 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
       modify fun s => { s with cache := cacheSaved }
 
 /--
-Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
--/
-@[inline] def withTrackingZetaDelta : n α → n α :=
-  mapMetaM fun x =>
-    withFreshCache <| withReader (fun ctx => { ctx with trackZetaDelta := true }) x
+If `s` is nonempty, then `withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
+The cache is temporarily reset while executing `x`.
 
-/--
-`withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
-The cache is reset while executing `x` if `s` is not empty.
+If `s` is empty, then runs `x` without changing `zetaDeltaSet` or resetting the cache.
+
+See also `withTrackingZetaDeltaSet` for tracking zeta-delta reductions.
 -/
 def withZetaDeltaSet (s : FVarIdSet) : n α → n α :=
   mapMetaM fun x =>
@@ -1138,14 +1129,59 @@ def withZetaDeltaSet (s : FVarIdSet) : n α → n α :=
       withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s }) x
 
 /--
-Similar to `withZetaDeltaSet`, but also enables `withTrackingZetaDelta` if `s` is not empty.
+Gets the current `zetaDeltaFVarIds` set.
+If `Context.trackZetaDelta` is true, then `whnf` adds to this set
+those local definitions that are unfolded ("zeta-delta reduced") .
+
+See `withTrackingZetaDelta` and `withTrackingZetaDeltaSet`.
+-/
+def getZetaDeltaFVarIds : MetaM FVarIdSet :=
+  return (← get).zetaDeltaFVarIds
+
+/--
+`withResetZetaDeltaFVarIds x` executes `x` in a context where the `zetaDeltaFVarIds` is temporarily cleared.
+
+**Warning:** This does not reset the cache.
+-/
+@[inline] private def withResetZetaDeltaFVarIds : n α → n α :=
+  mapMetaM fun x => do
+    let zetaDeltaFVarIdsSaved ← modifyGet fun s => (s.zetaDeltaFVarIds, { s with zetaDeltaFVarIds := {} })
+    try
+      x
+    finally
+      modify fun s => { s with zetaDeltaFVarIds := zetaDeltaFVarIdsSaved }
+
+/--
+`withTrackingZetaDelta x` executes `x` while tracking zeta-delta reductions performed by `whnf`.
+Furthermore, the `zetaDeltaFVarIds` set is temporarily cleared,
+and also the cache is temporarily reset so that reductions are accurately tracked.
+
+Any zeta-delta reductions recorded while executing `x` will *not* persist when leaving `withTrackingZetaDelta`.
+-/
+@[inline] def withTrackingZetaDelta : n α → n α :=
+  mapMetaM fun x =>
+    withFreshCache <| withReader (fun ctx => { ctx with trackZetaDelta := true }) <| withResetZetaDeltaFVarIds x
+
+@[deprecated withTrackingZetaDelta (since := "2025-06-12")]
+def resetZetaDeltaFVarIds : MetaM Unit :=
+  modify fun s => { s with zetaDeltaFVarIds := {} }
+
+/--
+`withTrackingZetaDeltaSet s x` executes `x` in a context where `zetaDeltaFVarIds` has been temporarily cleared.
+- If `s` is nonempty, zeta-delta tracking is enabled and `zetaDeltaSet := s`.
+  Furthermore, the cache is temporarily reset so that zeta-delta tracking is accurate.
+- If `s` is empty, then zeta-delta tracking is disabled. The `zetaDeltaSet` is *not* modified, and the cache is not cleared.
+
+Any zeta-delta reductions recorded while executing `x` will *not* persist when leaving `withTrackingZetaDeltaSet`.
+
+See also `withZetaDeltaSet`, which does not interact with zeta-delta tracking.
 -/
 def withTrackingZetaDeltaSet (s : FVarIdSet) : n α → n α :=
   mapMetaM fun x =>
     if s.isEmpty then
-      x
+      withReader (fun ctx => { ctx with trackZetaDelta := false }) <| withResetZetaDeltaFVarIds x
     else
-      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s, trackZetaDelta := true }) x
+      withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s, trackZetaDelta := true }) <| withResetZetaDeltaFVarIds x
 
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x

src/Lean/Meta/Closure.lean

@@ -343,7 +343,6 @@ structure MkValueTypeClosureResult where
   exprArgs    : Array Expr
 
 def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do
-  resetZetaDeltaFVarIds
   withTrackingZetaDelta do
     let type  ← collectExpr type
     let value ← collectExpr value

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

@@ -800,14 +800,26 @@ where
   withTrackingZetaDeltaSet ctx.zetaDeltaSet <|
   withReducible x
 
-private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (usedZetaDelta : FVarIdSet) : UsedSimps :=
-  usedZetaDelta.fold (init := s) fun s fvarId =>
-    s.insert <| .fvar fvarId
+/--
+Adds the fvars from `usedZetaDelta` to `s` if they are present in
+the set `zetaDeltaSet` of fvars that are explicitly added to the simp context.
+
+*Note:* `usedZetaDelta` might contain fvars that are not in `zetaDeltaSet`,
+since within `withResetZetaDeltaFVarIds` it is possible for `whnf` to be run with different configurations,
+ones that allow zeta-delta reducing fvars not in `zetaDeltaSet` (e.g. `withInferTypeConfig` sets `zetaDelta := true`).
+This also means that `usedZetaDelta` set might be reporting fvars in `zetaDeltaSet` that weren't "used".
+-/
+private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (zetaDeltaSet : FVarIdSet) (usedZetaDelta : FVarIdSet) : UsedSimps :=
+  zetaDeltaSet.fold (init := s) fun s fvarId =>
+    if usedZetaDelta.contains fvarId then
+      s.insert <| .fvar fvarId
+    else
+      s
 
 private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM Stats := do
   let used := stats.usedTheorems
-  let used := updateUsedSimpsWithZetaDeltaCore used ctx.initUsedZetaDelta
-  let used := updateUsedSimpsWithZetaDeltaCore used (← getZetaDeltaFVarIds)
+  let used := updateUsedSimpsWithZetaDeltaCore used ctx.zetaDeltaSet ctx.initUsedZetaDelta
+  let used := updateUsedSimpsWithZetaDeltaCore used ctx.zetaDeltaSet (← getZetaDeltaFVarIds)
   return { stats with usedTheorems := used }
 
 @[inline] def withCatchingRuntimeEx (x : SimpM α) : SimpM α := do

tests/lean/run/6655.lean

@@ -0,0 +1,109 @@
+/-!
+# Improve zeta-delta tracking for `simp?`
+
+https://github.com/leanprover/lean4/issues/6655 reports issues with `simp?` where
+it would over-report local variables. This comes down to two kinds of issues:
+- zeta-delta tracking wasn't being reset, so previous `simp?`s would contribute variables
+- `simp?` would report variables that weren't explicitly mentioned,
+  because `whnf` would be run with different configurations during the tracking.
+  (e.g. `withInferTypeConfig` enables `zetaDelta`.)
+
+This file tests that it resets the tracking and filters the list.
+-/
+
+/-!
+Example from #6655. This used to suggest `simp only [e, d]`.
+-/
+/--
+info: Try this: simp only [e]
+---
+trace: α : Type
+c : α → α
+x : α
+d : α → α := c
+e : α → α := d
+⊢ d x = x
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example {α : Type} (c : α → α) (x : α) : c x = x := by
+  let d := c
+  let e := d
+  change e x = x
+  simp? [e]
+  trace_state
+  sorry
+
+/-!
+Example from #6655. This used to suggest `simp only [d]`.
+-/
+/--
+info: Try this: simp only
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example {α : Type} (c : α → α) (x : α) : c x = x := by
+  let d := c
+  change d x = x
+  simp [d]
+  have : x = x := by
+    simp?
+  sorry
+
+/-!
+Example from comments of #6655. This used to suggest `simp only [Int.add_sub_cancel, p]`.
+(N.B. the goal at that point does not have `p` in it!)
+-/
+/-- info: Try this: simp only [Int.add_sub_cancel] -/
+#guard_msgs in
+example (a b : Int) : a + b - b = a := by
+  let p := 1
+  have h : p = 1 := by
+    simp only [p]
+  simp?
+
+/-!
+Example from https://github.com/leanprover/lean4/pull/7539 by JovanGerb.
+This used to suggest `simp only [a, b] ` and `simp only [a, b]`
+-/
+/--
+info: Try this: simp only [a]
+---
+info: Try this: simp only
+-/
+#guard_msgs in
+example : True := by
+  let a := 1
+  let b := 2
+  have : b = 2 := by simp [a,b]
+  have : a = 1 := by simp? [a]
+  have : 1 = 1 := by simp?
+  trivial
+
+/-!
+Test that there is still a deficiency. This should say `simp only [e]`.
+-/
+/--
+info: Try this: simp only [e, c]
+---
+trace: α : Type
+b : α → α
+x : α
+c : α → α := b
+d : α → α := c
+e : α → α := d
+⊢ d x = x
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example {α : Type} (b : α → α) (x : α) : b x = x := by
+  let c := b
+  let d := c
+  let e := d
+  change e x = x
+  simp? [e, c]
+  trace_state
+  sorry