From 6160d17e2d292d6afbd38afafaa0496a1017917b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Tue, 17 Mar 2026 13:08:21 +0000 Subject: [PATCH] feat: allow `@[cbv_eval]` to override `@[cbv_opaque]` (#12944) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes the interaction between `@[cbv_opaque]` and `@[cbv_eval]` attributes in the `cbv` tactic. Previously, `@[cbv_opaque]` completely blocked all reduction including `@[cbv_eval]` rewrite rules. Now, `@[cbv_eval]` rules can fire on `@[cbv_opaque]` constants, allowing users to provide custom rewrite rules without exposing the full definition. Equation theorems, unfold theorems, and kernel reduction remain suppressed for opaque constants. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- src/Lean/Meta/Tactic/Cbv/Main.lean | 39 ++++++++-------- tests/elab/cbv_opaque_guard.lean | 71 +++++++++++++++++++++++++++--- 2 files changed, 86 insertions(+), 24 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index cefe8baa89..584244b0da 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -70,17 +70,20 @@ There are also places where we deviate from strict call-by-value semantics: ## Attributes -- `@[cbv_opaque]`: prevents `cbv` from unfolding a definition. The constant is - returned as-is without attempting any rewrite rules, equation or unfold theorems. +- `@[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. + before equation theorems and can override `@[cbv_opaque]`. ## Unfolding order -For a constant application, `handleApp` first checks `@[cbv_opaque]` — if the -constant is opaque, it is returned as-is immediately. Otherwise it tries in 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 @@ -127,13 +130,6 @@ def tryUnfold : Simproc := fun e => do trace[Meta.Tactic.cbv.unfold] "unfold `{appFn}`:{indentExpr e}\n==>{indentExpr e'}" return result -/-- 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) - else - tryEquations <|> tryUnfold <| e - def betaReduce : Simproc := fun e => do -- TODO: Improve term sharing let new := e.headBeta @@ -149,9 +145,14 @@ def tryCbvTheorems : Simproc := fun e => do trace[Meta.Tactic.cbv.rewrite] "@[cbv_eval] `{fnName}`:{indentExpr e}\n==>{indentExpr e'}" return result +/-- Try equation theorems, then unfold equations. -/ +def handleConstApp : Simproc := fun e => do + tryEquations <|> tryUnfold <| e + /-- -Post-pass handler for applications. For a constant-headed application, checks -`@[cbv_opaque]` first, then tries `@[cbv_eval]` rules, equation/unfold theorems, +Post-pass handler for applications. For a constant-headed application, if the +constant is `@[cbv_opaque]`, only `@[cbv_eval]` rules are tried (and the result +is marked done). Otherwise tries `@[cbv_eval]` rules, equation/unfold theorems, and `reduceRecMatcher`. For a lambda-headed application, beta-reduces. -/ def handleApp : Simproc := fun e => do @@ -160,15 +161,17 @@ def handleApp : Simproc := fun e => do match fn with | .const constName _ => if (← isCbvOpaque constName) then - return .rfl (done := true) + return (← tryCbvTheorems e).markAsDone let info ← getConstInfo constName tryCbvTheorems <|> (guardSimproc (fun _ => info.hasValue) handleConstApp) <|> reduceRecMatcher <| e | .lam .. => betaReduce e | _ => return .rfl -def isOpaqueConst : Simproc := fun e => do +def handleOpaqueConst : Simproc := fun e => do let .const constName _ := e | return .rfl - return .rfl (← isCbvOpaque constName) + if (← isCbvOpaque constName) then + return (← tryCbvTheorems e).markAsDone + return .rfl def foldLit : Simproc := fun e => do let some n := e.rawNatLit? | return .rfl @@ -279,7 +282,7 @@ def cbvPreStep : Simproc := fun e => do match e with | .lit .. => foldLit e | .proj .. => handleProj e - | .const .. => isOpaqueConst >> (tryCbvTheorems <|> handleConst) <| e + | .const .. => handleOpaqueConst >> (tryCbvTheorems <|> handleConst) <| e | .app .. => tryMatcher <|> simplifyAppFn <| e | .letE .. => if e.letNondep! then diff --git a/tests/elab/cbv_opaque_guard.lean b/tests/elab/cbv_opaque_guard.lean index 588a01bdfe..5e0019ed94 100644 --- a/tests/elab/cbv_opaque_guard.lean +++ b/tests/elab/cbv_opaque_guard.lean @@ -89,16 +89,11 @@ def normalPair : Nat × Nat := (10, 20) example : normalPair.1 = 10 := by cbv example : normalPair.2 = 20 := by cbv -/-! `@[cbv_opaque]` takes precedence over `@[cbv_eval]`. -/ +/-! `@[cbv_eval]` can override `@[cbv_opaque]`. -/ @[cbv_opaque] def opaqueAdd (a b : Nat) : Nat := a + b @[cbv_eval] theorem opaqueAdd_eq (a b : Nat) : opaqueAdd a b = a + b := rfl -/-- -error: unsolved goals -⊢ opaqueAdd 1 2 = 3 --/ -#guard_msgs in example : opaqueAdd 1 2 = 3 := by conv => lhs; cbv /-! `@[cbv_eval]` works on bare constants (no arguments). -/ @@ -112,3 +107,67 @@ example : bareConst = 5 := by conv => lhs; cbv example : secret = 42 := by cbv example : secretPair.1 = 10 := by cbv + +/-! ## Interaction of `@[cbv_opaque]` and `@[cbv_eval]` -/ + +/-! `@[cbv_eval]` on an opaque bare constant rewrites it. -/ + +@[cbv_opaque] def opaqueConst : Nat := 99 +@[cbv_eval] theorem opaqueConst_eq : opaqueConst = 99 := rfl + +example : opaqueConst = 99 := by conv => lhs; cbv + +/-! `@[cbv_eval]` on an opaque function fires and the result is further reduced. -/ + +@[cbv_opaque] def opaqueMul (a b : Nat) : Nat := a * b +@[cbv_eval] theorem opaqueMul_eq (a b : Nat) : opaqueMul a b = a * b := rfl + +example : opaqueMul 3 4 + 1 = 13 := by conv => lhs; cbv + +/-! Without `@[cbv_eval]`, an opaque constant stays stuck (cbv_opaque alone blocks). -/ + +@[cbv_opaque] def pureOpaque : Nat := 7 + +/-- +error: unsolved goals +⊢ pureOpaque = 7 +-/ +#guard_msgs in +example : pureOpaque = 7 := by conv => lhs; cbv + +/-! `@[cbv_eval ←]` (inverted) also works with `@[cbv_opaque]`. -/ + +@[cbv_opaque] def opaqueAlias : Nat := 42 +@[cbv_eval ←] theorem opaqueAlias_eq : 42 = opaqueAlias := rfl + +example : opaqueAlias = 42 := by conv => lhs; cbv + +/-! `@[cbv_opaque]` with `@[cbv_eval]` still prevents unfolding of the definition itself. -/ + +@[cbv_opaque] def opaquePartial (n : Nat) : Nat := n * n +-- Only provide a rule for the specific case n=5 +@[cbv_eval] theorem opaquePartial_5 : opaquePartial 5 = 25 := rfl + +example : opaquePartial 5 = 25 := by conv => lhs; cbv + +-- No rule for n=3, so it stays stuck +/-- +error: unsolved goals +⊢ opaquePartial 3 = 9 +-/ +#guard_msgs in +example : opaquePartial 3 = 9 := by conv => lhs; cbv + +/-! Opaque constant used as argument to a non-opaque function stays opaque. -/ + +def double (n : Nat) : Nat := n + n + +/-- +error: unsolved goals +⊢ (match pureOpaque, pureOpaque with + | a, Nat.zero => a + | a, b.succ => (a.add b).succ) = + 14 +-/ +#guard_msgs in +example : double pureOpaque = 14 := by conv => lhs; cbv