fix: bitvec simproc bug (#14370)

This PR fixes a bug in the `BitVec` simproc when `bitVecOfNat := false`.
This bug
affects `grind` since it uses `bitVecOfNat := false`. Here is an example
reported by Henrik
that exposed the issue.

```lean
example (x : BitVec 4) (_h1 : x = 0#2 ++ 1#2) (_h2 : x = 1#4) : True := by
  grind
```

It also removes a redundant `grind` theorem, and adds support for
normalizing terms such as `0#n` when `bitVecOfNat := false`.

Author: leodemoura

src/Init/Data/BitVec/Basic.lean

@@ -45,7 +45,8 @@ instance instNatCast : NatCast (BitVec w) where
 
 /-- Theorem for normalizing the bitvector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
-@[simp, bitvec_to_nat, grind =] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
+-- **Note**: `grind` normal form for bitvector literals uses `OfNat.ofNat`. Thus, we should not mark this theorem as a `grind` theorem.
+@[simp, bitvec_to_nat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
 
 -- Note. Mathlib would like this to go the other direction.
 @[simp] theorem natCast_eq_ofNat (w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x := rfl

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -241,11 +241,22 @@ builtin_dsimproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   let_expr BitVec.ofNat n v ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
   let some v ← Nat.fromExpr? v | return .continue
-  let bv := BitVec.ofNat n v
-  if bv.toNat == v then return .continue -- already normalized
-  return .done <| (← toExpr' (BitVec.ofNat n v))
+  if let some n ← Nat.fromExpr? n then
+    let bv := BitVec.ofNat n v
+    -- `BitVec.ofNat` is the normal form only when `bitVecOfNat := true`; otherwise
+    -- literals must be rewritten to the `OfNat.ofNat` form produced by `toExpr'`.
+    if bv.toNat == v && (← Simp.getConfig).bitVecOfNat then return .continue -- already normalized
+    return .done (← toExpr' (BitVec.ofNat n v))
+  else if (← Simp.getConfig).bitVecOfNat then
+    return .continue
+  else
+    /-
+    **Note** If `bitVecOfNat := false`, we still want to convert terms such as `0#n` to the `OfNat.ofNat` form.
+    Recall that `grind` uses `bitVecOfNat := false`, but many bit-vector theorems such as `sdiv_zero` are stated using
+    terms such as `0#n`. These theorems will not be applicable to terms `x.sdiv 0#32` since `0#32` is normalized using `OfNat.ofNat`.
+    -/
+    return .done (← mkNumeral (mkApp (mkConst ``BitVec) n) v)
 
 /-- Simplification procedure for `=` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceEq  (( _ : BitVec _) = _)  := reduceBinPred ``Eq 3 (. = .)

tests/elab/grind_bitvec_lit_norm.lean

@@ -0,0 +1,17 @@
+/-!
+Tests that `grind` normalizes `BitVec.ofNat` literals (e.g. `1#4`) to the same canonical
+form used for other evaluated bitvector literals. `grind` normalization uses the config
+`bitVecOfNat := false`, so `BitVec.reduceOfNat` must rewrite `1#4` to the `OfNat.ofNat`
+form; otherwise `1#4` and the result of reducing `0#2 ++ 1#2` are treated as two distinct
+interpreted values, and `grind` produces an invalid inconsistency proof rejected by the
+kernel.
+-/
+
+example (x : BitVec 4) (_h1 : x = 0#2 ++ 1#2) (_h2 : x = 1#4) : True := by
+  grind
+
+example (x : BitVec 4) (h : x = 0#2 ++ 1#2) : x = 1#4 := by
+  grind
+
+example (x : BitVec 4) (h1 : x = 0#2 ++ 1#2) (h2 : x = 2#4) : False := by
+  grind

tests/elab/grind_internalize_bitvec_lit.lean.out.expected

@@ -1 +1 @@
-BitVec.sdiv_zero: [@BitVec.sdiv #1 #0 (BitVec.ofNat #1 `[0])]
+BitVec.sdiv_zero: [@BitVec.sdiv #1 #0 (@OfNat.ofNat (BitVec _) `[0] _)]