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. For a stuck tower of projections base.π₁.…​.πₙ​.πₙ over a base that is only propositionally a constructor, we additionally try congrArg with the composite projection function: even when the intermediate levels are dependent, the composite is often non-dependent (e.g. fun p => p.snd.len : … → Nat) and the whole spine can be rewritten in one step.

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 the goal target (used by the cbv tactic)
• cbvHyp: reduces a hypothesis type (used by cbv at)
• 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.cbvGoalCore (mvarId : MVarId) : Sym.SymM (Option MVarId)

Core of cbvGoal: reduces the target of an already preprocessed mvarId using call-by-value evaluation, within the caller's SymM context.

Equations

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

def Lean.Meta.Tactic.Cbv.cbvHyp (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option MVarId)

Reduce the type of hypothesis fvarId using call-by-value evaluation, in its own SymM session (like conv at h => cbv). The local context is only mutated after the session ends, so the SymM incrementality invariant is preserved.

Equations

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

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

Reduce the goal target using call-by-value evaluation.

Preprocesses the goal via Sym.preprocessMVar (instantiates metavariables, unfolds reducibles, shares common subterms), then reduces the goal type via cbvCore. If the reduced type is True, the goal is closed. Otherwise, the target is replaced.

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

Equations

• Lean.Meta.Tactic.Cbv.cbvGoal mvarId = (do let __do_lift ← Lean.Meta.Sym.preprocessMVar mvarId Lean.Meta.Tactic.Cbv.cbvGoalCore __do_lift).run

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.