Expand description
Counterexamples — when a goal is FALSE, exhibit a model instead of failing silently. Lean ships no built-in counterexample finder with its automation; this closes that gap.
Two routes, both of which RE-VERIFY the model before reporting it (zero false accusations — a returned witness provably satisfies every premise and falsifies the goal):
- Propositional — treat the ground atoms as booleans, search assignments that make all premises true and the goal false.
- Arithmetic QuickCheck — sample the free integer variables over a grid (with shrinking toward the smallest witness) and evaluate.
The evaluator is a pure-Rust ground interpreter over ProofExpr, so a
counterexample is a plain, checkable assignment — not an opaque solver
verdict.
Enums§
- Counterexample
- A refuting model.
Functions§
- find_
counterexample - Search for a counterexample to
premises ⊢ goal: an assignment satisfying every premise while falsifying the goal.Nonewhen none is found on the covered fragment (which does NOT prove the goal — absence of a witness here is not a proof).