feat: add getMsbD_sshiftRight, getMsbD_sshiftRight', getLsbD_sshiftRight, getMsbD_ushiftRight

SSA/Projects/InstCombine/ForLean.lean

@@ -543,6 +543,121 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
 theorem zero_sub {x : BitVec w} : 0#w - x = - x := by
     simp [bv_toNat]
 
+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
+  · simp [h]
+    by_cases h₁ : w ≤ w - 1 - i
+    · have h₂ : ¬(i < n) := by omega
+      simp only [h, decide_True, h₁, Bool.not_true, Bool.false_and, Bool.and_false, h₂, ↓reduceIte,
+        Bool.true_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq]
+      omega
+    · simp only [h, decide_True, h₁, decide_False, Bool.not_false, Bool.true_and]
+      by_cases h₂ : ¬(i < n)
+      · have h₃ : n + (w - 1 - i) < w := by omega
+        have h₄ : i - n < w := by omega
+        simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and]
+        congr
+        omega
+      · simp_all
+        omega
+  · simp [h]
+
+-- this was basically copied from the analogous getLsbD_sshiftRight'
+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']
+  rcases hmsb : x.msb with rfl | rfl
+  · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right]
+    by_cases hi : i ≥ w
+    · simp only [hi, decide_True, Bool.not_true, Bool.false_and]
+      apply getLsbD_ge
+      omega
+    · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
+        decide_eq_true_eq]
+      intros hlsb
+      apply BitVec.lt_of_getLsbD hlsb
+  · by_cases hi : i ≥ w
+    · simp [hi]
+    · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and,
+        Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and,
+        Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
+        Nat.not_lt, decide_eq_true_eq]
+      omega
+
+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']
+  simp only [getMsbD]
+  rw [BitVec.getLsbD_sshiftRight]
+  by_cases h : i < w
+  · simp [h]
+    by_cases h₁ : w ≤ w - 1 - i
+    · have h₂ : (i < y.toNat) := by omega
+      simp [h₁, h₂]
+      omega
+    · -- if i only put simp_all it breaks. i am confused
+      simp [h₁]
+      simp_all
+      by_cases h₂ : y.toNat + (w - 1 - i) < w
+      · have h₃ : ¬(i < y.toNat) := by omega
+        have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega
+        -- if I put h₄ in the simp only it stops working. i am confused again
+        simp only [h, h₁, h₂, ↓reduceIte, h₃, Bool.iff_and_self, decide_eq_true_eq]
+        simp [h₄]
+        omega
+      · have h₃ : (i < y.toNat) := by omega
+        simp [h₂, h₃]
+  · simp [h]
+
+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
+  · simp [h]
+    by_cases h₁ : i < n
+    · simp [h₁]
+      rw [BitVec.getLsbD_ge]
+      omega
+    · have h₂ : (i - n < w) := by omega
+      simp [h₁, h₂]
+      congr
+      omega
+  · simp [h]
+
+theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
+    (x <<< n).msb = x.getMsbD n := by
+  simp [BitVec.msb]
+
+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 =>
+  -- if i remove the only here everything breaks. why?
+    simp only [gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true,
+      ↓reduceIte, ih, BitVec.msb, getMsbD_ushiftRight, Bool.and_false]
+
+-- this one exists already under the name : sshiftRight_msb_eq_msb
+-- theorem msb_sshiftRight {x : BitVec w} {n : Nat} :
+--     (x.sshiftRight n).msb = x.msb := by
+--   rw [sshiftRight_msb_eq_msb]
+
+-- got the proof from sshiftRight_msb_eq_msb
+theorem msb_sshiftRight' {x y: BitVec w} :
+    (x.sshiftRight' y).msb = x.msb := by
+  rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last]
+  by_cases hw₀ : w = 0
+  · simp [hw₀]
+  · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and,
+      ite_eq_right_iff]
+    intros h
+    simp [show y.toNat = 0 by omega]
+
 end BitVec
 
 namespace Bool