get_elem_tactic timeout from similar hyps

Stream: lean4

[James Gallicchio]

I have an unusual proof where I accumulate facts about getElem on a few vectors. But then, when I try to state another fact with more getElems, I end up timing out get_elem_tactic because trivial tries to unify hypotheses that will fail to unify.
image.png
I will try to make a minimal reproduction tomorrow.

[James Gallicchio]

The statement that triggers this timeout is

  -- then, b/c c7 and c11 are adjacent, either c7_3 = c3_3 or c11_2 = c3_2
  have : (tc.kclique.get 7)[3] = (tc.kclique.get 3)[3] ∨
        (tc.kclique.get 11)[2] = (tc.kclique.get 3)[2] := sorry

where the context is

n s : ℕ
tc : TwoCubes (n + 3) s
c3_3 : (tc.kclique.get 3)[3] ≠ 0
c3_2 : (tc.kclique.get 3)[2] ≠ 0
c7_0 : (tc.kclique.get 7)[0] = 0
c7_1 : (tc.kclique.get 7)[1] = 1
c7_2 : (tc.kclique.get 7)[2] = (tc.kclique.get 3)[2]
c11_0 : (tc.kclique.get 11)[0] = 0
c11_1 : (tc.kclique.get 11)[1] = 1
c11_3 : (tc.kclique.get 11)[3] = (tc.kclique.get 3)[3]
⊢ ...

[James Gallicchio]

tc.kclique.get : BitVec (n+5) -> Vector (Fin _) (n+5), so there are interesting casts happening for all of those numerals, which I suspect may be contributing to how slow it is.

[James Gallicchio]

actually, found a quick repro! this takes 3 seconds to elaborate on my machine :sweat_smile:

set_option trace.profiler true in
example (f : BitVec (n+5) -> Vector (Fin (s+2)) (n+5)) : False :=
  have : (f 7)[0] = 0 := sorry
  have : (f 7)[1] ≠ 0 := sorry
  have : (f 7)[2] = (f 3)[2] := sorry
  have : (f 11)[0] = 0 := sorry
  have : (f 11)[1] ≠ 0 := sorry
  have : (f 11)[2] = (f 3)[2] := sorry
  have : (f 7)[3] = (f 3)[3] ∨
        (f 11)[2] = (f 3)[2] := sorry
  sorry

[Jovan Gerbscheid]

The reason is that Lean tries to figure out what the numbers 7 and 11 are modulo 2 ^ (n + 5), by unfolding them. To stop lean from doing this, you can write something like seal BitVec.ofNat before the definition.

[Jovan Gerbscheid]

This unification takes exponential time as you increase the 5:

set_option trace.profiler true in
example : (1 : BitVec (n + 5)) = (0 : BitVec (n + 5)) := rfl

[James Gallicchio]

seal BitVec.ofNat improves the elaboration time by about 50%, but it is still quite slow (2s to compile 10 lines on a new machine). How can I further debug this?

[James Gallicchio]

(note that adding explicit proof terms to each getElem completely sidesteps the slow elaboration, since it is triggered by getElem's proof obligation machinery)

[Jovan Gerbscheid]

The example you posted is only 0.2 seconds on the lean web when using seal BitVec.ofNat

[James Gallicchio]

oh dear, the difference seems to be whether mathlib is imported

[James Gallicchio]

	not sealed	sealed
mathlib	2.46	0.68
core	1.89	0.10

[James Gallicchio]

so I guess the .5 seconds is just the overhead of mathlib bigness, and the other 1.8 seconds is avoided by sealing

[James Gallicchio]

wait. Importing all of mathlib is significantly faster than a minimized import set. huh? this takes 2.4 seconds on lean web:

import Mathlib.Algebra.Order.Group.Defs
import Mathlib.Data.Fintype.Card

seal BitVec.ofNat
set_option trace.profiler true in
example (f : BitVec (n+5) -> Vector (Fin (s+2)) (n+5)) : False :=
  have : (f 7)[0] = 0 := sorry
  have : (f 7)[1] ≠ 0 := sorry
  have : (f 7)[2] = (f 3)[2] := sorry
  have : (f 11)[0] = 0 := sorry
  have : (f 11)[1] ≠ 0 := sorry
  have : (f 11)[2] = (f 3)[2] := sorry
  have : (f 7)[3] = (f 3)[3] ∨
        (f 11)[2] = (f 3)[2] := sorry
  sorry

probably could be minimized more but I have to run now

[Damiano Testa]

Synthesizing instances could benefit from shortcuts available in all of mathlib that are not available in a reduced environment, so maybe this is not too surprising. I would say that increasing imports is not necessarily a guarantee of slow-downs/speed-ups.

[Damiano Testa]

After all, elaboration is dependent on the order of the imports.

[James Gallicchio]

@Parth Shastri pointed out that lt_add_iff_pos_left can apply whenever 0 is on the LHS (regardless of the RHS), which significantly slows down the get_elem_tactic's simp search:

example : 0 < n + 1 := by
  repeat rw [Nat.lt_add_left_iff_pos]

removing simp from this lemma, sealing BitVec.ofNat, and importing more of Mathlib all help speed up the example significantly. thanks y'all!