From 24380fc9009783fe2629143a9ab36dd534be8430 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Mon, 23 Feb 2026 11:46:57 +0000
Subject: [PATCH] feat: unfold nullary constants in `cbv` (#12646)

This PR enables the `cbv` tactic to unfold nullary (non-function)
constant
definitions such as `def myNat : Nat := 42`, allowing ground term
evaluation
(e.g. `evalEq`, `evalLT`) to recognize their values as literals.

Previously, `handleConst` skipped all nullary constants. Now it performs
direct
delta reduction using `instantiateValueLevelParams` instead of going
through
the equation theorem machinery (`getUnfoldTheorem`), which would trigger
`realizeConst` and fail for constants (such as derived typeclass
instances)
where `enableRealizationsForConst` has not been called.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Meta/Tactic/Cbv/Main.lean | 12 ++++----
 tests/lean/run/cbv_nullary.lean    | 46 ++++++++++++++++++++++++++++++
 2 files changed, 52 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/cbv_nullary.lean

diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index f4d6abd104..27547ebcff 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -233,16 +233,16 @@ def simplifyAppFn : Simproc := fun e => do
       return .step newValue newProof
 
 def handleConst : Simproc := fun e => do
-  let .const n _ := e | return .rfl
+  let .const n lvls := e | return .rfl
   let info ← getConstInfo n
   unless info.isDefinition do return .rfl
   let eType ← Sym.inferType e
   let eType ← whnfD eType
-  unless eType matches .forallE .. do
-    return .rfl
-  -- TODO: Check if we need to look if we applied all the levels correctly
-  let some thm ← getUnfoldTheorem n | return .rfl
-  Simproc.tryCatch (fun e => Theorem.rewrite thm e) e
+  if eType matches .forallE .. then return .rfl
+  unless info.hasValue && info.levelParams.length == lvls.length do return .rfl
+  let fBody ← instantiateValueLevelParams info lvls
+  let eNew ← Sym.share fBody
+  return .step eNew (← Sym.mkEqRefl eNew)
 
 /--
 Pre-pass structural dispatch. Routes each expression form to the appropriate handler:
diff --git a/tests/lean/run/cbv_nullary.lean b/tests/lean/run/cbv_nullary.lean
new file mode 100644
index 0000000000..b3058f011d
--- /dev/null
+++ b/tests/lean/run/cbv_nullary.lean
@@ -0,0 +1,46 @@
+set_option cbv.warning false
+
+/-! Tests for `cbv` evaluation of nullary (non-function) constants.
+
+Nullary definitions like `def myNat : Nat := 42` should be unfolded by `cbv`
+so that ground term evaluation (e.g. `evalEq`, `evalLT`) can recognize their
+values as literals.
+-/
+
+def myNat : Nat := 42
+
+-- Arithmetic: argument goes through pattern matching in Nat.add
+example : myNat + 1 = 43 := by cbv
+
+-- Direct equality
+example : myNat = 42 := by cbv
+
+-- Prop-level equality and comparisons
+example : (myNat = myNat) = True := by cbv
+example : (myNat = 42) = True := by cbv
+example : (myNat < 100) = True := by cbv
+example : (myNat ≤ 42) = True := by cbv
+
+-- Bool-level equality
+example : (myNat == 42) = true := by cbv
+
+-- Condition involving a nullary constant
+example : (if myNat = 42 then 1 else 0) = 1 := by cbv
+
+-- String nullary constant
+def myStr : String := "hello"
+
+example : myStr.length = 5 := by cbv
+example : (myStr = "hello") = True := by cbv
+
+-- Custom inductive type
+inductive Color where | red | green | blue
+
+def myColor : Color := .red
+
+def colorToNat : Color → Nat
+  | .red => 1
+  | .green => 2
+  | .blue => 3
+
+example : colorToNat myColor = 1 := by cbv