Abysmal performance when doing large inductions

Stream: lean4

[Jad Ghalayini]

So when I'm trying to do a large induction with e.g. 30 cases; I get really really bad performance, especially if I have a large automated branch at the end handling say 25 of the cases: every time I modify one of the upper 5 cases, I need to wait for 2 minutes before the infoview updates and I can think about what to write next. Would it be possible to somehow cache work so this is not the case (the cases of the induction should be completely independent of each other no?)

[Leonardo de Moura]

We have a new checkpoint tactic. It is an experimental stage right now, but it was added for this kind of scenario.
Could you try the following?

checkpoint induction n <;> try (<tactic that takes care of the 25 cases>)
case <remainin-case-1> => ...
...
case <remainin-case-5> => ...

Here is an example

constant f : Nat → Nat
@[simp] axiom f_eq_1 (n : Nat) : f (n+1) = f n
@[simp] axiom f_eq_2 : f 0 = 1

inductive Foo where
  | c1 | c2 | c3 | c4 | c5 | c6 | c7

def h (n : Nat) := 1

def g (n : Foo) (x : Nat) : Nat :=
  match n with
  | .c7 => h x
  | _   => f 1000

set_option maxRecDepth 100000

example : g n x = 1 := by
  checkpoint induction n <;> try simp [g]
  case c7 =>
   simp [h]

[Leonardo de Moura]

Another trick is to temporarily use the stop tactic to disable parts of your proof.
We could also write the example above as

example : g n x = 1 := by
  induction n with
  | c7 => /- we can now comfortably work on this branch without delay -/ done
  | _ => stop simp [g] /- stop disabled the else branch. -/

[Leonardo de Moura]

@Mario Carneiro suggested other tricks in the following thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Partial.20evaluation.20of.20a.20file

[Mario Carneiro]

the stop tactic is called sorry { ... } in current lean 3

[Leonardo de Moura]

We have added the save tactic yesterday. It is often more convenient to use than checkpoint.
See https://github.com/leanprover/lean4/blob/master/RELEASES.md for additional details.

[Leonardo de Moura]

Example:

