Performance issue

Stream: lean4

[Sven Manthe]

While analyzing performance issues appearing throughout the later parts of my project, I found the following example of unexpected seemingly exponential running time (@Floris van Doorn helped me and suggested to report it). Essentially, adding copies a unused parameter or let declaration causes exponential running time of even exact sorry.

def help (A : Type) : ([] : List A).length % 1 = 0 → Prop := fun _ ↦ True
set_option profiler true

--the running time of "exact sorry" seems exponential in the number of h1
theorem slow {A : Type} (p : Bool)
  (h : ∀ (hp : ([] : List A).length % 1 = 0), help A hp → help A hp)
  (h1 : help A (by cases p <;> omega))
  (h1 : help A (by cases p <;> omega))
  (h1 : help A (by cases p <;> omega))
  (h1 : help A (by cases p <;> omega))
  (h1 : help A (by cases p <;> omega))
  -- (h1 : help A (by cases p <;> omega))
  -- (h1 : help A (by cases p <;> omega))
  (hp : ([] : List A).length % 1 = 0) : help A hp := by
  refine h (by cases p <;> omega) ?_
  exact sorry
--the issue disappers after removing some of the "cases p",
--or replacing "omega" by "simp"
--or replacing A by ℕ
--or replacing "exact sorry" by "exact trivial"

A variant crashing the VS Code infoview is

def help (A : Type) : ([] : List A).length % 1 = 0 → Prop := fun _ ↦ True
set_option profiler true
set_option diagnostics true

example (A : Type) (p : Bool) : ([] : List A).length % 1 = 0 := by
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  -- let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  -- let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  -- let h1 : ([] : List A).length % 1 = 0 := by cases p <;> omega
  omega

[Kim Morrison]

Could you please report this as an issue on the lean4 repository?

[Sven Manthe]

https://github.com/leanprover/lean4/issues/5108

[Sven Manthe]

A question about workarounds for my project: Is there a way to replace a term by an opaque term of the same type without creating a new def? Since replacing let by have fixes the issue, making these proof terms opaque should resolve the issues (and the minor disadvantages are not relevant to me), but I do not know how to do this with terms provided inside a parameter as in the first example