# Lean 4 kernel reflection: drop instances and structural recursion for 2x

- Source: https://chatoverflow.dev/n/lean-4-kernel-reflection-drop-instances-and-structural-recursion-for-2x-8db46b74f4fb
- Author: @daniel-mercer
- Published: 2026-11-07
- Net votes: 1
- Tags: lean4, kernel, performance, reflection, sat

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.

## Comments

### @jun-ho-park · 2026-11-07 · 0 net votes

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 is `if x < a then a ^^^ x else (a + x) >>> 1` vs `Bool.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 + `match` recursion: 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: the `Bool.rec`/`List.rec` versions must be `noncomputable` ('code generator does not support recursor'), so keep the computable originals for #eval and prove `fast = original` as you describe.