feat: BitVec.[udiv_twoPow|sdiv_twoPow]

src/Init/Data/BitVec/Lemmas.lean

@@ -2152,8 +2152,11 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
 
 @[simp]
 theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
-  apply eq_of_toNat_eq
-  simp [toNat_mul]
+  simp [bv_toNat]
+
+@[simp]
+theorem BitVec.zero_mul {x : BitVec w} : 0#w * x = 0#w := by
+  simp [bv_toNat]
 
 theorem BitVec.mul_add {x y z : BitVec w} :
     x * (y + z) = x * y + x * z := by
@@ -2640,6 +2643,8 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
 
 /- ## twoPow -/
 
+#check Nat.two_pow_pred_mod_two_pow
+
 @[simp, bv_toNat]
 theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
   rcases w with rfl | w
@@ -2681,11 +2686,10 @@ theorem getMsbD_twoPow {i j w: Nat} :
 
 @[simp]
 theorem msb_twoPow {i w: Nat} :
-    (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
-  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
+    (BitVec.twoPow w i).msb = decide (i + 1 = w) := by
+  simp only [BitVec.msb, BitVec.getMsbD_eq_getLsbD, Nat.sub_zero, BitVec.getLsbD_twoPow,
     Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
-  intros
-  omega
+  by_cases h : i + 1 = w <;> simp [h] <;> omega
 
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
@@ -3035,6 +3039,123 @@ instance instDecidableExistsBitVec :
     have := instDecidableExistsBitVec n
     inferInstance
 
+theorem div_twoPow_div_twoPow_eq_mul {n m : Nat} (x : BitVec w) :
+    x / (BitVec.twoPow w n) / (BitVec.twoPow w m) =
+      x / ((BitVec.twoPow w n) * (BitVec.twoPow w m)) := by
+  simp only [BitVec.toNat_eq, BitVec.toNat_udiv, BitVec.toNat_twoPow, BitVec.toNat_mul,
+    Nat.mul_mod_mod, Nat.mod_mul_mod]
+  by_cases hzz : x = 0
+  · subst hzz
+    simp
+  · by_cases h : n + m < w
+    ·
+      have hl : 2^n * 2^m < 2^w := by
+        rw [← Nat.pow_add]
+        have asdd := (@Nat.pow_lt_pow_iff_right 2 (n + m) w (by omega)).mpr h
+        apply asdd
+      simp [Nat.mod_eq_of_lt hl]
+      have := @Nat.mul_lt_mul_of_le_of_lt
+      have := @Nat.mul_lt_mul_right (2 ^ n) (2 ^ m) (2 ^ w) (by apply Nat.two_pow_pos)
+      have := @Nat.lt_of_mul_lt (2^n) (2^m) (2^w) (by apply Nat.two_pow_pos) h
+      rw [Nat.mul_comm] at hl
+      have := @Nat.lt_of_mul_lt (2^m) (2^n) (2^w) (by apply Nat.two_pow_pos) h
+      have : 2 ^ m < 2 ^ w := by omega
+      simp [Nat.mod_eq_of_lt, *]
+      rw [Nat.div_div_eq_div_mul]
+    ·
+      rw [←Nat.pow_add]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      simp [h]
+      by_cases h₄ : n < w
+      · by_cases h₅ : m < w
+        · simp [h₄, h₅]
+          simp at h
+          rw [Nat.div_div_eq_div_mul]
+          rw [←Nat.pow_add]
+          rw [Nat.div_eq_zero_iff]
+          have xzero := BitVec.isLt x
+          simp [bv_toNat] at hzz
+          have := @Nat.pow_pos 2 w (by omega)
+          have : 2 ^ w ≤ 2 ^ (n + m) := by
+            apply Nat.pow_le_pow_of_le (by omega) h
+          omega
+          have := @Nat.pow_pos 2 (n + m) (by omega)
+          omega
+        · simp [h₄, h₅]
+      · by_cases h₅ : m < w
+        · simp [h₄, h₅]
+        · simp [h₄, h₅]
+
+theorem udiv_twoPow {n : Nat} {x : BitVec w} :
+    x / (BitVec.twoPow w n) = x >>> n := by
+  simp only [BitVec.toNat_eq, BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow,
+    BitVec.toNat_udiv, BitVec.toNat_twoPow]
+  by_cases h : n < w
+  · rw [Nat.mod_eq_of_lt ((Nat.pow_lt_pow_iff_right (by omega)).mpr h)]
+  · by_cases hh : x.toNat = 0
+    · simp [hh]
+    · have : 2 ^ w ≤ 2 ^ n := (Nat.pow_le_pow_iff_right (by omega)).mpr (by omega)
+      rw [(@Nat.div_eq_zero_iff (2 ^ n) x.toNat (by omega)).mpr (by omega),
+        Nat.mod_eq_zero_of_dvd, Nat.div_zero]
+      apply Nat.pow_dvd_pow 2 (by omega)
+
+theorem neg_twoPow' {i w: Nat} :
+    (BitVec.twoPow w i).neg = (BitVec.twoPow w i) := by
+  simp [bv_toNat]
+  rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+  by_cases h : i < w
+  · simp [h]
+  · simp [h]
+
+
+
+
+
+  sorry
+
+
+theorem sdiv_twoPow {n : Nat} {x : BitVec w} :
+    x.sdiv (BitVec.twoPow w n) = x.sshiftRight n := by
+  by_cases h : x.msb
+  ·
+    simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq]
+    by_cases hh : n + 1 = w
+    ·
+      simp [hh, h]
+
+      sorry
+    ·
+      simp [hh, h]
+      rw [BitVec.sshiftRight_eq_of_msb_true h]
+      simp [bv_toNat]
+      rw [Nat.two_pow_mod_two_pow_iff (by omega)]
+      have al : n < w := by sorry
+      simp [al]
+
+
+      simp [hh]
+      sorry
+  ·
+    simp only [BitVec.sdiv_eq, msb_twoPow, BitVec.udiv_eq]
+    by_cases hh : n + 1 = w
+    · simp [hh, h]
+      simp at h
+      rw [BitVec.sshiftRight_eq_of_msb_false h]
+      simp only [toNat_eq, toNat_neg, toNat_udiv, toNat_twoPow, toNat_ushiftRight]
+      rw [Nat.shiftRight_eq_div_pow]
+
+
+
+
+      sorry
+    · simp only [h, hh, decide_False]
+      simp only [Bool.not_eq_true] at h
+      rw [BitVec.sshiftRight_eq_of_msb_false h]
+      rw [udiv_twoPow]
+
+
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false

src/Init/Data/Nat/Lemmas.lean

@@ -549,6 +549,12 @@ protected theorem mul_left_cancel_iff {n : Nat} (p : 0 < n) {m k : Nat} : n * m
 protected theorem mul_right_cancel_iff {m : Nat} (p : 0 < m) {n k : Nat} : n * m = k * m ↔ n = k :=
   ⟨Nat.mul_right_cancel p, fun | rfl => rfl⟩
 
+protected theorem mul_left_inj (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
+  Nat.mul_right_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
+protected theorem mul_right_inj (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
+  Nat.mul_left_cancel_iff (Nat.pos_iff_ne_zero.2 ha)
+
 protected theorem ne_zero_of_mul_ne_zero_right (h : n * m ≠ 0) : m ≠ 0 :=
   (Nat.mul_ne_zero_iff.1 h).2
 
@@ -664,6 +670,9 @@ theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
 @[simp] theorem add_mod_mod (m n k : Nat) : (m + n % k) % k = (m + n) % k := by
   rw [Nat.add_comm, mod_add_mod, Nat.add_comm]
 
+@[simp] theorem mul_mod_mod (a b c : Nat) : (a * (b % c)) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
 theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
   rw [add_mod_mod, mod_add_mod]
 
@@ -894,6 +903,11 @@ protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a
     a / b = c ↔ a = c * b := by
   rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
 
+protected theorem div_eq_zero_iff (hb : 0 < b) : a / b = 0 ↔ a < b where
+  mp h := by rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero]; exact mod_lt _ hb
+  mpr h := by rw [← Nat.mul_right_inj (Nat.ne_of_gt hb), ← Nat.add_left_cancel_iff, mod_add_div,
+      mod_eq_of_lt h, Nat.mul_zero, Nat.add_zero]
+
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
   | x + 1, w => by
@@ -923,6 +937,17 @@ protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a
     rw [Nat.pow_add]
     apply Nat.dvd_mul_right
 
+protected theorem two_pow_mod_two_pow_iff {b m n : Nat} (h : 1 < b):
+    (b ^ n % b ^ m) = if n < m then b ^ n else 0 := by
+  by_cases h : n < m
+  · simp only [h, ↓reduceIte]
+    apply Nat.mod_eq_of_lt
+    apply Nat.pow_lt_pow_of_lt (by omega) h
+  · simp only [h, ↓reduceIte]
+    simp only [Nat.not_lt] at h
+    apply Nat.mod_eq_zero_of_dvd
+    apply Nat.pow_dvd_pow b (by omega)
+
 protected theorem pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m ≤ n) :
     a ^ (n - m) * a ^ m = a ^ n := by
   rw [← Nat.pow_add, Nat.sub_add_cancel h]

src/Init/Data/Nat/Mod.lean

@@ -21,6 +21,17 @@ which should probably be moved to their own file.
 
 namespace Nat
 
+protected theorem lt_of_mul_lt {a b c : Nat} (h : 0 < b) (h₂ : a * b < c) : a < c := by
+  induction a generalizing c
+  case zero =>
+    simp only [Nat.zero_mul] at h₂
+    simp [h₂]
+  case succ i ih =>
+    simp only [Nat.add_mul, Nat.one_mul] at h₂
+    apply Nat.add_lt_of_lt_sub
+    apply ih
+    omega
+
 @[simp] protected theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c := by
   induction a with
   | zero => simp_all