Reproducer for mathlib4 PR #40110 — linarith atomization speedup

gen-bench.py

#!/usr/bin/env python3
"""
Reproducer for mathlib4 PR #40110 — linarith atomization speedup.

Generates two Lean files (Bench80.lean, Bench160.lean) that each call
`linarith (config := {})` several times on a dense rational LP:
  0 ≤ xᵢ, xᵢ ≤ 1, Σxᵢ ≤ n
with n distinct atoms and 2n bound hypotheses.

Usage
-----
  python3 gen-bench.py                  # writes Bench80.lean and Bench160.lean
  lake env lean Bench80.lean  | grep 'tactic execution'
  lake env lean Bench160.lean | grep 'tactic execution'

Compare numbers between the master branch and PR branch.
Apple Silicon M-series, lean-toolchain v4.31.0-rc1:

  | benchmark         | before   | after    | speedup |
  |-------------------|---------:|---------:|--------:|
  | n = 80  (5 calls) | 338 ms   | 216 ms   | 1.56×   |
  | n = 160 (3 calls) | 513 ms   | 292 ms   | 1.76×   |
"""
for N, reps in [(80, 5), (160, 3)]:
    xs = ' '.join(f'x{i}' for i in range(N))
    lo = ' '.join(f'(a{i} : 0 ≤ x{i})' for i in range(N))
    hi = ' '.join(f'(b{i} : x{i} ≤ 1)' for i in range(N))
    goal = ' + '.join(f'x{i}' for i in range(N))
    body = (f'example ({xs} : ℚ) {lo} {hi} :\n'
            f'    {goal} ≤ {N} := by\n'
            f'  linarith (config := {{}})')
    with open(f'Bench{N}.lean', 'w') as f:
        f.write('import Mathlib.Tactic.Linarith\n\nset_option profiler true\n\n')
        for _ in range(reps):
            f.write(body + '\n\n')
    print(f'wrote Bench{N}.lean ({reps} invocations)')