feat: BitVec and Int results for finite types (#7685)

This PR contains additional material about `BitVec` and `Int` spun off
from #7592.

Author: TwoFX

src/Init/Data/BitVec/Bitblast.lean

@@ -588,13 +588,31 @@ theorem zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb
 theorem zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : BitVec.sle 0#w x ↔ x.msb = false := by
   simp [zero_sle_eq_not_msb]
 
-theorem toNat_toInt_of_sle {w : Nat} (b : BitVec w) (hb : BitVec.sle 0#w b) : b.toInt.toNat = b.toNat :=
-  toNat_toInt_of_msb b (zero_sle_iff_msb_eq_false.1 hb)
+theorem toNat_toInt_of_sle {w : Nat} (x : BitVec w) (hx : BitVec.sle 0#w x) : x.toInt.toNat = x.toNat :=
+  toNat_toInt_of_msb x (zero_sle_iff_msb_eq_false.1 hx)
 
 theorem sle_eq_carry (x y : BitVec w) :
     x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
   rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
 
+theorem neg_slt_zero (h : 0 < w) (x : BitVec w) :
+    (-x).slt 0#w = ((x == intMin w) || (0#w).slt x) := by
+  rw [slt_zero_eq_msb, msb_neg, slt_eq_sle_and_ne, zero_sle_eq_not_msb]
+  apply Bool.eq_iff_iff.2
+  cases hmsb : x.msb with
+  | false => simpa [ne_intMin_of_msb_eq_false h hmsb] using Decidable.not_iff_not.2 (eq_comm)
+  | true =>
+    simp only [Bool.bne_true, Bool.not_and, Bool.or_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,
+      bne_eq_false_iff_eq, Bool.false_and, Bool.or_false, beq_iff_eq,
+      _root_.or_iff_right_iff_imp]
+    rintro rfl
+    simp at hmsb
+
+theorem neg_sle_zero (h : 0 < w) (x : BitVec w) :
+    (-x).sle 0#w = (x == intMin w || (0#w).sle x) := by
+  rw [sle_eq_slt_or_eq, neg_slt_zero h, sle_eq_slt_or_eq]
+  simp [Bool.beq_eq_decide_eq (-x), Bool.beq_eq_decide_eq _ x, Eq.comm (a := x), Bool.or_assoc]
+
 /-! ### mul recurrence for bitblasting -/
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -732,7 +732,7 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
     rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
     omega
 
-/-! ### slt -/
+/-! ### sle/slt -/
 
 /--
 A bitvector, when interpreted as an integer, is less than zero iff
@@ -756,12 +756,21 @@ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
 theorem slt_zero_eq_msb {w : Nat} {x : BitVec  w} : x.slt 0#w = x.msb := by
   rw [Bool.eq_iff_iff, BitVec.slt_zero_iff_msb_cond]
 
-theorem sle_iff_toInt_le {w : Nat} {b b' : BitVec w} : b.sle b' ↔ b.toInt ≤ b'.toInt :=
+theorem sle_iff_toInt_le {w : Nat} {x y : BitVec w} : x.sle y ↔ x.toInt ≤ y.toInt :=
   decide_eq_true_iff
 
-theorem slt_iff_toInt_lt {w : Nat} {b b' : BitVec w} : b.slt b' ↔ b.toInt < b'.toInt :=
+theorem slt_iff_toInt_lt {w : Nat} {x y : BitVec w} : x.slt y ↔ x.toInt < y.toInt :=
   decide_eq_true_iff
 
+theorem sle_eq_slt_or_eq {x y : BitVec w} : x.sle y = (x.slt y || x == y) := by
+  apply Bool.eq_iff_iff.2
+  simp only [BitVec.sle, decide_eq_true_eq, BitVec.slt, Bool.or_eq_true, beq_iff_eq, ← toInt_inj]
+  omega
+
+theorem slt_eq_sle_and_ne {x y : BitVec w} : x.slt y = (x.sle y && x != y) := by
+  apply Bool.eq_iff_iff.2
+  simp [BitVec.slt, BitVec.sle, Int.lt_iff_le_and_ne, BitVec.toInt_inj]
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -1618,10 +1627,20 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
 protected theorem not_inj {x y : BitVec w} : ~~~x = ~~~y ↔ x = y :=
   ⟨fun h => by rw [← @not_not w x, ← @not_not w y, h], congrArg _⟩
 
-@[simp] theorem and_not_self (x : BitVec n) : x &&& ~~~x = 0 := by
+@[simp] theorem and_not_self (x : BitVec w) : x &&& ~~~x = 0 := by
    ext i
    simp_all
 
+@[simp] theorem not_and_self (x : BitVec w) : ~~~x &&& x = 0 := by
+  simp [and_comm]
+
+@[simp] theorem or_not_self (x : BitVec w) : x ||| ~~~x = allOnes w := by
+  ext
+  simp
+
+@[simp] theorem not_or_self (x : BitVec w) : ~~~x ||| x = allOnes w := by
+  simp [or_comm]
+
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
   · intro h
@@ -3377,21 +3396,8 @@ theorem sub_eq_self {x : BitVec 1} : -x = x := by
   have ha : x = 0 ∨ x = 1 := eq_zero_or_eq_one _
   rcases ha with h | h <;> simp [h]
 
-theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
-  rcases w with _ | w
-  · apply Subsingleton.elim
-  · rw [BitVec.not_eq_comm]
-    apply BitVec.eq_of_toNat_eq
-    simp only [BitVec.toNat_neg, BitVec.toNat_not, BitVec.toNat_add, BitVec.toNat_ofNat,
-      Nat.add_mod_mod]
-    by_cases hx : x.toNat = 0
-    · simp [hx]
-    · rw [show (_ - 1 % _) = _ by rw [Nat.mod_eq_of_lt (by omega)],
-        show _ + (_ - 1) = (x.toNat - 1) + 2^(w + 1) by omega,
-        Nat.add_mod_right,
-        show (x.toNat - 1) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)],
-        show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
-      omega
+theorem not_neg (x : BitVec w) : ~~~(-x) = x - 1#w := by
+  rw [not_eq_neg_add, neg_neg]
 
 theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
   apply eq_of_toInt_eq
@@ -3982,6 +3988,18 @@ theorem srem_eq (x y : BitVec w) : srem x y =
   rw [BitVec.srem]
   rcases x.msb <;> rcases y.msb <;> simp
 
+@[simp] theorem srem_zero {x : BitVec w} : x.srem 0#w = x := by
+  cases h : x.msb <;> simp [h, srem_eq]
+
+@[simp] theorem zero_srem {x : BitVec w} : (0#w).srem x = 0#w := by
+  cases h : x.msb <;> simp [h, srem_eq]
+
+@[simp] theorem srem_one {x : BitVec w} : x.srem 1#w = 0#w := by
+  cases h : x.msb <;> by_cases hw : w = 1 <;> (try subst hw) <;> simp_all [srem_eq]
+
+@[simp] theorem srem_self {x : BitVec w} : x.srem x = 0#w := by
+  cases h : x.msb <;> simp [h, srem_eq]
+
 /-! ### smod -/
 
 /-- Equation theorem for `smod` in terms of `umod`. -/
@@ -4017,11 +4035,15 @@ theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
   <;> simp [h'', h''']
 
 @[simp]
-theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
+theorem smod_zero {x : BitVec w} : x.smod 0#w = x := by
   simp only [smod_eq, msb_zero]
   rcases x.msb with msb | msb <;> apply eq_of_toNat_eq
   · simp
-  · by_cases h : x = 0#n <;> simp [h]
+  · by_cases h : x = 0#w <;> simp [h]
+
+@[simp]
+theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by
+  cases _ : x.msb <;> simp_all [smod_eq]
 
 /-! ### ofBoolList -/
 
@@ -4751,6 +4773,12 @@ theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w) := by
   simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]
   by_cases h : 0 < w <;> simp_all
 
+theorem ne_intMin_of_msb_eq_false (h : 0 < w) {n : BitVec w} (hn : n.msb = false) :
+    n ≠ intMin w := by
+  rintro rfl
+  simp only [msb_intMin, decide_eq_false_iff_not, Nat.not_lt, Nat.le_zero_eq] at hn
+  omega
+
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/

src/Init/Data/Int/LemmasAux.lean

@@ -39,6 +39,9 @@ protected theorem sub_eq_iff_eq_add' {b a c : Int} : a - b = c ↔ a = b + c :=
 @[simp] theorem neg_ofNat_le_natCast (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (m : Int) :=
   Int.le_trans (by simp) (ofNat_zero_le m)
 
+theorem neg_lt_self_iff {n : Int} : -n < n ↔ 0 < n := by
+  omega
+
 /-! ### toNat -/
 
 @[simp] theorem toNat_sub' (a : Int) (b : Nat) : (a - b).toNat = a.toNat - b := by
@@ -70,6 +73,9 @@ protected theorem sub_eq_iff_eq_add' {b a c : Int} : a - b = c ↔ a = b + c :=
 @[simp] theorem toNat_le {m : Int} {n : Nat} : m.toNat ≤ n ↔ m ≤ n := by omega
 @[simp] theorem toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < n := by omega
 
+theorem pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat := by
+  omega
+
 /-! ### natAbs -/
 
 theorem eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) :

src/Init/System/Platform.lean

@@ -49,6 +49,7 @@ The LLVM target triple of the current platform. Empty if missing when Lean was c
 -/
 def target : String := getTarget ()
 
+@[simp]
 theorem numBits_pos : 0 < numBits := by
   cases numBits_eq <;> next h => simp [h]
 

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -220,7 +220,7 @@ theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w := by
 @[bv_normalize]
 theorem BitVec.not_neg (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w := by
   rw [← BitVec.neg_eq_not_add x]
-  rw [_root_.BitVec.not_neg]
+  rw [_root_.BitVec.not_neg, _root_.BitVec.sub_toAdd]
 
 @[bv_normalize]
 theorem BitVec.not_neg' (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w := by