Cbv Evaluator

Proof-producing symbolic evaluator that tries to match call-by-value evaluation semantics as closely as possible. Built on top of Lean.Meta.Sym.Simp, it runs as a pair of Simprocs (pre/post) that drive the simplifier loop.

Evaluation strategy

The pre-pass (cbvPre) handles structural dispatch: projections, let-bindings, constants, and control flow. Before doing any work, it short-circuits on proof terms and ground literal values (Nat, Int, BitVec, String, etc.), marking them as done so the simplifier does not recurse into them.

For applications, the pre-pass first tries control flow simprocs (ite, dite, cond, match, Decidable.rec) before the simplifier recurses into the arguments. This matters because control flow reduction can eliminate branches entirely, avoiding unnecessary work on arguments that would be discarded.

It converts non-dependent lets into beta-applications (via toBetaApp) so the simplifier's congruence machinery can process arguments in parallel.

The post-pass (cbvPost) fires after the simplifier has recursed into subterms. It evaluates ground arithmetic (evalGround) and unfolds/beta-reduces remaining applications (handleApp).

Neither pass enters binders — lambdas, foralls, and free variables are marked done := true immediately.

Limitations

This is a best-effort tactic. It reduces as far as it can, but cannot always fully evaluate a term.

Rewriting is fundamentally non-dependent: congruence lemmas like congrArg cannot rewrite an argument when the return type of the function depends on it. When the simplifier encounters such a dependency, it leaves that subterm alone.

There are also places where we deviate from strict call-by-value semantics:

• Dependent let-expressions are zeta-reduced (substituted directly) rather than evaluated as an argument first, because the type dependency prevents us from using congruence-based rewriting on the value.
• Dependent projections that cannot be rewritten via congrArg are reduced directly when possible. As a last resort, if the types on which the projection function depends are definitionally equal, we use HCongr to build the proof.

Attributes

• @[cbv_opaque]: prevents cbv from unfolding a definition. The constant is returned as-is without attempting any equation or unfold theorems.
• @[cbv_eval]: registers a theorem as a custom rewrite rule for cbv. The theorem must be an unconditional equality whose LHS is an application of a constant. Use @[cbv_eval ←] to rewrite right-to-left. These rules are tried before equation theorems, so they can be used together with @[cbv_opaque] to replace the default unfolding behavior with a controlled set of evaluation rules.

Unfolding order

For a constant application, handleApp tries in order:

1. @[cbv_eval] rewrite rules
2. Equation theorems (e.g. foo.eq_1, foo.eq_2)
3. Unfold equations
4. Kernel matcher reduction (reduceRecMatcher), which also handles quotients and recursors

Entry points

• cbvEntry: reduces a single expression (used by conv => cbv)
• cbvGoal: reduces both sides of an equation goal (used by the cbv tactic)
• cbvDecideGoal: reduces decide P = true and closes or errors (used by decide_cbv)

opaque Lean.Meta.Tactic.Cbv.cbv.warning : Lean.Option Bool

def Lean.Meta.Tactic.Cbv.cbvEntry (e : Expr) : MetaM Sym.Simp.Result

Reduce a single expression. Unfolds reducibles, shares subterms, then runs the simplifier with cbvPre/cbvPost. Used by conv => cbv.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Tactic.Cbv.cbvGoalCore (m : MVarId) (inv : Bool := false) : MetaM (Option MVarId)

Reduce one side of an equation goal. When inv = false, reduces the LHS; when inv = true, reduces the RHS. Returns none if the goal is closed, or a residual goal with the reduced side.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Tactic.Cbv.cbvGoal (m : MVarId) : MetaM (Option MVarId)

Reduce both sides of an equation goal. Tries the LHS first, then the RHS. Used by the cbv tactic.

Equations

• Lean.Meta.Tactic.Cbv.cbvGoal m = do let __do_lift ← Lean.Meta.Tactic.Cbv.cbvGoalCore m match __do_lift with | none => pure none | some m' => Lean.Meta.Tactic.Cbv.cbvGoalCore m' true

def Lean.Meta.Tactic.Cbv.cbvDecideGoal (m : MVarId) : MetaM Unit

Attempt to close a goal of the form decide P = true by reducing only the LHS using cbv.

• If the LHS reduces to Bool.true, the goal is closed successfully.
• If the LHS reduces to Bool.false, throws a user-friendly error indicating the proposition is false.
• Otherwise, throws a user-friendly error showing where the reduction got stuck.

Equations

• One or more equations did not get rendered due to their size.