feat: complete BitVec.[getMsbD|getLsbD|msb] for shifts

src/Init/Data/BitVec/Lemmas.lean

@@ -463,6 +463,16 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
   simp [toInt_eq_toNat_cond]; omega
 
+theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
+  obtain ⟨a, ha⟩ := a
+  simp only [Nat.reducePow]
+  have acases : a = 0 ∨ a = 1 := by omega
+  rcases acases with ⟨rfl | rfl⟩
+  · simp
+  · case inr h =>
+    subst h
+    simp
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -1173,6 +1183,24 @@ theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
     · apply hn
   · apply Nat.pow_pos (by decide)
 
+theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
+    getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
+  simp only [getMsbD, Bool.if_false_left]
+  by_cases h : i < w
+  <;> by_cases h₁ : i < n
+  <;> by_cases h₂ : i - n < w
+  all_goals (simp [h, h₁, h₂]; try congr; try omega)
+  rw [BitVec.getLsbD_ge]
+  omega
+
+theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
+    (x.ushiftRight n).msb = if n > 0 then false else x.msb := by
+  induction n
+  case zero =>
+    simp
+  case succ n ih =>
+    simp [ih, ← BitVec.ushiftRight_eq, getMsbD_ushiftRight, BitVec.msb]
+
 /-! ### ushiftRight reductions from BitVec to Nat -/
 
 @[simp]
@@ -1181,6 +1209,7 @@ theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
 
 /-! ### sshiftRight -/
 
+
 theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
     x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i) := by
   apply BitVec.eq_of_toInt_eq
@@ -1322,11 +1351,44 @@ theorem not_sshiftRight_not {x : BitVec w} {n : Nat} :
     ~~~((~~~x).sshiftRight n) = x.sshiftRight n := by
   simp [not_sshiftRight]
 
+theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
+    getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by
+  simp only [getMsbD]
+  rw [BitVec.getLsbD_sshiftRight]
+  by_cases h : i < w
+  <;> by_cases h₁ : w ≤ w - 1 - i
+  <;> by_cases h₂ : ¬(i < n)
+  <;> by_cases h₃ : n + (w - 1 - i) < w
+  <;> by_cases h₄ : i - n < w
+  all_goals (simp [h, h₁, h₂, h₃, h₄]; try congr; try omega)
+  simp_all
+
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]
 theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl
 
+theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} :
+    getLsbD (x.sshiftRight' y) i =
+      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
+  simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
+
+theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
+    getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by
+  simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
+  by_cases h : i < w
+  <;> by_cases h₁ : w ≤ w - 1 - i
+  <;> by_cases h₂ : i < y.toNat
+  <;> by_cases h₃ : y.toNat + (w - 1 - i) < w
+  <;> by_cases h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat))
+  all_goals (simp [h, h₁, h₂, h₃, h₄]; try omega)
+  simp_all
+  omega
+
+theorem msb_sshiftRight' {x y: BitVec w} :
+    (x.sshiftRight' y).msb = x.msb := by
+  simp [BitVec.sshiftRight', BitVec.sshiftRight_msb_eq_msb]
+
 /-! ### udiv -/
 
 theorem udiv_eq {x y : BitVec n} : x.udiv y = BitVec.ofNat n (x.toNat / y.toNat) := by
@@ -1630,6 +1692,10 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
       · simp [hi₂]
       · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
 
+theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
+    (x <<< n).msb = x.getMsbD n := by
+  simp [BitVec.msb]
+
 @[deprecated shiftRight_add (since := "2024-06-02")]
 theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
     (x >>> n) >>> m = x >>> (n + m) := by
@@ -1910,6 +1976,11 @@ theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
   case succ n ih =>
     simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]
 
+theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### sub/neg -/
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
@@ -2019,6 +2090,11 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
     subst h'
     simp at h
 
+theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### abs -/
 
 @[simp, bv_toNat]
@@ -2086,6 +2162,11 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
   apply eq_of_toInt_eq
   simp
 
+theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### le and lt -/
 
 @[bv_toNat] theorem le_def {x y : BitVec n} :
@@ -2859,4 +2940,7 @@ abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true
 @[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
 abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
 
+@[deprecated sshiftRight_msb_eq_msb (since := "2024-10-03")]
+abbrev msb_sshiftRight := @sshiftRight_msb_eq_msb
+
 end BitVec