feat: add BitVec.intMin

src/Init/Data/BitVec/Lemmas.lean

@@ -1449,6 +1449,32 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
+/-! ### intMin -/
+
+/-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
+def intMin (w : Nat) : BitVec w := BitVec.ofNat w (2^(w - 1))
+
+theorem getLsb_intMin (w : Nat) : (intMin w).getLsb i = decide (i + 1 = w) := by
+  simp [intMin, BitVec.getLsb]
+  by_cases h : i + 1 = w
+  · subst h
+    simp
+  · by_cases i + 1 < w
+    · simp [h, @Nat.testBit_two_pow_of_ne (w-1) i (by omega)]
+    · simp [h] ; 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
+    subst h
+    simp [intMin]
+
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -315,6 +315,22 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp
 
+@[simp]
+theorem testBit_two_pow_self {n : Nat} : Nat.testBit (2 ^ n) n = true := by
+  rw [testBit, shiftRight_eq_div_pow, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]
+  simp
+
+@[simp]
+theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : Nat.testBit (2 ^ n) m = false := by
+  rw [testBit, shiftRight_eq_div_pow]
+  cases Nat.lt_or_lt_of_ne hm
+  · rw [div_eq_of_lt (Nat.pow_lt_pow_right (by omega) (by omega))]
+    simp
+  · rw [Nat.pow_div _ Nat.two_pos,
+       ← Nat.sub_add_cancel (succ_le_of_lt <| Nat.sub_pos_of_lt (by omega))]
+    simp [Nat.pow_succ, and_one_is_mod, mul_mod_left]
+    omega
+
 /-! ### bitwise -/
 
 theorem testBit_bitwise

src/Init/Data/Nat/Lemmas.lean

@@ -700,6 +700,35 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
   · intro w
     exact Nat.pow_lt_pow_of_lt h w
 
+@[simp]
+protected theorem pow_pred_mul {x w : Nat} (h : 0 < w) :
+    x ^ (w - 1) * x = x ^ w := by
+  simp [← Nat.pow_succ, succ_eq_add_one, Nat.sub_add_cancel h]
+
+protected theorem pow_pred_lt_pow {x w : Nat} (h1 : 1 < x) (h2 : 0 < w) :
+    x ^ (w - 1) < x ^ w :=
+  @Nat.pow_lt_pow_of_lt x (w - 1) w  h1 (by omega)
+
+protected theorem pow_lt_pow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
+  (Nat.pow_lt_pow_iff_right ha).2 h
+
+@[simp]
+protected theorem two_pow_pred_add_two_pow_pred (h : 0 < w) :
+    2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w:= by
+  rw [← Nat.pow_pred_mul h]
+  omega
+
+@[simp]
+protected theorem two_pow_sub_two_pow_pred (h : 0 < w) :
+    2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1) := by
+  simp [← Nat.two_pow_pred_add_two_pow_pred h]
+
+@[simp]
+protected theorem two_pow_pred_mod_two_pow (h : 0 < w):
+    2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1) := by
+  rw [mod_eq_of_lt]
+  apply Nat.pow_pred_lt_pow (by omega) h
+
 /-! ### log2 -/
 
 @[simp]