feat: Nat.decidableBallLT handles large numbers

[llllvvuu]

This PR enables the following:

example : ∀ a < 28000, a ^ 2 ≠ 7 := by decide

where currently, the following already causes "maximum recursion depth has been reached":

example : ∀ a < 200, a ^ 2 ≠ 7 := by decide

This PR also prevents a stack overflow in:

example : ∀ a < 10 ^ 7, a ^ 2 ≠ 7 := by native_decide

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6651 has successfully built against this PR. (2025-01-15 09:24:15) View Log
• ✅ Mathlib branch lean-pr-testing-6651 has successfully built against this PR. (2025-01-16 02:03:05) View Log
• 🟡 Mathlib branch lean-pr-testing-6651 build against this PR was cancelled. (2025-01-16 03:04:23) View Log
• ✅ Mathlib branch lean-pr-testing-6651 has successfully built against this PR. (2025-01-16 03:49:07) View Log

[kim-em]

How far does it get after these changes?

[kim-em]

!bench

[llllvvuu]

How far does it get after these changes?

This seems to be close to the limit:

set_option maxRecDepth 512 in
set_option maxHeartbeats 130000 in
example : ∀ a < 28000, a ^ 2 ≠ 7 := by decide

[leanprover-bot]

Here are the benchmark results for commit 1607174.
There were significant changes against commit e9bd980:

  Benchmark                   Metric                 Change
  ==================================================================
- big_omega.lean              branch-misses            4.0% (29.1 σ)
- big_omega.lean MT           branch-misses            6.3% (27.7 σ)
- bv_decide_inequality.lean   branch-misses            1.2% (16.8 σ)
- bv_decide_realworld         branch-misses            1.4% (11.4 σ)
- simp_arith1                 branch-misses            2.7% (28.8 σ)
- stdlib                      fix level params         1.5% (30.7 σ)
- stdlib                      instantiate metavars     6.4% (25.6 σ)

[kim-em]

The benchmark results are not encouraging. Would you mind opening a Mathlib PR (using the lean-pr-testing-6651 branch, and targeting the nightly-testing-2025-01-15 branch --- or whatever was the base of lean-pr-testing-6651, you may need to check), and then running !bench on that?

[llllvvuu]

The benchmark results are not encouraging. Would you mind opening a Mathlib PR (using the lean-pr-testing-6651 branch, and targeting the nightly-testing-2025-01-15 branch --- or whatever was the base of lean-pr-testing-6651, you may need to check), and then running !bench on that?

leanprover-community/mathlib4#20799 (comment)

[kim-em]

Wow, is that for real?! I'm confused how a 10% wall-clock improvement is possible while not touching the instruction count.

[nomeata]

Looks like a fluke to me, I usually don't trust wall-time measurements.

[llllvvuu]

I think it's more that the base commit was 10% slower than usual for some reason (some kind of noise). I'm not sure how to re-run the base commit.

[llllvvuu]

IIUC none of the benchmarks flagged in #6651 (comment) use this instance

FWIW performance-wise there is a slight heartbeats overhead (something like 20) for values of n that previously ran, in exchange for supporting more values of n