From 8f6ade06ea2964d55625a9809f3349a0112aee04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 19 Mar 2026 11:23:57 +0000 Subject: [PATCH] fix: interaction between `cbv_opaque` and `inline` (#12981) This PR fixes the interaction between `cbv_opaque` and `inline`/`always_inline` annotations, to make sure that inlined definitions marked as `cbv_opaque` are not unfolded during the preprocessing stage of `cbv` tactic. --- src/Lean/Meta/Tactic/Cbv/Main.lean | 51 +++++++++++- tests/elab/cbv_opaque_inline.lean | 126 +++++++++++++++++++++++++++++ 2 files changed, 174 insertions(+), 3 deletions(-) create mode 100644 tests/elab/cbv_opaque_inline.lean diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 584244b0da..aded084c72 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -100,6 +100,51 @@ is marked done regardless of whether a rule fires. Otherwise it tries in order: namespace Lean.Meta.Tactic.Cbv open Lean.Meta.Sym.Simp +/-- Like `Sym.unfoldReducibleStep` but skips `@[cbv_opaque]` declarations. -/ +private def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do + let .const declName _ := e.getAppFn | return .continue + unless (← isReducible declName) do return .continue + if (← getEnv).isProjectionFn declName then return .continue + if (← isCbvOpaque declName) then return .continue + let some v ← unfoldDefinition? e | return .continue + return .visit v + +/-- Like `Sym.unfoldReducible` but skips `@[cbv_opaque]` declarations. -/ +private def unfoldReducible (e : Expr) : MetaM Expr := do + Meta.transform e (pre := unfoldReducibleStep) + +/-- Like `Sym.preprocessExpr` but skips `@[cbv_opaque]` declarations during unfolding. -/ +private def preprocessExpr (e : Expr) : Sym.SymM Expr := do + Sym.shareCommon (← unfoldReducible (← instantiateMVars e)) + +/-- Like `Sym.preprocessMVar` but skips `@[cbv_opaque]` declarations during unfolding. -/ +private def preprocessMVar (mvarId : MVarId) : Sym.SymM MVarId := do + let mvarDecl ← mvarId.getDecl + let lctx ← preprocessLCtx mvarDecl.lctx + let type ← preprocessExpr mvarDecl.type + let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances type .syntheticOpaque mvarDecl.userName + mvarId.assign mvarNew + return mvarNew.mvarId! +where + preprocessLCtx (lctx : LocalContext) : Sym.SymM LocalContext := do + let auxDeclToFullName := lctx.auxDeclToFullName + let mut fvarIdToDecl := {} + let mut decls := {} + let mut index := 0 + for decl in lctx do + let decl ← match decl with + | .cdecl _ fvarId userName type bi kind => + let type ← preprocessExpr type + pure <| LocalDecl.cdecl index fvarId userName type bi kind + | .ldecl _ fvarId userName type value nondep kind => + let type ← preprocessExpr type + let value ← preprocessExpr value + pure <| LocalDecl.ldecl index fvarId userName type value nondep kind + index := index + 1 + decls := decls.push (some decl) + fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl + return { fvarIdToDecl, decls, auxDeclToFullName } + public register_builtin_option cbv.warning : Bool := { defValue := true descr := "disable `cbv` usage warning" @@ -320,7 +365,7 @@ public def cbvEntry (e : Expr) : MetaM Result := do let simprocs ← getCbvSimprocs let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) } let methods := mkCbvMethods simprocs - let e ← Sym.unfoldReducible e + let e ← unfoldReducible e Sym.SymM.run do let e ← Sym.shareCommon e SimpM.run' (simp e) (methods := methods) (config := config) @@ -342,7 +387,7 @@ After all reductions, attempts `refl` to close equation goals of the form `v = v public def cbvGoal (mvarId : MVarId) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) } Sym.SymM.run do - let mvarId ← Sym.preprocessMVar mvarId + let mvarId ← preprocessMVar mvarId mvarId.withContext do let mut mvarIdNew := mvarId let mut toAssert : Array Hypothesis := #[] @@ -403,7 +448,7 @@ public def cbvDecideGoal (m : MVarId) : MetaM Unit := do | .error err => return m!"decide_cbv: {err.toMessageData}") do let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) } Sym.SymM.run do - let m ← Sym.preprocessMVar m + let m ← preprocessMVar m let mType ← m.getType let some (_, lhs, _) := mType.eq? | throwError "`decide_cbv`: expected goal of the form `decide _ = true`, got: {indentExpr mType}" diff --git a/tests/elab/cbv_opaque_inline.lean b/tests/elab/cbv_opaque_inline.lean new file mode 100644 index 0000000000..d8a9249055 --- /dev/null +++ b/tests/elab/cbv_opaque_inline.lean @@ -0,0 +1,126 @@ +set_option cbv.warning false + +/-! Test that `@[cbv_opaque]` is respected for `@[inline]` and `@[always_inline]` definitions. +These are reducible, so the preprocessing stage must skip them when they are also `@[cbv_opaque]`. -/ + +/-! ## `@[inline]` + `@[cbv_opaque]` -/ + +@[inline, cbv_opaque] def inlineSecret : Nat := 42 + +/-- +error: unsolved goals +⊢ inlineSecret = 42 +-/ +#guard_msgs in +example : inlineSecret = 42 := by conv => lhs; cbv + +@[inline, cbv_opaque] def inlineAdd (a b : Nat) : Nat := a + b + +/-- +error: unsolved goals +⊢ inlineAdd 1 2 = 3 +-/ +#guard_msgs in +example : inlineAdd 1 2 = 3 := by conv => lhs; cbv + +/-! ## `@[always_inline]` + `@[cbv_opaque]` -/ + +@[always_inline, cbv_opaque] def alwaysInlineSecret : Nat := 99 + +/-- +error: unsolved goals +⊢ alwaysInlineSecret = 99 +-/ +#guard_msgs in +example : alwaysInlineSecret = 99 := by conv => lhs; cbv + +@[always_inline, cbv_opaque] def alwaysInlineMul (a b : Nat) : Nat := a * b + +/-- +error: unsolved goals +⊢ alwaysInlineMul 3 4 = 12 +-/ +#guard_msgs in +example : alwaysInlineMul 3 4 = 12 := by conv => lhs; cbv + +/-! ## `@[cbv_eval]` overrides `@[cbv_opaque]` even for inline definitions -/ + +@[inline, cbv_opaque] def inlineOpaqueAdd (a b : Nat) : Nat := a + b +@[cbv_eval] theorem inlineOpaqueAdd_eq (a b : Nat) : inlineOpaqueAdd a b = a + b := rfl + +example : inlineOpaqueAdd 1 2 = 3 := by conv => lhs; cbv + +@[always_inline, cbv_opaque] def alwaysInlineOpaqueMul (a b : Nat) : Nat := a * b +@[cbv_eval] theorem alwaysInlineOpaqueMul_eq (a b : Nat) : alwaysInlineOpaqueMul a b = a * b := rfl + +example : alwaysInlineOpaqueMul 3 4 = 12 := by conv => lhs; cbv + +/-! ## Inline definitions without `@[cbv_opaque]` still unfold normally -/ + +@[inline] def inlineNormal (n : Nat) : Nat := n + 1 + +example : inlineNormal 5 = 6 := by cbv + +@[always_inline] def alwaysInlineNormal (n : Nat) : Nat := n * 2 + +example : alwaysInlineNormal 5 = 10 := by cbv + +/-! ## `@[cbv_opaque]` + `@[inline]` with `cbvGoal` (uses `preprocessMVar`) -/ + +/-- The kernel's `isDefEq` in `cbvGoal` still closes inline opaque goals. -/ +example : inlineSecret = 42 := by cbv +example : alwaysInlineSecret = 99 := by cbv + +/-! ## `@[cbv_opaque]` + `@[inline]` used as argument to a non-opaque function -/ + +def mySucc (n : Nat) : Nat := n + 1 + +/-- +error: unsolved goals +⊢ inlineSecret.succ = 43 +-/ +#guard_msgs in +example : mySucc inlineSecret = 43 := by conv => lhs; cbv + +/-! ## Pattern matching on `@[cbv_opaque]` + `@[inline]` discriminant gets stuck -/ + +def isEven : Nat → Bool + | 0 => true + | 1 => false + | n + 2 => isEven n + +/-- +error: unsolved goals +⊢ (match inlineSecret with + | 0 => true + | 1 => false + | a.succ.succ => isEven a) = + true +-/ +#guard_msgs in +example : isEven inlineSecret = true := by conv => lhs; cbv + +/-! ## Projections on `@[cbv_opaque]` + `@[inline]` structures are not reduced -/ + +@[inline, cbv_opaque] def inlinePair : Nat × Nat := (10, 20) + +/-- +error: unsolved goals +⊢ inlinePair.1 = 10 +-/ +#guard_msgs in +example : inlinePair.1 = 10 := by conv => lhs; cbv + +/-! ## `decide_cbv` with `@[cbv_opaque]` + `@[inline]` -/ + +@[inline, cbv_opaque] def inlineBoolVal : Bool := true +@[cbv_eval] theorem inlineBoolVal_eq : inlineBoolVal = true := rfl + +example : inlineBoolVal = true := by decide_cbv + +/-! Without `@[cbv_eval]`, `decide_cbv` gets stuck on inline opaque -/ + +@[inline, cbv_opaque] def inlineBoolStuck : Bool := true + +#guard_msgs (drop error) in +example : inlineBoolStuck = true := by decide_cbv