lean-crush

An SMT hammer for Lean 4. Write by crush and an SMT solver does the tedious part of the proof for you.

Read the lean-crush user manual for installation, configuration, extension APIs, and complete examples. Maintainers should also read the optimization and search-heuristic guide before changing reconstruction or instantiation bounds.

Lean's own automation is strong at goals that follow by rewriting and case analysis. It is weaker at goals that are really just constraint solving — chains of arithmetic inequalities, equalities pushed through uninterpreted functions, bitvector identities, combinations of a dozen hypotheses where only three matter. SMT solvers are very good at exactly that. lean-crush hands them the goal and turns the answer back into a Lean proof.

Three things set it apart from existing Lean–SMT bridges:

• Higher-order goals survive the trip. Functions passed as arguments, partial applications, and lambdas are the point at which other bridges stop; lean-crush eliminates them on the way out (or hands them to cvc5's higher-order solver directly).
• The solver's answer can be checked, not just trusted. lean-crush can replay cvc5's proof certificate inference by inference, or reconstruct the argument from the unsat core, producing a proof the Lean kernel verifies. When it trusts instead, it says so in #print axioms.
• You can teach it your own constants. The Lean-to-SMT mapping is open: one line for simple cases, or a metaprogram for full control — the same API the built-in theories use.

example (f : Int → Int) (a b : Int) (h : a = b) : f a = f b := by crush

example (x y : Int) (h1 : x ≤ y) (h2 : y ≤ x) : x = y := by crush

example (g : Int → Int) (x : Int) (h : ∀ z, g z = z + 1) : g (g x) = x + 2 := by crush

-- a function taken as an argument, and a lambda passed to it
example (g : (Int → Int) → Int) (h : ∀ k, g k = k 1) : g (fun x => x + 1) = 2 := by crush

When the solver satisfies the encoded facts, you get the model instead of a failure:

example (x : Int) : x + 1 = x := by crush
-- crush: could not prove the goal — the solver found a model:
--   x := 0
-- The encoding is incomplete, so a model does not necessarily describe a Lean
-- counterexample.

Install

Requires the Lean toolchain in lean-toolchain and at least one solver on your PATH — z3 (≥ 4.12.2), cvc5 (≥ 1.3), or bitwuzla. z3 is the default and enough to start; cvc5 additionally enables proof replay and native higher-order support.

Add to your lakefile.lean:

require crush from git "https://github.com/AD1024/lean-crush" @ "main"

Then import Crush and the crush tactic is available. The package has no third-party Lean dependencies; Mathlib integration tests live in a separate package.

lake build              # the library
lake build Test.Smoke   # smoke tests (needs z3 for the round-trip)

Maintainers can run the optional Mathlib integration suite separately:

cd MathlibTest
lake exe cache get
lake build

Using it

crush reads every hypothesis in context, so a bare call is usually what you want. To go further:

crush [h, myLemma]   -- use exactly these facts (lemmas need not be in context)
crush [*, myLemma]   -- everything in context, plus a lemma
crush u[myFn]        -- unfold `myFn` via its equation lemmas

Explicit lemmas are also instantiated at relevant ground terms before SMT translation. This lets one lemma create the term that triggers another, including existential-witness chains that SMT E-matching cannot start on its own. The pass is bounded by crush.inst.fuel and crush.inst.rounds. When Lean can simplify the ground consequences to useful propositions without discarding terms needed as witnesses, they replace the unrestricted quantifier and avoid solver instantiation loops. Other lemmas remain quantified as fallbacks. Set either option to 0 to disable this pass and send the original quantifiers directly.

Selected definitions are rewritten in the actual hypotheses and goal before SMT translation; their equations also remain available as fallback solver facts. This makes u[...] useful without depending entirely on SMT quantifier instantiation.

Mark a definition and its equations come along automatically, with no u[…] needed:

@[crush_unfold]
def myFn : Nat → Nat
  | 0 => 0
  | n + 1 => myFn n + 2

Predicates marked with Lean's standard @[reducible] attribute are also normalized automatically, but their equations are not added as quantified SMT facts. Recursive predicates use only constructor-specific rewrite equations; use @[crush_unfold] when SMT also needs their quantified fallback.

You can also enable automatic unfolding for definitions from Lean or another library:

attribute [local crush_unfold] List.length

example (l : List Int) : l.length = 0 ↔ l = [] := by crush

Use local to keep the setting in the current section or file. Omit it when the setting should be exported to modules that import yours. The same approach works for definitions such as Monotone and Function.Injective.

crush proves goals, not inductions — so drive the induction yourself and let it close the cases:

inductive N where | Z | S (n : N)

@[crush_unfold]
def N.add : N → N → N
  | x, .Z   => x
  | x, .S y => .S (N.add x y)

theorem zero_add (x : N) : N.add .Z x = x := by
  induction x with
  | Z => crush            -- @[crush_unfold] on N.add supplies its equations
  | S x ih => crush [ih]  -- feed the induction hypothesis as a fact

By default crush takes the solver at its word. To demand a proof the Lean kernel checks — so the goal fails rather than closing if none can be built:

set_option crush.trust "reconstruct" in
theorem checked (x y : Int) (h1 : x = y) (h2 : y = 3) : x = 3 := by crush

#print axioms checked
-- 'checked' depends on axioms: [propext, Classical.choice, Quot.sound]

Under the default policy that same command reports [Crush.crushSorry] instead, which is how you tell the two apart at a glance.

If SMT can prove a domain-specific fact but checked reconstruction needs a bridge theorem, register that theorem for bounded reconstruction search:

inductive Phase where
  | initial
  | next (previous : Phase)

def Advances (source target : Phase) : Prop :=
  target = .next source

@[crush_reconstruct]
theorem advancesNext (phase : Phase) : Advances phase (.next phase) :=
  rfl

@[crush_reconstruct] affects only kernel-checked core reconstruction. It does not send the theorem to SMT or participate in Alethe replay; use crush [...], @[crush_unfold], or a lowering when the solver also needs the fact's semantics. Rules are indexed by their conclusion and searched to a fixed depth, so rules for unrelated datatypes are not added wholesale to grind.

Other behaviour is controlled by set_options (crush.backend, crush.timeout, and others); each carries its own documentation where it is declared.

Library premise selection is opt-in and uses Lean's registered LibrarySuggestions engine:

set_option crush.premises true
set_option crush.premises.max 32

It applies to bare crush calls. An explicit [...] list remains a strict restriction and disables automatic premise selection.

How it works

The tactic collects your hypotheses together with the negation of your goal, translates that package to SMT, and runs a solver under a strict time budget. If the package is contradictory, your goal follows. If the solver instead finds a model, that model is your counterexample.

Trusting that verdict is the fast path, and what hammers normally do. Building a real Lean proof from it takes one of two routes:

• replaying the solver's proof — cvc5 can emit its refutation as a certificate, and lean-crush walks it one inference at a time, proving each in Lean. Since the solver already found the argument, each step is small, which reaches goals no single Lean tactic cracks in one shot. Replay covers propositional logic, EUF, integer and Nat arithmetic, strings, bitvectors, datatype injectivity, quantified formulas, and defunctionalized higher-order terms, including nested Alethe subproof blocks.
• reconstructing from the unsat core — the solver reports which few hypotheses actually mattered, and a Lean tactic redoes the argument from just those. This needs no certificate, but it does require a backend-provided unsat core. Z3 and cvc5 provide one; Bitwuzla currently does not.

Beyond plain logic and arithmetic, lean-crush covers bitvectors, string length, append, emptiness, String-pattern prefix/suffix/containment, and your own inductive types. It keeps functions-as-arguments alive all the way to the solver — the case where Lean-to-SMT bridges usually give up. Polymorphic lemmas are specialized to the types a goal mentions, so a general lemma still applies to your concrete instance.

You can also teach it to translate your own constants, which is how the built-in theory mappings are themselves written:

crush_map Nat.add => "+"
crush_map_sort Nat => "Int"

For full control, register a metaprogram that runs at elaboration time:

@[crush_lower Int.sign]
def lowerSign : Crush.LoweringHandler := fun ctx => do
  let #[x] := ctx.args | return none
  let sx ← ctx.emitTerm x
  return some (smt| (ite (> $sx 0) 1 (ite (= $sx 0) 0 (- 1))))

Use @[crush_lower_result T] when the application head is unstable but the result-family head is stable. The dispatcher first matches the immediate head of the term's type; for a syntactic dependent function type, it peels binders and matches the codomain head. Named aliases are separate keys, so the built-in decision lowering registers both Decidable and DecidableEq. It represents decision evidence with an axiomatized singleton SMT sort and lowers decide p to p; equality decisions therefore become SMT equality without depending on a particular procedure implementation. Pair a result lowering with a compatible @[crush_translate_sort] handler whenever it changes representation.

The (smt| ...) quotation is a shallow embedding of SMT-LIB terms. Symbols, applications, numerals, Booleans, and strings use SMT-LIB syntax; $term splices an existing Crush.SMT.Term. The result is a structured term representation, not an unchecked string; lean-crush sort-checks the final SMT script.

When a custom lowering emits an SMT operator that checked replay does not know, register its inverse with the replay DSL:

def MultipleOfThree (x : Int) : Prop := x % 3 = 0

@[crush_lower MultipleOfThree]
def lowerMultipleOfThree : Crush.LoweringHandler := fun ctx => do
  let #[x] := ctx.args | return none
  return some (.app (.indexed "divisible" #[.inr 3]) #[← ctx.emitTerm x])

register_crush_replay term <<
  ((_ divisible (int divisor)) (term value : Int)) |
  (divisible (term divisor : Int) (term value : Int)) =>
    value % divisor = 0
>>

The two patterns accept indexed SMT-LIB and cvc5's normalized ordinary form. term, nat, int, string, atom, sexp, sort, and prop introduce typed Lean names for the right-hand side; _ matches one item and a final .. matches the remainder. Alternatives must bind the same names.

Certificate inference rules are extensible in the same style:

register_crush_replay rule low <<
  (my_arithmetic_rule (term x : Int) (term y : Int) ..) =>
    by omega
>>

The tactic sees only the replayed premises, its captures, and the step target. Every proof and generated auxiliary declaration is kernel-checked. Add high, low, or a numeric priority after term or rule when handlers overlap.

Rule registrations can also use a typeclass-dispatched, metaprogrammed condition:

structure RuleArgumentIs where
  expected : String

instance : Crush.ReplayCondition RuleArgumentIs where
  check condition ctx :=
    return ctx.args[0]? == some (.atom condition.expected)

def enabledRule : RuleArgumentIs where
  expected := "enabled"

register_crush_replay rule <<
  (my_conditional_rule ..) if enabledRule =>
    by exact True.intro
>>

The condition is not a proposition and creates no proof obligation. It runs after pattern matching; false delegates to the next registration. The ReplayRuleContext exposes the target, premises, raw arguments, and named captures through binding?.

For dynamic matching, use @[crush_replay "operator"] on a Crush.ReplayTermHandler or @[crush_replay_rule "rule"] on a Crush.ReplayRuleHandler; returning none defers to the next handler. See Test/AletheExtension.lean for an Alethe-only end-to-end example.

Array-backed operations can reuse Crush's finite Array representation instead of reimplementing its length/data encoding:

def overwriteFirst {α : Type} (xs : Array α) (value : α) : Array α :=
  xs.setIfInBounds 0 value

@[crush_lower overwriteFirst]
def lowerOverwriteFirst : Crush.LoweringHandler := fun ctx => do
  let #[elem, xs, value] := ctx.args | return none
  let svalue ← ctx.emitTerm value
  Crush.withFiniteArray ctx elem xs fun view => do
    let data := (smt| (store $(view.data) 0 $svalue))
    let updated := view.mkValue view.length data
    return (smt| (ite (> $(view.length) 0) $updated $(view.value)))

withFiniteArray returns none if another sort handler has replaced Array's representation, and inserts an SMT let so nested updates are not duplicated. The built-in lowerings use this API for replicate, size, bounded/defaulting/optional indexing, set/setIfInBounds/set!, push, pop, swap/ swapIfInBounds, isEmpty, back!, and back?.

Limitations

• No induction. A goal needing an inductive hypothesis will not be solved merely by increasing the timeout. Drive the induction yourself and let crush close each case — that is the intended workflow.
• Not every function translates. Arithmetic, canonical divisibility, Bool, String, BitVec, and your own inductive types do; some library operations such as Finset.card do not, and an untranslated one becomes uninterpreted — so the solver reports a counterexample, not an error. Definitions such as |·|, List.length, and Monotone work after enabling crush_unfold as shown above. Otherwise, provide a suitable lemma, state the needed property directly, or add a custom lowering. Array operations that copy a symbolic range (append, extract, map, filter) still need lemmas or custom lowerings; unlike push/pop, they require quantified element-wise encodings. String replacement, character-pattern search, slice/position operations, numeric parsing, and lexicographic order are also untranslated: Lean's empty-pattern replacement differs from SMT str.replace_all, symbolic Char values do not yet have a codepoint encoding, positions are UTF-8 byte offsets, numeric parsers accept underscores, and SMT-LIB's string alphabet ends at U+2FFFF while Lean's does not.
• A goal is only as strong as its premises. A missing premise usually leaves the encoded negation satisfiable, and quantifiers can instead make the solver return unknown — so check the goal actually follows before blaming the solver.
• Reconstruction is narrower than solving. Under crush.trust "reconstruct", some goals the solver proves cannot be replayed as a Lean proof. In particular, cvc5 1.3 does not emit Alethe certificates for finite-datatype exhaustiveness, finite-array reasoning, or native higher-order proofs, and rejects certificates containing signed bitvector-to-Int conversion; automatic mode may still reconstruct these from the unsat core. "reconstructOrTrust" falls back to the axiom with a warning when both checked paths fail. For bit-vector-heavy reconstruction, crush.reconstruct.trustBvDecide true enables bv_decide as an explicit native-code-trusting fallback. The resulting theorem names an auditable _native.bv_decide.ax_* dependency; the option is off by default, preserving kernel-only reconstruction. crush.reconstruct.trustNativeDecide true enables the broader native_decide fallback for finite or computational goals. It trusts Lean's native compiler, runtime, and all executable definitions reached by the decision procedure; accepted proofs expose an _native.native_decide.ax_* dependency. This option is also off by default.
• Rough edges. Indirectly recursive datatypes (Rose with a List Rose field) become an opaque sort; Alethe replay needs cvc5 ≥ 1.3.

Relation to lean-auto

lean-crush is a from-scratch redesign in the spirit of lean-auto. The three points above are exactly where it diverges, and in each case lean-auto's limitation is visible in its source: it reifies into a higher-order logic but then hard-fails ("Higher order input?") on any function-typed argument while emitting SMT; its Lean→SMT mapping is closed, so extending it means forking; and its SMT backend has no proof reconstruction yet, either producing no proof or closing the goal with the autoSMTSorry axiom.

Examples and case studies

Test/ has runnable examples across every supported theory, including recursive functions and nested datatypes (Test/Recursive.lean) and the harder reconstruction cases for both routes (Test/AletheReplay.lean, Test/ReconstructHard.lean).

Test/CaseStudies/ runs crush against lean-auto's test suite and Loom/Velvet/Cashmere verification conditions. The optional MathlibTest package checks Mathlib lemma statements restated at Int, with operations that have no first-order translation pinned as expected failures so the boundary is recorded rather than implied.

Complete downstream integrations are available in the Loom crush-backend branch and Velvet crush-backend branch. They show lean-crush wired into verification-condition generation and used on real array, arithmetic, and quantified proof obligations.

To compare trusted Crush with lean-auto, Duper, and grind on LeanHammer, Loom, Cashmere, and Velvet, run scripts/benchmark-corpora.sh. It clones and builds pinned source revisions, checks them out in temporary worktrees, overlays the local lean-crush build, and writes fixed-workload coverage plus pairwise matched-VC timing under BenchmarkResults/. Set Z3_BIN/CVC5_BIN when the solvers are not on PATH; RUN_AUTO=false, RUN_DUPER=false, or RUN_CRUSH=false selects backends for focused profiling. scripts/benchmark-plean.sh provisions the pinned PLean revisions. Exact self-contained commands and output definitions are in the benchmark script guide. See BENCHMARKS.md for the latest recorded comparison. The user manual also presents the coverage, outcome, and reconstruction figures.

The Cedar crush-backend branch contains a CedarCrushCaseStudy module built on Cedar.Thm. It demonstrates crush as an interactive leaf tactic for Cedar foundation proofs, using kernel reconstruction rather than Crush.crushSorry.

Acknowledgements

lean-crush builds on ideas and test material from several projects:

• lean-auto — the tool this redesigns; its monomorphization approach, typed SMT IR shape, and test corpus informed the design, and its SmtTranslation suite is ported in the case studies.
• Loom and its verifiers Velvet (Dafny-style imperative) and Cashmere (effectful monadic) — the source of the verification-condition case study.
• Cedar — the formal specification and Lean foundation used by the Cedar case study.
• Strata — its Lambda type matcher and proof structure underpin the extracted soundness, completeness, and occurs-check case study.
• Veil — its model-minimization approach (z3model.py) informs the planned counterexample minimization.