From bb264e1ff02824b7916feee7a4cba4ec0c2328b9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 12 Dec 2025 18:50:38 +0100
Subject: [PATCH] feat: `BitVec.ofNat` in `grind lia` (#11640)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds support for `BitVec.ofNat` in `grind lia`. Example:

```lean
example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
  grind
```
---
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean | 10 ++++++++--
 tests/lean/run/grind_cutsat_toint_1.lean           |  6 ++++++
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
index db2daab0be..5bf95b8f1d 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean
@@ -422,6 +422,13 @@ private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
       if let some (k, neZeroInst) ← isFinInstOfNat? inst then
         let h := mkApp2 (mkConst ``Lean.Grind.ofNat_FinZero) k neZeroInst
         return (mkIntLit 0, h)
+    toIntOfNat e n
+  | BitVec.ofNat _ n =>
+    let some n ← getNatValue? n | mkToIntVar e
+    toIntOfNat e n
+  | _ => mkToIntVar e
+where
+  toIntOfNat (e : Expr) (n : Nat) : ToIntM (Expr × Expr) := do
     let some thm ← getOfNatThm? | mkToIntVar e
     let h := mkApp thm (toExpr n)
     if (← hasNumericLoHi) then
@@ -429,8 +436,7 @@ private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
       return (r, h)
     else
       expandWrap e (mkIntLit n) h
-  | _ => mkToIntVar e
-where
+
   toIntBin (toIntOp : ToIntThms) (mkBinOp : Expr → Expr → Expr) (a b : Expr) : ToIntM (Expr × Expr) := do
     unless toIntOp.c?.isSome do return (← mkToIntVar e)
     let (a', h₁) ← toInt' a
diff --git a/tests/lean/run/grind_cutsat_toint_1.lean b/tests/lean/run/grind_cutsat_toint_1.lean
index 10df6531fe..061d08f692 100644
--- a/tests/lean/run/grind_cutsat_toint_1.lean
+++ b/tests/lean/run/grind_cutsat_toint_1.lean
@@ -117,3 +117,9 @@ example {n : Nat} (x y : Fin ((n + 1) + 1)) (h₂ : ¬x = y) (h : ¬x < y) : y <
 
 example {n m : Nat} (x : BitVec n) : 2 ≤ n → n ≤ m → m = 2 → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 := by
   grind
+
+example (x : BitVec 8) : x > 2#8 → x > 1#8 := by
+  grind
+
+example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
+  grind