simp? adding let reduction

Stream: mathlib4

[Sébastien Gouëzel]

In the following example

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

the line simp [e] changes to d x = x, i.e., it does not reduce d, which is perfect. But simp? [e] suggests simp only [e, d], pulling d into the simpset for no reason. Is that a known behavior?

[Kyle Miller]

That's odd. The diagnostics show that only e was used, so I'm not sure how d is being included in the simp only syntax.

[Sébastien Gouëzel]

In previous Lean versions, simp was reducing lets by default. Maybe the behavior has been changed for simp, but not perfectly cleaned up for simp? ?

[Sébastien Gouëzel]

Something really weird is going on here. In

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

the simp? reduces to simp only, but if you uncomment the line simp [d] then the simp? reduced to simp only [d].

[Bhavik Mehta]

I've observed this too, and I also find it confusing behaviour - my example was similar to your original one

[Kyle Miller]

I was reading through the simp? code, and it looks like it does exactly what simp does. It'd be worth double checking, but it seems like the bug could be in how the simp only syntax is generated.

[Sébastien Gouëzel]

Reported at lean4#6655.