`simp?` unfolds more let definitions than a bare `simp` call

[sgouezel]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In some situations, simp? creates a simp only call wrongly unfolding let variables.

Context

Zulip discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simp.3F.20adding.20let.20reduction/near/493985664

Steps to Reproduce

Run the following snippet:

theorem foo {α : Type} (c : α → α) (x : α) : c x = x := by
  let d := c
  let e := d
  change e x = x
  simp? [e]
  sorry

Expected behavior:
simp? [e] should suggest simp only [e]

Actual behavior:
simp? [e] suggests simp only [e, d], pulling in d while this is not used in the simp call

Another example of misbehavior (probably due to the same bug) is

theorem foo {α : Type} (c : α → α) (x : α) : c x = x := by
  let d := c
  change d x = x
  -- simp [d]
  have : x = x := by
    simp?
  sorry

where the simp? call unfolds to simp only, unless you uncomment simp [d] two lines above: then simp? unfolds to simp only [d].

Versions

Lean 4.16.0-nightly-2025-01-15

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for the report. So the issue is just™ that the simp argument set suggested by simp? is too large, but otherwise this works as expected? So the impact of this bug is on the low side, or am I missing something?

[sgouezel]

Yes, it's "just" that simp? is suggesting a simpset which is too large. It breaks proofs, though, by unfolding too much if you don't realize what is going on and fix the simpset. Not a deal breaker, but a minor inconvenience for expert users, and can be confusing for newcomers.

[nomeata]

Ah, I see: for a non-terminal simp this is more than just a small nuisance. Got it!

[MichaelStollBayreuth]

Here is another example; see #lean4 > simp? lists let variables unnecessarily @ 💬.

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]

[kmill]

PR #8753 appears to fix all the examples here, so I've set it to close this issue once it's merged.

There's still a lingering issue that will be harder to fix, which is that simp? can be conservative. The underlying problem is that the local declaration unfolding mechanism gets triggered from inside things like inferType and some parts of isDefEq when they set zetaDelta to true. (This is a why random local declarations were being included. #8753 is fixing the first example by just filtering the reported local declarations.)

It seems like we need some flag like trackZetaUnlessZetaDelta that simp could set, so that tracking can be turned off whenever isDefEq/whnf/inferType temporarily set zetaDelta to true, but there are some difficulties with caching (I think we'd have to clear the cache when crossing through withInferTypeConfig when trackZetaUnlessZetaDelta is true, otherwise we might miss some used local declarations!)