Tips to avoid time-out?

Stream: general

[Congyan (Cruise) Song]

Hi, I am a new member here. I am working on a project with Lean 3 and my program time-out a lot (probably due to the heavy use of linarith). I am wondering if there is any general advice on how to speed up the program?

I am also curious about if there are ways to 1) forget some assumptions that are no longer useful for the rest of the proof 2) manually increase the maximum memory for Lean in VS code environment, so that I can avoid the time-out?

Thank you in advance for your help!

[Heather Macbeth]

Congyan (Cruise) Song said:

I am working on a project with Lean 3 and my program time-out a lot (probably due to the heavy use of linarith). I am wondering if there is any general advice on how to speed up the program?

Hi @Congyan (Cruise) Song. Often in a proof containing many assertions proved by linarith, it's possible to reorganize the proof so that there's just a single thing proved by a big linarith (combining many hypotheses). This is typically faster.

You can also write linarith only [h1, h2] for a linarith which you expect to use only the two hypotheses h1 and h2, again this is typically faster.

Congyan (Cruise) Song said:

I am also curious about if there are ways to 1) forget some assumptions that are no longer useful for the rest of the proof

Yes (and good idea!), look up the clear tactic.

[Heather Macbeth]

For example, here's a problem with a proof which naively follows what you'd write on paper; it has 3 uses of linarith and takes 0.61s.

import Mathlib.Tactic.Linarith

example {x y z w : ℤ}
    (h0 : 4 * x + 3 * y + 2 * z + w = 10)
    (h1 : 3 * x + 2 * y + z = 6)
    (h2 : 2 * x + y = 3)
    (hx : x = 1) :
    w = 1 := by
  have hy : y = 1 := by linarith
  have hz : z = 1 := by linarith
  linarith

[Heather Macbeth]

If you switch to linarith only everywhere it takes 0.47s:

example {x y z w : ℤ}
    (h0 : 4 * x + 3 * y + 2 * z + w = 10)
    (h1 : 3 * x + 2 * y + z = 6)
    (h2 : 2 * x + y = 3)
    (hx : x = 1) :
    w = 1 := by
  have hy : y = 1 := by linarith only [h2, hx]
  have hz : z = 1 := by linarith only [h1, hx, hy]
  linarith only [h0, hx, hy, hz]

[Heather Macbeth]

And if you switch to a more Lean-idiomatic style, forgetting what you'd write on paper and exploiting that linarith is a full decision procedure, it takes 0.32s:

example {x y z w : ℤ}
    (h0 : 4 * x + 3 * y + 2 * z + w = 10)
    (h1 : 3 * x + 2 * y + z = 6)
    (h2 : 2 * x + y = 3)
    (hx : x = 1) :
    w = 1 := by
  linarith

[Congyan (Cruise) Song]

Heather Macbeth said:

For example, here's a problem with a proof which naively follows what you'd write on paper; it has 3 uses of linarith and takes 0.61s.

import Mathlib.Tactic.Linarith

example {x y z w : ℤ}
    (h0 : 4 * x + 3 * y + 2 * z + w = 10)
    (h1 : 3 * x + 2 * y + z = 6)
    (h2 : 2 * x + y = 3)
    (hx : x = 1) :
    w = 1 := by
  have hy : y = 1 := by linarith
  have hz : z = 1 := by linarith
  linarith

Thank you for your detailed suggestions and examples! I will try to reorganize my proof this way.