fastest tactic for proving Nat literal inequalities

Stream: lean4

[Gavin Zhao]

What's the fastest tactic for proving Nat literal inequalities like 3 < 5, 159 < 300, etc? You can assume literals don't exceed three digits. I've been using simp but I'm curious if I can make it even faster.

The context is for bounds check proofs for array indexing. For type-checking performance, I have a custom syntax for array indexing where both the size and the index are literals, e.g. Main : Vector Nat 355 and I access Main[42]$.

syntax:max term noWs "[" withoutPosition(term) "]$" : term
macro_rules | `($x[$i]$) => `(getElem $x $i (by simp))

I currently have simp in place, but for functions with many array index operations (e.g. I have a parameter Main : Vector Nat 251 and there are 752 constant index operations on Main) I still need to adjust maxHeartbeats. I wonder if this can be even faster.

btw I'm not using the default a[i]syntax because the time complexity of get_elem_tactic is quadratic w.r.t. the size of the context, due to the use of assumption.

[Gavin Zhao]

Truely a "Lean at scale" moment :sweat_smile:

[Kenny Lau]

mathlib's norm_num

[Kenny Lau]

by decide might also be fast

[Robin Arnez]

decide is probably faster than norm_num

[Michael Rothgang]

omega might not be faster, but it's my standard tactic for natural number or integer arithmetic.

[Robin Arnez]

When you use a[i], it should already use decide though

[Robin Arnez]

and simp +arith when that fails

[Robin Arnez]

Oh it's because decide comes too late...

[Robin Arnez]

Wait no decide comes before assumption

[Robin Arnez]

Oh but get_elem_tactic puts assumption before decide

[Gavin Zhao]

Robin Arnez said:

Oh but get_elem_tactic puts assumption before decide

Yeah that was the biggest issue for me. I understand the rationale for putting assumption first but when your context gets large with 600 lets this doesn't scale.

[Robin Arnez]

Can't you split up what ever you have into multiple functions..?

[Robin Arnez]

You're probably not using all 600 lets at the same time, are you?

[Gavin Zhao]

You're probably not using all 600 lets at the same time, are you?

Well actually yes.

[Kyle Miller]

Are you able to create some self-contained test case for this @Gavin Zhao? It might be worth creating a Lean issue pointing out these performance issues with index notation.

[Gavin Zhao]

@Kyle Miller Not yet but I'll give it a try. This issues comes from some company code that will be open-sourced later but right now I don't think I can share the function that has the performance issue.

[Devon Tuma]

Seems like

macro_rules
  | `(tactic| get_elem_tactic) => `(tactic| (decide +kernel); get_elem_tactic; done)

provides similar speedup. Doesn't work with get_elem_tactic_extensible though because of the previously mentioned assumption tactic taking priority

[Robin Arnez]

decide is a terminal tactic so get_elem_tactic; done doesn't do anything though

[Devon Tuma]

Yeah I've just seen that any other different cases now break

[Robin Arnez]

Really? This still seems to work:

macro_rules
  | `(tactic| get_elem_tactic) => `(tactic| decide)

example (h : a ≤ 3) : a ≠ 4 := by
  get_elem_tactic

[Devon Tuma]

I've been looking and I think it seems like it was actually a problem with decide not terminating in time in some edge cases we have, not a global thing. Adding norm_num1 seems to give similar speedups without that being an issue