doc: add module and function docstrings for cbv tactic (#12616)

This PR adds documentation to the Cbv evaluator files under
`Meta/Tactic/Cbv/`. Module docstrings describe the evaluation strategy,
limitations, attributes, and unfolding order. Function docstrings cover
the public API and key internal simprocs.

## Summary
- `Main.lean`: module docstring covering evaluation strategy,
limitations, attributes, unfolding order, and entry points; function
docstrings on `handleConstApp`, `handleApp`, `handleProj`,
`simplifyAppFn`, `cbvPreStep`, `cbvPre`, `cbvPost`, `cbvEntry`,
`cbvGoalCore`, `cbvGoal`
- `ControlFlow.lean`: module docstring on how Cbv control flow differs
from standard `Sym.Simp`; function docstrings on `simpIteCbv`,
`simpDIteCbv`, `simpControlCbv`
- `CbvEvalExt.lean`: module docstring on the `@[cbv_eval]` extension;
function docstring on `mkCbvTheoremFromConst`
- `Opaque.lean`: module docstring on the `@[cbv_opaque]` extension
- `TheoremsLookup.lean`: module docstring on the theorem cache
- `Util.lean`: module docstring; function docstrings on
`isBuiltinValue`, `isProofTerm`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean

@@ -12,6 +12,17 @@ public import Lean.Meta.Sym.Simp.Theorems
 import Lean.Meta.Tactic.AuxLemma
 import Lean.Meta.AppBuilder
 
+/-!
+# `@[cbv_eval]` Attribute and Extension
+
+Environment extension for user-provided `cbv` rewrite rules. Each theorem is converted
+to a `Sym.Simp.Theorem` (precomputed `Pattern` + `DiscrTree` key) and indexed by the
+head constant on its LHS.
+
+`@[cbv_eval ←]` inverts the theorem: an auxiliary lemma with swapped sides is created
+via `mkAuxLemma`.
+-/
+
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -31,6 +42,8 @@ structure CbvEvalEntry where
   thm  : Theorem
   deriving BEq, Inhabited
 
+/-- Create a `CbvEvalEntry` from a theorem declaration. When `inv = true`, creates an
+auxiliary lemma with swapped sides so the theorem can be used for right-to-left rewriting. -/
 def mkCbvTheoremFromConst (declName : Name) (inv : Bool := false) : MetaM CbvEvalEntry := do
   let cinfo ← getConstVal declName
   let us := cinfo.levelParams.map mkLevelParam

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -19,9 +19,24 @@ import Lean.Meta.AppBuilder
 import Init.Sym.Lemmas
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.Opaque
+
+/-!
+# Control Flow Handling for Cbv
+
+Cbv-specific simprocs for `ite`, `dite`, `cond`, `match`, and `Decidable.rec`.
+
+The standard `Sym.Simp` control flow simprocs (`simpIte`, `simpDIte`) give up
+when the condition does not reduce to `True` or `False` directly. The Cbv variants
+(`simpIteCbv`, `simpDIteCbv`) go further: they evaluate `Decidable.decide` on the
+condition and use `eq_true_of_decide` / `eq_false_of_decide` to take the
+corresponding branch.
+-/
+
 namespace Lean.Meta.Sym.Simp
 open Internal
 
+/-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not
+reduce to `True`/`False` directly. -/
 public def simpIteCbv : Simproc := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
@@ -74,6 +89,8 @@ public def simpIteCbv : Simproc := fun e => do
         let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
         return .step e' h'
 
+/-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not
+reduce to `True`/`False` directly. -/
 public def simpDIteCbv : Simproc := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
@@ -193,9 +210,8 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
-/-
-  Precondition: `e` is an application
--/
+/-- Dispatch control flow constructs to their specialized simprocs.
+Precondition: `e` is an application. -/
 public def simpControlCbv : Simproc := fun e => do
   let .const declName _ := e.getAppFn | return .rfl
   if declName == ``ite then

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -16,6 +16,78 @@ import Lean.Meta.Tactic.Cbv.CbvEvalExt
 import Lean.Meta.Sym
 import Lean.Meta.Tactic.Refl
 
+/-!
+# 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 `Simproc`s (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`)
+-/
+
 namespace Lean.Meta.Tactic.Cbv
 open Lean.Meta.Sym.Simp
 
@@ -38,6 +110,7 @@ def tryUnfold : Simproc := fun e => do
   let some thm ← getUnfoldTheorem appFn | return .rfl
   Simproc.tryCatch (fun e => Theorem.rewrite thm e) e
 
+/-- Try equation theorems, then unfold equations. Skip `@[cbv_opaque]` constants. -/
 def handleConstApp : Simproc := fun e => do
   if (← isCbvOpaque e.getAppFn.constName!) then
     return .rfl (done := true)
@@ -55,6 +128,11 @@ def tryCbvTheorems : Simproc := fun e => do
   let some evalLemmas ← getCbvEvalLemmas fnName | return .rfl
   Simproc.tryCatch (Theorems.rewrite evalLemmas (d := dischargeNone)) e
 
+/--
+Post-pass handler for applications. For a constant-headed application, tries
+`@[cbv_eval]` rules, then equation/unfold theorems, then `reduceRecMatcher`.
+For a lambda-headed application, beta-reduces.
+-/
 def handleApp : Simproc := fun e => do
   unless e.isApp do return .rfl
   let fn := e.getAppFn
@@ -89,6 +167,12 @@ def zetaReduce : Simproc := fun e => do
   let new ← Sym.share new
   return .step new (← Sym.mkEqRefl new)
 
+/--
+Recursively simplifies the struct inside a projection, then reduces the projection.
+For non-dependent projection types, uses `congrArg` to lift the proof.
+For dependent projection types, tries direct reduction first; if that fails and
+the original and rewritten struct are definitionally equal, falls back to `HCongr`.
+-/
 def handleProj : Simproc := fun e => do
   let Expr.proj typeName idx struct := e | return .rfl
   -- We recursively simplify the projection
@@ -128,6 +212,10 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof
 
+/--
+For an application whose head is neither a constant nor a lambda (e.g. a projection
+like `p.1 x`), simplify the function head and lift the proof via `congrArg`.
+-/
 def simplifyAppFn : Simproc := fun e => do
     unless e.isApp do return .rfl
     let fn := e.getAppFn
@@ -156,6 +244,12 @@ def handleConst : Simproc := fun e => do
   let some thm ← getUnfoldTheorem n | return .rfl
   Simproc.tryCatch (fun e => Theorem.rewrite thm e) e
 
+/--
+Pre-pass structural dispatch. Routes each expression form to the appropriate handler:
+literals, projections, constants, applications (control flow first), and let-bindings
+(non-dependent → `toBetaApp`, dependent → zeta-reduce). Binders and variables are
+marked done immediately.
+-/
 def cbvPreStep : Simproc := fun e => do
   match e with
   | .lit .. => foldLit e
@@ -171,10 +265,14 @@ def cbvPreStep : Simproc := fun e => do
   | .forallE .. | .lam .. | .fvar .. | .mvar .. | .bvar .. | .sort .. => return .rfl (done := true)
   | _ => return .rfl
 
+/-- Pre-pass: skip builtin values and proofs, then dispatch structurally. -/
 def cbvPre : Simproc := isBuiltinValue <|> isProofTerm <|> cbvPreStep
 
+/-- Post-pass: evaluate ground arithmetic, then try unfolding/beta-reducing applications. -/
 def cbvPost : Simproc := evalGround <|> handleApp
 
+/-- Reduce a single expression. Unfolds reducibles, shares subterms, then runs the
+simplifier with `cbvPre`/`cbvPost`. Used by `conv => cbv`. -/
 public def cbvEntry (e : Expr) : MetaM Result := do
   trace[Meta.Tactic.cbv] "Called cbv tactic to simplify {e}"
   let methods := {pre := cbvPre, post := cbvPost}
@@ -183,6 +281,9 @@ public def cbvEntry (e : Expr) : MetaM Result := do
     let e ← Sym.shareCommon e
     SimpM.run' (simp e) (methods := methods)
 
+/-- 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. -/
 public def cbvGoalCore (m : MVarId) (inv : Bool := false) : MetaM (Option MVarId) := do
   Sym.SymM.run do
     let methods := {pre := cbvPre, post := cbvPost}
@@ -217,6 +318,8 @@ public def cbvGoalCore (m : MVarId) (inv : Bool := false) : MetaM (Option MVarId
           m.assign toAssign
           return newGoal.mvarId!
 
+/-- Reduce both sides of an equation goal. Tries the LHS first, then the RHS.
+Used by the `cbv` tactic. -/
 public def cbvGoal (m : MVarId) : MetaM (Option MVarId) := do
   match (← cbvGoalCore m (inv := false)) with
   | .none => return .none

src/Lean/Meta/Tactic/Cbv/Opaque.lean

@@ -8,6 +8,13 @@ module
 prelude
 public import Lean.ScopedEnvExtension
 
+/-!
+# `@[cbv_opaque]` Attribute and Extension
+
+Scoped set of declaration names that `cbv` should not unfold.
+Supports `erase` to remove a declaration from the set within a scope.
+-/
+
 public section
 
 namespace Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/TheoremsLookup.lean

@@ -12,6 +12,14 @@ import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Eqns
 
 
+/-!
+# Cached Theorem Lookup
+
+Per-function cache of `Sym.Simp.Theorem` objects for equation theorems, unfold
+equations, and match equations. Avoids repeated `mkTheoremFromDecl` calls (which
+involve pattern extraction and discrimination tree insertion).
+-/
+
 namespace Lean.Meta.Sym.Simp
 
 def Theorems.insertMany (thms : Theorems) (toInsert : Array Theorem) : Theorems :=
@@ -22,10 +30,6 @@ end Lean.Meta.Sym.Simp
 namespace Lean.Meta.Tactic.Cbv
 open Lean.Meta.Sym.Simp
 
-/--
-Get or create cached Theorems for function equations.
-Retrieves equations via `getEqnsFor?` and caches the resulting Theorems object.
--/
 public structure CbvTheoremsLookupState where
   eqnTheorems : PHashMap Name Theorems := {}
   unfoldTheorems : PHashMap Name Theorem := {}

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -12,6 +12,14 @@ import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.LitValues
 
+/-!
+# Cbv Utility Functions
+
+Predicates for recognizing ground literal values (`isVal`, `isBuiltinValue`) and
+proof terms (`isProofTerm`) in the `SymM` monad. Both are used by `cbvPre` to
+short-circuit before structural dispatch.
+-/
+
 namespace Lean.Meta.Tactic.Cbv
 
 open Lean.Meta.Sym.Simp
@@ -53,6 +61,9 @@ public def isVal (e : Expr) : Bool :=
     isInt64Value
   ].any (· e)
 
+/-- Returns `.rfl (done := true)` for ground literal values of any recognized builtin type,
+preventing the simplifier from recursing into them. For example, this stops the evaluator
+from trying to unfold `OfNat.ofNat 2` further. -/
 public def isBuiltinValue : Simproc := fun e => return .rfl (isVal e)
 
 public def guardSimproc (p : Expr → Bool) (s : Simproc) : Simproc := fun e => do
@@ -86,6 +97,7 @@ def isProof (e : Expr) : Sym.SymM Bool := do
   | .false => return false
   | .undef => isProp (← Sym.inferType e)
 
+/-- Marks proof terms as done so the simplifier does not recurse into them. -/
 public def isProofTerm : Simproc := fun e => do
   return .rfl (← isProof e)