simp hang on simplifying: build a structure, followed by a projection

[bollu]

#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
  -- simp [Note.containsNote, Note.lowerSemitone] -- uncomment to see Lean hang
  sorry

• live lean-lang URL
• Zulip thread of report

[kmill]

@bollu also reported that dsimp can hang here:

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.

[llllvvuu]

bisection: this is broken back to 4.0.0

[llllvvuu]

It is due to unfolding UInt64 subtraction = Fin subtraction. Here is a minimization:

structure Note where
  pitch : UInt32
  start : Nat

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

set_option maxRecDepth 100 in
set_option maxHeartbeats 1000 in
theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    Nat.zero ≤ n.lowerSemitone.start := by
  dsimp (config := { proj := true }) only [Note.lowerSemitone]
  exact Nat.zero_le n.start

The elaboration completes and returns:

fun (n : Note) => id.{0} (LE.le.{0} Nat instLENat Nat.zero (Note.start (Note.lowerSemitone n))) (Nat.zero_le (Note.start n))

it seems to be the type checking which is slow, as it is unfolding Fin subtraction - 0 to + 65535 and then succ 65535 times.

Another variant:

structure Note where
  pitch : UInt64
  start : Nat

def lowerSemitone := fun (n : Note) => Note.mk (n.1 - 0) n.2
-- same issue:
-- def lowerSemitone := fun (n : Note) => Note.mk (n.1 + 100) n.2

set_option maxRecDepth 100 in
theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    0 ≤ (lowerSemitone n).start :=
  (Nat.zero_le (Note.start n))

This one never finishes elaborating.

But there is no issue if the def is inlined into the statement:

-- doesn't hang
theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    0 ≤ ((fun (n : Note) => Note.mk (n.1 - 0) n.2) n).start :=
  (Nat.zero_le (Note.start n))

-- also doesn't hang
theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
    let lowerSemitone := fun (n : Note) => Note.mk (n.1 - 0) n.2
    0 ≤ (lowerSemitone n).start :=
  (Nat.zero_le (Note.start n))