From 00a809eb199a1afbc82eb0a45c584576dce17235 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Fri, 13 Mar 2026 13:29:59 +0000 Subject: [PATCH] fix: interaction of `cbv_eval` and `cbv_opaque` attributes --- src/Lean/Meta/Tactic/Cbv/Main.lean | 28 ++++++++----------- tests/elab/cbv1.lean | 8 ++---- tests/elab/cbv_eval_inv.lean | 10 +++---- tests/elab/cbv_opaque_guard.lean | 19 +++++++++++++ .../CbvAttr/InvertedLocalTheorem.lean | 2 +- .../pkg/cbv_attr/CbvAttr/InvertedTheorem.lean | 2 +- .../CbvAttr/PublicFunctionLocalTheorem.lean | 2 +- .../CbvAttr/PublicFunctionPrivateTheorem.lean | 2 +- .../CbvAttr/PubliclyVisibleTheorem.lean | 2 +- 9 files changed, 43 insertions(+), 32 deletions(-) diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 036448d2fa15..cefe8baa89d0 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/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 diff --git a/tests/elab/cbv1.lean b/tests/elab/cbv1.lean index ab493972ac1b..5a963b5dde85 100644 --- a/tests/elab/cbv1.lean +++ b/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 diff --git a/tests/elab/cbv_eval_inv.lean b/tests/elab/cbv_eval_inv.lean index c869a1cafe6d..afdba59e4403 100644 --- a/tests/elab/cbv_eval_inv.lean +++ b/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 diff --git a/tests/elab/cbv_opaque_guard.lean b/tests/elab/cbv_opaque_guard.lean index 300668c8e469..588a01bdfe25 100644 --- a/tests/elab/cbv_opaque_guard.lean +++ b/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 diff --git a/tests/pkg/cbv_attr/CbvAttr/InvertedLocalTheorem.lean b/tests/pkg/cbv_attr/CbvAttr/InvertedLocalTheorem.lean index c82353823194..d1d92589ae47 100644 --- a/tests/pkg/cbv_attr/CbvAttr/InvertedLocalTheorem.lean +++ b/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 diff --git a/tests/pkg/cbv_attr/CbvAttr/InvertedTheorem.lean b/tests/pkg/cbv_attr/CbvAttr/InvertedTheorem.lean index af852aa4f299..62bdc4199d98 100644 --- a/tests/pkg/cbv_attr/CbvAttr/InvertedTheorem.lean +++ b/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 diff --git a/tests/pkg/cbv_attr/CbvAttr/PublicFunctionLocalTheorem.lean b/tests/pkg/cbv_attr/CbvAttr/PublicFunctionLocalTheorem.lean index a61afac85f93..29d879415575 100644 --- a/tests/pkg/cbv_attr/CbvAttr/PublicFunctionLocalTheorem.lean +++ b/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 diff --git a/tests/pkg/cbv_attr/CbvAttr/PublicFunctionPrivateTheorem.lean b/tests/pkg/cbv_attr/CbvAttr/PublicFunctionPrivateTheorem.lean index cc405ba20aa6..ebf7cb531f1a 100644 --- a/tests/pkg/cbv_attr/CbvAttr/PublicFunctionPrivateTheorem.lean +++ b/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 diff --git a/tests/pkg/cbv_attr/CbvAttr/PubliclyVisibleTheorem.lean b/tests/pkg/cbv_attr/CbvAttr/PubliclyVisibleTheorem.lean index 411a0ab0cc5b..7492be89ee26 100644 --- a/tests/pkg/cbv_attr/CbvAttr/PubliclyVisibleTheorem.lean +++ b/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