chore: generalize shifts (#650)

Co-authored-by: luisacicolini <[email protected]>
opencompl · Sep 24, 2024 · d770d3e · d770d3e
1 parent 6daa533
commit d770d3e
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -606,6 +606,11 @@ theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
     rw [Nat.mod_eq_of_eq]
     omega
 
+@[simp]
+theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
+    x <<< n &&& y <<< (m + n) = (x &&& y <<< m) <<< n := by
+  simp [BitVec.shiftLeft_and_distrib, BitVec.shiftLeft_add]
+
 @[simp]
 theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) :
     BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by