From e7d4c9dcf96a3a42c80bc9dae970bd484bb84c3c Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 22 Oct 2024 18:01:46 -0700
Subject: [PATCH] chore: force use of msb_eq_decide

---
 src/Init/Data/BitVec/Lemmas.lean | 77 +++++++++++++++-----------------
 1 file changed, 37 insertions(+), 40 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 87d8cd5c999d..fbced15bb63f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -388,20 +388,12 @@ theorem msb_eq_getLsbD_last (x : BitVec w) :
     x.getLsbD w = decide (2 ^ w ≤ x.toNat) := getLsbD_last x
 
 
-/-- 
-An alternative to `msb_eq_decide` in terms of `2 * x.toNat`,
-in order to avoid `2 ^ (w - 1)`.
--/
-@[bv_toNat] theorem msb_eq_decide_le_mul_two (x : BitVec w) : 
+@[bv_toNat] theorem msb_eq_decide (x : BitVec w) : 
     BitVec.msb x = decide (2 ^ w ≤ 2 * x.toNat) := by
   rw [x.msb_eq_getLsbD_last, x.getLsbD_last]
   simp
   rcases w with rfl | w  <;> simp <;> omega
 
-@[bv_toNat, deprecated msb_eq_decide_le_mul_two (since := "21-10-2024") ]
-theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat) := by
-  simp [msb_eq_getLsbD_last, getLsbD_last]
-
 theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1) := by
   match n with
   | 0 =>
@@ -409,7 +401,7 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
   | n + 1 =>
     simp only [msb_eq_decide, Nat.add_one_sub_one, decide_eq_true_eq] at p
     simp only [Nat.add_sub_cancel]
-    exact p
+    omega
 
 /-! ### cast -/
 
@@ -515,7 +507,7 @@ integer is between `[0..2^n/2)`.
 -/
 theorem toInt_bounds_of_msb_eq_false {x : BitVec n} (hmsb : x.msb = false) :
     0 ≤ x.toInt ∧ 2 * x.toInt < 2^n := by
-  have := x.msb_eq_decide_le_mul_two
+  have := x.msb_eq_decide
   rw [hmsb] at this
   simp only [false_eq_decide_iff, Nat.not_le] at this
   rw [BitVec.toInt_eq_toNat_cond]
@@ -530,7 +522,7 @@ integer is between `[-2^n..0).
 -/
 theorem toInt_bounds_of_msb_eq_true {x : BitVec n} (hmsb : x.msb = true) :
     -2^n ≤ x.toInt ∧ x.toInt < 0 := by
-  have := x.msb_eq_decide_le_mul_two
+  have := x.msb_eq_decide
   rw [hmsb] at this
   simp only [true_eq_decide_iff] at this
   rw [BitVec.toInt_eq_toNat_cond]
@@ -2871,6 +2863,23 @@ theorem toInt_intMin {w : Nat} :
     rw [Nat.mul_comm]
     simp [w_pos]
 
+/--
+If the width is zero, then `intMin` is `0`,
+and otherwise it is `-2^(n - 1)`.
+-/
+theorem toInt_intMin_eq_if (n : Nat) : (BitVec.intMin n).toInt =
+    if n = 0 then 0 else - 2^(n - 1) := by
+  simp [BitVec.toInt_intMin]
+  rcases n with rfl | n
+  · simp
+  · simp
+    norm_cast
+    have : 2^n > 0 := by exact Nat.two_pow_pos n
+    have : 2^n < 2^(n + 1) := by
+      simp [Nat.pow_succ]
+      omega
+    rw [Nat.mod_eq_of_lt (by omega)]
+
 @[simp]
 theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   by_cases h : 0 < w
@@ -2878,7 +2887,7 @@ theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
   · simp only [Nat.not_lt, Nat.le_zero_eq] at h
     simp [bv_toNat, h]
 
-theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
+theorem toInt_neg_eq_neg_toInt {x : BitVec w} (rs : x ≠ intMin w) :
     (-x).toInt = -(x.toInt) := by
   simp only [ne_eq, toNat_eq, toNat_intMin] at rs
   by_cases x_zero : x = 0
@@ -2895,36 +2904,16 @@ theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
   split <;> split <;> omega
 
 /-- The msb of `intMin w` is `true` for all  `w > 0` -/
-@[simp] theorem msb_intMin : (intMin w).msb = decide (w > 0) := by
+@[simp] theorem msb_intMin : (intMin w).msb = decide (0 < w) := by
   rw [intMin]
   rw [msb_eq_decide]
-  simp
+  simp only [toNat_twoPow, decide_eq_decide]
   rcases w with rfl | w 
   · rfl
-  · simp
-    have : 0 < 2^w := Nat.pow_pos (by decide)
-    have : 2^w < 2^(w + 1) := by
-      rw [Nat.pow_succ]
-      omega
-    rw [Nat.mod_eq_of_lt (by omega)]
-    simp
-
-/--
-If the width is zero, then `intMin` is `0`,
-and otherwise it is `-2^(n - 1)`.
--/
-theorem toInt_intMin_eq_if (n : Nat) : (BitVec.intMin n).toInt =
-    if n = 0 then 0 else - 2^(n - 1) := by
-  simp [BitVec.toInt_intMin]
-  rcases n with rfl | n
-  · simp
-  · simp
-    norm_cast
-    have : 2^n > 0 := by exact Nat.two_pow_pos n
-    have : 2^n < 2^(n + 1) := by
-      simp [Nat.pow_succ]
-      omega
+  · have : 0 < 2^w := Nat.pow_pos (by decide)
+    simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, iff_true, ge_iff_le]
     rw [Nat.mod_eq_of_lt (by omega)]
+    omega
 
 /--
 Negating `intMin` returns `intMin`.
@@ -2934,8 +2923,7 @@ theorem toInt_neg_eq_if {x : BitVec n} :
     (-x).toInt = if x = intMin n then x.toInt else - x.toInt := by
   by_cases hx : x = intMin n
   · simp [hx]
-  · simp [hx]
-    rw [toInt_neg_of_ne_intMin hx]
+  · simp [hx, toInt_neg_eq_neg_toInt hx]
 
 /-! ### intMax -/
 
@@ -2972,6 +2960,15 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) :=
 
 theorem abs_def {x : BitVec w} : x.abs = if x.msb then .neg x else x := rfl
 
+@[simp, bv_toNat]
+theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
+  simp only [abs_def, neg_eq]
+  by_cases h : x.msb = true
+  · simp only [h, ↓reduceIte, toNat_neg]
+    have : 2 * x.toNat ≥ 2 ^ w := BitVec.msb_eq_true_iff_two_mul_ge.mp h
+    rw [Nat.mod_eq_of_lt (by omega)]
+  · simp [h]
+
 theorem abs_eq_if (x : BitVec w) : x.abs = 
     if x.msb = true then
       if x = BitVec.intMin w then (BitVec.intMin w) else -x