Lean hangs on simping on v4.9.0-rc1

Stream: lean4

[Siddharth Bhat]

Consider the MWE:

#eval Lean.versionString -- "4.9.0-rc1"

structure Note where
  pitch : UInt64
  start : Nat

def Note.containsNote (n1 n2 : Note) : Prop :=
  n1.start ≤ n2.start

def Note.lowerSemitone (n : Note) : Note :=
  { n with pitch := n.pitch - 1 }

theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    n.containsNote (Note.lowerSemitone n) := by
  simp [Note.containsNote]
  unfold Note.lowerSemitone
  /-
  n : Note
  ⊢ n.start ≤ { pitch := n.pitch - 1, start := n.start }.start
  -/
  -- simp (config := { etaStruct := .none }) -- uncomment line to see lean hang.

On uncommenting the last simp line, Lean hangs. Experiment at this live.lean-lang.org URL. It feels like a bug to me, since the file has nothing in it, but I'm wondering if I'm holding simp wrong somehow? Should I file this as an issue?

[Kyle Miller]

This is enough to hang simp:

theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    n.containsNote (Note.lowerSemitone n) := by
  simp [Note.containsNote, Note.lowerSemitone]

[Kyle Miller]

You can use dsimp as a workaround here:

theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    n.containsNote (Note.lowerSemitone n) := by
  unfold Note.containsNote Note.lowerSemitone
  dsimp
  simp

[Siddharth Bhat]

@Kyle Miller Thanks, though the actual scenario is more complex, so Is settled on the workaround:

theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    n.containsNote (Note.lowerSemitone n) := by
  simp [Note.containsNote]
  unfold Note.lowerSemitone
  simp only [le_refl, true_and]
  simp only [Note.lastPlayed, le_refl]

Am I right in assuming that this is in fact a bug I should file?

[Kyle Miller]

Should I file this as an issue?

Yeah, I think this is an issue that you should report. Unless you think etaStruct should be part of it, I'd suggest using my single-simp version in the report, since it shows it has nothing to do with interactions between simp, unfold, and the etaStruct setting.

[Siddharth Bhat]

Thanks!

[Siddharth Bhat]

A little more playing around suggests:

#eval Lean.versionString -- "4.9.0-nightly-2024-05-23"

structure Note where
  pitch : UInt64
  start : Nat

def Note.containsNote (n1 n2 : Note) : Prop :=
  n1.start ≤ n2.start

def Note.lowerSemitone (n : Note) : Note :=
  { n with pitch := n.pitch - 1 }

theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    n.containsNote (Note.lowerSemitone n) := by
  -- dsimp (config := { proj := false }) [Note.containsNote, Note.lowerSemitone] -- does not hang
  dsimp (config := { proj := true })[Note.containsNote, Note.lowerSemitone] -- hangs.

So it's something to do with projections?

[Siddharth Bhat]

OK, filed as https://github.com/leanprover/lean4/issues/4413