feat: BitVec.msb_sdiv

src/Init/Data/BitVec/Bitblast.lean

@@ -1715,6 +1715,120 @@ theorem toInt_sdiv (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).
   · rw [← toInt_bmod_cancel]
     rw [BitVec.toInt_sdiv_of_ne_or_ne _ _ (by simpa only [Decidable.not_and_iff_not_or_not] using h)]
 
+/-- Unsigned division is zero if and only if either the denominator is zero,
+or the numerator is unsigned less than the denominator -/
+@[simp]
+theorem udiv_eq_zero_iff_eq_zero_or_lt {x y : BitVec w} :
+     x / y = 0#w ↔ (y = 0#w ∨ x < y) := by
+  constructor
+  · intros h
+    obtain h := toNat_inj.mpr h
+    simp only [toNat_udiv, toNat_ofNat, zero_mod, Nat.div_eq_zero_iff] at h
+    rcases h with h | h
+    · left
+      apply eq_of_toNat_eq
+      simp [h]
+    · right
+      simp [lt_def, h]
+  · intros h 
+    apply eq_of_toNat_eq
+    simp only [toNat_udiv, toNat_ofNat, zero_mod, Nat.div_eq_zero_iff]
+    simp only [lt_def] at h
+    rcases h with h | h <;> simp [h]
+
+@[simp]
+theorem udiv_ne_zero_iff_ne_zero_and_le {x y : BitVec w} :
+     x / y ≠ 0#w ↔ (y ≠ 0#w ∧ y ≤ x) := by
+  simp only [ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt]
+
+private theorem neg_udiv_eq_intmin_iff_eq_intmin_eq_one_of_msb_eq_true
+    {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) :
+    -x / y = intMin w ↔ (x = intMin w ∧ y = 1#w) := by
+  constructor
+  · intros h
+    rcases w with _ | w; decide +revert
+    have : (-x / y).msb = true := by simp [h, msb_intMin]; 
+    rw [msb_udiv] at this
+    simp only [bool_to_prop] at this
+    obtain ⟨hx₂, hy⟩ := this
+    simp at hy
+    subst hy
+    simp
+    simp at h
+    simp [h]
+  · rintro ⟨hx, hy⟩
+    subst hx
+    subst hy
+    simp
+
+theorem msb_sdiv_eq_decide {x y : BitVec w} :
+    (x.sdiv y).msb = ((0 < w) && 
+      -- x +ve, y +ve: never negative..
+      (!x.msb && y.msb && (-y ≤ x ∧ y ≠ 0#w)) || -- x +ve, y -ve: -ve when result nonzero.
+      (x.msb && !y.msb && (y ≤ -x && y ≠ 0#w)) || -- x -ve, y +ve: -ve when result nonzero.
+      (x.msb && y.msb && (x = intMin w && y = -1#w))) -- x -ve, y -ve:  `intMin / -1 = intMin` -ve.
+     := by
+  by_cases hw : w = 0; subst hw; decide +revert
+  simp only [show 0 < w by omega, decide_true, ne_eq, decide_and, decide_not, Bool.true_and]
+  simp only [sdiv_eq, udiv_eq]
+  rcases hxmsb : x.msb <;> rcases hymsb : y.msb 
+  · -- x:false, y:false
+    simp only [hxmsb, hymsb, msb_udiv_eq_false_of, Bool.not_false, Bool.and_false, Bool.false_and,
+      Bool.and_true, Bool.or_self, Bool.and_self]
+  · -- x:false, y:true
+    simp only [hxmsb, hymsb, msb_neg, msb_udiv_eq_false_of, bne_false, Bool.not_false,
+      Bool.and_self, ne_zero_of_msb_true, decide_false, Bool.and_true, Bool.true_and, Bool.not_true,
+      Bool.false_and, Bool.or_false]
+    simp only[bool_to_prop]
+    have : x / -y ≠ intMin w := by
+        intros h
+        have : (x  / -y).msb = (intMin w).msb := by simp only [h]
+        simp only [msb_intMin, show 0 < w by omega, decide_true] at this
+        rw [msb_udiv] at this
+        simp only [and_eq_true, beq_iff_eq] at this
+        obtain ⟨hcontra, _⟩ := this
+        simp only [hcontra, true_eq_false] at hxmsb
+    simp only [bne_iff_ne, ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, neg_eq_zero_iff,
+      ne_zero_of_msb_true hymsb, _root_.false_or, BitVec.not_lt, this, not_false_eq_true,
+      _root_.and_true]
+  · -- x:true, y:false
+    simp only [hxmsb, hymsb, Bool.not_true, Bool.and_self, Bool.false_and, Bool.not_false,
+      Bool.true_and, Bool.false_or, Bool.and_false, Bool.or_false]
+    by_cases hx₁ : x = 0#w
+    · simp only [hx₁, neg_zero, zero_udiv, msb_zero, le_zero_iff, Bool.and_not_self]
+    · by_cases hy₁ : y = 0#w
+      · simp only [hy₁, udiv_zero, neg_zero, msb_zero, decide_true, Bool.not_true, Bool.and_false]
+      · simp only [hy₁, decide_false, Bool.not_false, Bool.and_true]
+        by_cases hxy₁ : (- x / y) = 0#w
+        · simp only [hxy₁, neg_zero, msb_zero, false_eq_decide_iff, BitVec.not_le]
+          simp only [udiv_eq_zero_iff_eq_zero_or_lt] at hxy₁
+          simp only [hy₁, _root_.false_or] at hxy₁
+          bv_omega
+        · simp only [udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt] at hxy₁
+          simp only [hy₁, not_false_eq_true, _root_.true_and] at hxy₁
+          simp only [hxy₁, decide_true]
+          simp only [msb_neg, bne_iff_ne, ne_eq]
+          simp only [bool_to_prop]
+          simp only [bne_iff_ne, ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or,
+            BitVec.not_lt, hxy₁, _root_.true_and, decide_not, not_eq_eq_eq_not, not_eq_not]
+          rw [msb_udiv, msb_neg]
+          simp only [bool_to_prop]
+          simp only [bne_iff_ne, ne_eq, hx₁, not_false_eq_true, _root_.true_and, decide_not, hxmsb,
+            bne_true, Bool.not_not, decide_eq_true_eq, beq_iff_eq]
+          apply neg_udiv_eq_intmin_iff_eq_intmin_eq_one_of_msb_eq_true hxmsb hymsb
+  ·  -- x:true, y:true
+    simp only [hxmsb, hymsb, Bool.not_true, Bool.and_true, ne_zero_of_msb_true, decide_false,
+    Bool.not_false, Bool.false_and, Bool.and_false, Bool.or_self, Bool.and_self, Bool.true_and,
+    Bool.false_or]
+    rw [msb_udiv, msb_neg]
+    simp only [hxmsb, bne_true, Bool.not_and]
+    simp only [bool_to_prop]
+    simp only [not_eq_eq_eq_not, Bool.not_true, bne_eq_false_iff_eq, beq_iff_eq]
+    have hxne0 : ¬ (x = 0#w) := by 
+      intros h
+      simp [h] at hxmsb
+    simp only [hxne0, _root_.false_or, neg_eq_iff_eq_neg]
+
 theorem msb_umod_eq_false_of_left {x : BitVec w} (hx : x.msb = false) (y : BitVec w) : (x % y).msb = false := by
   rw [msb_eq_false_iff_two_mul_lt] at hx ⊢
   rw [toNat_umod]