feat: add BitVec.intMin

src/Init/Data/BitVec/Lemmas.lean

@@ -1457,20 +1457,6 @@ 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
 
-/-! ### 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).getLsb i = decide (i < w) := by
-  simp [intMax, getLsb]
-
-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 getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
@@ -1794,4 +1780,54 @@ theorem getLsb_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.getLsb_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. -/
+abbrev intMin (w : Nat) := twoPow w (w - 1)
+
+theorem getLsb_intMin (w : Nat) : (intMin w).getLsb i = decide (i + 1 = w) := by
+  simp only [getLsb_twoPow, boolToPropSimps]
+  omega
+
+@[simp, bv_toNat]
+theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
+  simp
+
+@[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. -/
+abbrev 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 getLsb_intMax (w : Nat) : (intMax w).getLsb 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)]
+
 end BitVec

src/Init/Data/Bool.lean

@@ -563,6 +563,21 @@ protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = tru
     decide (p ↔ q) = (decide p == decide q) := by
   cases dp with | _ p => simp [p]
 
+@[boolToPropSimps]
+theorem and_eq_decide (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
+    (p && q) = decide (p ∧ q) := by
+  cases dp with | _ p => simp [p]
+
+@[boolToPropSimps]
+theorem or_eq_decide (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
+    (p || q) = decide (p ∨ q) := by
+  cases dp with | _ p => simp [p]
+
+@[boolToPropSimps]
+theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
+    (decide p == decide q) = decide (p ↔ q) := by
+  cases dp with | _ p => simp [p]
+
 end Bool
 
 export Bool (cond_eq_if)

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

@@ -324,6 +324,28 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp
 
+theorem testBit_two_pow {n m : Nat} : testBit (2 ^ n) m = decide (n = m) := by
+  rw [testBit, shiftRight_eq_div_pow]
+  by_cases h : n = m
+  · simp [h, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]
+  · simp only [h]
+    cases Nat.lt_or_lt_of_ne h
+    · rw [div_eq_of_lt (Nat.pow_lt_pow_of_lt (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
+
+@[simp]
+theorem testBit_two_pow_self {n : Nat} : testBit (2 ^ n) n = true := by
+  simp [testBit_two_pow]
+
+@[simp]
+theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : testBit (2 ^ n) m = false := by
+  simp [testBit_two_pow]
+  omega
+
 @[simp] theorem two_pow_sub_one_mod_two : (2 ^ n - 1) % 2 = 1 % 2 ^ n := by
   cases n with
   | zero => simp

src/Init/Data/Nat/Lemmas.lean

@@ -666,6 +666,9 @@ protected theorem one_le_two_pow : 1 ≤ 2 ^ n :=
     rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega))]
     simp
 
+@[simp] theorem one_mod_two_pow (h : 0 < n) : 1 % 2 ^ n = 1 :=
+  one_mod_two_pow_eq_one.mpr h
+
 protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
   match n with
   | 0 => Nat.zero_lt_one
@@ -717,6 +720,36 @@ 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} (h₁ : 1 < x) (h₂ : 0 < w) :
+    x ^ (w - 1) < x ^ w :=
+  Nat.pow_lt_pow_of_lt h₁ (by omega)
+
+protected theorem two_pow_pred_lt_two_pow {w : Nat} (h : 0 < w) :
+    2 ^ (w - 1) < 2 ^ w :=
+  Nat.pow_pred_lt_pow (by omega) 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]

src/Init/PropLemmas.lean

@@ -390,7 +390,7 @@ else isTrue fun h2 => absurd h2 h
 
 theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp
 
-@[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
+@[simp, boolToPropSimps] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
     decide p = decide q ↔ (p ↔ q) :=
   ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩
 

src/Lean/Elab/Tactic.lean

@@ -42,3 +42,4 @@ import Lean.Elab.Tactic.Rfl
 import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
+import Lean.Elab.Tactic.BoolToPropSimps

src/Lean/Elab/Tactic/BoolToPropSimps.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 University of Cambridge. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tobias Grosser
+-/
+
+prelude
+import Lean.Meta.Tactic.Simp.Attr
+
+builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
+  Lean.Meta.registerSimpAttr `boolToPropSimps
+    "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"