Slow interaction

Stream: lean4

[Joachim Breitner]

Sorry for the vague question, but maybe there are obvious remidies to try: lean in vscode is getting slower and slower as I progress with my proof, that it is almost not interactive anymore. I have 550 lines, the current lemma is 80 lines, so not huge. Any quick ideas?

[Ruben Van de Velde]

80 lines in a proof is quite a lot already

[Henrik Böving]

use save while interactively writing it. Generally speaking Lean is (right now) not as smart as Coq about proof editing and will re-elaborate all of your proof script every time that it is edited, you can however manually instruct it to create checkpoints in your proof. It will then only re-elaborate stuff after those checkpoints.

So for example I can go

  tac1
  tac2
  tac3
  tac4
  save
  tac5
  <edit>

now it will only ree-lab tac5 + the stuff you added

[Joachim Breitner]

Thanks! Although even with save based on the colour flashes it re-processes more than it ought. Maybe it’s just normal and I’m spoiled, and I should write smaller lemmas :-)

[Henrik Böving]

The colour flashes are not telling the truth in this case. It says that it is re-relaborating the whole section of your file, which is correct, but save should cache the part above so it should go through faster regardless.

[Henrik Böving]

You can measure with a stopwatch if it actually works I guess :D

[Kevin Buzzard]

80 lines is really long. Open a random mathlib file and I bet that no proof in it is anywhere near that long.

[Joachim Breitner]

It’s only one page in the paper I’m mechanizing :-)

[Kevin Buzzard]

That doesn't mean it has to be one proof!

[Joachim Breitner]

True… but at least during initial development I’d prefer to be able to just plow ahead, without having to break it up just because it overwhealms lean. (I may be slightly spoiled by other tools here, and have somewhat unreasonable first expectations)

[Kevin Buzzard]

This might just be the price you pay for using a more complex type theory. Doesn't AFP compile in like 10 seconds or something? And Mathlib is half the size but takes 6 hours.

[Joachim Breitner]

Nah, AFP certainly takes a long time, too. And I’m not sure if type theory is to be blamed here; maybe I am just too optimistic about how much processing lean can re-use as I edit in leafs in a structured proofs.

[Kevin Buzzard]

I would be interested to know if the save thing actually makes your life any better. I hadn't realised that it was working, I just remember people talking about it.

[Joachim Breitner]

(I hope zulip will collapse this message, lest I be more impolite than I intend to)…
So I shouldn’t be expecting that I can write my proofs like this then ;-)

