feat: IntX theory for simprocs and bv_decide (#7259)

This PR contains theorems about `IntX` that are required for `bv_decide`
and the `IntX` simprocs.

A more comprehensive set of theorems about `IntX` will be part of future
PRs.

src/Init/Data/BitVec/Lemmas.lean

@@ -13,6 +13,7 @@ import Init.Data.Nat.Div.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Data.Int.LemmasAux
 import Init.Data.Int.Pow
 
 set_option linter.missingDocs true
@@ -569,6 +570,11 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   have p : 0 ≤ i % (2^n : Nat) := by omega
   simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
 
+theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int}
+    (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = n := by
+  have hw : w = (w - 1) + 1 := by omega
+  rw [toInt_ofInt, Int.bmod_eq_self_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
+
 @[simp] theorem ofInt_natCast (w n : Nat) :
   BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
 
@@ -2693,6 +2699,9 @@ theorem toInt_neg {x : BitVec w} :
   rw [← BitVec.zero_sub, toInt_sub]
   simp [BitVec.toInt_ofNat]
 
+theorem ofInt_neg {w : Nat} {n : Int} : BitVec.ofInt w (-n) = -BitVec.ofInt w n :=
+  eq_of_toInt_eq (by simp [toInt_neg])
+
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl

src/Init/Data/Int/LemmasAux.lean

@@ -46,4 +46,23 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
   · rw [Int.emod_eq_of_lt xpos (by omega)]; omega
   · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega
 
+@[simp] theorem natCast_le_zero : {n : Nat} → (n : Int) ≤ 0 ↔ n = 0 := by omega
+
+@[simp] theorem toNat_eq_zero : ∀ {n : Int}, n.toNat = 0 ↔ n ≤ 0 := by omega
+
+theorem eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) :
+    n = 0 := by
+  obtain ⟨a, rfl⟩ := h
+  rw [natAbs_mul] at h₁
+  suffices ¬ 0 < a.natAbs by simp [Int.natAbs_eq_zero.1 (Nat.eq_zero_of_not_pos this)]
+  exact fun h => Nat.lt_irrefl _ (Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_right d.natAbs h) h₁)
+
+theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m + 1) / 2) :
+    n.bmod m = n := by
+  rw [← Int.sub_eq_zero]
+  have := le_bmod (x := n) (m := m) (by omega)
+  have := bmod_lt (x := n) (m := m) (by omega)
+  apply eq_zero_of_dvd_of_natAbs_lt_natAbs Int.dvd_bmod_sub_self
+  omega
+
 end Int

src/Init/Data/SInt.lean

@@ -8,6 +8,7 @@ import Init.Data.SInt.Basic
 import Init.Data.SInt.Float
 import Init.Data.SInt.Float32
 import Init.Data.SInt.Lemmas
+import Init.Data.SInt.Bitwise
 
 /-!
 This module contains the definitions and basic theory about signed fixed width integer types.

src/Init/Data/SInt/Basic.lean

