From 5e4c90c3d1cfe95ef8094e114ac8d42676d65966 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 12 Dec 2025 18:28:35 +0100
Subject: [PATCH] feat: bitvec literal internalization in `grind` (#11638)

This PR fixes bitvector literal internalization in `grind`. The fix
ensures theorems indexed by `BitVec.ofNat` are properly activated.
---
 src/Lean/Meta/Tactic/Grind/Internalize.lean    | 18 +++++++++++++++---
 .../lean/run/grind_internalize_bitvec_lit.lean |  7 +++++++
 2 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/grind_internalize_bitvec_lit.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 1ff7785b6f..d4857854ef 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -469,6 +469,20 @@ private def useFunCongrAtFn (f : Expr) : GrindM Bool := do
   let .const declName _ := f | return true
   useFunCongrAtDecl declName
 
+private def internalizeLiteral (e : Expr) (generation : Nat) (parent? : Option Expr) : GoalM Unit := do
+  -- We do not want to internalize the components of a literal value.
+  mkENode e generation
+  Solvers.internalize e parent?
+  /-
+  **Note**: Functions used to construct literals may be used for indexing theorem.
+  `OfNat.ofNat` is not used for indexing, but `BitVec.ofNat` is.
+  **Note**: We should revise whether we should normalize `BitVec.ofNat` to `OfNat.ofNat` in `grind`.
+  -/
+  if let .const declName _ := e.getAppFn then
+    unless declName == ``OfNat.ofNat do
+      updateIndicesFound (.const declName)
+      activateTheorems declName generation
+
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then
@@ -535,9 +549,7 @@ where
       mkENode' e generation
     | .app .. =>
       if (← isLitValue e) then
-        -- We do not want to internalize the components of a literal value.
-        mkENode e generation
-        Solvers.internalize e parent?
+        internalizeLiteral e generation parent?
       else if e.isAppOfArity ``Grind.MatchCond 1 then
         internalizeMatchCond e generation
       else e.withApp fun f args => do
diff --git a/tests/lean/run/grind_internalize_bitvec_lit.lean b/tests/lean/run/grind_internalize_bitvec_lit.lean
new file mode 100644
index 0000000000..590acda700
--- /dev/null
+++ b/tests/lean/run/grind_internalize_bitvec_lit.lean
@@ -0,0 +1,7 @@
+attribute [grind? =] BitVec.sdiv_zero
+
+example {x : BitVec 32} : x.sdiv 0#32 = 0#32 := by
+  grind
+
+example {x : BitVec 32} : x.sdiv 0#32 = 0#32 := by
+  grind -ext