feat: BitVec.toInt_sshiftRight

src/Init/Data/BitVec/Lemmas.lean

@@ -14,6 +14,7 @@ import Init.Data.Nat.Mod
 import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.Pow
+import Init.Data.Int.LemmasAux
 
 set_option linter.missingDocs true
 
@@ -235,12 +236,16 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
 theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp [← getLsbD_eq_getElem]
 
 theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+theorem toInt_zero_length (x : BitVec 0) : x.toInt = 0 := by simp [of_length_zero]
+
 theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp
 theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp
 theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by
   subst h; simp [toNat_zero_length]
+theorem toInt_of_zero_length (h : w = 0) (x : BitVec w) : x.toInt = 0 := by
+  subst h; simp [toInt_zero_length]
 theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by
   subst h; simp [getLsbD_zero_length]
 theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by
@@ -608,6 +613,14 @@ theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem toInt_lt' {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by
+  by_cases h : w = 0
+  · subst h
+    simp [eq_nil x]
+  · have := @toInt_lt w x
+    rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this
+    omega
+
 /--
 `x.toInt` is greater than or equal to `-2^(w-1)`.
 We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
@@ -620,6 +633,14 @@ theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem le_toInt' {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by
+  by_cases h : w = 0
+  · subst h
+    simp [eq_nil x]
+  · have := @le_toInt w x
+    rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this
+    omega
+
 /-! ### slt -/
 
 /--
@@ -1833,6 +1854,46 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
         by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
   · simp [h]
 
+theorem toInt_le_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt ≤ 0 := by
+  simp only [BitVec.toInt]
+  have : 2 * x.toNat ≥ 2 ^ w := msb_eq_true_iff_two_mul_ge.mp h
+  omega
+
+theorem le_toInt_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt := by
+  simp only [BitVec.toInt]
+  have : 2 * x.toNat < 2 ^ w := msb_eq_false_iff_two_mul_lt.mp h
+  omega
+
+theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} :
+    x.toInt >>> n < 2 ^ (w - 1) := by
+  have := Int.shiftRight_le_of_nonneg x.toInt n
+  have := Int.shiftRight_le_of_nonpos x.toInt n
+  have := @BitVec.toInt_lt' w x
+  have := @Nat.one_le_two_pow (w-1)
+  norm_cast at *
+  omega
+
+theorem lt_toInt_shiftRight {x : BitVec w} {n : Nat} :
+    -(2 ^ (w - 1)) ≤ x.toInt >>> n := by
+  have := Int.le_shiftRight_of_nonpos x.toInt n
+  have := Int.le_shiftRight_of_nonneg x.toInt n
+  have := @BitVec.le_toInt' w x
+  have := @Nat.one_le_two_pow (w-1)
+  norm_cast at *
+  omega
+
+@[simp]
+theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
+    (x.sshiftRight n).toInt = x.toInt >>> n := by
+  by_cases h : w = 0
+  · subst h
+    simp [BitVec.eq_nil x]
+  · rw [sshiftRight, toInt_ofInt, ←Nat.two_pow_pred_add_two_pow_pred (by omega)]
+    have := @toInt_shiftRight_lt w x n
+    have := @lt_toInt_shiftRight w x n
+    norm_cast at *
+    exact Int.bmod_eq_of_le_of_lt (by omega) (by omega)
+
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -38,4 +38,48 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
+theorem le_shiftRight_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : n ≤ n >>> s := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp
+    simp [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · omega
+  case _ _ _ m =>
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      omega
+
+theorem shiftRight_le_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : n >>> s ≤ n := by
+  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
+  split
+  case _ _ _ m =>
+    simp only [Int.ofNat_eq_coe] at h
+    by_cases hm : m = 0
+    · simp [hm]
+    · have := Nat.shiftRight_le m s
+      simp
+      omega
+  case _ _ _ m =>
+    omega
+
+theorem le_shiftRight_of_nonneg (n : Int) (s : Nat) (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have := @Nat.pow_pos 2 s (by omega)
+    have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega)
+    norm_cast at *
+
+theorem shiftRight_le_of_nonpos (n : Int) (s : Nat) (h : n ≤ 0) : (n >>> s) ≤ 0 := by
+  rw [Int.shiftRight_eq_div_pow]
+  by_cases h' : s = 0
+  · simp [h', h]
+  · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega)
+    have rl : n / 2 ^ s ≤ 0 := Int.ediv_neg_of_neg_of_pos (by omega) (by norm_cast at *; omega)
+    norm_cast at *
+
 end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -484,6 +484,9 @@ theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
 theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by
   rw [← add_emod_self_left]; rfl
 
+theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b :=
+  Int.add_emod_self.symm
+
 @[simp] theorem emod_neg (a b : Int) : a % -b = a % b := by
   rw [emod_def, emod_def, Int.ediv_neg, Int.neg_mul_neg]
 
@@ -760,6 +763,9 @@ theorem le_of_mul_le_mul_right {a b c : Int} (w : b * a ≤ c * a) (h : 0 < a) :
 protected theorem ediv_le_of_le_mul {a b c : Int} (H : 0 < c) (H' : a ≤ b * c) : a / c ≤ b :=
   le_of_mul_le_mul_right (Int.le_trans (Int.ediv_mul_le _ (Int.ne_of_gt H)) H') H
 
+protected theorem ediv_neg_of_neg_of_pos {n s : Int} (h : n ≤ 0) (h2 : 0 < s) : n / s ≤ 0 :=
+  Int.ediv_le_of_le_mul h2 (by simp [h])
+
 protected theorem mul_lt_of_lt_ediv {a b c : Int} (H : 0 < c) (H3 : a < b / c) : a * c < b :=
   Int.lt_of_not_ge <| mt (Int.ediv_le_of_le_mul H) (Int.not_le_of_gt H3)
 
@@ -1287,6 +1293,9 @@ theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2 := by
       exact Int.sub_neg_of_lt this
     · exact Int.le.intro_sub _ rfl
 
+theorem bmod_eq_of_lt {x : Int} {m : Nat} (hx : x % m < (m + 1) / 2) : bmod x m = x % m := by
+  simp [bmod, hx]
+
 theorem bmod_le {x : Int} {m : Nat} (h : 0 < m) : bmod x m ≤ (m - 1) / 2 := by
   refine lt_add_one_iff.mp ?_
   calc

src/Init/Data/Int/LemmasAux.lean

@@ -45,4 +45,11 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
   · rw [Int.emod_eq_of_lt xpos (by omega)]; omega
   · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega
 
+theorem bmod_eq_of_le_of_lt {x : Int} {y : Nat} (hge : -y ≤ x * 2) (hlt : x * 2 < y) :
+    x.bmod y = x := by
+  simp only [Int.bmod_def]
+  rcases x
+  · rw [Int.emod_eq_of_lt (by simp only [ofNat_eq_coe]; omega) (by omega)]; omega
+  · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega
+
 end Int

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -74,6 +74,10 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
 theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by
   simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]
 
+theorem shiftRight_le (m n : Nat) : m >>> n ≤ m := by
+  simp [Nat.shiftRight_eq_div_pow]
+  apply Nat.div_le_self
+
 /-!
 ### testBit
 We define an operation for testing individual bits in the binary representation