feat: BitVec.msb_sdiv

src/Init/Data/BitVec/Bitblast.lean

@@ -1715,6 +1715,98 @@ 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)]
 
+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 only [beq_iff_eq] at hy
+    subst hy
+    simp only [udiv_one, zero_lt_succ, neg_eq_intMin] at h
+    simp [h]
+  · rintro ⟨hx, hy⟩
+    subst hx hy
+    simp
+
+/--
+the most significant bit of the signed division `x.sdiv y` can be computed
+by the following cases:
+(1) x nonneg, y nonneg: never neg.
+(2) x nonneg, y neg: neg when result nonzero.
+   We know that y is nonzero since it is negative, so we only check `|x| ≥ |y|`.
+(3) x neg, y nonneg: neg when result nonzero.
+  We check that `y ≠ 0` and `|x| ≥ |y|`.
+(4) x neg, y neg: neg when `x = intMin, `y = -1`, since `intMin / -1 = intMin`.
+
+The proof strategy is to perform a case analysis on the sign of `x` and `y`,
+followed by unfolding the `sdiv` into `udiv`.
+-/
+theorem msb_sdiv_eq_decide {x y : BitVec w} :
+    (x.sdiv y).msb = (decide (0 < w) &&
+      (!x.msb && y.msb && decide (-y ≤ x)) ||
+      (x.msb && !y.msb && decide (y ≤ -x) && decide (y ≠ 0#w)) ||
+      (x.msb && y.msb && decide (x = intMin w) && decide (y = -1#w)))
+     := 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,
+    sdiv_eq, udiv_eq]
+  rcases hxmsb : x.msb <;> rcases hymsb : y.msb
+  · -- x:nonneg, y:nonneg
+    simp [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:nonneg, y:neg
+    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, 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 [this, hymsb, udiv_ne_zero_iff_ne_zero_and_le]
+  · -- x:neg, y:nonneg
+    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 [hx₁, neg_zero, zero_udiv, msb_zero, le_zero_iff, Bool.and_not_self]
+    · by_cases hy₁ : y = 0#w
+      · simp [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,
+            decide_eq_true_eq, BitVec.not_le]
+          simp only [udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or] at hxy₁
+          bv_omega
+        · simp only [udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt,
+            hy₁, not_false_eq_true, _root_.true_and] at hxy₁
+          simp only [hxy₁, decide_true, msb_neg, bne_iff_ne, ne_eq,
+            bool_to_prop,
+            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,
+            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:neg, y:neg
+    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 := BitVec.ne_zero_of_msb_true (x := x) hxmsb
+    simp [hxne0, 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]

src/Init/Data/BitVec/Lemmas.lean

@@ -3994,6 +3994,16 @@ theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
     (x / y).toInt = x.toNat / y.toNat := by
   simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
 
+/-- Unsigned division is zero if and only if either the denominator is zero,
+or the numerator is unsigned less than the denominator -/
+theorem udiv_eq_zero_iff_eq_zero_or_lt {x y : BitVec w} :
+     x / y = 0#w ↔ (y = 0#w ∨ x < y) := by
+    simp [toNat_eq, toNat_udiv, toNat_ofNat, Nat.zero_mod, Nat.div_eq_zero_iff, BitVec.lt_def]
+
+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]
+
 /-! ### umod -/
 
 theorem umod_def {x y : BitVec n} :