Lean4 Performance Issues on Windows 10

Stream: general

[Sean]

Hello! Recently I have been encountering performance issues with Lean4 on Windows 10. For example, even running simple tactics like rfl or introducing goals with have can sometimes take 2-3 minutes to complete. Has anybody else encountered similar issues?

For reference, my machine has an i7-10750H and 16GB of memory, so I don't think my specs are the cause of the issue.

[Kim Morrison]

Oh dear! Can you show an example?

[Sean]

Sure, for example, I have the following lemma:

abbrev IncreasingIntList (L : List Int) :=
  0 < L.length ∧ L[(0 : Int)]! = 0 ∧
  ∀ (i j : Int),
    0 ≤ i ∧ i < L.length →
    0 ≤ j ∧ j < L.length →
    i < j →
    L[i]! < L[j]!

lemma search_unify L (H : IncreasingIntList L) (j a a' N : Int)
  (hlast : L[L.length - 1] = N)
  (ha1 : 0 ≤ a ∧ a < L.length - 1) (ha2 : L[a] ≤ j ∧ j < L[a + 1])
  (ha1' : 0 ≤ a' ∧ a' < L.length - 1) (ha2' : L[a'] ≤ j ∧ j < L[a' + 1]) :
  val_int a = val_int a' := by
  simp
  cases eqn:(decide (a' + 1 ≤ a))
  all_goals move: eqn=> /== eqn
  { cases eqn':(decide (a + 1 ≤ a'))
    all_goals move: eqn'=> /== eqn'
    all_goals sorry
    -- { omega }
    -- have imp:(L[a + 1] ≤ L[a'] → a = a') := by sorry
  }
  sorry

There are some custom tactics used here, but the key issue is in the two commented lines. In the first commented line, I am using omega to prove the goal a = a' where the context contains two hypotheses a < a' + 1 and a' < a + 1. However, this call to omega takes a few minutes to complete. The second commented line with the have similarly takes a very long time to execute.

[Kim Morrison]

Can you minimize? e.g.see the context immediately before omega (perhaps use extract_goal if Mathlib is available)?

[Kim Morrison]

Getting down to something that only used Mathlib, or ideally not even that, is probably essential to help diagnose.

[Sean]

Yes - I also remembered that I am using a custom instance to allow for integer indexing of lists. I've removed this by changing the indices to natural numbers and the issue still seems to persist after extracting the goal:

abbrev IncreasingIntList' (L : List Int) :=
  0 < L.length ∧ L[0]! = 0 ∧
  ∀ (i j : Nat),
    0 ≤ i ∧ i < L.length →
    0 ≤ j ∧ j < L.length →
    i < j →
    L[i]! < L[j]!

theorem extracted_1 (L : List ℤ) (H : IncreasingIntList' L) (j a a' : ℕ) (N : ℤ)
  (hlast : L[L.length - 1] = N) (ha1 : 0 ≤ a ∧ a < ↑L.length - 1)
  (ha2 : L[a] ≤ j ∧ j < L[a + 1]) (ha1' : 0 ≤ a' ∧ a' < ↑L.length - 1)
  (ha2' : L[a'] ≤ j ∧ j < L[a' + 1]) (eqn : a < a' + 1) (eqn' : a' < a + 1) :
  a = a' := by
  -- omega
  -- have imp:(L[a + 1] ≤ L[a'] → a = a') := by sorry
  sorry

However, after removing all the hypotheses except for those necessary for the proof (i.e. eqn and eqn') there are no performance issues.

theorem extracted_2 (eqn : a < a' + 1) (eqn' : a' < a + 1) :
  a = a' := by
  omega

Does this mean that the issue has something to do with the context?

UPDATE: After further investigation, the issue seems to be with omega, specifically when called inside get_elem_tactic for the array accesses. It seems that the goals/proofs generated are too large for omega to handle quickly. The fact that replacing the array accesses to use getElem! (i.e. changing L[a] to L[a]!) eliminates the performance issue seems to confirm the above explanation.

[Notification Bot]

Sean has marked this topic as resolved.

[Kim Morrison]

@Sean, don't resolve too quickly! :-) This sort of example --- a situation occurring in the wild where omega in get_elem_tactic blows up --- is really interesting to us. It would be really great to have a standalone example showing this. It can help guide future performance work on omega.

[Sean]

After removing the unnecessary hypotheses, I have this example where the omega blowup occurs:

theorem omega_blowup (L : List ℤ) (ha1 : 0 ≤ a ∧ a < L.length - 1)
  (ha2 : L[a] ≤ j ∧ j < L[a + 1]) (ha1' : 0 ≤ a' ∧ a' < L.length - 1)
  (ha2' : L[a'] ≤ j ∧ j < L[a' + 1]) :
  L[a] < L[a' + 1] := by
  omega

The issue seems to be tied to the need to solve for the validity of indices a + 1 and a' + 1 using the assumptions ha1 and ha1'. For instance, if we adjust the statement to remove the obligation for the validity of a + 1, the runtime decreases significantly, though there is still a noticeable delay:

theorem less_blowup (L : List ℤ) (ha1 : 0 ≤ a ∧ a < L.length)
  (ha2 : L[a] ≤ j) (ha1' : 0 ≤ a' ∧ a' < L.length - 1)
  (ha2' : j < L[a' + 1]) :
  L[a] < L[a' + 1] := by
  omega

And further adjusting the statement to also no longer require a' + 1 to be a valid index gets rid of the delay completely:

theorem no_blowup (L : List ℤ) (ha1 : 0 ≤ a ∧ a < L.length)
  (ha2 : L[a] ≤ j) (ha1' : 0 ≤ a' ∧ a' < L.length)
  (ha2' : j < L[a']) :
  L[a] < L[a'] := by
  omega

Is there any other sort of diagnostic information that would be helpful here?

[Notification Bot]

Sean has marked this topic as unresolved.

[Kim Morrison]

That's great, thanks, I'll try to find time to have a look. This example is really small and simple, and omega should have no problem!

[Kim Morrison]

set_option trace.omega true in omega

is the basic first step for looking for problems.

[Kim Morrison]

@Sean, sorry for the slow reply on this one.

theorem omega_less_blowup (L : List Int) (ha1 : 0 ≤ a ∧ a + 1 < L.length)
  (ha2 : L[a] ≤ j ∧ j < L[a + 1]) (ha1' : 0 ≤ a' ∧ a' + 1 < L.length)
  (ha2' : L[a'] ≤ j ∧ j < L[a' + 1]) :
  L[a] < L[a' + 1] := by
  omega

which is mathematically equivalent to the original, is much faster (although still not instant!)

The different is that this one doesn't involve natural number subtraction, which inevitably requires case splitting.