fix: support for Fin and BitVec literal normalization

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

@@ -225,6 +225,15 @@ builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
   let lit : Literal := { n, value := BitVec.ofInt n i }
   return .done { expr := lit.toExpr }
 
+/-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
+builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
+  unless e.isAppOfArity ``BitVec.ofNat 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some v ← Nat.fromExpr? e.appArg! | return .continue
+  let bv := BitVec.ofNat n v
+  if bv.toNat == v then return .continue -- already normalized
+  return .done { expr := { n, value := BitVec.ofNat n v : Literal }.toExpr }
+
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
 /-- Simplification procedure for `≤` on `BitVec`s. -/

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

@@ -69,9 +69,14 @@ builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred `
 builtin_simproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
-/-- Return `.done` for Fin values. We don't want to unfold in the symbolic evaluator. -/
-builtin_simproc [seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
-  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
-  return .done { expr := e }
+/-- Simplification procedure for ensuring `Fin` literals are normalized. -/
+builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
+  let some v ← fromExpr? e | return .continue
+  let v' ← Nat.fromExpr? e.appFn!.appArg!
+  if v.value == v' then
+    -- Design decision: should we return `.continue` instead of `.done` when simplifying.
+    -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
+    return .done { expr := e }
+  return .done { expr := v.toExpr }
 
 end Fin

tests/lean/run/bitvec_fin_literal_norm.lean

@@ -0,0 +1,21 @@
+open Std BitVec
+
+example : (5 : Fin 4) = x := by
+  simp
+  guard_target =ₛ 1 = x
+  sorry
+
+example : (1 : Fin 4) = x := by
+  fail_if_success simp
+  guard_target =ₛ 1 = x
+  sorry
+
+example : 17#4 = x := by
+  simp
+  guard_target =ₛ  1#4 = x
+  sorry
+
+example : (17 : BitVec 4) = x := by
+  simp
+  guard_target =ₛ  1#4 = x
+  sorry