avoid unfolding big constants

Stream: general

[Huỳnh Trần Khanh]

well, i still need some mathlib so it's not like I can use lean 4 for my project... anyway in the orange bar hell thread it's already been established that the 2147483648 constant is the culprit so... are there any workarounds to avoid unfolding that constant without breaking my favorite tactics (norm_num, simp, linarith, ring)?

[Huỳnh Trần Khanh]

or should I use num instead of nat? I think there might be some lemmas to transform lemmas about nat into lemmas about num?

[Scott Morrison]

I haven't looked at what you're doing, but does just writing 2^31 help?

[Huỳnh Trần Khanh]

sorry to be the bearer of bad news. I did a simple find and replace, it didn't help

[Huỳnh Trần Khanh]

ah well it helped lol, still somewhat slow but at least it didn't take forever... OOPS SPOKE TOO SOON I GOT A DEEP RECURSION ERROR

[Huỳnh Trần Khanh]

(the code is in the orange bar thread, I pasted exactly the bottleneck without anything extraneous so you might want to take a whack at it)

[Huỳnh Trần Khanh]

deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

[Yakov Pechersky]

One thing I would suggest would be to get rid of all the clear_except tactic lines, those only slow down the elaboration, since each call requires the tactic to iterate through the hypotheses and clear them away.

[Reid Barton]

Does it get faster if you make the constants not really big (but still big enough for the proof to be valid of course)?

[Reid Barton]

I don't think we have any good general techniques for what I am assuming is the issue here (something is causing Lean to do a calculation involving these big numbers). I would try to avoid exact and instead apply lemmas to leave goals that can be closed by norm_num. There are also more drastic options like using irreducible.

[Yakov Pechersky]

One option is to just start the proof of split2 with:

  intros x y,
  have lb : get_left_bound word_size_t.i32 ≤ -30 := by norm_num [get_left_bound],
  have ub : 30 < get_right_bound word_size_t.i32 := by norm_num [get_right_bound],
  refine ⟨lb.trans _, lt_trans _ ub⟩,

[Yakov Pechersky]

to get rid of your large numbers asap

[Yakov Pechersky]

or 600 or whatever it is that you actually hit

[Reid Barton]

I agree, in particular simp only [get_right_bound, get_left_bound, within_bounds] looks like a mistake, you exactly want to avoid seeing these big numbers

[Yakov Pechersky]

If you profile your existing proof, none of the norm_num on their own take that much time. I think there's some larger issue finalizing the whole tactic block, because even sorrying the final goal makes my tactic proof grind to a halt

[Reid Barton]

However, just because you don't see them doesn't mean that Lean won't unfold these definitions to check some definitional equality, unfortunately

[Reid Barton]

ok this looks like something dumb

[Reid Barton]

This is slow:

import tactic

inductive word_size_t
| char
| i32
| i64

def get_right_bound : word_size_t → ℤ
| word_size_t.char := 128
| word_size_t.i32 := 2147483648
| word_size_t.i64 := 9223372036854775808

lemma moo : get_right_bound word_size_t.i32 > 30 := by norm_num [get_right_bound]

lemma split2 (input : list ℤ) (h' : input.length ≤ 30) :
    (input.length : ℤ) < get_right_bound word_size_t.i32 :=
lt_of_le_of_lt (int.coe_nat_le.mpr h') moo

[Reid Barton]

but this is fast:

import tactic

inductive word_size_t
| char
| i32
| i64

def get_right_bound : word_size_t → ℤ
| word_size_t.char := 128
| word_size_t.i32 := 2147483648
| word_size_t.i64 := 9223372036854775808

lemma moo : 30 < get_right_bound word_size_t.i32 := by norm_num [get_right_bound]

lemma split2 (input : list ℤ) (h' : input.length ≤ 30) :
    (input.length : ℤ) < get_right_bound word_size_t.i32 :=
lt_of_le_of_lt (int.coe_nat_le.mpr h') moo

[Reid Barton]

so, it kind of looks as though the kernel is trying to test defeq of (<) x y and (>) y x by starting with the last arguments x =?= y, which isn't obviously false even when one of x, y is small because of the bit0/bit1 encoding

[Reid Barton]

mwe:

lemma L : (0 : ℤ) < 10000000007 := sorry
lemma L' : 10000000007 > (0 : ℤ) := L -- deep recursion

It doesn't happen with nat, or with <=, so probably related to some kernel reduction heuristic?

[Reid Barton]

ah I see, my theory from before didn't make sense, instead it's trying to reduce x < y (rather than y > x), which can go on for some time because it is a reflection-style definition, and I guess it doesn't happen for <= because the definition height is low enough compared to >= or something?

[Reid Barton]

Maybe >= and > should be made abbreviations so they get the kernel reduction hint?

[Reid Barton]

Also it might be better to make int.le and int.lt into inductive props so they don't reduce (like nat.le)

[Mario Carneiro]

Yep, int.le and int.lt applied to large integer literals are timebombs because they are defeq to true or false so anything that tries to whnf them will die

[Huỳnh Trần Khanh]

haha i finally found a workaround... i would like to share this workaround in case someone needs it...

lemma two_exists : ∃ x : ℤ, x = 2 := begin
  use 2,
end

noncomputable def two := Exists.some two_exists
lemma two_is_two : two = 2 := begin
  exact Exists.some_spec two_exists,
end

now every definition that relies on two is uncomputable but... i don't mind? it doesn't really matter for my use case

[Kevin Buzzard]

All the best twos are noncomputable

[Gabriel Ebner]

@[irreducible] def two : ℤ := 2 should have the same effect without being noncomputable, and you can prove two_is_two using by rw [two].

[Reid Barton]

This actually doesn't work in the example I gave above

@[irreducible] def two : ℤ := 10000000007
lemma L : (0 : ℤ) < two := sorry
lemma L' : two > (0 : ℤ) := L  -- still slow

[Eric Wieser]

But the noncomputable version does?

[Huỳnh Trần Khanh]

yeah @[irreducible] only affects elaboration, however the step after elaboration is actually the bottleneck :joy: the noncomputable version fixes the issue

[Huỳnh Trần Khanh]

bizarre workaround but if it works it works

[Gabriel Ebner]

Ah, right. So it's the kernel that takes too long. Bad news: then the irreducible won't help in Lean 3. Good news: it will in Lean 4.