Z3 / Knuckledragger Tactic

This example follows the same architecture as the SymPy Tactic example, but swaps the backend: instead of SymPy, the oracle is Z3 (optionally wrapped by Knuckledragger). Z3 is an SMT solver, so it can handle a richer fragment – quantified formulas, integer arithmetic, and more.

View full source on GitHub

Same architecture, different solver

The Lean side is structurally identical to the SymPy tactic:

axiom knuckle_oracle (p : Prop) : p

@[python "knuckle_expr_check_prop"]
def knuckleExprCheckProp (e : Lean.Expr) : IO Bool := do
  init ()
  let handle ← Py.ofLeanObj e
  let mod ← import_ "lean_to_z3"
  let checkFn ← mod.getAttr "decode_and_check_prop"
  (← checkFn.call #[handle]).toBool

syntax (name := knuckleTac) "knuckle" : tactic

The tactic gets the goal, sends the Lean.Expr to Python, and closes the goal if Z3 says it’s valid.

Converting Expr to Z3

The Python converter mirrors the SymPy version but targets Z3 expressions. Lean names like HAdd.hAdd map to Z3 arithmetic:

_DISPATCH = {
    "HAdd.hAdd": _binop(lambda a, b: a + b),
    "HSub.hSub": _binop(lambda a, b: a - b),
    "HMul.hMul": _binop(lambda a, b: a * b),
    "Eq":        (2, lambda args: expr_to_z3(args[-2])
                                  == expr_to_z3(args[-1])),
    ...
}

Z3 variables are created on demand:

_VAR_CACHE: dict[str, z3.ArithRef] = {}

def _get_var(name: str) -> z3.ArithRef:
    if name not in _VAR_CACHE:
        _VAR_CACHE[name] = z3.Int(name)
    return _VAR_CACHE[name]

The converter also handles ForAll expressions, which SymPy’s version cannot:

if ctor == "forallE":
    binder_name = name_to_str(expr.fields[0])
    body = expr.fields[2]
    var = z3.Int(binder_name)
    return z3.ForAll([var], expr_to_z3(body, bound=[var] + bound))

Checking with Knuckledragger

The proposition checker delegates to Knuckledragger’s lemma wrapper, which calls Z3 under the hood:

def check_prop(prop) -> bool:
    try:
        kdr.lemma(prop)
        return True
    except Exception:
        return False

Using the tactic

import KnuckleTactic

example : (1 : Int) + 1 = 2 := by knuckle
example : (3 : Int) * 4 = 12 := by knuckle
example : (5 : Int) * 6 = 30 := by knuckle

Running

cd examples/05_knuckledragger
cd lean && lake build && cd ..
uv run --project python python/main.py

Comparing SymPy and Z3

	SymPy tactic	Z3 tactic
Backend	CAS (symbolic algebra)	SMT solver
Strengths	Simplification, calculus	Quantifiers, satisfiability
`ForAll` support	No	Yes
Dependency	`sympy`	`z3-solver` + `kdrag`

Both share the same architecture: Lean sends Lean.Expr to Python, Python converts and checks, Lean closes the goal with an oracle. The only difference is what happens inside the converter and checker.

What to take away

The tactic architecture generalises: swap the converter and checker, and you can back a Lean tactic with any Python-accessible decision procedure.
Z3 handles richer formulas (quantifiers, SMT theories) than SymPy.
Knuckledragger wraps Z3 with a higher-level API (kdr.lemma) that handles proof logging and validation.