From 9ae8fb97b3236a8bf0fcf382abbb05f152741e10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 23 Feb 2026 09:29:59 +0000 Subject: [PATCH] doc: add module and function docstrings for cbv tactic (#12616) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean | 13 +++ src/Lean/Meta/Tactic/Cbv/ControlFlow.lean | 22 +++- src/Lean/Meta/Tactic/Cbv/Main.lean | 103 +++++++++++++++++++ src/Lean/Meta/Tactic/Cbv/Opaque.lean | 7 ++ src/Lean/Meta/Tactic/Cbv/TheoremsLookup.lean | 12 ++- src/Lean/Meta/Tactic/Cbv/Util.lean | 12 +++ 6 files changed, 162 insertions(+), 7 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean b/src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean index 3f37085667..27ac6867cd 100644 --- a/src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean index 0e8c454fa1..be3c54e859 100644 --- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 6780669385..f4d6abd104 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Cbv/Opaque.lean b/src/Lean/Meta/Tactic/Cbv/Opaque.lean index f85246d1ce..6c0df1707b 100644 --- a/src/Lean/Meta/Tactic/Cbv/Opaque.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Cbv/TheoremsLookup.lean b/src/Lean/Meta/Tactic/Cbv/TheoremsLookup.lean index 96ebee6036..34c2bb99d1 100644 --- a/src/Lean/Meta/Tactic/Cbv/TheoremsLookup.lean +++ b/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 := {} diff --git a/src/Lean/Meta/Tactic/Cbv/Util.lean b/src/Lean/Meta/Tactic/Cbv/Util.lean index d732e01614..5c53ef5082 100644 --- a/src/Lean/Meta/Tactic/Cbv/Util.lean +++ b/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)