fix: make cbv_opaque take precedence over cbv_eval (#12908)

This PR makes `@[cbv_opaque]` unconditionally block all evaluation of a
constant
by `cbv`, including `@[cbv_eval]` rewrite rules. Previously,
`@[cbv_eval]` could
bypass `@[cbv_opaque]`, and for bare constants (not applications),
`isOpaqueConst`
could fall through to `handleConst` which would unfold the definition
body.

The intended usage pattern is now: mark subterm-producing functions
(like
`DHashMap.insert`) as `@[cbv_opaque]` to prevent unfolding, and provide
`@[cbv_eval]` theorems on the *consuming* function (like
`DHashMap.contains`)
which pattern-matches against the opaque subterms.

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

@@ -71,16 +71,16 @@ 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 equation or unfold theorems.
+  returned as-is without attempting any rewrite rules, 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.
+  before equation theorems.
 
 ## Unfolding order
 
-For a constant application, `handleApp` tries in 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:
 1. `@[cbv_eval]` rewrite rules
 2. Equation theorems (e.g. `foo.eq_1`, `foo.eq_2`)
 3. Unfold equations
@@ -150,15 +150,17 @@ def tryCbvTheorems : Simproc := fun e => do
   return result
 
 /--
-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.
+Post-pass handler for applications. For a constant-headed application, checks
+`@[cbv_opaque]` first, then tries `@[cbv_eval]` rules, equation/unfold theorems,
+and `reduceRecMatcher`. For a lambda-headed application, beta-reduces.
 -/
 def handleApp : Simproc := fun e => do
   unless e.isApp do return .rfl
   let fn := e.getAppFn
   match fn with
   | .const constName _ =>
+    if (← isCbvOpaque constName) then
+      return .rfl (done := true)
     let info ← getConstInfo constName
     tryCbvTheorems <|> (guardSimproc (fun _ => info.hasValue) handleConstApp) <|> reduceRecMatcher <| e
   | .lam .. => betaReduce e
@@ -166,15 +168,7 @@ def handleApp : Simproc := fun e => do
 
 def isOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
-  let hasTheorems := (← getCbvEvalLemmas constName).isSome
-  if hasTheorems then
-   let res ← (tryCbvTheorems) e
-    match res with
-    | .rfl false =>
-      return .rfl
-    | _ => return res
-  else
-    return .rfl (← isCbvOpaque constName)
+  return .rfl (← isCbvOpaque constName)
 
 def foldLit : Simproc := fun e => do
   let some n := e.rawNatLit? | return .rfl
@@ -285,7 +279,7 @@ def cbvPreStep : Simproc := fun e => do
   match e with
   | .lit .. => foldLit e
   | .proj .. => handleProj e
-  | .const .. => isOpaqueConst >> handleConst <| e
+  | .const .. => isOpaqueConst >> (tryCbvTheorems <|> handleConst) <| e
   | .app .. => tryMatcher <|> simplifyAppFn <| e
   | .letE .. =>
     if e.letNondep! then

tests/elab/cbv1.lean

@@ -171,8 +171,6 @@ example : Nat.brazilianFactorial 7 = 125411328000 := by
 
 attribute [cbv_opaque] Std.DHashMap.emptyWithCapacity
 attribute [cbv_opaque] Std.DHashMap.insert
-attribute [cbv_opaque] Std.DHashMap.getEntry
-attribute [cbv_opaque] Std.DHashMap.contains
 attribute [cbv_eval] Std.DHashMap.contains_emptyWithCapacity
 attribute [cbv_eval] Std.DHashMap.contains_insert
 
@@ -181,11 +179,11 @@ example : ((Std.DHashMap.emptyWithCapacity : Std.DHashMap Nat (fun _ => Nat)).in
     lhs
     cbv
 
-@[cbv_opaque] def opaque_const : Nat := Nat.zero
+def myConst : Nat := Nat.zero
 
-@[cbv_eval] theorem opaque_fn_spec : opaque_const = 0 := by rfl
+@[cbv_eval] theorem myConst_spec : myConst = 0 := by rfl
 
-example : opaque_const = 0 := by conv => lhs; cbv
+example : myConst = 0 := by conv => lhs; cbv
 
 def myAdd (m n : Nat) := match m with
 | 0 => n

tests/elab/cbv_eval_inv.lean

@@ -4,7 +4,7 @@ set_option cbv.warning false
 -- Basic test: inverted cbv_eval attribute
 -- The theorem `42 = myConst` with ← becomes `myConst = 42`
 -- so cbv can rewrite `myConst` to `42`
-@[cbv_opaque] def myConst : Nat := 42
+def myConst : Nat := 42
 
 @[cbv_eval ←] theorem myConst_eq : 42 = myConst := by rfl
 
@@ -16,7 +16,7 @@ example : myConst = 42 := by
 -- Test with a function application on the RHS
 def myAdd (a b : Nat) : Nat := a + b
 
-@[cbv_opaque] def myAddAlias (a b : Nat) : Nat := myAdd a b
+def myAddAlias (a b : Nat) : Nat := myAdd a b
 
 -- The theorem `myAdd a b = myAddAlias a b` with ← becomes `myAddAlias a b = myAdd a b`
 -- so cbv can rewrite `myAddAlias a b` to `myAdd a b`, which it can then evaluate
@@ -29,7 +29,7 @@ example : myAddAlias 2 3 = 5 := by
     cbv
 
 -- Test with <- syntax (alternative arrow)
-@[cbv_opaque] def myConst2 : Nat := 100
+def myConst2 : Nat := 100
 
 @[cbv_eval <-] theorem myConst2_eq : 100 = myConst2 := by rfl
 
@@ -39,7 +39,7 @@ example : myConst2 = 100 := by
     cbv
 
 -- Test that non-inverted cbv_eval still works
-@[cbv_opaque] def myConst3 : Nat := 7
+def myConst3 : Nat := 7
 
 @[cbv_eval] theorem myConst3_eq : myConst3 = 7 := by rfl
 
@@ -49,7 +49,7 @@ example : 7 = 7 := by
     cbv
 
 -- Test with the optional ident argument (backward compatibility)
-@[cbv_opaque] def myFn (n : Nat) : Nat := n + 1
+def myFn (n : Nat) : Nat := n + 1
 
 @[cbv_eval myFn] theorem myFn_zero : myFn 0 = 1 := by rfl
 

tests/elab/cbv_opaque_guard.lean

@@ -89,6 +89,25 @@ 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_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). -/
+
+def bareConst : Nat := 2 + 3
+@[cbv_eval] theorem bareConst_eq : bareConst = 5 := rfl
+
+example : bareConst = 5 := by conv => lhs; cbv
+
 /-! The kernel's `isDefEq` in `cbvGoalCore` still closes `@[cbv_opaque]` goals. -/
 
 example : secret = 42 := by cbv

tests/pkg/cbv_attr/CbvAttr/InvertedLocalTheorem.lean

@@ -2,7 +2,7 @@ module
 
 set_option cbv.warning false
 
-@[cbv_opaque] public def f7 (x : Nat) :=
+public def f7 (x : Nat) :=
   x + 1
 
 private axiom myAx : x + 1 = f7 x

tests/pkg/cbv_attr/CbvAttr/InvertedTheorem.lean

@@ -2,7 +2,7 @@ module
 
 set_option cbv.warning false
 
-@[cbv_opaque] public def f6 (x : Nat) :=
+public def f6 (x : Nat) :=
   x + 1
 
 private axiom myAx : x + 1 = f6 x

tests/pkg/cbv_attr/CbvAttr/PublicFunctionLocalTheorem.lean

@@ -2,7 +2,7 @@ module
 
 set_option cbv.warning false
 
-@[cbv_opaque] public def f2 (x : Nat) :=
+public def f2 (x : Nat) :=
   x + 1
 
 private axiom myAx :  f2 x = x + 1

tests/pkg/cbv_attr/CbvAttr/PublicFunctionPrivateTheorem.lean

@@ -2,7 +2,7 @@ module
 
 set_option cbv.warning false
 
-@[cbv_opaque] public def f5 (x : Nat) :=
+public def f5 (x : Nat) :=
   x + 1
 
 @[cbv_eval] private theorem f5_spec : f5 x = x + 1 := rfl

tests/pkg/cbv_attr/CbvAttr/PubliclyVisibleTheorem.lean

@@ -2,7 +2,7 @@ module
 
 set_option cbv.warning false
 
-@[cbv_opaque] public def f1 (x : Nat) :=
+public def f1 (x : Nat) :=
   x + 1
 
 private axiom myAx :  f1 x = x + 1