simp_all? omits unfolded let hypotheses

[JLimperg]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

simp_all? does not mention unfolded let hypotheses in the generated simp_all only call:

example {P : Nat → Prop} : let x := 0; P x := by
  intro x
  simp_all? [x] -- Try this: simp_all only

example {P : Nat → Prop} : let x := 0; P x := by
  intro x
  simp_all only -- simp_all made no progress

The buggy code is here.

Context

Similar to #3501.

Versions

nightly 2024-02-27

Impact

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

[leodemoura]

Fixed by commit above. It has been squashed.

[m4lvin]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp_all.3F.20.E2.89.A0.20simp_all.20and.20an.20old.20bug.3F/near/476414205

This bug seems to be back since 4.12, so this should be reopened?

Note: the test case added by the above commit uses simp and not simp_all. Could that be why the bug is not caught by the CI tests?

[nomeata]

Note: the test case added by the above commit uses simp and not simp_all. Could that be why the bug is not caught by the CI tests?

Ah, I was just thoroughly confused by that as well. Yes, then the bug is not fully fixed, I’ll reopen.