@@ -77,6 +77,9 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int8
 -/
 @[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec
 
+theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y
+  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
+
 /-- Obtains the `Int8` that is 2's complement equivalent to the `UInt8`. -/
 @[inline] def UInt8.toInt8 (i : UInt8) : Int8 := Int8.ofUInt8 i
 @[inline, deprecated UInt8.toInt8 (since := "2025-02-13"), inherit_doc UInt8.toInt8]
@@ -110,8 +113,8 @@ instance : ReprAtom Int8 := ⟨⟩
 instance : Hashable Int8 where
   hash i := i.toUInt8.toUInt64
 
-instance : OfNat Int8 n := ⟨Int8.ofNat n⟩
-instance : Neg Int8 where
+instance Int8.instOfNat : OfNat Int8 n := ⟨Int8.ofNat n⟩
+instance Int8.instNeg : Neg Int8 where
   neg := Int8.neg
 
 /-- The maximum value an `Int8` may attain, that is, `2^7 - 1 = 127`. -/
@@ -213,6 +216,9 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int1
 -/
 @[inline] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
 
+theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y
+  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
+
 /-- Obtains the `Int16` that is 2's complement equivalent to the `UInt16`. -/
 @[inline] def UInt16.toInt16 (i : UInt16) : Int16 := Int16.ofUInt16 i
 @[inline, deprecated UInt16.toInt16 (since := "2025-02-13"), inherit_doc UInt16.toInt16]
@@ -250,8 +256,8 @@ instance : ReprAtom Int16 := ⟨⟩
 instance : Hashable Int16 where
   hash i := i.toUInt16.toUInt64
 
-instance : OfNat Int16 n := ⟨Int16.ofNat n⟩
-instance : Neg Int16 where
+instance Int16.instOfNat : OfNat Int16 n := ⟨Int16.ofNat n⟩
+instance Int16.instNeg : Neg Int16 where
   neg := Int16.neg
 
 /-- The maximum value an `Int16` may attain, that is, `2^15 - 1 = 32767`. -/
@@ -353,6 +359,9 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int3
 -/
 @[inline] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
 
+theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y
+  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
+
 /-- Obtains the `Int32` that is 2's complement equivalent to the `UInt32`. -/
 @[inline] def UInt32.toInt32 (i : UInt32) : Int32 := Int32.ofUInt32 i
 @[inline, deprecated UInt32.toInt32 (since := "2025-02-13"), inherit_doc UInt32.toInt32]
@@ -394,8 +403,8 @@ instance : ReprAtom Int16 := ⟨⟩
 instance : Hashable Int32 where
   hash i := i.toUInt32.toUInt64
 
-instance : OfNat Int32 n := ⟨Int32.ofNat n⟩
-instance : Neg Int32 where
+instance Int32.instOfNat : OfNat Int32 n := ⟨Int32.ofNat n⟩
+instance Int32.instNeg : Neg Int32 where
   neg := Int32.neg
 
 /-- The maximum value an `Int32` may attain, that is, `2^31 - 1 = 2147483647`. -/
@@ -497,6 +506,9 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int6
 -/
 @[inline] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
 
+theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y
+  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
+
 /-- Obtains the `Int64` that is 2's complement equivalent to the `UInt64`. -/
 @[inline] def UInt64.toInt64 (i : UInt64) : Int64 := Int64.ofUInt64 i
 @[inline, deprecated UInt64.toInt64 (since := "2025-02-13"), inherit_doc UInt64.toInt64]
@@ -542,8 +554,8 @@ instance : ReprAtom Int64 := ⟨⟩
 instance : Hashable Int64 where
   hash i := i.toUInt64
 
-instance : OfNat Int64 n := ⟨Int64.ofNat n⟩
-instance : Neg Int64 where
+instance Int64.instOfNat : OfNat Int64 n := ⟨Int64.ofNat n⟩
+instance Int64.instNeg : Neg Int64 where
   neg := Int64.neg
 
 /-- The maximum value an `Int64` may attain, that is, `2^63 - 1 = 9223372036854775807`. -/
@@ -645,6 +657,9 @@ Obtain the `BitVec` that contains the 2's complement representation of the `ISiz
 -/
 @[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
 
+theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y
+  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
+
 /-- Obtains the `ISize` that is 2's complement equivalent to the `USize`. -/
 @[inline] def USize.toISize (i : USize) : ISize := ISize.ofUSize i
 @[inline, deprecated USize.toISize (since := "2025-02-13"), inherit_doc USize.toISize]
@@ -700,8 +715,8 @@ instance : ReprAtom ISize := ⟨⟩
 instance : Hashable ISize where
   hash i := i.toUSize.toUInt64
 
-instance : OfNat ISize n := ⟨ISize.ofNat n⟩
-instance : Neg ISize where
+instance ISize.instOfNat : OfNat ISize n := ⟨ISize.ofNat n⟩
+instance ISize.instNeg : Neg ISize where
   neg := ISize.neg
 
 /-- The maximum value an `ISize` may attain, that is, `2^(System.Platform.numBits - 1) - 1`. -/

src/Init/Data/SInt/Bitwise.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.SInt.Lemmas
+
+set_option hygiene false in
+macro "declare_bitwise_int_theorems" typeName:ident bits:term:arg : command =>
+`(
+namespace $typeName
+
+@[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec.srem b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec.smod $bits) := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod $bits) := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_abs (a : $typeName) : a.abs.toBitVec = a.toBitVec.abs := rfl
+
+end $typeName
+)
+declare_bitwise_int_theorems Int8 8
+declare_bitwise_int_theorems Int16 16
+declare_bitwise_int_theorems Int32 32
+declare_bitwise_int_theorems Int64 64
+declare_bitwise_int_theorems ISize System.Platform.numBits
+
+@[simp, int_toBitVec]
+theorem Bool.toBitVec_toInt8 {b : Bool} : b.toInt8.toBitVec = (BitVec.ofBool b).setWidth 8 := by
+  cases b <;> simp [toInt8]
+
+@[simp, int_toBitVec]
+theorem Bool.toBitVec_toInt16 {b : Bool} : b.toInt16.toBitVec = (BitVec.ofBool b).setWidth 16 := by
+  cases b <;> simp [toInt16]
+
+@[simp, int_toBitVec]
+theorem Bool.toBitVec_toInt32 {b : Bool} : b.toInt32.toBitVec = (BitVec.ofBool b).setWidth 32 := by
+  cases b <;> simp [toInt32]
+
+@[simp, int_toBitVec]
+theorem Bool.toBitVec_toInt64 {b : Bool} : b.toInt64.toBitVec = (BitVec.ofBool b).setWidth 64 := by
+  cases b <;> simp [toInt64]
+
+@[simp, int_toBitVec]
+theorem Bool.toBitVec_toISize {b : Bool} :
+    b.toISize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits := by
+  cases b
+  · simp [toISize]
+  · apply BitVec.eq_of_toNat_eq
+    simp [toISize]

src/Init/Data/SInt/Lemmas.lean

@@ -5,6 +5,34 @@ Authors: Markus Himmel
 -/
 prelude
 import Init.Data.SInt.Basic
+import Init.Data.BitVec.Lemmas
+
+open Lean in
+set_option hygiene false in
+macro "declare_int_theorems" typeName:ident _bits:term:arg : command => do
+  let mut cmds ← Syntax.getArgs <$> `(
+  namespace $typeName
+
+  @[int_toBitVec] theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec.sle b.toBitVec := Iff.rfl
+  @[int_toBitVec] theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec.slt b.toBitVec := Iff.rfl
+  theorem toBitVec_inj {a b : $typeName} : a.toBitVec = b.toBitVec ↔ a = b :=
+    ⟨toBitVec.inj, (· ▸ rfl)⟩
+  @[int_toBitVec] theorem eq_iff_toBitVec_eq {a b : $typeName} : a = b ↔ a.toBitVec = b.toBitVec :=
+    toBitVec_inj.symm
+  @[int_toBitVec] theorem ne_iff_toBitVec_ne {a b : $typeName} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec :=
+    Decidable.not_iff_not.2 eq_iff_toBitVec_eq
+  @[simp] theorem toBitVec_ofNat {n : Nat} : toBitVec (ofNat n) = BitVec.ofNat _ n := rfl
+  @[simp, int_toBitVec] theorem toBitVec_ofNatOfNat {n : Nat} : toBitVec (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+  end $typeName
+  )
+  return ⟨mkNullNode cmds⟩
+
+declare_int_theorems Int8 8
+declare_int_theorems Int16 16
+declare_int_theorems Int32 32
+declare_int_theorems Int64 64
+declare_int_theorems ISize System.Platform.numBits
 
 @[simp] theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec := rfl
 @[simp] theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec := rfl
@@ -23,3 +51,48 @@ import Init.Data.SInt.Basic
 @[simp] theorem UInt32.toUInt32_toInt32 (x : UInt32) : x.toInt32.toUInt32 = x := rfl
 @[simp] theorem UInt64.toUInt64_toInt64 (x : UInt64) : x.toInt64.toUInt64 = x := rfl
 @[simp] theorem USize.toUSize_toISize (x : USize) : x.toISize.toUSize = x := rfl
+
+@[simp] theorem ISize.toBitVec_neg (x : ISize) : (-x).toBitVec = -x.toBitVec := rfl
+@[simp] theorem ISize.toBitVec_zero : (0 : ISize).toBitVec = 0 := rfl
+@[simp] theorem ISize.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt _ i := rfl
+
+@[simp] theorem Int8.neg_zero : -(0 : Int8) = 0 := rfl
+@[simp] theorem Int16.neg_zero : -(0 : Int16) = 0 := rfl
+@[simp] theorem Int32.neg_zero : -(0 : Int32) = 0 := rfl
+@[simp] theorem Int64.neg_zero : -(0 : Int64) = 0 := rfl
+@[simp] theorem ISize.neg_zero : -(0 : ISize) = 0 := ISize.toBitVec.inj (by simp)
+
+theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2^32) :
+    (ofNat n).toBitVec.toNat = n :=
+  Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h (by cases USize.size_eq <;> simp_all +decide))
+
+theorem ISize.toInt_ofInt {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self] <;> cases System.Platform.numBits_eq
+    <;> (simp_all; try omega)
+
+theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2^31 ≤ n) (hn' : n ≤ 0) :
+    toNatClampNeg (ofInt n) = 0 := by
+  rwa [toNatClampNeg, toInt_ofInt hn (by omega), Int.toNat_eq_zero]
+
+theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
+  toBitVec.inj (by simp [BitVec.ofInt_neg])
+
+theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n :=
+  toBitVec.inj (by simp)
+
+theorem ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
+  rw [← neg_ofInt, ofInt_eq_ofNat]
+
+theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) :
+    toNatClampNeg (ofNat n) = n := by
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega), Int.toNat_ofNat]
+
+theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) :
+    toNatClampNeg (-ofNat n) = 0 := by
+  rw [neg_ofNat, toNatClampNeg_ofInt_eq_zero (by omega) (by omega)]
+
+theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toInt (ofNat n) = n := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+
+theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : toInt (-ofNat n) = -n := by
+  rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt (by omega) (by omega)]