feat: allow @[cbv_eval] to override @[cbv_opaque] (#12944)

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 <noreply@anthropic.com>

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

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