From 78fe92507cddf1a4fb37bc7608238299134cff14 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Sun, 10 Nov 2024 22:08:43 +0000
Subject: [PATCH] feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is
 zero (#5616)

This PR is a follow-up to https://github.com/leanprover/lean4/pull/5609,
where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior
when the denominator is zero.

We build some `slt` theory, connecting it to `msb` for a clean proof. I
chose not to characterize `slt` in terms of `msb` a `simp` lemma, since
I anticipate use cases where we want to keep the arithmetic
interpretation of `slt`.
---
 src/Init/Data/BitVec/Lemmas.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 61ce0dbe2b..139d077050 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -512,6 +512,31 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
     subst h
     simp
 
+@[simp]
+theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
+  simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
+
+/-! ### slt -/
+
+/--
+A bitvector, when interpreted as an integer, is less than zero iff
+its most significant bit is true.
+-/
+theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w ↔ x.msb = true := by
+  have := toInt_eq_msb_cond x
+  constructor
+  · intros h
+    apply Classical.byContradiction
+    intros hmsb
+    simp only [Bool.not_eq_true] at hmsb
+    simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
+    simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
+    omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
+  · intros h
+    simp only [h, ↓reduceIte] at this
+    simp [BitVec.slt, this]
+    omega
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -2376,6 +2401,9 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
 theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
   simp [smtUDiv]
 
+@[simp]
+theorem smtUDiv_zero {x : BitVec n} : x.smtUDiv 0#n = allOnes n := rfl
+
 /-! ### sdiv -/
 
 /-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2443,6 +2471,10 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
   rw [BitVec.smtSDiv]
   rcases x.msb <;> rcases y.msb <;> simp
 
+@[simp]
+theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
+  rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, ← negOne_eq_allOnes]
+
 /-! ### srem -/
 
 theorem srem_eq (x y : BitVec w) : srem x y =