feat: simprocs for applying shiftLeft_shiftLeft and `shiftRight_shi…

…ftRight` (#4194)

src/Init/Data/BitVec/Lemmas.lean

@@ -705,7 +705,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
-theorem shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
+theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
     (x >>> n) >>> m = x >>> (n + m) := by
   ext i
   simp [Nat.add_assoc n m i]

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

@@ -8,6 +8,7 @@ import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Lemmas
 
 namespace BitVec
 open Lean Meta Simp
@@ -303,4 +304,25 @@ builtin_dsimproc [simp, seval] reduceBitVecToFin (BitVec.toFin _)  := fun e => d
   let some ⟨_, v⟩ ← getBitVecValue? v | return .continue
   return .done <| toExpr v.toFin
 
+/--
+Helper function for reducing `(x <<< i) <<< j` (and `(x >>> i) >>> j`) where `i` and `j` are
+natural number literals.
+-/
+@[inline] def reduceShiftShift (declName : Name) (thmName : Name) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName 6 do return .continue
+  let aux := e.appFn!.appArg!
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  unless aux.isAppOfArity declName 6 do return .continue
+  let x := aux.appFn!.appArg!
+  let some j ← Nat.fromExpr? aux.appArg! | return .continue
+  let i_add_j := toExpr (i + j)
+  let expr ← mkAppM declName #[x, i_add_j]
+  let proof ← mkAppM thmName #[x, aux.appArg!, e.appArg!]
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc reduceShiftLeftShiftLeft (((_ <<< _ : BitVec _) <<< _ : BitVec _)) :=
+  reduceShiftShift ``HShiftLeft.hShiftLeft ``shiftLeft_shiftLeft
+builtin_simproc reduceShiftRightShiftRight (((_ >>> _ : BitVec _) >>> _ : BitVec _)) :=
+  reduceShiftShift ``HShiftRight.hShiftRight ``shiftRight_shiftRight
+
 end BitVec

tests/lean/run/bitvec_simproc.lean

@@ -121,3 +121,19 @@ 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
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1#32) <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1) <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1) <<< 2 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1#32) <<< 2 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1#32) >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1) >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1) >>> 2 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1#32) >>> 2 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption