feat: BitVec.msb_sdiv (leanprover#8178)

This PR provides a compact formula for the MSB of the sdiv. Most of the
work in the PR involves handling the corner cases of division
overflowing (e.g. `intMin / -1 = intMin`)

---------

Co-authored-by: Luisa Cicolini <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>

Author: 3 people

src/Init/Data/BitVec/Bitblast.lean

@@ -1662,6 +1662,88 @@ 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
+  rcases w; decide +revert
+  case succ w =>
+    simp only [decide_true, ne_eq, decide_and, decide_not, Bool.true_and,
+      sdiv_eq, udiv_eq]
+    rcases hxmsb : x.msb <;> rcases hymsb : y.msb
+    · 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]
+    · 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 + 1) := by
+        intros h
+        have : (x / -y).msb = (intMin (w + 1)).msb := by simp only [h]
+        simp only [msb_udiv, msb_intMin, show 0 < w + 1 by omega, decide_true, 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]
+    · 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 + 1)
+      · simp [hx₁, neg_zero, zero_udiv, msb_zero, le_zero_iff, Bool.and_not_self]
+      · by_cases hy₁ : y = 0#(w + 1)
+        · 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 + 1)
+          · 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,
+              msb_udiv, msb_neg]
+            simp only [hx₁, not_false_eq_true, _root_.true_and, decide_not, hxmsb, not_eq_eq_eq_not,
+              Bool.not_true, decide_eq_false_iff_not, Decidable.not_not, beq_iff_eq]
+            rw [neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true hxmsb hymsb]
+    · simp only [msb_udiv, msb_neg, hxmsb, bne_true, Bool.not_and, Bool.not_true, Bool.and_true,
+        Bool.false_and, Bool.and_false, hymsb, ne_zero_of_msb_true, decide_false, Bool.not_false,
+        Bool.or_self, Bool.and_self, Bool.true_and, Bool.false_or]
+      simp only [bool_to_prop]
+      simp [BitVec.ne_zero_of_msb_true (x := x) hxmsb, 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

@@ -4119,6 +4119,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} :