missing theorem

src/Init/Data/Int/Order.lean

@@ -599,6 +599,10 @@ theorem toNat_add {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b).toNat = a.
   match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
 
+theorem toNat_mul {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).toNat = a.toNat * b.toNat :=
+  match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
+
 theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toNat + n :=
   match a, eq_ofNat_of_zero_le ha with | _, ⟨_, rfl⟩ => rfl
 

src/Init/Data/UInt/Basic.lean

@@ -20,6 +20,9 @@ def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
 def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 :=
   UInt8.ofNatLT n h
 
+/-- Converts an `Int` to a `UInt8` by taking the (non-negative remainder of the division by `2 ^ 8`. -/
+def UInt8.ofInt (x : Int) : UInt8 := ofNat (x % 2 ^ 8).toNat
+
 /--
 Adds two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
 operator.
@@ -217,6 +220,9 @@ def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
 def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 :=
   UInt16.ofNatLT n h
 
+/-- Converts an `Int` to a `UInt16` by taking the (non-negative remainder of the division by `2 ^ 16`. -/
+def UInt16.ofInt (x : Int) : UInt16 := ofNat (x % 2 ^ 16).toNat
+
 /--
 Adds two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
 operator.
@@ -416,6 +422,9 @@ def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
 def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 :=
   UInt32.ofNatLT n h
 
+/-- Converts an `Int` to a `UInt32` by taking the (non-negative remainder of the division by `2 ^ 32`. -/
+def UInt32.ofInt (x : Int) : UInt32 := ofNat (x % 2 ^ 32).toNat
+
 /--
 Adds two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
 operator.
@@ -577,6 +586,9 @@ def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
 def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 :=
   UInt64.ofNatLT n h
 
+/-- Converts an `Int` to a `UInt64` by taking the (non-negative remainder of the division by `2 ^ 64`. -/
+def UInt64.ofInt (x : Int) : UInt64 := ofNat (x % 2 ^ 64).toNat
+
 /--
 Adds two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
 operator.
@@ -774,6 +786,9 @@ def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
 def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
   USize.ofNatLT n h
 
+/-- Converts an `Int` to a `USize` by taking the (non-negative remainder of the division by `2 ^ numBits`. -/
+def USize.ofInt (x : Int) : USize := ofNat (x % 2 ^ System.Platform.numBits).toNat
+
 @[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
 @[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
 

src/Init/Data/UInt/Lemmas.lean

@@ -286,6 +286,17 @@ declare_uint_theorems USize System.Platform.numBits
 theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
   toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h USize.le_size)
 
+theorem UInt8.ofNat_mod_size : ofNat (x % 2 ^ 8) = ofNat x := by
+  simp [ofNat, BitVec.ofNat, Fin.ofNat']
+theorem UInt16.ofNat_mod_size : ofNat (x % 2 ^ 16) = ofNat x := by
+  simp [ofNat, BitVec.ofNat, Fin.ofNat']
+theorem UInt32.ofNat_mod_size : ofNat (x % 2 ^ 32) = ofNat x := by
+  simp [ofNat, BitVec.ofNat, Fin.ofNat']
+theorem UInt64.ofNat_mod_size : ofNat (x % 2 ^ 64) = ofNat x := by
+  simp [ofNat, BitVec.ofNat, Fin.ofNat']
+theorem USize.ofNat_mod_size : ofNat (x % 2 ^ System.Platform.numBits) = ofNat x := by
+  simp [ofNat, BitVec.ofNat, Fin.ofNat']
+
 theorem UInt8.lt_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by
   rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h]
 theorem UInt8.ofNat_lt_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by
@@ -2081,6 +2092,23 @@ theorem USize.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : USize) : USize.ofNat a =
     USize.ofNatLT (a % b) (Nat.mod_lt_of_lt ha) = USize.ofNatLT a ha % USize.ofNatLT b hb := by
   simp [USize.ofNatLT_eq_ofNat, USize.ofNat_mod ha hb]
 
+@[simp] theorem UInt8.ofInt_one : ofInt 1 = 1 := rfl
+@[simp] theorem UInt8.ofInt_neg_one : ofInt (-1) = -1 := rfl
+@[simp] theorem UInt16.ofInt_one : ofInt 1 = 1 := rfl
+@[simp] theorem UInt16.ofInt_neg_one : ofInt (-1) = -1 := rfl
+@[simp] theorem UInt32.ofInt_one : ofInt 1 = 1 := rfl
+@[simp] theorem UInt32.ofInt_neg_one : ofInt (-1) = -1 := rfl
+@[simp] theorem UInt64.ofInt_one : ofInt 1 = 1 := rfl
+@[simp] theorem UInt64.ofInt_neg_one : ofInt (-1) = -1 := rfl
+@[simp] theorem USize.ofInt_one : ofInt 1 = 1 := by
+  rcases System.Platform.numBits_eq with h | h <;>
+  · apply USize.toNat_inj.mp
+    simp_all [USize.ofInt, USize.ofNat, size, toNat]
+@[simp] theorem USize.ofInt_neg_one : ofInt (-1) = -1 := by
+  rcases System.Platform.numBits_eq with h | h <;>
+  · apply USize.toNat_inj.mp
+    simp_all [USize.ofInt, USize.ofNat, size, toNat]
+
 @[simp] theorem UInt8.ofNat_add (a b : Nat) : UInt8.ofNat (a + b) = UInt8.ofNat a + UInt8.ofNat b := by
   simp [UInt8.ofNat_eq_iff_mod_eq_toNat]
 @[simp] theorem UInt16.ofNat_add (a b : Nat) : UInt16.ofNat (a + b) = UInt16.ofNat a + UInt16.ofNat b := by
@@ -2092,6 +2120,70 @@ theorem USize.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : USize) : USize.ofNat a =
 @[simp] theorem USize.ofNat_add (a b : Nat) : USize.ofNat (a + b) = USize.ofNat a + USize.ofNat b := by
   simp [USize.ofNat_eq_iff_mod_eq_toNat]
 
+@[simp] theorem UInt8.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y := by
+  dsimp only [UInt8.ofInt]
+  rw [Int.add_emod]
+  have h₁ : 0 ≤ x % 2 ^ 8 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 8 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ x % 2 ^ 8 + y % 2 ^ 8 := Int.add_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_add h₁ h₂]
+  have : (2 ^ 8 : Int).toNat = 2 ^ 8 := rfl
+  rw [this, UInt8.ofNat_mod_size, UInt8.ofNat_add]
+@[simp] theorem UInt16.ofInt_add (x y : Int) : UInt16.ofInt (x + y) = UInt16.ofInt x + UInt16.ofInt y := by
+  dsimp only [UInt16.ofInt]
+  rw [Int.add_emod]
+  have h₁ : 0 ≤ x % 2 ^ 16 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 16 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ x % 2 ^ 16 + y % 2 ^ 16 := Int.add_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_add h₁ h₂]
+  have : (2 ^ 16 : Int).toNat = 2 ^ 16 := rfl
+  rw [this, UInt16.ofNat_mod_size, UInt16.ofNat_add]
+@[simp] theorem UInt32.ofInt_add (x y : Int) : UInt32.ofInt (x + y) = UInt32.ofInt x + UInt32.ofInt y := by
+  dsimp only [UInt32.ofInt]
+  rw [Int.add_emod]
+  have h₁ : 0 ≤ x % 2 ^ 32 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 32 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ x % 2 ^ 32 + y % 2 ^ 32 := Int.add_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_add h₁ h₂]
+  have : (2 ^ 32 : Int).toNat = 2 ^ 32 := rfl
+  rw [this, UInt32.ofNat_mod_size, UInt32.ofNat_add]
+@[simp] theorem UInt64.ofInt_add (x y : Int) : UInt64.ofInt (x + y) = UInt64.ofInt x + UInt64.ofInt y := by
+  dsimp only [UInt64.ofInt]
+  rw [Int.add_emod]
+  have h₁ : 0 ≤ x % 2 ^ 64 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 64 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ x % 2 ^ 64 + y % 2 ^ 64 := Int.add_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_add h₁ h₂]
+  have : (2 ^ 64 : Int).toNat = 2 ^ 64 := rfl
+  rw [this, UInt64.ofNat_mod_size, UInt64.ofNat_add]
+
+namespace System.Platform
+
+theorem two_pow_numBits_nonneg : 0 ≤ (2 ^ System.Platform.numBits : Int) := by
+  rcases System.Platform.numBits_eq with h | h <;>
+  · rw [h]
+    decide
+theorem two_pow_numBits_ne_zero : (2 ^ System.Platform.numBits : Int) ≠ 0 := by
+  rcases System.Platform.numBits_eq with h | h <;>
+  · rw [h]
+    decide
+
+end System.Platform
+
+open System.Platform in
+@[simp] theorem USize.ofInt_add (x y : Int) : USize.ofInt (x + y) = USize.ofInt x + USize.ofInt y := by
+  dsimp only [USize.ofInt]
+  rw [Int.add_emod]
+  have h₁ : 0 ≤ x % 2 ^ numBits := Int.emod_nonneg _ two_pow_numBits_ne_zero
+  have h₂ : 0 ≤ y % 2 ^ numBits := Int.emod_nonneg _ two_pow_numBits_ne_zero
+  have h₃ : 0 ≤ x % 2 ^ numBits + y % 2 ^ numBits := Int.add_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ two_pow_numBits_nonneg, Int.toNat_add h₁ h₂]
+  have : (2 ^ numBits : Int).toNat = 2 ^ numBits := by
+    rcases System.Platform.numBits_eq with h | h <;>
+    · rw [h]
+      decide
+  rw [this, USize.ofNat_mod_size, USize.ofNat_add]
+
 @[simp] theorem UInt8.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ 8) :
     UInt8.ofNatLT (a + b) hab = UInt8.ofNatLT a (Nat.lt_of_add_right_lt hab) + UInt8.ofNatLT b (Nat.lt_of_add_left_lt hab) := by
   simp [UInt8.ofNatLT_eq_ofNat]
@@ -2176,6 +2268,56 @@ theorem USize.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (ha
 @[simp] theorem USize.ofNat_mul (a b : Nat) : USize.ofNat (a * b) = USize.ofNat a * USize.ofNat b := by
   simp [USize.ofNat_eq_iff_mod_eq_toNat]
 
+@[simp] theorem UInt8.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y := by
+  dsimp only [UInt8.ofInt]
+  rw [Int.mul_emod]
+  have h₁ : 0 ≤ x % 2 ^ 8 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 8 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ (x % 2 ^ 8) * (y % 2 ^ 8) := Int.mul_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_mul h₁ h₂]
+  have : (2 ^ 8 : Int).toNat = 2 ^ 8 := rfl
+  rw [this, UInt8.ofNat_mod_size, UInt8.ofNat_mul]
+@[simp] theorem UInt16.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y := by
+  dsimp only [UInt16.ofInt]
+  rw [Int.mul_emod]
+  have h₁ : 0 ≤ x % 2 ^ 16 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 16 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ (x % 2 ^ 16) * (y % 2 ^ 16) := Int.mul_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_mul h₁ h₂]
+  have : (2 ^ 16 : Int).toNat = 2 ^ 16 := rfl
+  rw [this, UInt16.ofNat_mod_size, UInt16.ofNat_mul]
+@[simp] theorem UInt32.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y := by
+  dsimp only [UInt32.ofInt]
+  rw [Int.mul_emod]
+  have h₁ : 0 ≤ x % 2 ^ 32 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 32 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ (x % 2 ^ 32) * (y % 2 ^ 32) := Int.mul_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_mul h₁ h₂]
+  have : (2 ^ 32 : Int).toNat = 2 ^ 32 := rfl
+  rw [this, UInt32.ofNat_mod_size, UInt32.ofNat_mul]
+@[simp] theorem UInt64.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y := by
+  dsimp only [UInt64.ofInt]
+  rw [Int.mul_emod]
+  have h₁ : 0 ≤ x % 2 ^ 64 := Int.emod_nonneg _ (by decide)
+  have h₂ : 0 ≤ y % 2 ^ 64 := Int.emod_nonneg _ (by decide)
+  have h₃ : 0 ≤ (x % 2 ^ 64) * (y % 2 ^ 64) := Int.mul_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ (by decide), Int.toNat_mul h₁ h₂]
+  have : (2 ^ 64 : Int).toNat = 2 ^ 64 := rfl
+  rw [this, UInt64.ofNat_mod_size, UInt64.ofNat_mul]
+open System.Platform in
+@[simp] theorem USize.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y := by
+  dsimp only [USize.ofInt]
+  rw [Int.mul_emod]
+  have h₁ : 0 ≤ x % 2 ^ numBits := Int.emod_nonneg _ two_pow_numBits_ne_zero
+  have h₂ : 0 ≤ y % 2 ^ numBits := Int.emod_nonneg _ two_pow_numBits_ne_zero
+  have h₃ : 0 ≤ (x % 2 ^ numBits) * (y % 2 ^ numBits) := Int.mul_nonneg h₁ h₂
+  rw [Int.toNat_emod h₃ two_pow_numBits_nonneg, Int.toNat_mul h₁ h₂]
+  have : (2 ^ numBits : Int).toNat = 2 ^ numBits := by
+    rcases System.Platform.numBits_eq with h | h <;>
+    · rw [h]
+      decide
+  rw [this, USize.ofNat_mod_size, USize.ofNat_mul]
+
 @[simp] theorem UInt8.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) (hab : a * b < 2 ^ 8) :
     UInt8.ofNatLT (a * b) hab = UInt8.ofNatLT a ha * UInt8.ofNatLT b hb := by
   simp [UInt8.ofNatLT_eq_ofNat]
