Lean 4 kernel reflection: drop instances and structural recursion for 2x
A kernel-checked LRAT checker (theorem : chunkOK G a hints = true := Eq.refl true, about 20k hints per theorem) spent its kernel time mostly on cache traffic, not on GMP Nat ops. A ptrace stack sampler on Lean v4.35.0 showed ~32% in the whnf/infer expr->expr unordered_map find/insert, ~15% lean_dec_ref_cold, ~12% in the instantiate/replace (ptr,offset) cache and ~8% malloc/free. Rewriting the checker so the kernel takes fewer reduction steps halved the time (5.4 s -> 2.8 s per chunk). Use List.rec / Hint.casesOn / Option.casesOn directly instead of structurally recursive defs with match. Call Nat.blt, Nat.beq, Nat.land, Nat.xor, Nat.lor, Nat.shiftRight, Nat.pow directly instead of </decide, ==, &&&, ^^^, >>>, ^, since each instance chain costs several delta steps. Keep the original definitions and prove fast = original by induction (change to a one-step helper def, cases on the hint, simp with Nat.blt a b = decide (a < b) and Nat.beq a b = (a == b) via Bool.eq_iff_iff). Then soundness proofs need no change.
Reproduced the speed-up with a small core-only benchmark on Lean v4.35.0 and v4.36.0-rc2. A fold over 20k numbers, split into 10 theorems of 2000 elements (one chunk of 20k hit '(kernel) deep recursion detected'). Each theorem is
Nat.beq (chk (List.range' k 2000) a0) v = true := by decide +kernel. Step isif x < a then a ^^^ x else (a + x) >>> 1vsBool.rec (Nat.shiftRight (Nat.add a x) 1) (Nat.xor a x) (Nat.blt x a). Kernel time, net of a defs-only baseline, median of 3 on a loaded machine (so ±20%): - instances +matchrecursion: 1.47 s (4.35) / 1.98 s (rc2) - primitives +List.rec: 0.86 s / 0.79 s - primitives +match: 1.46 s / 1.13 s - instances +List.rec: 1.53 s / 1.01 s So doing both changes gave 1.7-2.5x, as you say. On v4.35.0 neither change alone helped here; on rc2 each helped on its own. Two practical notes: theBool.rec/List.recversions must benoncomputable('code generator does not support recursor'), so keep the computable originals for #eval and provefast = originalas you describe.