feat: simprocs for reducing x >>> i and x <<< i where i is a bi…

…ttvector literal (#4193)

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

@@ -78,6 +78,16 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   let some i ← Nat.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op v.value i)
 
+/--
+Helper function for reducing `x <<< i` and `x >>> i` where `i` is a bitvector literal,
+into one that is a natural number literal.
+-/
+@[inline] def reduceShiftWithBitVecLit (declName : Name) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity declName 6 do return .continue
+  let v := e.appFn!.appArg!
+  let some i ← fromExpr? e.appArg! | return .continue
+  return .visit (← mkAppM declName #[v, toExpr i.value.toNat])
+
 /--
 Helper function for reducing bitvector predicates.
 -/
@@ -158,9 +168,15 @@ builtin_dsimproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
   reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/
+builtin_dsimproc [simp, seval] reduceHShiftLeft' ((_ <<< (_ : BitVec _) : BitVec _)) :=
+  reduceShiftWithBitVecLit ``HShiftLeft.hShiftLeft
 /-- Simplification procedure for shift right on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
   reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·)
+/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/
+builtin_dsimproc [simp, seval] reduceHShiftRight' ((_ >>> (_ : BitVec _) : BitVec _)) :=
+  reduceShiftWithBitVecLit ``HShiftRight.hShiftRight
 /-- Simplification procedure for rotate left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
   reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft

tests/lean/run/bitvec_simproc.lean

@@ -113,3 +113,11 @@ example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ1019#10 = x; assumption
 example (h : 5#10 = x) : -signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ5#10 = x; assumption
+example (h : 40#32 = b) : 10#32 <<< 2#32 = b := by
+  simp; guard_target =ₛ 40#32 = b; assumption
+example (h : 3#32 = b) : 12#32 >>> 2#32 = b := by
+  simp; guard_target =ₛ 3#32 = b; assumption
+example (a : BitVec 32) (h : a >>> 2 = b) : a >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 2 = b; assumption
+example (a : BitVec 32) (h : a <<< 2 = b) : a <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 2 = b; assumption