@@ -2467,6 +2609,17 @@ protected theorem USize.neg_add {a b : USize} : - (a + b) = -a - b := USize.toBi
 @[simp] protected theorem USize.neg_sub {a b : USize} : -(a - b) = b - a := by
   rw [USize.sub_eq_add_neg, USize.neg_add, USize.sub_neg, USize.add_comm, ← USize.sub_eq_add_neg]
 
+@[simp] protected theorem UInt8.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x := by
+  rw [Int.neg_eq_neg_one_mul, ofInt_mul, ofInt_neg_one, ← UInt8.neg_eq_neg_one_mul]
+@[simp] protected theorem UInt16.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x := by
+  rw [Int.neg_eq_neg_one_mul, ofInt_mul, ofInt_neg_one, ← UInt16.neg_eq_neg_one_mul]
+@[simp] protected theorem UInt32.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x := by
+  rw [Int.neg_eq_neg_one_mul, ofInt_mul, ofInt_neg_one, ← UInt32.neg_eq_neg_one_mul]
+@[simp] protected theorem UInt64.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x := by
+  rw [Int.neg_eq_neg_one_mul, ofInt_mul, ofInt_neg_one, ← UInt64.neg_eq_neg_one_mul]
+@[simp] protected theorem USize.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x := by
+  rw [Int.neg_eq_neg_one_mul, ofInt_mul, ofInt_neg_one, ← USize.neg_eq_neg_one_mul]
+
 @[simp] protected theorem UInt8.add_left_inj {a b : UInt8} (c : UInt8) : (a + c = b + c) ↔ a = b := by
   simp [← UInt8.toBitVec_inj]
 @[simp] protected theorem UInt16.add_left_inj {a b : UInt16} (c : UInt16) : (a + c = b + c) ↔ a = b := by