From d66abc0fc05cbf2e6062a6f4bc85cd86ba30a084 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 18 Mar 2025 11:52:54 +0100 Subject: [PATCH] feat: lemmas about operations on finite unsigned integers (#7484) This PR adds some lemmas about operations defined on `UIntX` --- src/Init/Data/BitVec/Bitblast.lean | 1 + src/Init/Data/BitVec/Lemmas.lean | 3 + src/Init/Data/SInt/Bitwise.lean | 49 +++ src/Init/Data/String/Extra.lean | 8 +- src/Init/Data/UInt/Bitwise.lean | 366 ++++++++++++++++- src/Init/Data/UInt/Lemmas.lean | 622 ++++++++++++++++++++++++++++- 6 files changed, 1025 insertions(+), 24 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 1a99e02ea9..aeda7fc646 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -515,6 +515,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} : @[simp] theorem BitVec.setWidth_neg_of_le {x : BitVec v} (h : w ≤ v) : BitVec.setWidth w (-x) = -BitVec.setWidth w x := by simp [← BitVec.signExtend_eq_setWidth_of_le _ h, BitVec.signExtend_neg_of_le h] + /-! ### abs -/ theorem msb_abs {w : Nat} {x : BitVec w} : diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index aee476a82c..dfd9de79a6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3384,6 +3384,9 @@ theorem neg_mul_not_eq_add_mul {x y : BitVec w} : rw [not_eq_neg_add, mul_sub, neg_sub, ← BitVec.mul_neg, neg_neg, BitVec.mul_one, BitVec.add_comm] +theorem neg_eq_neg_one_mul (b : BitVec w) : -b = -1#w * b := + BitVec.eq_of_toInt_eq (by simp) + /-! ### le and lt -/ @[bitvec_to_nat] theorem le_def {x y : BitVec n} : diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean index a365f67292..8e4f59dbfb 100644 --- a/src/Init/Data/SInt/Bitwise.lean +++ b/src/Init/Data/SInt/Bitwise.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ prelude +import Init.Data.UInt.Bitwise import Init.Data.SInt.Lemmas set_option hygiene false in @@ -55,3 +56,51 @@ theorem Bool.toBitVec_toISize {b : Bool} : · simp [toISize] · apply BitVec.eq_of_toNat_eq simp [toISize] + +@[simp] theorem UInt8.toInt8_add (a b : UInt8) : (a + b).toInt8 = a.toInt8 + b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_add (a b : UInt16) : (a + b).toInt16 = a.toInt16 + b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_add (a b : UInt32) : (a + b).toInt32 = a.toInt32 + b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_add (a b : UInt64) : (a + b).toInt64 = a.toInt64 + b.toInt64 := rfl +@[simp] theorem USize.toISize_add (a b : USize) : (a + b).toISize = a.toISize + b.toISize := rfl + +@[simp] theorem UInt8.toInt8_neg (a : UInt8) : (-a).toInt8 = -a.toInt8 := rfl +@[simp] theorem UInt16.toInt16_neg (a : UInt16) : (-a).toInt16 = -a.toInt16 := rfl +@[simp] theorem UInt32.toInt32_neg (a : UInt32) : (-a).toInt32 = -a.toInt32 := rfl +@[simp] theorem UInt64.toInt64_neg (a : UInt64) : (-a).toInt64 = -a.toInt64 := rfl +@[simp] theorem USize.toISize_neg (a : USize) : (-a).toISize = -a.toISize := rfl + +@[simp] theorem UInt8.toInt8_sub (a b : UInt8) : (a - b).toInt8 = a.toInt8 - b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_sub (a b : UInt16) : (a - b).toInt16 = a.toInt16 - b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_sub (a b : UInt32) : (a - b).toInt32 = a.toInt32 - b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_sub (a b : UInt64) : (a - b).toInt64 = a.toInt64 - b.toInt64 := rfl +@[simp] theorem USize.toISize_sub (a b : USize) : (a - b).toISize = a.toISize - b.toISize := rfl + +@[simp] theorem UInt8.toInt8_mul (a b : UInt8) : (a * b).toInt8 = a.toInt8 * b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_mul (a b : UInt16) : (a * b).toInt16 = a.toInt16 * b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_mul (a b : UInt32) : (a * b).toInt32 = a.toInt32 * b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_mul (a b : UInt64) : (a * b).toInt64 = a.toInt64 * b.toInt64 := rfl +@[simp] theorem USize.toISize_mul (a b : USize) : (a * b).toISize = a.toISize * b.toISize := rfl + +@[simp] theorem UInt8.toInt8_and (a b : UInt8) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_and (a b : UInt16) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_and (a b : UInt32) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_and (a b : UInt64) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64 := rfl +@[simp] theorem USize.toISize_and (a b : USize) : (a &&& b).toISize = a.toISize &&& b.toISize := rfl + +@[simp] theorem UInt8.toInt8_or (a b : UInt8) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_or (a b : UInt16) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_or (a b : UInt32) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_or (a b : UInt64) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64 := rfl +@[simp] theorem USize.toISize_or (a b : USize) : (a ||| b).toISize = a.toISize ||| b.toISize := rfl + +@[simp] theorem UInt8.toInt8_xor (a b : UInt8) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8 := rfl +@[simp] theorem UInt16.toInt16_xor (a b : UInt16) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16 := rfl +@[simp] theorem UInt32.toInt32_xor (a b : UInt32) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32 := rfl +@[simp] theorem UInt64.toInt64_xor (a b : UInt64) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64 := rfl +@[simp] theorem USize.toISize_xor (a b : USize) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize := rfl + +@[simp] theorem UInt8.toInt8_not (a : UInt8) : (~~~a).toInt8 = ~~~a.toInt8 := rfl +@[simp] theorem UInt16.toInt16_not (a : UInt16) : (~~~a).toInt16 = ~~~a.toInt16 := rfl +@[simp] theorem UInt32.toInt32_not (a : UInt32) : (~~~a).toInt32 = ~~~a.toInt32 := rfl +@[simp] theorem UInt64.toInt64_not (a : UInt64) : (~~~a).toInt64 = ~~~a.toInt64 := rfl +@[simp] theorem USize.toISize_not (a : USize) : (~~~a).toISize = ~~~a.toISize := rfl diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 5080193ff9..29c2ac8fd1 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -44,7 +44,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32 guard (0x80 ≤ r) -- TODO: Prove h from the definition of r once we have the necessary lemmas - if h : r < 0xd800 then some ⟨r, .inl (UInt32.toNat_lt_of_lt (by decide) h)⟩ else none + if h : r < 0xd800 then some ⟨r, .inl ((UInt32.lt_ofNat_iff (by decide)).1 h)⟩ else none else if c &&& 0xf0 == 0xe0 then let c1 ← a[i+1]? let c2 ← a[i+2]? @@ -58,8 +58,8 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then have := match h with - | .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h) - | .inr h => Or.inr ⟨UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right⟩ + | .inl h => Or.inl ((UInt32.lt_ofNat_iff (by decide)).1 h) + | .inr h => Or.inr ⟨(UInt32.ofNat_lt_iff (by decide)).1 h.left, (UInt32.lt_ofNat_iff (by decide)).1 h.right⟩ some ⟨r, this⟩ else none @@ -74,7 +74,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do ((c2 &&& 0x3f).toUInt32 <<< 6) ||| (c3 &&& 0x3f).toUInt32 if h : 0x10000 ≤ r ∧ r < 0x110000 then - some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right⟩⟩ + some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) ((UInt32.ofNat_le_iff (by decide)).1 h.left), (UInt32.lt_ofNat_iff (by decide)).1 h.right⟩⟩ else none else none diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean index 24e905888d..4875077e24 100644 --- a/src/Init/Data/UInt/Bitwise.lean +++ b/src/Init/Data/UInt/Bitwise.lean @@ -6,20 +6,13 @@ Authors: Markus Himmel, Mac Malone prelude import Init.Data.UInt.Lemmas import Init.Data.Fin.Bitwise -import Init.Data.BitVec.Lemmas set_option hygiene false in macro "declare_bitwise_uint_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 / b.toBitVec := rfl -@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl @[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl -@[simp, int_toBitVec] protected theorem toBitVec_neg {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 @@ -71,3 +64,362 @@ theorem Bool.toBitVec_toUSize {b : Bool} : · simp [toUSize] · apply BitVec.eq_of_toNat_eq simp [toUSize] + +@[simp] theorem UInt8.toFin_and (a b : UInt8) : (a &&& b).toFin = a.toFin &&& b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt16.toFin_and (a b : UInt16) : (a &&& b).toFin = a.toFin &&& b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt32.toFin_and (a b : UInt32) : (a &&& b).toFin = a.toFin &&& b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt64.toFin_and (a b : UInt64) : (a &&& b).toFin = a.toFin &&& b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem USize.toFin_and (a b : USize) : (a &&& b).toFin = a.toFin &&& b.toFin := Fin.val_inj.1 (by simp) + +@[simp] theorem UInt8.toUInt16_and (a b : UInt8) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16 := rfl +@[simp] theorem UInt8.toUInt32_and (a b : UInt8) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32 := rfl +@[simp] theorem UInt8.toUInt64_and (a b : UInt8) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64 := rfl +@[simp] theorem UInt8.toUSize_and (a b : UInt8) : (a &&& b).toUSize = a.toUSize &&& b.toUSize := rfl + +@[simp] theorem UInt16.toUInt8_and (a b : UInt16) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt16.toUInt32_and (a b : UInt16) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32 := rfl +@[simp] theorem UInt16.toUInt64_and (a b : UInt16) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64 := rfl +@[simp] theorem UInt16.toUSize_and (a b : UInt16) : (a &&& b).toUSize = a.toUSize &&& b.toUSize := rfl + +@[simp] theorem UInt32.toUInt8_and (a b : UInt32) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt16_and (a b : UInt32) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt64_and (a b : UInt32) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64 := rfl +@[simp] theorem UInt32.toUSize_and (a b : UInt32) : (a &&& b).toUSize = a.toUSize &&& b.toUSize := rfl + +@[simp] theorem USize.toUInt8_and (a b : USize) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt16_and (a b : USize) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt32_and (a b : USize) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt64_and (a b : USize) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64 := rfl + +@[simp] theorem UInt64.toUInt8_and (a b : UInt64) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt16_and (a b : UInt64) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt32_and (a b : UInt64) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUSize_and (a b : UInt64) : (a &&& b).toUSize = a.toUSize &&& b.toUSize := USize.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt8.toFin_or (a b : UInt8) : (a ||| b).toFin = a.toFin ||| b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt16.toFin_or (a b : UInt16) : (a ||| b).toFin = a.toFin ||| b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt32.toFin_or (a b : UInt32) : (a ||| b).toFin = a.toFin ||| b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt64.toFin_or (a b : UInt64) : (a ||| b).toFin = a.toFin ||| b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem USize.toFin_or (a b : USize) : (a ||| b).toFin = a.toFin ||| b.toFin := Fin.val_inj.1 (by simp) + +@[simp] theorem UInt8.toUInt16_or (a b : UInt8) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16 := rfl +@[simp] theorem UInt8.toUInt32_or (a b : UInt8) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32 := rfl +@[simp] theorem UInt8.toUInt64_or (a b : UInt8) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64 := rfl +@[simp] theorem UInt8.toUSize_or (a b : UInt8) : (a ||| b).toUSize = a.toUSize ||| b.toUSize := rfl + +@[simp] theorem UInt16.toUInt8_or (a b : UInt16) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt16.toUInt32_or (a b : UInt16) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32 := rfl +@[simp] theorem UInt16.toUInt64_or (a b : UInt16) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64 := rfl +@[simp] theorem UInt16.toUSize_or (a b : UInt16) : (a ||| b).toUSize = a.toUSize ||| b.toUSize := rfl + +@[simp] theorem UInt32.toUInt8_or (a b : UInt32) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt16_or (a b : UInt32) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt64_or (a b : UInt32) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64 := rfl +@[simp] theorem UInt32.toUSize_or (a b : UInt32) : (a ||| b).toUSize = a.toUSize ||| b.toUSize := rfl + +@[simp] theorem USize.toUInt8_or (a b : USize) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt16_or (a b : USize) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt32_or (a b : USize) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt64_or (a b : USize) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64 := rfl + +@[simp] theorem UInt64.toUInt8_or (a b : UInt64) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt16_or (a b : UInt64) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt32_or (a b : UInt64) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUSize_or (a b : UInt64) : (a ||| b).toUSize = a.toUSize ||| b.toUSize := USize.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt8.toFin_xor (a b : UInt8) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt16.toFin_xor (a b : UInt16) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt32.toFin_xor (a b : UInt32) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem UInt64.toFin_xor (a b : UInt64) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin := Fin.val_inj.1 (by simp) +@[simp] theorem USize.toFin_xor (a b : USize) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin := Fin.val_inj.1 (by simp) + +@[simp] theorem UInt8.toUInt16_xor (a b : UInt8) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16 := rfl +@[simp] theorem UInt8.toUInt32_xor (a b : UInt8) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32 := rfl +@[simp] theorem UInt8.toUInt64_xor (a b : UInt8) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64 := rfl +@[simp] theorem UInt8.toUSize_xor (a b : UInt8) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize := rfl + +@[simp] theorem UInt16.toUInt8_xor (a b : UInt16) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt16.toUInt32_xor (a b : UInt16) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32 := rfl +@[simp] theorem UInt16.toUInt64_xor (a b : UInt16) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64 := rfl +@[simp] theorem UInt16.toUSize_xor (a b : UInt16) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize := rfl + +@[simp] theorem UInt32.toUInt8_xor (a b : UInt32) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt16_xor (a b : UInt32) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt64_xor (a b : UInt32) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64 := rfl +@[simp] theorem UInt32.toUSize_xor (a b : UInt32) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize := rfl + +@[simp] theorem USize.toUInt8_xor (a b : USize) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt16_xor (a b : USize) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt32_xor (a b : USize) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt64_xor (a b : USize) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64 := rfl + +@[simp] theorem UInt64.toUInt8_xor (a b : UInt64) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt16_xor (a b : UInt64) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt32_xor (a b : UInt64) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUSize_xor (a b : UInt64) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize := USize.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt8.toNat_not (a : UInt8) : (~~~a).toNat = UInt8.size - 1 - a.toNat := by + rw [← toNat_toBitVec, UInt8.toBitVec_not, BitVec.toNat_not, toNat_toBitVec] +@[simp] theorem UInt16.toNat_not (a : UInt16) : (~~~a).toNat = UInt16.size - 1 - a.toNat := by + rw [← toNat_toBitVec, UInt16.toBitVec_not, BitVec.toNat_not, toNat_toBitVec] +@[simp] theorem UInt32.toNat_not (a : UInt32) : (~~~a).toNat = UInt32.size - 1 - a.toNat := by + rw [← toNat_toBitVec, UInt32.toBitVec_not, BitVec.toNat_not, toNat_toBitVec] +@[simp] theorem UInt64.toNat_not (a : UInt64) : (~~~a).toNat = UInt64.size - 1 - a.toNat := by + rw [← toNat_toBitVec, UInt64.toBitVec_not, BitVec.toNat_not, toNat_toBitVec] +@[simp] theorem USize.toNat_not (a : USize) : (~~~a).toNat = USize.size - 1 - a.toNat := by + rw [← toNat_toBitVec, USize.toBitVec_not, BitVec.toNat_not, toNat_toBitVec] + +@[simp] theorem UInt8.toFin_not (a : UInt8) : (~~~a).toFin = a.toFin.rev := by + rw [← toFin_toBitVec, UInt8.toBitVec_not, BitVec.toFin_not, toFin_toBitVec] +@[simp] theorem UInt16.toFin_not (a : UInt16) : (~~~a).toFin = a.toFin.rev := by + rw [← toFin_toBitVec, UInt16.toBitVec_not, BitVec.toFin_not, toFin_toBitVec] +@[simp] theorem UInt32.toFin_not (a : UInt32) : (~~~a).toFin = a.toFin.rev := by + rw [← toFin_toBitVec, UInt32.toBitVec_not, BitVec.toFin_not, toFin_toBitVec] +@[simp] theorem UInt64.toFin_not (a : UInt64) : (~~~a).toFin = a.toFin.rev := by + rw [← toFin_toBitVec, UInt64.toBitVec_not, BitVec.toFin_not, toFin_toBitVec] +@[simp] theorem USize.toFin_not (a : USize) : (~~~a).toFin = a.toFin.rev := by + rw [← toFin_toBitVec, USize.toBitVec_not, BitVec.toFin_not, toFin_toBitVec] + +@[simp] theorem UInt16.toUInt8_not (a : UInt16) : (~~~a).toUInt8 = ~~~a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt8_not (a : UInt32) : (~~~a).toUInt8 = ~~~a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt8_not (a : UInt64) : (~~~a).toUInt8 = ~~~a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt8_not (a : USize) : (~~~a).toUInt8 = ~~~a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt32.toUInt16_not (a : UInt32) : (~~~a).toUInt16 = ~~~a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt16_not (a : UInt64) : (~~~a).toUInt16 = ~~~a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt16_not (a : USize) : (~~~a).toUInt16 = ~~~a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt64.toUInt32_not (a : UInt64) : (~~~a).toUInt32 = ~~~a.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt32_not (a : USize) : (~~~a).toUInt32 = ~~~a.toUInt32 := UInt32.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt64.toUSize_not (a : UInt64) : (~~~a).toUSize = ~~~a.toUSize := USize.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt8.toUInt16_not (a : UInt8) : (~~~a).toUInt16 = ~~~a.toUInt16 % 256 := by + simp [UInt8.toUInt16_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt32_not (a : UInt8) : (~~~a).toUInt32 = ~~~a.toUInt32 % 256 := by + simp [UInt8.toUInt32_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt64_not (a : UInt8) : (~~~a).toUInt64 = ~~~a.toUInt64 % 256 := by + simp [UInt8.toUInt64_eq_mod_256_iff] +@[simp] theorem UInt8.toUSize_not (a : UInt8) : (~~~a).toUSize = ~~~a.toUSize % 256 := by + simp [UInt8.toUSize_eq_mod_256_iff] + +@[simp] theorem UInt16.toUInt32_not (a : UInt16) : (~~~a).toUInt32 = ~~~a.toUInt32 % 65536 := by + simp [UInt16.toUInt32_eq_mod_65536_iff] +@[simp] theorem UInt16.toUInt64_not (a : UInt16) : (~~~a).toUInt64 = ~~~a.toUInt64 % 65536 := by + simp [UInt16.toUInt64_eq_mod_65536_iff] +@[simp] theorem UInt16.toUSize_not (a : UInt16) : (~~~a).toUSize = ~~~a.toUSize % 65536 := by + simp [UInt16.toUSize_eq_mod_65536_iff] + +@[simp] theorem UInt32.toUInt64_not (a : UInt32) : (~~~a).toUInt64 = ~~~a.toUInt64 % 4294967296 := by + simp [UInt32.toUInt64_eq_mod_4294967296_iff] +@[simp] theorem UInt32.toUSize_not (a : UInt32) : (~~~a).toUSize = ~~~a.toUSize % 4294967296 := by + simp [UInt32.toUSize_eq_mod_4294967296_iff] + +@[simp] theorem USize.toUInt64_not (a : USize) : (~~~a).toUInt64 = ~~~a.toUInt64 % UInt64.ofNat USize.size := by + simp [USize.toUInt64_eq_mod_usizeSize_iff] + +@[simp] theorem UInt8.toFin_shiftLeft (a b : UInt8) (hb : b < 8) : (a <<< b).toFin = a.toFin <<< b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 8) hb]) +@[simp] theorem UInt16.toFin_shiftLeft (a b : UInt16) (hb : b < 16) : (a <<< b).toFin = a.toFin <<< b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 16) hb]) +@[simp] theorem UInt32.toFin_shiftLeft (a b : UInt32) (hb : b < 32) : (a <<< b).toFin = a.toFin <<< b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 32) hb]) +@[simp] theorem UInt64.toFin_shiftLeft (a b : UInt64) (hb : b < 64) : (a <<< b).toFin = a.toFin <<< b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 64) hb]) +@[simp] theorem USize.toFin_shiftLeft (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toFin = a.toFin <<< b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := System.Platform.numBits) hb]) + + +theorem UInt8.shiftLeft_eq_shiftLeft_mod (a b : UInt8) : a <<< b = a <<< (b % 8) := UInt8.toBitVec_inj.1 (by simp) +theorem UInt16.shiftLeft_eq_shiftLeft_mod (a b : UInt16) : a <<< b = a <<< (b % 16) := UInt16.toBitVec_inj.1 (by simp) +theorem UInt32.shiftLeft_eq_shiftLeft_mod (a b : UInt32) : a <<< b = a <<< (b % 32) := UInt32.toBitVec_inj.1 (by simp) +theorem UInt64.shiftLeft_eq_shiftLeft_mod (a b : UInt64) : a <<< b = a <<< (b % 64) := UInt64.toBitVec_inj.1 (by simp) +theorem USize.shiftLeft_eq_shiftLeft_mod (a b : USize) : a <<< b = a <<< (b % USize.ofNat System.Platform.numBits) := + USize.toBitVec_inj.1 (by simp) + +theorem UInt8.shiftRight_eq_shiftRight_mod (a b : UInt8) : a >>> b = a >>> (b % 8) := UInt8.toBitVec_inj.1 (by simp) +theorem UInt16.shiftRight_eq_shiftRight_mod (a b : UInt16) : a >>> b = a >>> (b % 16) := UInt16.toBitVec_inj.1 (by simp) +theorem UInt32.shiftRight_eq_shiftRight_mod (a b : UInt32) : a >>> b = a >>> (b % 32) := UInt32.toBitVec_inj.1 (by simp) +theorem UInt64.shiftRight_eq_shiftRight_mod (a b : UInt64) : a >>> b = a >>> (b % 64) := UInt64.toBitVec_inj.1 (by simp) +theorem USize.shiftRight_eq_shiftRight_mod (a b : USize) : a >>> b = a >>> (b % USize.ofNat System.Platform.numBits) := + USize.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt16.toUInt8_shiftLeft (a b : UInt16) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + apply UInt8.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt16.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_trans hb (by decide : 8 < 16))] + +@[simp] theorem UInt32.toUInt8_shiftLeft (a b : UInt32) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + apply UInt8.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt32.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_trans hb (by decide : 8 < 32))] +@[simp] theorem UInt32.toUInt16_shiftLeft (a b : UInt32) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + apply UInt16.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt32.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_trans hb (by decide : 16 < 32))] + +@[simp] theorem USize.toUInt8_shiftLeft (a b : USize) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + apply UInt8.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, USize.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb System.Platform.eight_le_numBits)] +@[simp] theorem USize.toUInt16_shiftLeft (a b : USize) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + apply UInt16.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, USize.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb System.Platform.sixteen_le_numBits)] +@[simp] theorem USize.toUInt32_shiftLeft (a b : USize) (hb : b < 32) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 := by + apply UInt32.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, USize.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb System.Platform.le_numBits)] + +@[simp] theorem UInt64.toUInt8_shiftLeft (a b : UInt64) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + apply UInt8.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt64.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb (by decide : 8 ≤ 64))] +@[simp] theorem UInt64.toUInt16_shiftLeft (a b : UInt64) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + apply UInt16.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt64.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb (by decide : 16 ≤ 64))] +@[simp] theorem UInt64.toUInt32_shiftLeft (a b : UInt64) (hb : b < 32) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 := by + apply UInt32.toBitVec_inj.1 + simp only [lt_iff_toNat_lt, UInt64.reduceToNat] at hb + simp [Nat.mod_eq_of_lt hb, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb (by decide : 32 ≤ 64))] +@[simp] theorem UInt64.toUSize_shiftLeft (a b : UInt64) (hb : b.toNat < System.Platform.numBits) : + (a <<< b).toUSize = a.toUSize <<< b.toUSize := by + apply USize.toBitVec_inj.1 + have h₁ : b.toNat % 64 = b.toNat := Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le hb System.Platform.numBits_le) + have h₂ : b.toNat % (2 ^ System.Platform.numBits) % System.Platform.numBits = b.toNat := by + rw [Nat.mod_eq_of_lt (a := b.toNat), Nat.mod_eq_of_lt hb] + exact Nat.lt_trans hb (Nat.lt_pow_self Nat.one_lt_two) + simp [h₁, h₂] + +@[simp] theorem UInt16.toUInt8_shiftLeft_mod (a b : UInt16) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + rw [UInt16.toUInt8_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt16.toUInt8_mod_of_dvd _ _ (by simp)] + simp [← UInt8.shiftLeft_eq_shiftLeft_mod] + +@[simp] theorem UInt32.toUInt8_shiftLeft_mod (a b : UInt32) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + rw [UInt32.toUInt8_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt32.toUInt8_mod_of_dvd _ _ (by simp)] + simp [← UInt8.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem UInt32.toUInt16_shiftLeft_mod (a b : UInt32) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + rw [UInt32.toUInt16_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt32.toUInt16_mod_of_dvd _ _ (by simp)] + simp [← UInt16.shiftLeft_eq_shiftLeft_mod] + +@[simp] theorem USize.toUInt8_shiftLeft_mod (a b : USize) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + rw [USize.toUInt8_shiftLeft _ _ (Nat.mod_lt _ (by simp [-toBitVec_ofNat])), USize.toUInt8_mod_of_dvd _ _ (by simp)] + simp [← UInt8.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem USize.toUInt16_shiftLeft_mod (a b : USize) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + rw [USize.toUInt16_shiftLeft _ _ (Nat.mod_lt _ (by simp [-toBitVec_ofNat])), USize.toUInt16_mod_of_dvd _ _ (by simp)] + simp [← UInt16.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem USize.toUInt32_shiftLeft_mod (a b : USize) : (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32 := by + rw [USize.toUInt32_shiftLeft _ _ (Nat.mod_lt _ (by simp [-toBitVec_ofNat])), USize.toUInt32_mod_of_dvd _ _ (by simp)] + simp [← UInt32.shiftLeft_eq_shiftLeft_mod] + +@[simp] theorem UInt64.toUInt8_shiftLeft_mod (a b : UInt64) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8 := by + rw [UInt64.toUInt8_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt64.toUInt8_mod_of_dvd _ _ (by simp)] + simp [← UInt8.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem UInt64.toUInt16_shiftLeft_mod (a b : UInt64) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16 := by + rw [UInt64.toUInt16_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt64.toUInt16_mod_of_dvd _ _ (by simp)] + simp [← UInt16.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem UInt64.toUInt32_shiftLeft_mod (a b : UInt64) : (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32 := by + rw [UInt64.toUInt32_shiftLeft _ _ (Nat.mod_lt _ (by decide)), UInt64.toUInt32_mod_of_dvd _ _ (by simp)] + simp [← UInt32.shiftLeft_eq_shiftLeft_mod] +@[simp] theorem UInt64.toUSize_shiftLeft_mod (a b : UInt64) : (a <<< (b % UInt64.ofNat System.Platform.numBits)).toUSize = a.toUSize <<< b.toUSize := by + rw [UInt64.toUSize_shiftLeft, UInt64.toUSize_mod_of_dvd] + · simp [← USize.shiftLeft_eq_shiftLeft_mod] + · cases System.Platform.numBits_eq <;> simp_all + · cases System.Platform.numBits_eq <;> simp_all [Nat.mod_lt] + +theorem UInt8.toUInt16_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt16 = (a.toUInt16 <<< b.toUInt16) % 256 := by + rwa [UInt8.toUInt16_eq_mod_256_iff, UInt16.toUInt8_shiftLeft, toUInt8_toUInt16, toUInt8_toUInt16] +theorem UInt8.toUInt32_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt32 = (a.toUInt32 <<< b.toUInt32) % 256 := by + rwa [UInt8.toUInt32_eq_mod_256_iff, UInt32.toUInt8_shiftLeft, toUInt8_toUInt32, toUInt8_toUInt32] +theorem UInt8.toUInt64_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt64 = (a.toUInt64 <<< b.toUInt64) % 256 := by + rwa [UInt8.toUInt64_eq_mod_256_iff, UInt64.toUInt8_shiftLeft, toUInt8_toUInt64, toUInt8_toUInt64] +theorem UInt8.toUSize_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUSize = (a.toUSize <<< b.toUSize) % 256 := by + rw [UInt8.toUSize_eq_mod_256_iff, USize.toUInt8_shiftLeft, toUInt8_toUSize, toUInt8_toUSize] + simpa [USize.lt_iff_toNat_lt] + +theorem UInt16.toUInt32_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUInt32 = (a.toUInt32 <<< b.toUInt32) % 65536 := by + rwa [UInt16.toUInt32_eq_mod_65536_iff, UInt32.toUInt16_shiftLeft, toUInt16_toUInt32, toUInt16_toUInt32] +theorem UInt16.toUInt64_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUInt64 = (a.toUInt64 <<< b.toUInt64) % 65536 := by + rwa [UInt16.toUInt64_eq_mod_65536_iff, UInt64.toUInt16_shiftLeft, toUInt16_toUInt64, toUInt16_toUInt64] +theorem UInt16.toUSize_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUSize = (a.toUSize <<< b.toUSize) % 65536 := by + rw [UInt16.toUSize_eq_mod_65536_iff, USize.toUInt16_shiftLeft, toUInt16_toUSize, toUInt16_toUSize] + simpa [USize.lt_iff_toNat_lt] + +theorem UInt32.toUInt64_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) : (a <<< b).toUInt64 = (a.toUInt64 <<< b.toUInt64) % 4294967296 := by + rwa [UInt32.toUInt64_eq_mod_4294967296_iff, UInt64.toUInt32_shiftLeft, toUInt32_toUInt64, toUInt32_toUInt64] +theorem UInt32.toUSize_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) : (a <<< b).toUSize = (a.toUSize <<< b.toUSize) % 4294967296 := by + rw [UInt32.toUSize_eq_mod_4294967296_iff, USize.toUInt32_shiftLeft, toUInt32_toUSize, toUInt32_toUSize] + simpa [USize.lt_iff_toNat_lt] + +theorem USize.toUInt64_shiftLeft_of_lt (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toUInt64 = (a.toUInt64 <<< b.toUInt64) % UInt64.ofNat USize.size := by + rwa [USize.toUInt64_eq_mod_usizeSize_iff, UInt64.toUSize_shiftLeft, toUSize_toUInt64, toUSize_toUInt64] + +@[simp] theorem UInt8.toUInt16_shiftLeft (a b : UInt8) : (a <<< b).toUInt16 = (a.toUInt16 <<< (b % 8).toUInt16) % 256 := by + simp [UInt8.toUInt16_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt32_shiftLeft (a b : UInt8) : (a <<< b).toUInt32 = (a.toUInt32 <<< (b % 8).toUInt32) % 256 := by + simp [UInt8.toUInt32_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt64_shiftLeft (a b : UInt8) : (a <<< b).toUInt64 = (a.toUInt64 <<< (b % 8).toUInt64) % 256 := by + simp [UInt8.toUInt64_eq_mod_256_iff] +@[simp] theorem UInt8.toUSize_shiftLeft (a b : UInt8) : (a <<< b).toUSize = (a.toUSize <<< (b % 8).toUSize) % 256 := by + simp [UInt8.toUSize_eq_mod_256_iff] + +@[simp] theorem UInt16.toUInt32_shiftLeft (a b : UInt16) : (a <<< b).toUInt32 = (a.toUInt32 <<< (b % 16).toUInt32) % 65536 := by + simp [UInt16.toUInt32_eq_mod_65536_iff] +@[simp] theorem UInt16.toUInt64_shiftLeft (a b : UInt16) : (a <<< b).toUInt64 = (a.toUInt64 <<< (b % 16).toUInt64) % 65536 := by + simp [UInt16.toUInt64_eq_mod_65536_iff] +@[simp] theorem UInt16.toUSize_shiftLeft (a b : UInt16) : (a <<< b).toUSize = (a.toUSize <<< (b % 16).toUSize) % 65536 := by + simp [UInt16.toUSize_eq_mod_65536_iff] + +@[simp] theorem UInt32.toUInt64_shiftLeft (a b : UInt32) : (a <<< b).toUInt64 = (a.toUInt64 <<< (b % 32).toUInt64) % 4294967296 := by + simp [UInt32.toUInt64_eq_mod_4294967296_iff] +@[simp] theorem UInt32.toUSize_shiftLeft (a b : UInt32) : (a <<< b).toUSize = (a.toUSize <<< (b % 32).toUSize) % 4294967296 := by + simp [UInt32.toUSize_eq_mod_4294967296_iff] + +@[simp] theorem USize.toUInt64_shiftLeft (a b : USize) : + (a <<< b).toUInt64 = (a.toUInt64 <<< (b % USize.ofNat System.Platform.numBits).toUInt64) % UInt64.ofNat USize.size := by + have : System.Platform.numBits < USize.size := Nat.lt_of_le_of_lt System.Platform.numBits_le (Nat.lt_of_lt_of_le (by decide) USize.le_size) + simp [USize.toUInt64_eq_mod_usizeSize_iff, toUInt64_ofNat' this] + +@[simp] theorem UInt8.toFin_shiftRight (a b : UInt8) (hb : b < 8) : (a >>> b).toFin = a.toFin >>> b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 8) hb]) +@[simp] theorem UInt16.toFin_shiftRight (a b : UInt16) (hb : b < 16) : (a >>> b).toFin = a.toFin >>> b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 16) hb]) +@[simp] theorem UInt32.toFin_shiftRight (a b : UInt32) (hb : b < 32) : (a >>> b).toFin = a.toFin >>> b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 32) hb]) +@[simp] theorem UInt64.toFin_shiftRight (a b : UInt64) (hb : b < 64) : (a >>> b).toFin = a.toFin >>> b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := 64) hb]) +@[simp] theorem USize.toFin_shiftRight (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a >>> b).toFin = a.toFin >>> b.toFin := + Fin.val_inj.1 (by simp [Nat.mod_eq_of_lt (a := b.toNat) (b := System.Platform.numBits) hb]) + +@[simp] theorem UInt8.toUInt16_shiftRight (a b : UInt8) : (a >>> b).toUInt16 = a.toUInt16 >>> (b.toUInt16 % 8) := + UInt16.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 8 ∣ 16)]) +@[simp] theorem UInt8.toUInt32_shiftRight (a b : UInt8) : (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 8) := + UInt32.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 8 ∣ 32)]) +@[simp] theorem UInt8.toUInt64_shiftRight (a b : UInt8) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 8) := + UInt64.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 8 ∣ 64)]) +@[simp] theorem UInt8.toUSize_shiftRight (a b : UInt8) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 8) := + USize.toBitVec_inj.1 (by cases System.Platform.numBits_eq <;> + simp_all [Nat.mod_mod_of_dvd' (by decide : 8 ∣ 32), Nat.mod_mod_of_dvd' (by decide : 8 ∣ 64)]) + +@[simp] theorem UInt16.toUInt32_shiftRight (a b : UInt16) : (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 16) := + UInt32.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 16 ∣ 32)]) +@[simp] theorem UInt16.toUInt64_shiftRight (a b : UInt16) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 16) := + UInt64.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 16 ∣ 64)]) +@[simp] theorem UInt16.toUSize_shiftRight (a b : UInt16) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 16) := + USize.toBitVec_inj.1 (by cases System.Platform.numBits_eq <;> + simp_all [Nat.mod_mod_of_dvd' (by decide : 16 ∣ 32), Nat.mod_mod_of_dvd' (by decide : 16 ∣ 64)]) + +@[simp] theorem UInt32.toUInt64_shiftRight (a b : UInt32) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 32) := + UInt64.toBitVec_inj.1 (by simp [Nat.mod_mod_of_dvd' (by decide : 32 ∣ 64)]) +@[simp] theorem UInt32.toUSize_shiftRight (a b : UInt32) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 32) := + USize.toBitVec_inj.1 (by cases System.Platform.numBits_eq <;> + simp_all [Nat.mod_mod_of_dvd' (by decide : 32 ∣ 32), Nat.mod_mod_of_dvd' (by decide : 32 ∣ 64)]) + +@[simp] theorem USize.toUInt64_shiftRight (a b : USize) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % UInt64.ofNat System.Platform.numBits) := + UInt64.toBitVec_inj.1 (by cases System.Platform.numBits_eq <;> simp_all [Nat.mod_mod_of_dvd' (by decide : 32 ∣ 64)]) + +/-! +There is no reasonable statement for`UInt16.toUInt8_shiftRight`; in fact for `a b : UInt16` the +expression `(a >>> b).toUInt8` is not a function of `a.toUInt8` and `b.toUInt8`. +-/ diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index 82ab94f584..776ceb4cc4 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -6,8 +6,11 @@ Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Mar prelude import Init.Data.UInt.Basic import Init.Data.Fin.Lemmas +import Init.Data.Fin.Bitwise import Init.Data.BitVec.Lemmas import Init.Data.BitVec.Bitblast +import Init.Data.Nat.Div.Lemmas +import Init.System.Platform open Lean in set_option hygiene false in @@ -220,6 +223,13 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do @[deprecated ofBitVec_ofNat (since := "2025-02-12")] theorem mk_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := rfl + @[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 / b.toBitVec := rfl + @[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl + @[simp, int_toBitVec] protected theorem toBitVec_neg {a : $typeName} : (-a).toBitVec = -a.toBitVec := rfl + ) if let some nbits := bits.raw.isNatLit? then if nbits > 8 then @@ -265,21 +275,72 @@ 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 UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by - rw [lt_def, BitVec.lt_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h] - exact id +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 + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt8.le_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] +theorem UInt8.ofNat_le_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] -theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by - rw [lt_def, BitVec.lt_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h] - exact id +theorem UInt16.lt_ofNat_iff {n : UInt16} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt16.ofNat_lt_iff {n : UInt16} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt16.le_ofNat_iff {n : UInt16} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] +theorem UInt16.ofNat_le_iff {n : UInt16} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] -theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by - rw [le_def, BitVec.le_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h] - exact id +theorem UInt32.lt_ofNat_iff {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt32.ofNat_lt_iff {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt32.le_ofNat_iff {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] +theorem UInt32.ofNat_le_iff {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] -theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by - rw [le_def, BitVec.le_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h] - exact id +@[deprecated UInt32.lt_ofNat_iff (since := "2025-03-18")] +theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := + (UInt32.lt_ofNat_iff h).1 + +@[deprecated UInt32.ofNat_lt_iff (since := "2025-03-18")] +theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := + (UInt32.ofNat_lt_iff h).1 + +@[deprecated UInt32.le_ofNat_iff (since := "2025-03-18")] +theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := + (UInt32.le_ofNat_iff h).1 + +@[deprecated UInt32.ofNat_le_iff (since := "2025-03-18")] +theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := + (UInt32.ofNat_le_iff h).1 + +theorem UInt64.lt_ofNat_iff {n : UInt64} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt64.ofNat_lt_iff {n : UInt64} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem UInt64.le_ofNat_iff {n : UInt64} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] +theorem UInt64.ofNat_le_iff {n : UInt64} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] + +theorem USize.lt_ofNat_iff {n : USize} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem USize.ofNat_lt_iff {n : USize} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat := by + rw [lt_iff_toNat_lt, toNat_ofNat_of_lt' h] +theorem USize.le_ofNat_iff {n : USize} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] +theorem USize.ofNat_le_iff {n : USize} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat := by + rw [le_iff_toNat_le, toNat_ofNat_of_lt' h] + +theorem UInt8.mod_eq_of_lt {a b : UInt8} (h : a < b) : a % b = a := UInt8.toNat_inj.1 (Nat.mod_eq_of_lt h) +theorem UInt16.mod_eq_of_lt {a b : UInt16} (h : a < b) : a % b = a := UInt16.toNat_inj.1 (Nat.mod_eq_of_lt h) +theorem UInt32.mod_eq_of_lt {a b : UInt32} (h : a < b) : a % b = a := UInt32.toNat_inj.1 (Nat.mod_eq_of_lt h) +theorem UInt64.mod_eq_of_lt {a b : UInt64} (h : a < b) : a % b = a := UInt64.toNat_inj.1 (Nat.mod_eq_of_lt h) +theorem USize.mod_eq_of_lt {a b : USize} (h : a < b) : a % b = a := USize.toNat_inj.1 (Nat.mod_eq_of_lt h) @[simp] theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8 := n.toFin.isLt @[simp] theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16 := n.toFin.isLt @@ -800,12 +861,19 @@ theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < USize.size) : @[simp] theorem USize.toUSize_toUInt64 (n : USize) : n.toUInt64.toUSize = n := USize.toNat.inj (by simp) +@[simp] theorem USize.toUSize_toUInt32 (n : USize) : n.toUInt32.toUSize = n % 4294967296 := by + apply USize.toNat.inj + simp only [UInt32.toNat_toUSize, toNat_toUInt32, Nat.reducePow, USize.toNat_mod] + cases USize.size_eq + · next h => rw [Nat.mod_eq_of_lt (h ▸ n.toNat_lt_size), USize.toNat_ofNat, + ← USize.size_eq_two_pow, h, Nat.mod_self, Nat.mod_zero] + · next h => rw [USize.toNat_ofNat_of_lt]; simp_all + -- Note: we are currently missing the following four results for which there does not seem to -- be a good candidate for the RHS: -- @[simp] theorem UInt64.toUInt64_toUSize (n : UInt64) : n.toUSize.toUInt64 = ? := -- @[simp] theorem UInt64.toUSize_toUInt32 (n : UInt64) : n.toUInt32.toUSize = ? := -- @[simp] theorem USize.toUInt64_toUInt32 (n : USize) : n.toUInt32.toUInt64 = ? := --- @[simp] theorem USize.toUSize_toUInt32 (n : USize) : n.toInt32.toUSize = ? := @[simp] theorem UInt8.toNat_ofFin (x : Fin UInt8.size) : (UInt8.ofFin x).toNat = x.val := rfl @[simp] theorem UInt16.toNat_ofFin (x : Fin UInt16.size) : (UInt16.ofFin x).toNat = x.val := rfl @@ -1344,3 +1412,531 @@ theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) : BitVec.eq_of_toNat_eq (by simp) @[simp] theorem BitVec.ofNat_uSizeToNat (n : USize) : BitVec.ofNat System.Platform.numBits n.toNat = n.toBitVec := BitVec.eq_of_toNat_eq (by simp) + +@[simp] protected theorem UInt8.toFin_div (a b : UInt8) : (a / b).toFin = a.toFin / b.toFin := rfl +@[simp] protected theorem UInt16.toFin_div (a b : UInt16) : (a / b).toFin = a.toFin / b.toFin := rfl +@[simp] protected theorem UInt32.toFin_div (a b : UInt32) : (a / b).toFin = a.toFin / b.toFin := rfl +@[simp] protected theorem UInt64.toFin_div (a b : UInt64) : (a / b).toFin = a.toFin / b.toFin := rfl +@[simp] protected theorem USize.toFin_div (a b : USize) : (a / b).toFin = a.toFin / b.toFin := rfl + +@[simp] theorem UInt8.toUInt16_div (a b : UInt8) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16 := rfl +@[simp] theorem UInt8.toUInt32_div (a b : UInt8) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32 := rfl +@[simp] theorem UInt8.toUInt64_div (a b : UInt8) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64 := rfl +@[simp] theorem UInt8.toUSize_div (a b : UInt8) : (a / b).toUSize = a.toUSize / b.toUSize := rfl + +@[simp] theorem UInt16.toUInt32_div (a b : UInt16) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32 := rfl +@[simp] theorem UInt16.toUInt64_div (a b : UInt16) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64 := rfl +@[simp] theorem UInt16.toUSize_div (a b : UInt16) : (a / b).toUSize = a.toUSize / b.toUSize := rfl + +@[simp] theorem UInt32.toUInt64_div (a b : UInt32) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64 := rfl +@[simp] theorem UInt32.toUSize_div (a b : UInt32) : (a / b).toUSize = a.toUSize / b.toUSize := rfl + +@[simp] theorem USize.toUInt64_div (a b : USize) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64 := rfl + +theorem UInt16.toUInt8_div (a b : UInt16) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) + +theorem UInt32.toUInt8_div (a b : UInt32) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) +theorem UInt32.toUInt16_div (a b : UInt32) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) + +theorem USize.toUInt8_div (a b : USize) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8 := + UInt8.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt8.size_lt_usizeSize] using Nat.div_mod_eq_mod_div_mod ha hb) +theorem USize.toUInt16_div (a b : USize) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16 := + UInt16.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt16.size_lt_usizeSize] using Nat.div_mod_eq_mod_div_mod ha hb) + +theorem UInt64.toUInt8_div (a b : UInt64) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) +theorem UInt64.toUInt16_div (a b : UInt64) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) +theorem UInt64.toUInt32_div (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32 := + UInt32.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) +theorem UInt64.toUSize_div (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a / b).toUSize = a.toUSize / b.toUSize := + USize.toNat.inj (Nat.div_mod_eq_mod_div_mod (Nat.lt_of_lt_of_le ha UInt32.size_le_usizeSize) (Nat.lt_of_lt_of_le hb UInt32.size_le_usizeSize)) +theorem UInt64.toUSize_div_of_toNat_lt (a b : UInt64) (ha : a.toNat < USize.size) (hb : b.toNat < USize.size) : + (a / b).toUSize = a.toUSize / b.toUSize := + USize.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb) + +@[simp] protected theorem UInt8.toFin_mod (a b : UInt8) : (a % b).toFin = a.toFin % b.toFin := rfl +@[simp] protected theorem UInt16.toFin_mod (a b : UInt8) : (a % b).toFin = a.toFin % b.toFin := rfl +@[simp] protected theorem UInt32.toFin_mod (a b : UInt32) : (a % b).toFin = a.toFin % b.toFin := rfl +@[simp] protected theorem UInt64.toFin_mod (a b : UInt64) : (a % b).toFin = a.toFin % b.toFin := rfl +@[simp] protected theorem USize.toFin_mod (a b : USize) : (a % b).toFin = a.toFin % b.toFin := rfl + +@[simp] theorem UInt8.toUInt16_mod (a b : UInt8) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := rfl +@[simp] theorem UInt8.toUInt32_mod (a b : UInt8) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := rfl +@[simp] theorem UInt8.toUInt64_mod (a b : UInt8) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64 := rfl +@[simp] theorem UInt8.toUSize_mod (a b : UInt8) : (a % b).toUSize = a.toUSize % b.toUSize := rfl + +@[simp] theorem UInt16.toUInt32_mod (a b : UInt16) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := rfl +@[simp] theorem UInt16.toUInt64_mod (a b : UInt16) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64 := rfl +@[simp] theorem UInt16.toUSize_mod (a b : UInt16) : (a % b).toUSize = a.toUSize % b.toUSize := rfl + +@[simp] theorem UInt32.toUInt64_mod (a b : UInt32) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64 := rfl +@[simp] theorem UInt32.toUSize_mod (a b : UInt32) : (a % b).toUSize = a.toUSize % b.toUSize := rfl + +@[simp] theorem USize.toUInt64_mod (a b : USize) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64 := rfl + +theorem UInt16.toUInt8_mod (a b : UInt16) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt16.toUInt8_mod_of_dvd (a b : UInt16) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) + +theorem UInt32.toUInt8_mod (a b : UInt32) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt32.toUInt16_mod (a b : UInt32) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt32.toUInt8_mod_of_dvd (a b : UInt32) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem UInt32.toUInt16_mod_of_dvd (a b : UInt32) (hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) + +theorem USize.toUInt8_mod (a b : USize) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt8.size_lt_usizeSize] using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem USize.toUInt16_mod (a b : USize) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt16.size_lt_usizeSize] using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem USize.toUInt32_mod (a b : USize) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := by + apply UInt32.toNat.inj + simp only [toNat_toUInt32, USize.toNat_mod, Nat.reducePow, UInt32.toNat_mod] + have := Nat.mod_mod_eq_mod_mod_mod ha hb + obtain (h|h) := USize.size_eq + · have ha' := h ▸ a.toNat_lt_size + have hb' := h ▸ b.toNat_lt_size + rw [Nat.mod_eq_of_lt ha', Nat.mod_eq_of_lt hb', Nat.mod_eq_of_lt] + exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) ha' + · simp_all +theorem USize.toUInt8_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt8.size_lt_usizeSize] using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem USize.toUInt16_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa [Nat.mod_eq_of_lt UInt16.size_lt_usizeSize] using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem USize.toUInt32_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := by + apply UInt32.toNat.inj + simp only [toNat_toUInt32, USize.toNat_mod, Nat.reducePow, UInt32.toNat_mod] + have := Nat.mod_mod_eq_mod_mod_mod_of_dvd (a := a.toNat) hb + obtain (h|h) := USize.size_eq + · have ha' := h ▸ a.toNat_lt_size + have hb' := h ▸ b.toNat_lt_size + rw [Nat.mod_eq_of_lt ha', Nat.mod_eq_of_lt hb', Nat.mod_eq_of_lt] + exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) ha' + · simp_all + +theorem UInt64.toUInt8_mod (a b : UInt64) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt64.toUInt16_mod (a b : UInt64) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt64.toUInt32_mod (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := + UInt32.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt64.toUSize_mod (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUSize = a.toUSize % b.toUSize := + USize.toNat.inj (Nat.mod_mod_eq_mod_mod_mod (Nat.lt_of_lt_of_le ha UInt32.size_le_usizeSize) (Nat.lt_of_lt_of_le hb UInt32.size_le_usizeSize)) +theorem UInt64.toUSize_mod_of_toNat_lt (a b : UInt64) (ha : a.toNat < USize.size) (hb : b.toNat < USize.size) : (a % b).toUSize = a.toUSize % b.toUSize := + USize.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod ha hb) +theorem UInt64.toUInt8_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8 := + UInt8.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem UInt64.toUInt16_mod_of_dvd (a b : UInt64)(hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16 := + UInt16.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem UInt64.toUInt32_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32 := + UInt32.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) +theorem UInt64.toUSize_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 4294967296) : (a % b).toUSize = a.toUSize % b.toUSize := + USize.toNat.inj (Nat.mod_mod_eq_mod_mod_mod_of_dvd (Nat.dvd_trans hb UInt32.size_dvd_usizeSize)) +theorem UInt64.toUSize_mod_of_dvd_usizeSize (a b : UInt64) (hb : b.toNat ∣ USize.size) : (a % b).toUSize = a.toUSize % b.toUSize := + USize.toNat.inj (by simpa using Nat.mod_mod_eq_mod_mod_mod_of_dvd hb) + +@[simp] protected theorem UInt8.toFin_add (a b : UInt8) : (a + b).toFin = a.toFin + b.toFin := rfl +@[simp] protected theorem UInt16.toFin_add (a b : UInt16) : (a + b).toFin = a.toFin + b.toFin := rfl +@[simp] protected theorem UInt32.toFin_add (a b : UInt32) : (a + b).toFin = a.toFin + b.toFin := rfl +@[simp] protected theorem UInt64.toFin_add (a b : UInt64) : (a + b).toFin = a.toFin + b.toFin := rfl +@[simp] protected theorem USize.toFin_add (a b : USize) : (a + b).toFin = a.toFin + b.toFin := rfl + +@[simp] theorem UInt16.toUInt8_add (a b : UInt16) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem UInt32.toUInt8_add (a b : UInt32) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem UInt64.toUInt8_add (a b : UInt64) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem USize.toUInt8_add (a b : USize) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8 := UInt8.toNat.inj (by simp) + +@[simp] theorem UInt32.toUInt16_add (a b : UInt32) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16 := UInt16.toNat.inj (by simp) +@[simp] theorem UInt64.toUInt16_add (a b : UInt64) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16 := UInt16.toNat.inj (by simp) +@[simp] theorem USize.toUInt16_add (a b : USize) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16 := UInt16.toNat.inj (by simp) + +@[simp] theorem UInt64.toUInt32_add (a b : UInt64) : (a + b).toUInt32 = a.toUInt32 + b.toUInt32 := UInt32.toNat.inj (by simp) +@[simp] theorem USize.toUInt32_add (a b : USize) : (a + b).toUInt32 = a.toUInt32 + b.toUInt32 := UInt32.toNat.inj (by simp) + +@[simp] theorem UInt64.toUSize_add (a b : UInt64) : (a + b).toUSize = a.toUSize + b.toUSize := USize.toNat.inj (by simp) + +@[simp] theorem UInt8.toUInt16_add (a b : UInt8) : (a + b).toUInt16 = (a.toUInt16 + b.toUInt16) % 256 := UInt16.toNat.inj (by simp) +@[simp] theorem UInt8.toUInt32_add (a b : UInt8) : (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 256 := UInt32.toNat.inj (by simp) +@[simp] theorem UInt8.toUInt64_add (a b : UInt8) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 256 := UInt64.toNat.inj (by simp) +@[simp] theorem UInt8.toUSize_add (a b : UInt8) : (a + b).toUSize = (a.toUSize + b.toUSize) % 256 := USize.toNat.inj (by simp) + +@[simp] theorem UInt16.toUInt32_add (a b : UInt16) : (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 65536 := UInt32.toNat.inj (by simp) +@[simp] theorem UInt16.toUInt64_add (a b : UInt16) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 65536 := UInt64.toNat.inj (by simp) +@[simp] theorem UInt16.toUSize_add (a b : UInt16) : (a + b).toUSize = (a.toUSize + b.toUSize) % 65536 := USize.toNat.inj (by simp) + +@[simp] theorem UInt32.toUInt64_add (a b : UInt32) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 4294967296 := UInt64.toNat.inj (by simp) +/-- Note that on 32-bit machines we are doing a modulo by zero. -/ +@[simp] theorem UInt32.toUSize_add (a b : UInt32) : (a + b).toUSize = (a.toUSize + b.toUSize) % 4294967296 := + USize.toNat.inj (by cases System.Platform.numBits_eq <;> simp_all [USize.toNat_ofNat]) + +@[simp] protected theorem UInt8.toFin_sub (a b : UInt8) : (a - b).toFin = a.toFin - b.toFin := rfl +@[simp] protected theorem UInt16.toFin_sub (a b : UInt16) : (a - b).toFin = a.toFin - b.toFin := rfl +@[simp] protected theorem UInt32.toFin_sub (a b : UInt32) : (a - b).toFin = a.toFin - b.toFin := rfl +@[simp] protected theorem UInt64.toFin_sub (a b : UInt64) : (a - b).toFin = a.toFin - b.toFin := rfl +@[simp] protected theorem USize.toFin_sub (a b : USize) : (a - b).toFin = a.toFin - b.toFin := rfl + +@[simp] protected theorem UInt8.toFin_mul (a b : UInt8) : (a * b).toFin = a.toFin * b.toFin := rfl +@[simp] protected theorem UInt16.toFin_mul (a b : UInt16) : (a * b).toFin = a.toFin * b.toFin := rfl +@[simp] protected theorem UInt32.toFin_mul (a b : UInt32) : (a * b).toFin = a.toFin * b.toFin := rfl +@[simp] protected theorem UInt64.toFin_mul (a b : UInt64) : (a * b).toFin = a.toFin * b.toFin := rfl +@[simp] protected theorem USize.toFin_mul (a b : USize) : (a * b).toFin = a.toFin * b.toFin := rfl + +@[simp] theorem UInt16.toUInt8_mul (a b : UInt16) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem UInt32.toUInt8_mul (a b : UInt32) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem UInt64.toUInt8_mul (a b : UInt64) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8 := UInt8.toNat.inj (by simp) +@[simp] theorem USize.toUInt8_mul (a b : USize) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8 := UInt8.toNat.inj (by simp) + +@[simp] theorem UInt32.toUInt16_mul (a b : UInt32) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16 := UInt16.toNat.inj (by simp) +@[simp] theorem UInt64.toUInt16_mul (a b : UInt64) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16 := UInt16.toNat.inj (by simp) +@[simp] theorem USize.toUInt16_mul (a b : USize) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16 := UInt16.toNat.inj (by simp) + +@[simp] theorem UInt64.toUInt32_mul (a b : UInt64) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32 := UInt32.toNat.inj (by simp) +@[simp] theorem USize.toUInt32_mul (a b : USize) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32 := UInt32.toNat.inj (by simp) + +@[simp] theorem UInt64.toUSize_mul (a b : UInt64) : (a * b).toUSize = a.toUSize * b.toUSize := USize.toNat.inj (by simp) + +@[simp] theorem UInt8.toUInt16_mul (a b : UInt8) : (a * b).toUInt16 = (a.toUInt16 * b.toUInt16) % 256 := UInt16.toNat.inj (by simp) +@[simp] theorem UInt8.toUInt32_mul (a b : UInt8) : (a * b).toUInt32 = (a.toUInt32 * b.toUInt32) % 256 := UInt32.toNat.inj (by simp) +@[simp] theorem UInt8.toUInt64_mul (a b : UInt8) : (a * b).toUInt64 = (a.toUInt64 * b.toUInt64) % 256 := UInt64.toNat.inj (by simp) +@[simp] theorem UInt8.toUSize_mul (a b : UInt8) : (a * b).toUSize = (a.toUSize * b.toUSize) % 256 := USize.toNat.inj (by simp) + +@[simp] theorem UInt16.toUInt32_mul (a b : UInt16) : (a * b).toUInt32 = (a.toUInt32 * b.toUInt32) % 65536 := UInt32.toNat.inj (by simp) +@[simp] theorem UInt16.toUInt64_mul (a b : UInt16) : (a * b).toUInt64 = (a.toUInt64 * b.toUInt64) % 65536 := UInt64.toNat.inj (by simp) +@[simp] theorem UInt16.toUSize_mul (a b : UInt16) : (a * b).toUSize = (a.toUSize * b.toUSize) % 65536 := USize.toNat.inj (by simp) + +@[simp] theorem UInt32.toUInt64_mul (a b : UInt32) : (a * b).toUInt64 = (a.toUInt64 * b.toUInt64) % 4294967296 := UInt64.toNat.inj (by simp) +/-- Note that on 32-bit machines we are doing a modulo by zero. -/ +@[simp] theorem UInt32.toUSize_mul (a b : UInt32) : (a * b).toUSize = (a.toUSize * b.toUSize) % 4294967296 := + USize.toNat.inj (by cases System.Platform.numBits_eq <;> simp_all [USize.toNat_ofNat]) + +theorem UInt16.toUInt8_eq (a b : UInt16) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256 := by + simp [← UInt8.toNat_inj, ← UInt16.toNat_inj] +theorem UInt32.toUInt8_eq (a b : UInt32) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256 := by + simp [← UInt8.toNat_inj, ← UInt32.toNat_inj] +theorem UInt64.toUInt8_eq (a b : UInt64) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256 := by + simp [← UInt8.toNat_inj, ← UInt64.toNat_inj] +theorem USize.toUInt8_eq (a b : USize) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256 := by + simp [← UInt8.toNat_inj, ← USize.toNat_inj] + +theorem UInt32.toUInt16_eq (a b : UInt32) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536 := by + simp [← UInt16.toNat_inj, ← UInt32.toNat_inj] +theorem UInt64.toUInt16_eq (a b : UInt64) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536 := by + simp [← UInt16.toNat_inj, ← UInt64.toNat_inj] +theorem USize.toUInt16_eq (a b : USize) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536 := by + simp [← UInt16.toNat_inj, ← USize.toNat_inj] + +theorem UInt64.toUInt32_eq (a b : UInt64) : a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296 := by + simp [← UInt32.toNat_inj, ← UInt64.toNat_inj] +theorem USize.toUInt32_eq (a b : USize) : a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296 := by + simp [← UInt32.toNat_inj, ← USize.toNat_inj, USize.toNat_ofNat] + have := Nat.mod_eq_of_lt a.toNat_lt_two_pow_numBits + have := Nat.mod_eq_of_lt b.toNat_lt_two_pow_numBits + cases System.Platform.numBits_eq <;> simp_all + +theorem UInt8.toUInt16_eq_mod_256_iff (a : UInt8) (b : UInt16) : a.toUInt16 = b % 256 ↔ a = b.toUInt8 := by + simp [← UInt8.toNat_inj, ← UInt16.toNat_inj] +theorem UInt8.toUInt32_eq_mod_256_iff (a : UInt8) (b : UInt32) : a.toUInt32 = b % 256 ↔ a = b.toUInt8 := by + simp [← UInt8.toNat_inj, ← UInt32.toNat_inj] +theorem UInt8.toUInt64_eq_mod_256_iff (a : UInt8) (b : UInt64) : a.toUInt64 = b % 256 ↔ a = b.toUInt8 := by + simp [← UInt8.toNat_inj, ← UInt64.toNat_inj] +theorem UInt8.toUSize_eq_mod_256_iff (a : UInt8) (b : USize) : a.toUSize = b % 256 ↔ a = b.toUInt8 := by + simp [← UInt8.toNat_inj, ← USize.toNat_inj] + +theorem UInt16.toUInt32_eq_mod_65536_iff (a : UInt16) (b : UInt32) : a.toUInt32 = b % 65536 ↔ a = b.toUInt16 := by + simp [← UInt16.toNat_inj, ← UInt32.toNat_inj] +theorem UInt16.toUInt64_eq_mod_65536_iff (a : UInt16) (b : UInt64) : a.toUInt64 = b % 65536 ↔ a = b.toUInt16 := by + simp [← UInt16.toNat_inj, ← UInt64.toNat_inj] +theorem UInt16.toUSize_eq_mod_65536_iff (a : UInt16) (b : USize) : a.toUSize = b % 65536 ↔ a = b.toUInt16 := by + simp [← UInt16.toNat_inj, ← USize.toNat_inj] + +theorem UInt32.toUInt64_eq_mod_4294967296_iff (a : UInt32) (b : UInt64) : a.toUInt64 = b % 4294967296 ↔ a = b.toUInt32 := by + simp [← UInt32.toNat_inj, ← UInt64.toNat_inj] +theorem UInt32.toUSize_eq_mod_4294967296_iff (a : UInt32) (b : USize) : a.toUSize = b % 4294967296 ↔ a = b.toUInt32 := by + simp [← UInt32.toNat_inj, ← USize.toNat_inj, USize.toNat_ofNat] + have := Nat.mod_eq_of_lt b.toNat_lt_two_pow_numBits + cases System.Platform.numBits_eq <;> simp_all + +theorem USize.toUInt64_eq_mod_usizeSize_iff (a : USize) (b : UInt64) : a.toUInt64 = b % UInt64.ofNat USize.size ↔ a = b.toUSize := by + simp [← USize.toNat_inj, ← UInt64.toNat_inj, USize.size_eq_two_pow] + cases System.Platform.numBits_eq <;> simp_all + +theorem UInt8.toUInt16_inj {a b : UInt8} : a.toUInt16 = b.toUInt16 ↔ a = b := + ⟨fun h => by rw [← toUInt8_toUInt16 a, h, toUInt8_toUInt16], by rintro rfl; rfl⟩ +theorem UInt8.toUInt32_inj {a b : UInt8} : a.toUInt32 = b.toUInt32 ↔ a = b := + ⟨fun h => by rw [← toUInt8_toUInt32 a, h, toUInt8_toUInt32], by rintro rfl; rfl⟩ +theorem UInt8.toUInt64_inj {a b : UInt8} : a.toUInt64 = b.toUInt64 ↔ a = b := + ⟨fun h => by rw [← toUInt8_toUInt64 a, h, toUInt8_toUInt64], by rintro rfl; rfl⟩ +theorem UInt8.toUSize_inj {a b : UInt8} : a.toUSize = b.toUSize ↔ a = b := + ⟨fun h => by rw [← toUInt8_toUSize a, h, toUInt8_toUSize], by rintro rfl; rfl⟩ + +theorem UInt16.toUInt32_inj {a b : UInt16} : a.toUInt32 = b.toUInt32 ↔ a = b := + ⟨fun h => by rw [← toUInt16_toUInt32 a, h, toUInt16_toUInt32], by rintro rfl; rfl⟩ +theorem UInt16.toUInt64_inj {a b : UInt16} : a.toUInt64 = b.toUInt64 ↔ a = b := + ⟨fun h => by rw [← toUInt16_toUInt64 a, h, toUInt16_toUInt64], by rintro rfl; rfl⟩ +theorem UInt16.toUSize_inj {a b : UInt16} : a.toUSize = b.toUSize ↔ a = b := + ⟨fun h => by rw [← toUInt16_toUSize a, h, toUInt16_toUSize], by rintro rfl; rfl⟩ + +theorem UInt32.toUInt64_inj {a b : UInt32} : a.toUInt64 = b.toUInt64 ↔ a = b := + ⟨fun h => by rw [← toUInt32_toUInt64 a, h, toUInt32_toUInt64], by rintro rfl; rfl⟩ +theorem UInt32.toUSize_inj {a b : UInt32} : a.toUSize = b.toUSize ↔ a = b := + ⟨fun h => by rw [← toUInt32_toUSize a, h, toUInt32_toUSize], by rintro rfl; rfl⟩ + +theorem USize.toUInt64_inj {a b : USize} : a.toUInt64 = b.toUInt64 ↔ a = b := + ⟨fun h => by rw [← toUSize_toUInt64 a, h, toUSize_toUInt64], by rintro rfl; rfl⟩ + +@[simp] theorem UInt8.toUInt16_lt {a b : UInt8} : a.toUInt16 < b.toUInt16 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt16.lt_iff_toNat_lt] +@[simp] theorem UInt8.toUInt32_lt {a b : UInt8} : a.toUInt32 < b.toUInt32 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt32.lt_iff_toNat_lt] +@[simp] theorem UInt8.toUInt64_lt {a b : UInt8} : a.toUInt64 < b.toUInt64 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt64.lt_iff_toNat_lt] +@[simp] theorem UInt8.toUSize_lt {a b : UInt8} : a.toUSize < b.toUSize ↔ a < b := by + simp [lt_iff_toNat_lt, USize.lt_iff_toNat_lt] + +@[simp] theorem UInt16.toUInt32_lt {a b : UInt16} : a.toUInt32 < b.toUInt32 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt32.lt_iff_toNat_lt] +@[simp] theorem UInt16.toUInt64_lt {a b : UInt16} : a.toUInt64 < b.toUInt64 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt64.lt_iff_toNat_lt] +@[simp] theorem UInt16.toUSize_lt {a b : UInt16} : a.toUSize < b.toUSize ↔ a < b := by + simp [lt_iff_toNat_lt, USize.lt_iff_toNat_lt] + +@[simp] theorem UInt32.toUInt64_lt {a b : UInt32} : a.toUInt64 < b.toUInt64 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt64.lt_iff_toNat_lt] +@[simp] theorem UInt32.toUSize_lt {a b : UInt32} : a.toUSize < b.toUSize ↔ a < b := by + simp [lt_iff_toNat_lt, USize.lt_iff_toNat_lt] + +@[simp] theorem USize.toUInt64_lt {a b : USize} : a.toUInt64 < b.toUInt64 ↔ a < b := by + simp [lt_iff_toNat_lt, UInt64.lt_iff_toNat_lt] + +@[simp] theorem UInt16.toUInt8_lt {a b : UInt16} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256 := by + simp [lt_iff_toNat_lt, UInt8.lt_iff_toNat_lt] +@[simp] theorem UInt32.toUInt8_lt {a b : UInt32} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256 := by + simp [lt_iff_toNat_lt, UInt8.lt_iff_toNat_lt] +@[simp] theorem UInt64.toUInt8_lt {a b : UInt64} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256 := by + simp [lt_iff_toNat_lt, UInt8.lt_iff_toNat_lt] +@[simp] theorem USize.toUInt8_lt {a b : USize} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256 := by + simp [lt_iff_toNat_lt, UInt8.lt_iff_toNat_lt] + +@[simp] theorem UInt32.toUInt16_lt {a b : UInt32} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536 := by + simp [lt_iff_toNat_lt, UInt16.lt_iff_toNat_lt] +@[simp] theorem UInt64.toUInt16_lt {a b : UInt64} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536 := by + simp [lt_iff_toNat_lt, UInt16.lt_iff_toNat_lt] +@[simp] theorem USize.toUInt16_lt {a b : USize} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536 := by + simp [lt_iff_toNat_lt, UInt16.lt_iff_toNat_lt] + +@[simp] theorem UInt64.toUInt32_lt {a b : UInt64} : a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296 := by + simp [lt_iff_toNat_lt, UInt32.lt_iff_toNat_lt] +@[simp] theorem USize.toUInt32_lt {a b : USize} : a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296 := by + rw [← UInt32.toUSize_lt, toUSize_toUInt32] + simp [lt_iff_toNat_lt, UInt32.lt_iff_toNat_lt] + +@[simp] theorem UInt64.toUSize_lt {a b : UInt64} : a.toUSize < b.toUSize ↔ a % UInt64.ofNat USize.size < b % UInt64.ofNat USize.size := by + simp only [USize.lt_iff_toNat_lt, toNat_toUSize, lt_iff_toNat_lt, UInt64.toNat_mod, toNat_ofNat', Nat.reducePow] + cases System.Platform.numBits_eq <;> simp_all [USize.size] + +@[simp] theorem UInt8.toUInt16_le {a b : UInt8} : a.toUInt16 ≤ b.toUInt16 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt16.le_iff_toNat_le] +@[simp] theorem UInt8.toUInt32_le {a b : UInt8} : a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt32.le_iff_toNat_le] +@[simp] theorem UInt8.toUInt64_le {a b : UInt8} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt64.le_iff_toNat_le] +@[simp] theorem UInt8.toUSize_le {a b : UInt8} : a.toUSize ≤ b.toUSize ↔ a ≤ b := by + simp [le_iff_toNat_le, USize.le_iff_toNat_le] + +@[simp] theorem UInt16.toUInt32_le {a b : UInt16} : a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt32.le_iff_toNat_le] +@[simp] theorem UInt16.toUInt64_le {a b : UInt16} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt64.le_iff_toNat_le] +@[simp] theorem UInt16.toUSize_le {a b : UInt16} : a.toUSize ≤ b.toUSize ↔ a ≤ b := by + simp [le_iff_toNat_le, USize.le_iff_toNat_le] + +@[simp] theorem UInt32.toUInt64_le {a b : UInt32} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt64.le_iff_toNat_le] +@[simp] theorem UInt32.toUSize_le {a b : UInt32} : a.toUSize ≤ b.toUSize ↔ a ≤ b := by + simp [le_iff_toNat_le, USize.le_iff_toNat_le] + +@[simp] theorem USize.toUInt64_le {a b : USize} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b := by + simp [le_iff_toNat_le, UInt64.le_iff_toNat_le] + +@[simp] theorem UInt16.toUInt8_le {a b : UInt16} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256 := by + simp [le_iff_toNat_le, UInt8.le_iff_toNat_le] +@[simp] theorem UInt32.toUInt8_le {a b : UInt32} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256 := by + simp [le_iff_toNat_le, UInt8.le_iff_toNat_le] +@[simp] theorem UInt64.toUInt8_le {a b : UInt64} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256 := by + simp [le_iff_toNat_le, UInt8.le_iff_toNat_le] +@[simp] theorem USize.toUInt8_le {a b : USize} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256 := by + simp [le_iff_toNat_le, UInt8.le_iff_toNat_le] + +@[simp] theorem UInt32.toUInt16_le {a b : UInt32} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536 := by + simp [le_iff_toNat_le, UInt16.le_iff_toNat_le] +@[simp] theorem UInt64.toUInt16_le {a b : UInt64} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536 := by + simp [le_iff_toNat_le, UInt16.le_iff_toNat_le] +@[simp] theorem USize.toUInt16_le {a b : USize} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536 := by + simp [le_iff_toNat_le, UInt16.le_iff_toNat_le] + +@[simp] theorem UInt64.toUInt32_le {a b : UInt64} : a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296 := by + simp [le_iff_toNat_le, UInt32.le_iff_toNat_le] +@[simp] theorem USize.toUInt32_le {a b : USize} : a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296 := by + rw [← UInt32.toUSize_le, toUSize_toUInt32] + simp [le_iff_toNat_le, UInt32.le_iff_toNat_le] + +@[simp] theorem UInt64.toUSize_le {a b : UInt64} : a.toUSize ≤ b.toUSize ↔ a % UInt64.ofNat USize.size ≤ b % UInt64.ofNat USize.size := by + simp only [USize.le_iff_toNat_le, toNat_toUSize, le_iff_toNat_le, UInt64.toNat_mod, UInt64.reduceToNat] + cases System.Platform.numBits_eq <;> simp_all [USize.size] + +@[simp] theorem UInt16.toUInt8_neg (a : UInt16) : (-a).toUInt8 = -a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt32.toUInt8_neg (a : UInt32) : (-a).toUInt8 = -a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt32.toUInt16_neg (a : UInt32) : (-a).toUInt16 = -a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt64.toUInt8_neg (a : UInt64) : (-a).toUInt8 = -a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt16_neg (a : UInt64) : (-a).toUInt16 = -a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUInt32_neg (a : UInt64) : (-a).toUInt32 = -a.toUInt32 := UInt32.toBitVec_inj.1 (by simp) +@[simp] theorem UInt64.toUSize_neg (a : UInt64) : (-a).toUSize = -a.toUSize := USize.toBitVec_inj.1 (by simp) + +@[simp] theorem USize.toUInt8_neg (a : USize) : (-a).toUInt8 = -a.toUInt8 := UInt8.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt16_neg (a : USize) : (-a).toUInt16 = -a.toUInt16 := UInt16.toBitVec_inj.1 (by simp) +@[simp] theorem USize.toUInt32_neg (a : USize) : (-a).toUInt32 = -a.toUInt32 := UInt32.toBitVec_inj.1 (by simp) + +@[simp] theorem UInt8.toUInt16_neg (a : UInt8) : (-a).toUInt16 = -a.toUInt16 % 256 := by + simp [UInt8.toUInt16_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt32_neg (a : UInt8) : (-a).toUInt32 = -a.toUInt32 % 256 := by + simp [UInt8.toUInt32_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt64_neg (a : UInt8) : (-a).toUInt64 = -a.toUInt64 % 256 := by + simp [UInt8.toUInt64_eq_mod_256_iff] +@[simp] theorem UInt8.toUSize_neg (a : UInt8) : (-a).toUSize = -a.toUSize % 256 := by + simp [UInt8.toUSize_eq_mod_256_iff] + +@[simp] theorem UInt16.toUInt32_neg (a : UInt16) : (-a).toUInt32 = -a.toUInt32 % 65536 := by + simp [UInt16.toUInt32_eq_mod_65536_iff] +@[simp] theorem UInt16.toUInt64_neg (a : UInt16) : (-a).toUInt64 = -a.toUInt64 % 65536 := by + simp [UInt16.toUInt64_eq_mod_65536_iff] +@[simp] theorem UInt16.toUSize_neg (a : UInt16) : (-a).toUSize = -a.toUSize % 65536 := by + simp [UInt16.toUSize_eq_mod_65536_iff] + +@[simp] theorem UInt32.toUInt64_neg (a : UInt32) : (-a).toUInt64 = -a.toUInt64 % 4294967296 := by + simp [UInt32.toUInt64_eq_mod_4294967296_iff] +@[simp] theorem UInt32.toUSize_neg (a : UInt32) : (-a).toUSize = -a.toUSize % 4294967296 := by + simp [UInt32.toUSize_eq_mod_4294967296_iff] + +@[simp] theorem USize.toUInt64_neg (a : USize) : (-a).toUInt64 = -a.toUInt64 % UInt64.ofNat USize.size := by + simp [USize.toUInt64_eq_mod_usizeSize_iff] + +@[simp] theorem UInt8.toNat_neg (a : UInt8) : (-a).toNat = (UInt8.size - a.toNat) % UInt8.size := rfl +@[simp] theorem UInt16.toNat_neg (a : UInt16) : (-a).toNat = (UInt16.size - a.toNat) % UInt16.size := rfl +@[simp] theorem UInt32.toNat_neg (a : UInt32) : (-a).toNat = (UInt32.size - a.toNat) % UInt32.size := rfl +@[simp] theorem UInt64.toNat_neg (a : UInt64) : (-a).toNat = (UInt64.size - a.toNat) % UInt64.size := rfl +@[simp] theorem USize.toNat_neg (a : USize) : (-a).toNat = (USize.size - a.toNat) % USize.size := rfl + +theorem UInt8.sub_eq_add_neg (a b : UInt8) : a - b = a + (-b) := UInt8.toBitVec_inj.1 (BitVec.sub_toAdd _ _) +theorem UInt16.sub_eq_add_neg (a b : UInt16) : a - b = a + (-b) := UInt16.toBitVec_inj.1 (BitVec.sub_toAdd _ _) +theorem UInt32.sub_eq_add_neg (a b : UInt32) : a - b = a + (-b) := UInt32.toBitVec_inj.1 (BitVec.sub_toAdd _ _) +theorem UInt64.sub_eq_add_neg (a b : UInt64) : a - b = a + (-b) := UInt64.toBitVec_inj.1 (BitVec.sub_toAdd _ _) +theorem USize.sub_eq_add_neg (a b : USize) : a - b = a + (-b) := USize.toBitVec_inj.1 (BitVec.sub_toAdd _ _) + +theorem UInt8.neg_one_eq : (-1 : UInt8) = 255 := rfl +theorem UInt16.neg_one_eq : (-1 : UInt16) = 65535 := rfl +theorem UInt32.neg_one_eq : (-1 : UInt32) = 4294967295 := rfl +theorem UInt64.neg_one_eq : (-1 : UInt64) = 18446744073709551615 := rfl +theorem USize.neg_one_eq : (-1 : USize) = USize.ofNatLT (USize.size - 1) (Nat.sub_one_lt (Nat.pos_iff_ne_zero.1 size_pos)) := + USize.toNat.inj (by simp) + +theorem UInt8.toBitVec_zero : toBitVec 0 = 0#8 := rfl +theorem UInt16.toBitVec_zero : toBitVec 0 = 0#16 := rfl +theorem UInt32.toBitVec_zero : toBitVec 0 = 0#32 := rfl +theorem UInt64.toBitVec_zero : toBitVec 0 = 0#64 := rfl +theorem USize.toBitVec_zero : toBitVec 0 = 0#System.Platform.numBits := rfl + +theorem UInt8.toBitVec_one : toBitVec 1 = 1#8 := rfl +theorem UInt16.toBitVec_one : toBitVec 1 = 1#16 := rfl +theorem UInt32.toBitVec_one : toBitVec 1 = 1#32 := rfl +theorem UInt64.toBitVec_one : toBitVec 1 = 1#64 := rfl +theorem USize.toBitVec_one : toBitVec 1 = 1#System.Platform.numBits := rfl + +theorem UInt8.neg_eq_neg_one_mul (a : UInt8) : -a = -1 * a := by + apply UInt8.toBitVec_inj.1 + rw [UInt8.toBitVec_neg, UInt8.toBitVec_mul, UInt8.toBitVec_neg, UInt8.toBitVec_one, BitVec.neg_eq_neg_one_mul] +theorem UInt16.neg_eq_neg_one_mul (a : UInt16) : -a = -1 * a := by + apply UInt16.toBitVec_inj.1 + rw [UInt16.toBitVec_neg, UInt16.toBitVec_mul, UInt16.toBitVec_neg, UInt16.toBitVec_one, BitVec.neg_eq_neg_one_mul] +theorem UInt32.neg_eq_neg_one_mul (a : UInt32) : -a = -1 * a := by + apply UInt32.toBitVec_inj.1 + rw [UInt32.toBitVec_neg, UInt32.toBitVec_mul, UInt32.toBitVec_neg, UInt32.toBitVec_one, BitVec.neg_eq_neg_one_mul] +theorem UInt64.neg_eq_neg_one_mul (a : UInt64) : -a = -1 * a := by + apply UInt64.toBitVec_inj.1 + rw [UInt64.toBitVec_neg, UInt64.toBitVec_mul, UInt64.toBitVec_neg, UInt64.toBitVec_one, BitVec.neg_eq_neg_one_mul] +theorem USize.neg_eq_neg_one_mul (a : USize) : -a = -1 * a := by + apply USize.toBitVec_inj.1 + rw [USize.toBitVec_neg, USize.toBitVec_mul, USize.toBitVec_neg, USize.toBitVec_one, BitVec.neg_eq_neg_one_mul] + +theorem UInt8.sub_eq_add_mul (a b : UInt8) : a - b = a + 255 * b := by + rw [sub_eq_add_neg, neg_eq_neg_one_mul, neg_one_eq] +theorem UInt16.sub_eq_add_mul (a b : UInt16) : a - b = a + 65535 * b := by + rw [sub_eq_add_neg, neg_eq_neg_one_mul, neg_one_eq] +theorem UInt32.sub_eq_add_mul (a b : UInt32) : a - b = a + 4294967295 * b := by + rw [sub_eq_add_neg, neg_eq_neg_one_mul, neg_one_eq] +theorem UInt64.sub_eq_add_mul (a b : UInt64) : a - b = a + 18446744073709551615 * b := by + rw [sub_eq_add_neg, neg_eq_neg_one_mul, neg_one_eq] +theorem USize.sub_eq_add_mul (a b : USize) : a - b = a + USize.ofNatLT (USize.size - 1) (Nat.sub_one_lt (Nat.pos_iff_ne_zero.1 size_pos)) * b := by + rw [sub_eq_add_neg, neg_eq_neg_one_mul, neg_one_eq] + +@[simp] theorem UInt8.ofNat_usizeSize_sub_one : UInt8.ofNat (USize.size - 1) = 255 := UInt8.toNat.inj (by simp) +@[simp] theorem UInt16.ofNat_usizeSize_sub_one : UInt16.ofNat (USize.size - 1) = 65535 := UInt16.toNat.inj (by simp) +@[simp] theorem UInt32.ofNat_usizeSize_sub_one : UInt32.ofNat (USize.size - 1) = 4294967295 := UInt32.toNat.inj (by simp) +@[simp] theorem USize.ofNat_uInt64Size_sub_one : USize.ofNat (UInt64.size - 1) = USize.ofNatLT (USize.size - 1) (Nat.sub_one_lt (Nat.pos_iff_ne_zero.1 size_pos)) := + USize.toNat.inj (by simp [USize.toNat_ofNat]) + +@[simp] theorem UInt16.toUInt8_sub (a b : UInt16) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8 := by + simp [sub_eq_add_neg, UInt8.sub_eq_add_neg] + +@[simp] theorem UInt32.toUInt8_sub (a b : UInt32) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8 := by + simp [sub_eq_add_neg, UInt8.sub_eq_add_neg] +@[simp] theorem UInt32.toUInt16_sub (a b : UInt32) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16 := by + simp [sub_eq_add_neg, UInt16.sub_eq_add_neg] + +@[simp] theorem UInt64.toUInt8_sub (a b : UInt64) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8 := by + simp [sub_eq_add_neg, UInt8.sub_eq_add_neg] +@[simp] theorem UInt64.toUInt16_sub (a b : UInt64) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16 := by + simp [sub_eq_add_neg, UInt16.sub_eq_add_neg] +@[simp] theorem UInt64.toUInt32_sub (a b : UInt64) : (a - b).toUInt32 = a.toUInt32 - b.toUInt32 := by + simp [sub_eq_add_neg, UInt32.sub_eq_add_neg] +@[simp] theorem UInt64.toUSize_sub (a b : UInt64) : (a - b).toUSize = a.toUSize - b.toUSize := by + simp [sub_eq_add_neg, USize.sub_eq_add_neg] + +@[simp] theorem USize.toUInt8_sub (a b : USize) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8 := by + simp [sub_eq_add_neg, UInt8.sub_eq_add_neg] +@[simp] theorem USize.toUInt16_sub (a b : USize) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16 := by + simp [sub_eq_add_neg, UInt16.sub_eq_add_neg] +@[simp] theorem USize.toUInt32_sub (a b : USize) : (a - b).toUInt32 = a.toUInt32 - b.toUInt32 := by + simp [sub_eq_add_neg, UInt32.sub_eq_add_neg] + +@[simp] theorem UInt8.toUInt16_sub (a b : UInt8) : (a - b).toUInt16 = (a.toUInt16 - b.toUInt16) % 256 := by + simp [UInt8.toUInt16_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt32_sub (a b : UInt8) : (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 256 := by + simp [UInt8.toUInt32_eq_mod_256_iff] +@[simp] theorem UInt8.toUInt64_sub (a b : UInt8) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 256 := by + simp [UInt8.toUInt64_eq_mod_256_iff] +@[simp] theorem UInt8.toUSize_sub (a b : UInt8) : (a - b).toUSize = (a.toUSize - b.toUSize) % 256 := by + simp [UInt8.toUSize_eq_mod_256_iff] + +@[simp] theorem UInt16.toUInt32_sub (a b : UInt16) : (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 65536 := by + simp [UInt16.toUInt32_eq_mod_65536_iff] +@[simp] theorem UInt16.toUInt64_sub (a b : UInt16) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 65536 := by + simp [UInt16.toUInt64_eq_mod_65536_iff] +@[simp] theorem UInt16.toUSize_sub (a b : UInt16) : (a - b).toUSize = (a.toUSize - b.toUSize) % 65536 := by + simp [UInt16.toUSize_eq_mod_65536_iff] + +@[simp] theorem UInt32.toUInt64_sub (a b : UInt32) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 4294967296 := by + simp [UInt32.toUInt64_eq_mod_4294967296_iff] +@[simp] theorem UInt32.toUSize_sub (a b : UInt32) : (a - b).toUSize = (a.toUSize - b.toUSize) % 4294967296 := by + simp [UInt32.toUSize_eq_mod_4294967296_iff] + +@[simp] theorem USize.toUInt64_sub (a b : USize) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % UInt64.ofNat USize.size := by + simp [USize.toUInt64_eq_mod_usizeSize_iff]