lemma lemma1
  p (hp1 : phi_le p) (hp2 : p < 1) :
  ∀ n, v p (n+1) + 1 ≤ v p (n+2)
       ∧ v p (n+2) < (n+2) - ((1-p)/p)^(n+3) := by
  intro n
  rw [phi_le] at hp1
  have hp3 : 1 < 2 * p := by nlinarith
  induction n using Nat.case_strong_induction_on
  case hz =>
    norm_num
    constructor
    . rw [ v_2 _ (le_of_lt hp2) ]
      nlinarith
    . apply lt_of_mul_lt_mul_right _ (by nlinarith : 0 ≤ p^3)
      rw [ v_2 _ (le_of_lt hp2), sub_mul, sub_mul, div_mul_cancel ]
      case h => nlinarith
      apply lt_of_sub_neg
      rw [(by nlinarith :
        3 * p * p ^ 3 - p ^ 3 * p ^ 3 - (2 * p^3 - (1 - p) ^ 3)
        = - (p-1)^2 * (p^4 + 2*p^3 + p -1 )) ]
      apply mul_neg_of_neg_of_pos
      . nlinarith
      . have : 1 < 2 * p := by nlinarith
        calc
          p ^ 4 + 2 * p ^ 3 + p - 1 ≥ 2 * p ^ 3 + p - 1 := by nlinarith
          _ > p ^ 2 + p - 1 := by nlinarith
          _ ≥ 0 := by nlinarith
  case hi n IH =>
    simp only [<- add_one, add_assoc, cast_add]
    norm_num
    rewrite [(?eq :
      v p (n + 3) = v p (n + 2) + 1 + p^(n+3) * (n+2 - v p (n+2)) - (1-p)^(n+3))]
    case eq =>
      trans
      . apply v_eq_v_simp p (by nlinarith) hp2
        . intro i hi1 hi2
          unfold pointless
          have : i - 1 ≤ n := by nat_intervals
          replace IH : _ := (IH (i - 1) this).1
          rw [(by cases i; simp at hi1; simp : i - 1 + 1 = i)] at IH
          rw [(by cases i; simp at hi1; simp : i - 1 + 2 = i + 1)] at IH
          exact IH
      . unfold v_simp
        rw [if_neg]; case hnc => linarith
        rw [max_eq_left]
        . simp; left; linarith
        . simp_rw [cast_add]
          have : v p (1 + (n + 1)) ≥ v p 1 + (n + 1 : ℕ) := by
            apply iter_fast_growth_add _ 1 (n+2)
            . intro i hi1 hi2
              have : i - 1 ≤ n := by nat_intervals
              replace IH : _ := (IH (i - 1) this).1
              rw [(by cases i; simp at hi1; simp : i - 1 + 1 = i)] at IH
              rw [(by cases i; simp at hi1; simp : i - 1 + 2 = i + 1)] at IH
              exact IH
            . exact (le_refl _)
            . linarith
          simp [cast_add] at this
          rw [cast_ofNat]
          rw [(by linarith : 1 + (n + 1) = n + 2)] at this
          rw [(by linarith : ↑n + 3 - 2 + p = p + (n + 1))]
          simp [this]

    specialize IH n (le_refl _)
    cases' IH  with IH1 IH2
    constructor
    case left =>
      suffices : (1 - p) ^ (n + 3) ≤ p ^ (n + 3) * (↑n + 2 - v p (n + 2))
      linarith
      rw [ ← mul_inv_le_iff, ← div_eq_mul_inv, ← div_pow ]
      linarith
      cases hp1; positivity
    case right =>
      calc
        v p (n + 2) + 1 + p ^ (n + 3) * (↑n + 2 - v p (n + 2)) - (1 - p) ^ (n + 3)
          = (1 - p^(n+3)) * v p (n + 2) + 1 + p ^ (n + 3) * (↑n + 2) - (1 - p) ^ (n + 3) := by
          ring
        _ < (1 - p^(n+3)) * (↑n + 2 - ((1 - p) / p) ^ (n + 3)) + 1 + p ^ (n + 3) * (↑n + 2) - (1 - p) ^ (n + 3) := by
          -- congr_rel!
          apply sub_lt_sub_right
          apply add_lt_add_right
          apply add_lt_add_right
          apply mul_lt_mul_of_pos_left
          . exact IH2
          . apply lt_sub_right_of_add_lt
            rw [zero_add]
            apply pow_lt_one
            . linarith
            . exact hp2
            . simp
        _ = ↑n + 3 - ((1 - p) / p) ^ (n + 3) := by
          simp_rw [mul_add, mul_sub, sub_mul, one_mul, ← mul_pow]
          rw [mul_div_cancel']
          ring
          linarith
        _ ≤ ↑n + 3 - ((1 - p) / p) ^ (n + 4) := by
          -- congr_rel
          apply sub_le_sub_left
          rw [ _root_.pow_succ ]
          apply mul_le_of_le_one_left
          . apply pow_nonneg
            apply div_nonneg
            linarith
            linarith
          . rw [ div_le_iff ]
            linarith
            linarith
        _ = ↑n + 3 - (1 - p) ^ (n + 4) / p ^ (n + 4) := by
          rw [ div_pow ]

[Joachim Breitner]

It didn't noticably help here. When I was at the bottom of that proof, even with save I was tempted to switch to zulip and chat while waiting for the next apply to be processed, or the next tooltip to appear.

[Kevin Buzzard]

linarith and nlinarith might be quite costly tactics (esp nlinarith, at least in Lean 3). As is ring if you don't use it as a finishing tactic. I have no idea about the concept of compiling tactics but I thought that one of the perks of Lean 4 was that you were supposed to be able to compile tactics. Question which indicates that I have no understanding of what's going on: is nlinarith a compiled tactic? If not, what happens if you compile it (if that is indeed possible)?

[Henrik Böving]

Tactics in Isabelle too can be compiled that's not really a unique advantage of Lean. The compile tactics things can be enable with the precompiledModules flag in lake although I do remember I think it might have been Sebastian or Gabriel mentioning that the performance impact was not that crazy.

[Joachim Breitner]

My feeling is that it is less about tactics being slow, but rather that they are more often re-run than needed, i.e. not robust enough incremental editing.
It seems that an empty . to structure the proofs throws the parser off a bit (or something like that), the next character fixes that, but by then lean has thrown away all the work it did on the lines above.

[Damiano Testa]

For me, the most effective way of speeding up proofs while I'm writing them is to sorry out as much as I can, put #exit after the proof and . before it (the dot might be a Lean3 thing, I do not remember).

[Kevin Buzzard]

Yeah in Lean 3 if you really wanted to write a long proof then the trick was to get a costly part of it compiling and then sorry it out, and only unsorry at the very end. I was hoping that save would save us from having to do this.

[Eric Wieser]

Do we have an easy way to sorry things out?

[Eric Wieser]

In lean3 you could replace { with sorry {

[Eric Wieser]

I don't know how to do that with \.

[Mario Carneiro]

stop is the lean 4 spelling of sorry {

[Kevin Buzzard]

@Joachim Breitner do save and stop together solve your problems? It would be great to actually have a way of writing 80 line proofs. I kind of like the idea that in general there is a policy of "lots of small proofs, not one big proof", but perhaps that policy is partly driven by the issue which you have discovered, namely that right now "one big proof" is very inconvenient to work with. As you observe, there is not obviously a reason why this should be the case; why should we be recompiling all of a long and possibly inefficient (if we're experimenting) proof every time someone presses a button?

[Joachim Breitner]

Putting stop in various other branches of the proof certainly helps (from 7 second to 1.5 seconds until lean tells me after adding one letter that linarithx isn’t a tactic). So thanks, I’ll keep that in mind!
(save doesn’t seem to be needed and doesn't seem to do much in my simple experiments.)