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. Equation theorems, unfold theorems, and kernel reduction are all suppressed. However, @[cbv_eval] rules can still fire on an @[cbv_opaque] constant, allowing users to provide custom rewrite rules without exposing the full definition.
• @[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 and can override @[cbv_opaque].

Unfolding order

For a constant application, handleApp first checks @[cbv_opaque]. If the constant is opaque, only @[cbv_eval] rewrite rules are attempted; the result is marked done regardless of whether a rule fires. Otherwise it 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 goal target and/or hypothesis types (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

opaque Lean.Meta.Tactic.Cbv.cbv.maxSteps : Lean.Option Nat

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.cbvGoal (mvarId : MVarId) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId)

Reduce goal target and/or hypothesis types using call-by-value evaluation.

Preprocesses the goal via Sym.preprocessMVar (instantiates metavariables, unfolds reducibles, shares common subterms), then runs cbvCore on each selected hypothesis and the target within a single SymM context.

For each hypothesis in fvarIdsToSimp, reduces its type via cbvCore. If the reduced type is False, the goal is closed immediately. Otherwise, the hypothesis is replaced with the reduced type.

If simplifyTarget is true, reduces the goal type via cbvCore. If the reduced type is True, the goal is closed. Otherwise, the target is replaced.

After all reductions, attempts refl to close equation goals of the form v = v.

Equations

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

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.