chore: undo intMax change

src/Init/Data/BitVec/Lemmas.lean

@@ -1675,20 +1675,6 @@ theorem le_iff_not_lt {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
   constructor <;>
     (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)
 
-/-! ### intMax -/
-
-/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
-def intMax (w : Nat) : BitVec w := BitVec.ofNat w (2^w - 1)
-
-theorem getLsb_intMax_eq (w : Nat) : (intMax w).getLsbD i = decide (i < w) := by
-  simp [intMax, getLsbD]
-
-theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
-  have h : 2^w - 1 < 2^w := by
-    have pos : 2^w > 0 := Nat.pow_pos (by decide)
-    omega
-  simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
-
 /-! ### ofBoolList -/
 
 @[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by
@@ -2015,6 +2001,56 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
       simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
       apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
 
+/-! ### intMin -/
+
+/-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
+def intMin (w : Nat) := twoPow w (w - 1)
+
+theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) := by
+  simp only [intMin, getLsbD_twoPow, boolToPropSimps]
+  omega
+
+@[simp, bv_toNat]
+theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
+  simp [intMin]
+
+@[simp]
+theorem neg_intMin {w : Nat} : -intMin w = intMin w := by
+  by_cases h : 0 < w
+  · simp [bv_toNat, h]
+  · simp only [Nat.not_lt, Nat.le_zero_eq] at h
+    simp [bv_toNat, h]
+
+/-! ### intMax -/
+
+/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
+def intMax (w : Nat) := (twoPow w (w - 1)) - 1
+
+@[simp, bv_toNat]
+theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1 := by
+  simp only [intMax]
+  by_cases h : w = 0
+  · simp [h]
+  · have h' : 0 < w := by omega
+    rw [toNat_sub, toNat_twoPow, ← Nat.sub_add_comm (by simpa [h'] using Nat.one_le_two_pow),
+      Nat.add_sub_assoc (by simpa [h'] using Nat.one_le_two_pow),
+      Nat.two_pow_pred_mod_two_pow h', ofNat_eq_ofNat, toNat_ofNat, Nat.one_mod_two_pow h',
+      Nat.add_mod_left, Nat.mod_eq_of_lt]
+    have := Nat.two_pow_pred_lt_two_pow h'
+    have := Nat.two_pow_pos w
+    omega
+
+@[simp]
+theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := by
+  rw [← testBit_toNat, toNat_intMax, Nat.testBit_two_pow_sub_one, decide_eq_decide]
+  omega
+
+@[simp] theorem intMax_add_one {w : Nat} : intMax w + 1#w = intMin w := by
+  simp only [toNat_eq, toNat_intMax, toNat_add, toNat_intMin, toNat_ofNat, Nat.add_mod_mod]
+  by_cases h : w = 0
+  · simp [h]
+  · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)]
+
 /-! ### Lemmas about non-overflowing computations -/
 
 /-- If `y ≤ x`, then `x - y` does not overflow, thus `(x - y).toNat = x.toNat - y.toNat`. -/