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.

Note this issue may be related to #2281, I am not sure.

Description

simp (config :={zeta := false}) sometimes unfold let values.

Context

This is a regression compared to Lean 3 that complicates porting the sphere eversion project for instance. It was discussed on Zulip.

Steps to Reproduce

def f : Nat → Nat := fun x ↦ x - x

@[simp]
theorem f_zero (n : Nat) : f n = 0 := Nat.sub_self n

example (n : Nat) : False := by
  let g := f n
  have : g + n = n := by 
    simp (config := {zeta := false}) [Nat.zero_add]
  sorry

Expected behavior:

The simp should fail. In Lean 3 the dsimp line below is needed.

-- Lean 3 code
def f : nat → nat := fun x, x - x

@[simp]
lemma f_zero (n : ℕ) : f n = 0 := nat.sub_self n

example (n : nat) : false :=
begin
  let g := f n,
  have : g + n = n,
  { -- dsimp only [g],
    simp [nat.zero_add] },
  sorry
end

Actual behavior:

Lean 4 happily closes the goal. Of course in my example this looks like a feature, but in actual examples it prevents simp from closing the goal, by sending it to a dead end.

Versions

Lean (version 4.2.0-rc1, commit a62d2fd, Release)
Ubuntu 22.04

Impact

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