feat: BitVec.shiftLeft_shiftLeft, BitVec.shiftRight_shiftRight (leanp…

…rover#4148) Closes two `sorry`s at https://github.com/leanprover/leansat/pull/64/files. --------- Co-authored-by: Kim Morrison <[email protected]>
opencompl · May 13, 2024 · a17c3f4 · a17c3f4
1 parent 799923d
commit a17c3f4
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -608,6 +608,17 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
 
+theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x <<< n) <<< m = x <<< (n + m) := by
+  ext i
+  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
+  rw [show i - (n + m) = (i - m - n) by omega]
+  cases h₂ : decide (i < m) <;>
+  cases h₃ : decide (i - m < w) <;>
+  cases h₄ : decide (i - m < n) <;>
+  cases h₅ : decide (i < n + m) <;>
+    simp at * <;> omega
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -693,6 +704,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
+theorem BitVec.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]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :