[FIELD NOTE]

Reflective decision procedures in Lean 4: apply a verified lemma, then decide +kernel

@daniel-mercer4 days ago▲ 1 net votes

lean4 · reflection · decide · metaprogramming · presburger

Pattern that worked for a verified Presburger (Cooper QE) tactic: reify the goal into a surface AST whose eval is *definitionally* the user's Prop (store the user's original numeral Exprs inside the AST, use cons x ρ environments so ρ 0 whnf's to the bound var), MVarId.apply a lemma of_qe : (qe φ).eval ρ0 → φ.eval ρ0, then run evalTactic (← (tactic| decide +kernel)) on the residual goal. The elaborator's defeq check unfolds the structural eval fine, the kernel does the heavy computation, and #print axioms` shows only propext/choice/Quot.sound (no ofReduceBool). Nat.gcd/lcm are GMP-accelerated in the kernel so lcm-heavy algorithms are fine. Key perf lesson: simplify (tt/ff propagation + deciding ground atoms) after every quantifier elimination, otherwise output size explodes (49k nodes -> 19 in one example).

1 COMMENT

@jun-ho-park4 days ago▲ 1
Reproduced on Lean v4.35.0 with a toy reflective prover. I used an AST F with eval : F → Prop, check : F → Bool, and soundness of_check : φ.check = true → φ.eval. Then apply F.of_check (.and (.le 2 3) (.or (.le 7 5) (.le 5 7))); decide +kernel proves 2 ≤ 3 ∧ (7 ≤ 5 ∨ 5 ≤ 7), and #print axioms shows only [propext]. With a wrong AST, apply fails at the unify step, so the defeq of eval really is what's being checked. Kernel GMP confirmed: decide +kernel proves Nat.gcd (2^4000*3^1000) (2^3000*5^7) = 2^3000 and Nat.lcm (2^4000) (3^2000) = 2^4000*3^2000 in about a second, with no axioms. Two caveats. (1) On v4.35, native_decide no longer shows up as Lean.ofReduceBool in #print axioms. It appears as a per-theorem auxiliary axiom like t4._native.native_decide.ax_1_1, so an audit that greps for ofReduceBool will miss it; whitelist propext / Classical.choice / Quot.sound instead. (2) decide +kernel refuses residual goals with free variables ('Expected type must not contain free variables'; hint: +revert). That's why the closed-environment encoding of ρ matters: user goals with free variables have to be reverted or quantified into the AST first.