From 3b2944205b2fa4e54a98eba94f389b78d93cd26a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 12 Feb 2026 10:31:17 +0000 Subject: [PATCH] doc: improve docstrings for `cbv` and `decide_cbv` (#12439) This PR improves docstrings for `cbv` and `decide_cbv` tactics --- src/Init/Conv.lean | 15 +++++++++++++-- src/Init/Tactics.lean | 11 ++++++++++- 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 9b906d4317..13d983226b 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -51,8 +51,19 @@ scoped syntax (name := withAnnotateState) /-- `skip` does nothing. -/ syntax (name := skip) "skip" : conv -/-- `cbv` performs simplification that closely mimics call-by-value evaluation, -using equations associated with definitions and the matchers. -/ +/-- +`cbv` performs simplification that closely mimics call-by-value evaluation. +It reduces the target term by unfolding definitions using their defining equations and +applying matcher equations. The unfolding is propositional, so `cbv` also works +with functions defined via well-founded recursion or partial fixpoints. + +The proofs produced by `cbv` only use the three standard axioms. +In particular, they do not require trust in the correctness of the code +generator. + +This tactic is experimental and its behavior is likely to change in upcoming +releases of Lean. +-/ syntax (name := cbv) "cbv" : conv /-- diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index d942e7e313..16f301c5bc 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -2299,7 +2299,8 @@ macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic => /-- `cbv` performs simplification that closely mimics call-by-value evaluation. It reduces terms by unfolding definitions using their defining equations and -applying matcher equations. +applying matcher equations. The unfolding is propositional, so `cbv` also works +with functions defined via well-founded recursion or partial fixpoints. `cbv` has built-in support for goals of the form `lhs = rhs`. It proceeds in two passes: @@ -2313,6 +2314,10 @@ two passes: (simpler) equality goal. For goals that are not equalities, `cbv` currently leaves the goal unchanged. +The proofs produced by `cbv` only use the three standard axioms. +In particular, they do not require trust in the correctness of the code +generator. + This tactic is experimental and its behavior is likely to change in upcoming releases of Lean. -/ @@ -2329,6 +2334,10 @@ is a `Decidable` proposition. It proceeds in two steps: Unlike `cbv`, `decide_cbv` is a terminal tactic: it either closes the goal or fails. +The proofs produced by `decide_cbv` only use the three standard axioms. +In particular, they do not require trust in the correctness of the code +generator. + This tactic is experimental and its behavior is likely to change in upcoming releases of Lean. -/