macro "expensive_tactic" : tactic => `(sleep 5000) -- sleeps for 5 seconds

example (h₁ : x = y) (h₂ : y = z) : z = x := by
  expensive_tactic
  save
  -- We can comfortably  make changes after the `save`
  -- and get quick feedback from the editor.
  have : y = x := h₁.symm
  have : z = y := h₂.symm
  trace "hello world"
  apply this.trans
  exact ‹y = x›

[Jad Ghalayini]

Would it be possible to automatically detect that branches of an induction are independent , rather than depending on a certain order? For example, the expensive tactic which solves the 25 cases is in the last branch.

[Jad Ghalayini]

Or are they not actually independent in the case of induction ... generalizing ... with | ...

[Jad Ghalayini]

On a related note, why is simp on anything defined via a large match expression so slow?

[Jad Ghalayini]

My proofs all become super slow whenever I do simp only [big_match] for an expression like big_match (constructor_14 a) (constructor_3 b)

[Jad Ghalayini]

Even though as far as I can tell it should be fast as it's just a simple rewrite; and similar rewrites using theorems are very fast

[Jad Ghalayini]

Should I prove a theorem for each case of the match?

[Jad Ghalayini]

Seems hard to automate, and harder to put into simp in the case of the automated cases

[Jad Ghalayini]

Is there a better way to do such "obvious" reductions?

[Leonardo de Moura]

Jad Ghalayini said:

On a related note, why is simp on anything defined via a large match expression so slow?

It is hard to tell without seeing the actual example, but I suspect the problem is not simp, but the generation of equality theorems for the match expression. I have seen some massive proofs when the match expression has many overlapping patterns.
Lean 4 generates these theorems on demand when they are first needed.

[Leonardo de Moura]

Jad Ghalayini said:

My proofs all become super slow whenever I do simp only [big_match] for an expression like big_match (constructor_14 a) (constructor_3 b)

If you copy and paste the theorem as an example after the theorem is the example also slow?

[Leonardo de Moura]

Jad Ghalayini said:

Should I prove a theorem for each case of the match?

You should not need to. Have you tried the new save and stop tactics?

[Leonardo de Moura]

Jad Ghalayini said:

Is there a better way to do such "obvious" reductions?

If the reductions are definitional, then we can add an option that skips the match equality theorem generation and relies only on definitional reduction for match expressions.

[Leonardo de Moura]

Jad Ghalayini said:

Would it be possible to automatically detect that branches of an induction are independent , rather than depending on a certain order? For example, the expensive tactic which solves the 25 cases is in the last branch.

It is not clear to me what you are asking and/or proposing.

[Jad Ghalayini]

Leonardo de Moura said:

Jad Ghalayini said:

My proofs all become super slow whenever I do simp only [big_match] for an expression like big_match (constructor_14 a) (constructor_3 b)

If you copy and paste the theorem as an example after the theorem is the example also slow?

No it's actually instant. I even made sure it wasn't parallelism by commenting it out, letting everything run, and then uncommenting it

[Jad Ghalayini]

Leonardo de Moura said:

Jad Ghalayini said:

Should I prove a theorem for each case of the match?

You should not need to. Have you tried the new save and stop tactics?

These don't seem to be working for me; editing below a save still causes the whole thing to start again for some reason and takes forever (even when there's nothing or very little under the save, and when replacing other tactics with stop does seem to speed things up)

[Jad Ghalayini]

Leonardo de Moura said:

Jad Ghalayini said:

Would it be possible to automatically detect that branches of an induction are independent , rather than depending on a certain order? For example, the expensive tactic which solves the 25 cases is in the last branch.

It is not clear to me what you are asking and/or proposing.

Well as far as I understand, say we do

induction H with
| label1 => ...
| label2 => ...
| label3 => ...

As far as I understand, those branches are totally independent, so why not save them individually as checkpoints so editing one branch does not affect the others?

[Jad Ghalayini]

Leonardo de Moura said:

Jad Ghalayini said:

On a related note, why is simp on anything defined via a large match expression so slow?

It is hard to tell without seeing the actual example, but I suspect the problem is not simp, but the generation of equality theorems for the match expression. I have seen some massive proofs when the match expression has many overlapping patterns.
Lean 4 generates these theorems on demand when they are first needed.

This is weird because I have a lot of thoerems using simp to handle the same match statemement, and they're all very very slow. Like it's not just one slow one. But, as I said, copying the exact same theorem was indeed fast.

[Jad Ghalayini]

Thanks so much for your help btw, I really appreciate the responsiveness!

[Jad Ghalayini]

Also btw I've managed to get by a little using the reduce tactic before rewriting, but apparently that's for debugging purposes only. Much faster, though...

[Jad Ghalayini]

Since I am basically using simp to do reduction; is there a better way to do this?

[Henrik Böving]

maybe dsimp ? It performs simp using definitional equality only

[Leonardo de Moura]

These don't seem to be working for me; editing below a save still causes the whole thing to start again for some reason and takes forever (even when there's nothing or very little under the save)

This is the expected behavior. There is no cache yet when you are typing save, and the whole tactic will be executed from the beginning. Our plan is to add in the future an option set_option tactic.cache true that will introduce save automatically for us for potentially expensive tactics such as simp. We also want to allow the user to register their own tactics as "expensive".

As far as I understand, those branches are totally independent, so why not save them individually as checkpoints so editing one branch does not affect the others?

It is not that simple. As you are typing in one of the branches, you are introducing syntax errors. The syntax errors temporarily disable branches. Try the following

inductive Foo where
  | c1 | c2 | c3

example (x : Foo) : True := by
  induction x with
  | c1 => case -- You are tying here
  | c2 => simp -- Note that `simp` is not highlighted because it was not even parsed, let alone elaborated
--^ parsing error here
  | c3 => simp

EDIT: this is not the only obstacle, but it is the simplest to explain.

This is weird because I have a lot of thoerems using simp to handle the same match statemement, and they're all very very slow. Like it's not just one slow one. But, as I said, copying the exact same theorem was indeed fast.

We may have a bug in our cache, and may be recomputing things. A #mwe would help us a lot.

Also btw I've managed to get by a little using the reduce tactic before rewriting, but apparently that's for debugging purposes only. Much faster, though...

It makes sense. reduce performs only definitional reductions and will never try to generate equation theorems for a match expression.

[Leonardo de Moura]

Jad Ghalayini said:

Since I am basically using simp to do reduction; is there a better way to do this?

simp is the way to go. We should work together to fix the performance problem and avoid unnecessary workarounds.

[Jad Ghalayini]

@Leonardo de Moura sounds good! I can get started on an MWE probably tonight; that said, do you know when a definitional-match-only simp could be available, as it's getting to the point where it's stalling all my progress as theorems just become unworkable?

[Leonardo de Moura]

Yes, we have support for definitional and non-definitional match simplifications. simp by default tries both. I am hopeful we will be able to fix the performance issue. If it cannot be fixed, we can add a flag to simp to disable non-definitional match simplifications.

[Jad Ghalayini]

Would it be possible to add the flag now as a stopgap so I can get on with my proofs haha?

[Jad Ghalayini]

Or is there some kind of dsimp-like tactic I can use?

[Leonardo de Moura]

I will add a dsimp-like tactic.

[Leonardo de Moura]

We have dsimp and dsimp! tactics in the nightly build https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-04-24

[Jad Ghalayini]

Unfortunately, even using dsimp, it's still about the same speed

[Jad Ghalayini]

The test program,

import LeanExperiments.Dependencies

set_option maxHeartbeats 1000000

theorem Term.stlc_wknth_true {t: Term} {Γ: Sparsity} {n: Nat}
: (t.wknth n).stlc (Γ.wknth n true) = (t.stlc Γ).wknth (Γ.ix n)
:= by {
  revert Γ n;
  induction t with
  | var v =>
    intro Γ n;
    dsimp only [wknth, wk]
    repeat rw [stlc_var]
    dsimp only [Sparsity.stlc]
    split
    . have H: Γ.dep v = true := by
        rw [<-Sparsity.wknth_dep]
        assumption
      rw [Sparsity.wknth_ix_true' H]
      rw [if_pos H]
      dsimp only [Stlc.wknth, Stlc.wk]
      simp only [Wk.wknth_var]
    . rw [if_neg]
      rfl
      simp only [Sparsity.wknth_dep] at *
      assumption
  | _ =>
    intro Γ n;
    dsimp only [wknth, wk]
    repeat rw [Wk.lift_wknth_merge]
    repeat rw [Wk.liftn_wknth_merge]
    repeat rw [<-wknth_def]
    try (rename TermKind _ => k; cases k);
    try (rename AnnotSort => s; cases s);
    all_goals try rfl;
    all_goals (
      dsimp only [stlc]
      simp only [Sparsity.wknth_merge]
      simp only [*]
      repeat rw [Term.stlc_ty_wknth]
      try rfl
    )
}

still takes 29 seconds to typecheck; and even simply just writing dsimp [stlc] takes a few seconds each time

[Jad Ghalayini]

Now this match isn't that huge, only about 20 branches, so I'm confused

[Jad Ghalayini]

I can probably work towards an MWE tomorrow, but any idea what gives?

[Jad Ghalayini]

This does seem to be quite simp-specific since rw and reduce are both so fast I can't even tell I'm waiting for anything

[Leonardo de Moura]

The split tactic will (indirectly) generate the equality theorems for the match-expression.

[Jad Ghalayini]

On the other hand intuition tells me this kind of simple unfolding should be faster than reduce, so why isn't it?

[Jad Ghalayini]

@Leonardo de Moura ah but even my other programs without split are still slow

[Jad Ghalayini]

Lemme give another example

[Leonardo de Moura]

Jad Ghalayini said:

On the other hand intuition tells me this kind of simple unfolding should be faster than reduce, so why isn't it?

We need a #mwe to be able to answer this question.

[Jad Ghalayini]

Makes sense will get to it

[Leonardo de Moura]

Thanks.

[Jad Ghalayini]

Np, sorry for putting it off, just had a hectic week, barely time to even work on the proofs themselves haha!

[Jad Ghalayini]

Thanks for all the support, really appreciate it!

[Jad Ghalayini]

Actually decided to stop procrastinating and made an MWE

[Jad Ghalayini]

@Leonardo de Moura the program

inductive Level1: Type
| one
| two
| three
| four
| five
| six
| seven
| eight
| nine
| ten

inductive Level2: Type
| emp
| yi (l: Level1) (e: Level2)
| er (l: Level1) (e: Level2)
| san (l: Level1) (e: Level2)
| si (l: Level1) (e: Level2)
| wu (l: Level1) (e: Level2)
| liu (l: Level1) (e: Level2)
| qi (l: Level1) (e: Level2)
| ba (l: Level1) (e: Level2)
| jiu (l: Level1) (e: Level2)
| shi (l: Level1) (e: Level2)

open Level1
open Level2

def Level1.make_sentence: List Level1 -> Level2
| [] => emp
| one::xs => yi one (make_sentence xs)
| two::xs => er two (make_sentence xs)
| three::xs => san three (make_sentence xs)
| four::xs => si four (make_sentence xs)
| five::xs => wu five (make_sentence xs)
| six::xs => liu six (make_sentence xs)
| seven::xs => qi seven (make_sentence xs)
| eight::xs => ba eight (make_sentence xs)
| nine::xs => jiu nine (make_sentence xs)
| ten::xs => shi ten (make_sentence xs)

def Level2.is_translation: Level2 -> Bool
| yi one e => e.is_translation
| er two e => e.is_translation
| san three e => e.is_translation
| si four e => e.is_translation
| wu five e => e.is_translation
| liu six e => e.is_translation
| qi seven e => e.is_translation
| ba eight e => e.is_translation
| jiu nine e => e.is_translation
| shi ten e => e.is_translation
| emp => true
| _ => false


def Level1.sentence_is_translation' {l: List Level1}:
  (make_sentence l).is_translation = true
:= by {
  induction l with
  | nil => rfl
  | cons l xs I =>
    cases l <;>
    conv =>
      lhs
      reduce
      rw [I]
}

def Level1.sentence_is_translation {l: List Level1}:
  (make_sentence l).is_translation = true
:= by {
  induction l with
  | nil => rfl
  | cons l xs I =>
    cases l <;>
    dsimp only [make_sentence, is_translation] <;>
    exact I
}

[Jad Ghalayini]

Could probably be made slightly smaller but illustrates the point

[Jad Ghalayini]

sentence_is_translation' typechecks instantaneously

[Jad Ghalayini]

sentence_is_translation takes a couple of seconds

[Leonardo de Moura]

Thanks for creating the #mwe. I will work on it.

[Leonardo de Moura]

Pushed the following fix: https://github.com/leanprover/lean4/commit/3cf642688bcf12356292590822a8a372fbe04630
Level1.sentence_is_translation should be very fast now.
The bottle neck is the equation theorem generation as we suspected. I will try to improve it tomorrow.

[Jad Ghalayini]

@Leonardo de Moura works great now, thanks!

[Jad Ghalayini]

Any chance we could get dsimp support in conv though?