13
$\begingroup$

I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I make any change in the proof it takes quite some time before the "Lean infoview" is updated - currently up to a minute for a proof of 100 lines).

So, I am wondering if there are any tricks to make Lean run faster? Specific tactics one should avoid/use? Or even some settings one can use during the proof finding stage?

Are there any specific writing styles that lead to faster checkable proofs? E.g., does it help to give Lean information explicitly that it could also figure out itself? (e.g. write rw add_comm a b instead of rw add_comm)

$\endgroup$
5
  • 3
    $\begingroup$ It might be helpful to give a MWE here. (But I guess this depends on if you want help for your specific proof or for an answer which covers general advice on writing fast proofs in Lean.) $\endgroup$
    – Jason Rute
    Commented Mar 17, 2022 at 21:24
  • 7
    $\begingroup$ Even without a MWE I would say a proof of 100 lines long probably needs splitting up into a sequence of lemmas. This way lean won't recheck the whole thing all the time. It also provides a clearer compartmentalization which hypotheses are necessary for each part of the proof. There probably are 100 line lean proofs out there but they are the exception not the norm. $\endgroup$ Commented Mar 17, 2022 at 21:29
  • 9
    $\begingroup$ On the other hand it should be stressed that "number of lines of code" often does not correspond at all to "time taken to elaborate". I have seen 5 line proofs which take a very long time to elaborate and 50 line proofs which evaluate instantly. The issue is that different Lean tactics have different time costs. Are you using finish a lot? tidy? omega? Those are your problems, not the length of your code. 1 minute is completely unacceptable but there is usually a good reason. Like Jason I'd urge you to post a minimal working example. $\endgroup$ Commented Mar 17, 2022 at 22:08
  • 4
    $\begingroup$ The leanprover-community.github.io/tips_and_tricks.html page has some suggestions. $\endgroup$
    – Ricky
    Commented Mar 18, 2022 at 12:37
  • $\begingroup$ FYI for those questioning the addition of the tag high-performance-computing. I checked the edit queue history and the OP of the question GraffL approved of the change. (ref) So end of discussion! $\endgroup$
    – Guy Coder
    Commented Mar 29, 2022 at 12:12

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.