chore: cleanup of finite integer lemmas (#7706)

This PR performs various cleanup tasks on `Init/Data/UInt/*` and
`Init/Data/SInt/*`.
This commit is contained in:
Markus Himmel 2025-03-28 13:13:07 +01:00 committed by GitHub
parent c33c2c5fbd
commit 4e51487b1c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 1088 additions and 1077 deletions

View file

@ -204,7 +204,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_add"]
def Int8.add (a b : Int8) : Int8 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
protected def Int8.add (a b : Int8) : Int8 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
/--
Subtracts one 8-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.
@ -212,7 +212,7 @@ accessed via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_sub"]
def Int8.sub (a b : Int8) : Int8 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
protected def Int8.sub (a b : Int8) : Int8 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
/--
Multiplies two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the `*` operator.
@ -220,7 +220,7 @@ the `*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_mul"]
def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
protected def Int8.mul (a b : Int8) : Int8 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
/--
Truncating division for 8-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.
@ -237,7 +237,7 @@ Examples:
* `Int8.div 10 0 = 0`
-/
@[extern "lean_int8_div"]
def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
protected def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
/--
The modulo operator for 8-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int8.div`. Usually accessed via the `%`
@ -258,7 +258,7 @@ Examples:
* `Int8.mod (-4) 0 = (-4)`
-/
@[extern "lean_int8_mod"]
def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
protected def Int8.mod (a b : Int8) : Int8 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
/--
Bitwise and for 8-bit signed integers. Usually accessed via the `&&&` operator.
@ -268,7 +268,7 @@ according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_land"]
def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
protected def Int8.land (a b : Int8) : Int8 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
/--
Bitwise or for 8-bit signed integers. Usually accessed via the `|||` operator.
@ -278,7 +278,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_lor"]
def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
protected def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
/--
Bitwise exclusive or for 8-bit signed integers. Usually accessed via the `^^^` operator.
@ -288,7 +288,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_xor"]
def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
protected def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
/--
Bitwise left shift for 8-bit signed integers. Usually accessed via the `<<<` operator.
@ -297,7 +297,7 @@ Signed integers are interpreted as bitvectors according to the two's complement
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_shift_left"]
def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 8)⟩⟩
protected def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 8)⟩⟩
/--
Arithmetic right shift for 8-bit signed integers. Usually accessed via the `<<<` operator.
@ -306,7 +306,7 @@ The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_shift_right"]
def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 8)⟩⟩
protected def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 8)⟩⟩
/--
Bitwise complement, also known as bitwise negation, for 8-bit signed integers. Usually accessed via
the `~~~` prefix operator.
@ -317,7 +317,7 @@ Integers use the two's complement representation, so `Int8.complement a = -(a +
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_complement"]
def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
protected def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
/--
Computes the absolute value of an 8-bit signed integer.
@ -327,7 +327,7 @@ mapped to `Int8.minValue`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int8_abs"]
def Int8.abs (a : Int8) : Int8 := ⟨⟨a.toBitVec.abs⟩⟩
protected def Int8.abs (a : Int8) : Int8 := ⟨⟨a.toBitVec.abs⟩⟩
/--
Decides whether two 8-bit signed integers are equal. Usually accessed via the `DecidableEq Int8`
@ -353,12 +353,12 @@ def Int8.decEq (a b : Int8) : Decidable (a = b) :=
Strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
-/
def Int8.lt (a b : Int8) : Prop := a.toBitVec.slt b.toBitVec
protected def Int8.lt (a b : Int8) : Prop := a.toBitVec.slt b.toBitVec
/--
Non-strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
-/
def Int8.le (a b : Int8) : Prop := a.toBitVec.sle b.toBitVec
protected def Int8.le (a b : Int8) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int8 where
default := 0
@ -563,7 +563,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_add"]
def Int16.add (a b : Int16) : Int16 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
protected def Int16.add (a b : Int16) : Int16 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
/--
Subtracts one 16-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.
@ -571,7 +571,7 @@ accessed via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_sub"]
def Int16.sub (a b : Int16) : Int16 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
protected def Int16.sub (a b : Int16) : Int16 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
/--
Multiplies two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the `*` operator.
@ -579,7 +579,7 @@ the `*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_mul"]
def Int16.mul (a b : Int16) : Int16 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
protected def Int16.mul (a b : Int16) : Int16 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
/--
Truncating division for 16-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.
@ -596,7 +596,7 @@ Examples:
* `Int16.div 10 0 = 0`
-/
@[extern "lean_int16_div"]
def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
protected def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
/--
The modulo operator for 16-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int16.div`. Usually accessed via the `%`
@ -617,7 +617,7 @@ Examples:
* `Int16.mod (-4) 0 = (-4)`
-/
@[extern "lean_int16_mod"]
def Int16.mod (a b : Int16) : Int16 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
protected def Int16.mod (a b : Int16) : Int16 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
/--
Bitwise and for 16-bit signed integers. Usually accessed via the `&&&` operator.
@ -627,7 +627,7 @@ according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_land"]
def Int16.land (a b : Int16) : Int16 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
protected def Int16.land (a b : Int16) : Int16 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
/--
Bitwise or for 16-bit signed integers. Usually accessed via the `|||` operator.
@ -637,7 +637,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_lor"]
def Int16.lor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
protected def Int16.lor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
/--
Bitwise exclusive or for 16-bit signed integers. Usually accessed via the `^^^` operator.
@ -647,7 +647,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_xor"]
def Int16.xor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
protected def Int16.xor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
/--
Bitwise left shift for 16-bit signed integers. Usually accessed via the `<<<` operator.
@ -656,7 +656,7 @@ Signed integers are interpreted as bitvectors according to the two's complement
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_shift_left"]
def Int16.shiftLeft (a b : Int16) : Int16 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 16)⟩⟩
protected def Int16.shiftLeft (a b : Int16) : Int16 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 16)⟩⟩
/--
Arithmetic right shift for 16-bit signed integers. Usually accessed via the `<<<` operator.
@ -665,7 +665,7 @@ The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_shift_right"]
def Int16.shiftRight (a b : Int16) : Int16 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 16)⟩⟩
protected def Int16.shiftRight (a b : Int16) : Int16 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 16)⟩⟩
/--
Bitwise complement, also known as bitwise negation, for 16-bit signed integers. Usually accessed via
the `~~~` prefix operator.
@ -676,7 +676,7 @@ Integers use the two's complement representation, so `Int16.complement a = -(a +
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_complement"]
def Int16.complement (a : Int16) : Int16 := ⟨⟨~~~a.toBitVec⟩⟩
protected def Int16.complement (a : Int16) : Int16 := ⟨⟨~~~a.toBitVec⟩⟩
/--
Computes the absolute value of a 16-bit signed integer.
@ -686,7 +686,7 @@ mapped to `Int16.minValue`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int16_abs"]
def Int16.abs (a : Int16) : Int16 := ⟨⟨a.toBitVec.abs⟩⟩
protected def Int16.abs (a : Int16) : Int16 := ⟨⟨a.toBitVec.abs⟩⟩
/--
Decides whether two 16-bit signed integers are equal. Usually accessed via the `DecidableEq Int16`
@ -712,12 +712,12 @@ def Int16.decEq (a b : Int16) : Decidable (a = b) :=
Strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
-/
def Int16.lt (a b : Int16) : Prop := a.toBitVec.slt b.toBitVec
protected def Int16.lt (a b : Int16) : Prop := a.toBitVec.slt b.toBitVec
/--
Non-strict inequality of 16-bit signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `≤` operator.
-/
def Int16.le (a b : Int16) : Prop := a.toBitVec.sle b.toBitVec
protected def Int16.le (a b : Int16) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int16 where
default := 0
@ -938,7 +938,7 @@ Adds two 32-bit signed integers, wrapping around on over- or underflow. Usually
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_add"]
def Int32.add (a b : Int32) : Int32 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
protected def Int32.add (a b : Int32) : Int32 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
/--
Subtracts one 32-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.
@ -946,7 +946,7 @@ accessed via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_sub"]
def Int32.sub (a b : Int32) : Int32 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
protected def Int32.sub (a b : Int32) : Int32 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
/--
Multiplies two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the `*` operator.
@ -954,7 +954,7 @@ the `*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_mul"]
def Int32.mul (a b : Int32) : Int32 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
protected def Int32.mul (a b : Int32) : Int32 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
/--
Truncating division for 32-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.
@ -971,7 +971,7 @@ Examples:
* `Int32.div 10 0 = 0`
-/
@[extern "lean_int32_div"]
def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
protected def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
/--
The modulo operator for 32-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int32.div`. Usually accessed via the `%`
@ -992,7 +992,7 @@ Examples:
* `Int32.mod (-4) 0 = (-4)`
-/
@[extern "lean_int32_mod"]
def Int32.mod (a b : Int32) : Int32 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
protected def Int32.mod (a b : Int32) : Int32 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
/--
Bitwise and for 32-bit signed integers. Usually accessed via the `&&&` operator.
@ -1002,7 +1002,7 @@ according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_land"]
def Int32.land (a b : Int32) : Int32 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
protected def Int32.land (a b : Int32) : Int32 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
/--
Bitwise or for 32-bit signed integers. Usually accessed via the `|||` operator.
@ -1012,7 +1012,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_lor"]
def Int32.lor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
protected def Int32.lor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
/--
Bitwise exclusive or for 32-bit signed integers. Usually accessed via the `^^^` operator.
@ -1022,7 +1022,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_xor"]
def Int32.xor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
protected def Int32.xor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
/--
Bitwise left shift for 32-bit signed integers. Usually accessed via the `<<<` operator.
@ -1031,7 +1031,7 @@ Signed integers are interpreted as bitvectors according to the two's complement
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_shift_left"]
def Int32.shiftLeft (a b : Int32) : Int32 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 32)⟩⟩
protected def Int32.shiftLeft (a b : Int32) : Int32 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 32)⟩⟩
/--
Arithmetic right shift for 32-bit signed integers. Usually accessed via the `<<<` operator.
@ -1040,7 +1040,7 @@ The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_shift_right"]
def Int32.shiftRight (a b : Int32) : Int32 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 32)⟩⟩
protected def Int32.shiftRight (a b : Int32) : Int32 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 32)⟩⟩
/--
Bitwise complement, also known as bitwise negation, for 32-bit signed integers. Usually accessed via
the `~~~` prefix operator.
@ -1051,7 +1051,7 @@ Integers use the two's complement representation, so `Int32.complement a = -(a +
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_complement"]
def Int32.complement (a : Int32) : Int32 := ⟨⟨~~~a.toBitVec⟩⟩
protected def Int32.complement (a : Int32) : Int32 := ⟨⟨~~~a.toBitVec⟩⟩
/--
Computes the absolute value of a 32-bit signed integer.
@ -1061,7 +1061,7 @@ mapped to `Int32.minValue`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int32_abs"]
def Int32.abs (a : Int32) : Int32 := ⟨⟨a.toBitVec.abs⟩⟩
protected def Int32.abs (a : Int32) : Int32 := ⟨⟨a.toBitVec.abs⟩⟩
/--
Decides whether two 32-bit signed integers are equal. Usually accessed via the `DecidableEq Int32`
@ -1087,12 +1087,12 @@ def Int32.decEq (a b : Int32) : Decidable (a = b) :=
Strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
-/
def Int32.lt (a b : Int32) : Prop := a.toBitVec.slt b.toBitVec
protected def Int32.lt (a b : Int32) : Prop := a.toBitVec.slt b.toBitVec
/--
Non-strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
-/
def Int32.le (a b : Int32) : Prop := a.toBitVec.sle b.toBitVec
protected def Int32.le (a b : Int32) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int32 where
default := 0
@ -1333,7 +1333,7 @@ Adds two 64-bit signed integers, wrapping around on over- or underflow. Usually
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_add"]
def Int64.add (a b : Int64) : Int64 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
protected def Int64.add (a b : Int64) : Int64 := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
/--
Subtracts one 64-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.
@ -1341,7 +1341,7 @@ accessed via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_sub"]
def Int64.sub (a b : Int64) : Int64 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
protected def Int64.sub (a b : Int64) : Int64 := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
/--
Multiplies two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the `*` operator.
@ -1349,7 +1349,7 @@ the `*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_mul"]
def Int64.mul (a b : Int64) : Int64 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
protected def Int64.mul (a b : Int64) : Int64 := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
/--
Truncating division for 64-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.
@ -1366,7 +1366,7 @@ Examples:
* `Int64.div 10 0 = 0`
-/
@[extern "lean_int64_div"]
def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
protected def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
/--
The modulo operator for 64-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int64.div`. Usually accessed via the `%`
@ -1387,7 +1387,7 @@ Examples:
* `Int64.mod (-4) 0 = (-4)`
-/
@[extern "lean_int64_mod"]
def Int64.mod (a b : Int64) : Int64 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
protected def Int64.mod (a b : Int64) : Int64 := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
/--
Bitwise and for 64-bit signed integers. Usually accessed via the `&&&` operator.
@ -1397,7 +1397,7 @@ according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_land"]
def Int64.land (a b : Int64) : Int64 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
protected def Int64.land (a b : Int64) : Int64 := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
/--
Bitwise or for 64-bit signed integers. Usually accessed via the `|||` operator.
@ -1407,7 +1407,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_lor"]
def Int64.lor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
protected def Int64.lor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
/--
Bitwise exclusive or for 64-bit signed integers. Usually accessed via the `^^^` operator.
@ -1417,7 +1417,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_xor"]
def Int64.xor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
protected def Int64.xor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
/--
Bitwise left shift for 64-bit signed integers. Usually accessed via the `<<<` operator.
@ -1426,7 +1426,7 @@ Signed integers are interpreted as bitvectors according to the two's complement
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_shift_left"]
def Int64.shiftLeft (a b : Int64) : Int64 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 64)⟩⟩
protected def Int64.shiftLeft (a b : Int64) : Int64 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 64)⟩⟩
/--
Arithmetic right shift for 64-bit signed integers. Usually accessed via the `<<<` operator.
@ -1435,7 +1435,7 @@ The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_shift_right"]
def Int64.shiftRight (a b : Int64) : Int64 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 64)⟩⟩
protected def Int64.shiftRight (a b : Int64) : Int64 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 64)⟩⟩
/--
Bitwise complement, also known as bitwise negation, for 64-bit signed integers. Usually accessed via
the `~~~` prefix operator.
@ -1446,7 +1446,7 @@ Integers use the two's complement representation, so `Int64.complement a = -(a +
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_complement"]
def Int64.complement (a : Int64) : Int64 := ⟨⟨~~~a.toBitVec⟩⟩
protected def Int64.complement (a : Int64) : Int64 := ⟨⟨~~~a.toBitVec⟩⟩
/--
Computes the absolute value of a 64-bit signed integer.
@ -1456,7 +1456,7 @@ mapped to `Int64.minValue`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_int64_abs"]
def Int64.abs (a : Int64) : Int64 := ⟨⟨a.toBitVec.abs⟩⟩
protected def Int64.abs (a : Int64) : Int64 := ⟨⟨a.toBitVec.abs⟩⟩
/--
Decides whether two 64-bit signed integers are equal. Usually accessed via the `DecidableEq Int64`
@ -1482,12 +1482,12 @@ def Int64.decEq (a b : Int64) : Decidable (a = b) :=
Strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `<` operator.
-/
def Int64.lt (a b : Int64) : Prop := a.toBitVec.slt b.toBitVec
protected def Int64.lt (a b : Int64) : Prop := a.toBitVec.slt b.toBitVec
/--
Non-strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
-/
def Int64.le (a b : Int64) : Prop := a.toBitVec.sle b.toBitVec
protected def Int64.le (a b : Int64) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited Int64 where
default := 0
@ -1670,7 +1670,7 @@ Negates word-sized signed integers. Usually accessed via the `-` prefix operator
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_neg"]
def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
protected def ISize.neg (i : ISize) : ISize := ⟨⟨-i.toBitVec⟩⟩
instance : ToString ISize where
toString i := toString i.toInt
@ -1711,7 +1711,7 @@ the `+` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_add"]
def ISize.add (a b : ISize) : ISize := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
protected def ISize.add (a b : ISize) : ISize := ⟨⟨a.toBitVec + b.toBitVec⟩⟩
/--
Subtracts one word-sized signed integer from another, wrapping around on over- or underflow. Usually
accessed via the `-` operator.
@ -1719,7 +1719,7 @@ accessed via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_sub"]
def ISize.sub (a b : ISize) : ISize := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
protected def ISize.sub (a b : ISize) : ISize := ⟨⟨a.toBitVec - b.toBitVec⟩⟩
/--
Multiplies two word-sized signed integers, wrapping around on over- or underflow. Usually accessed
via the `*` operator.
@ -1727,7 +1727,7 @@ via the `*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_mul"]
def ISize.mul (a b : ISize) : ISize := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
protected def ISize.mul (a b : ISize) : ISize := ⟨⟨a.toBitVec * b.toBitVec⟩⟩
/--
Truncating division for word-sized signed integers, rounding towards zero. Usually accessed via the
`/` operator.
@ -1744,7 +1744,7 @@ Examples:
* `ISize.div 10 0 = 0`
-/
@[extern "lean_isize_div"]
def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
protected def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
/--
The modulo operator for word-sized signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `ISize.div`. Usually accessed via the `%`
@ -1765,7 +1765,7 @@ Examples:
* `ISize.mod (-4) 0 = (-4)`
-/
@[extern "lean_isize_mod"]
def ISize.mod (a b : ISize) : ISize := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
protected def ISize.mod (a b : ISize) : ISize := ⟨⟨BitVec.srem a.toBitVec b.toBitVec⟩⟩
/--
Bitwise and for word-sized signed integers. Usually accessed via the `&&&` operator.
@ -1775,7 +1775,7 @@ according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_land"]
def ISize.land (a b : ISize) : ISize := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
protected def ISize.land (a b : ISize) : ISize := ⟨⟨a.toBitVec &&& b.toBitVec⟩⟩
/--
Bitwise or for word-sized signed integers. Usually accessed via the `|||` operator.
@ -1785,7 +1785,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_lor"]
def ISize.lor (a b : ISize) : ISize := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
protected def ISize.lor (a b : ISize) : ISize := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
/--
Bitwise exclusive or for word-sized signed integers. Usually accessed via the `^^^` operator.
@ -1795,7 +1795,7 @@ integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_xor"]
def ISize.xor (a b : ISize) : ISize := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
protected def ISize.xor (a b : ISize) : ISize := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
/--
Bitwise left shift for word-sized signed integers. Usually accessed via the `<<<` operator.
@ -1804,7 +1804,7 @@ Signed integers are interpreted as bitvectors according to the two's complement
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_shift_left"]
def ISize.shiftLeft (a b : ISize) : ISize := ⟨⟨a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)⟩⟩
protected def ISize.shiftLeft (a b : ISize) : ISize := ⟨⟨a.toBitVec <<< (b.toBitVec.smod System.Platform.numBits)⟩⟩
/--
Arithmetic right shift for word-sized signed integers. Usually accessed via the `<<<` operator.
@ -1814,7 +1814,7 @@ the most significant bit.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_shift_right"]
def ISize.shiftRight (a b : ISize) : ISize := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)⟩⟩
protected def ISize.shiftRight (a b : ISize) : ISize := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod System.Platform.numBits)⟩⟩
/--
Bitwise complement, also known as bitwise negation, for word-sized signed integers. Usually accessed
via the `~~~` prefix operator.
@ -1825,7 +1825,7 @@ Integers use the two's complement representation, so `ISize.complement a = -(a +
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_complement"]
def ISize.complement (a : ISize) : ISize := ⟨⟨~~~a.toBitVec⟩⟩
protected def ISize.complement (a : ISize) : ISize := ⟨⟨~~~a.toBitVec⟩⟩
/--
Computes the absolute value of a word-sized signed integer.
@ -1836,7 +1836,7 @@ mapped to `ISize.minValue`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_isize_abs"]
def ISize.abs (a : ISize) : ISize := ⟨⟨a.toBitVec.abs⟩⟩
protected def ISize.abs (a : ISize) : ISize := ⟨⟨a.toBitVec.abs⟩⟩
/--
Decides whether two word-sized signed integers are equal. Usually accessed via the
@ -1862,12 +1862,12 @@ def ISize.decEq (a b : ISize) : Decidable (a = b) :=
Strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `<` operator.
-/
def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
protected def ISize.lt (a b : ISize) : Prop := a.toBitVec.slt b.toBitVec
/--
Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the `≤` operator.
-/
def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
protected def ISize.le (a b : ISize) : Prop := a.toBitVec.sle b.toBitVec
instance : Inhabited ISize where
default := 0

View file

@ -252,11 +252,11 @@ theorem Int32.not_eq_neg_sub (a : Int32) : ~~~a = -a - 1 := Int32.toBitVec_inj.1
theorem Int64.not_eq_neg_sub (a : Int64) : ~~~a = -a - 1 := Int64.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
theorem ISize.not_eq_neg_sub (a : ISize) : ~~~a = -a - 1 := ISize.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
theorem Int8.or_assoc (a b c : Int8) : a ||| b ||| c = a ||| (b ||| c) := Int8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem Int16.or_assoc (a b c : Int16) : a ||| b ||| c = a ||| (b ||| c) := Int16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem Int32.or_assoc (a b c : Int32) : a ||| b ||| c = a ||| (b ||| c) := Int32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem Int64.or_assoc (a b c : Int64) : a ||| b ||| c = a ||| (b ||| c) := Int64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem ISize.or_assoc (a b c : ISize) : a ||| b ||| c = a ||| (b ||| c) := ISize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem Int8.or_assoc (a b c : Int8) : a ||| b ||| c = a ||| (b ||| c) := Int8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem Int16.or_assoc (a b c : Int16) : a ||| b ||| c = a ||| (b ||| c) := Int16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem Int32.or_assoc (a b c : Int32) : a ||| b ||| c = a ||| (b ||| c) := Int32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem Int64.or_assoc (a b c : Int64) : a ||| b ||| c = a ||| (b ||| c) := Int64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem ISize.or_assoc (a b c : ISize) : a ||| b ||| c = a ||| (b ||| c) := ISize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
instance : Std.Associative (α := Int8) (· ||| ·) := ⟨Int8.or_assoc⟩
instance : Std.Associative (α := Int16) (· ||| ·) := ⟨Int16.or_assoc⟩
@ -264,11 +264,11 @@ instance : Std.Associative (α := Int32) (· ||| ·) := ⟨Int32.or_assoc⟩
instance : Std.Associative (α := Int64) (· ||| ·) := ⟨Int64.or_assoc⟩
instance : Std.Associative (α := ISize) (· ||| ·) := ⟨ISize.or_assoc⟩
theorem Int8.or_comm (a b : Int8) : a ||| b = b ||| a := Int8.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem Int16.or_comm (a b : Int16) : a ||| b = b ||| a := Int16.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem Int32.or_comm (a b : Int32) : a ||| b = b ||| a := Int32.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem Int64.or_comm (a b : Int64) : a ||| b = b ||| a := Int64.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem ISize.or_comm (a b : ISize) : a ||| b = b ||| a := ISize.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem Int8.or_comm (a b : Int8) : a ||| b = b ||| a := Int8.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem Int16.or_comm (a b : Int16) : a ||| b = b ||| a := Int16.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem Int32.or_comm (a b : Int32) : a ||| b = b ||| a := Int32.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem Int64.or_comm (a b : Int64) : a ||| b = b ||| a := Int64.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem ISize.or_comm (a b : ISize) : a ||| b = b ||| a := ISize.toBitVec_inj.1 (BitVec.or_comm _ _)
instance : Std.Commutative (α := Int8) (· ||| ·) := ⟨Int8.or_comm⟩
instance : Std.Commutative (α := Int16) (· ||| ·) := ⟨Int16.or_comm⟩
@ -276,11 +276,11 @@ instance : Std.Commutative (α := Int32) (· ||| ·) := ⟨Int32.or_comm⟩
instance : Std.Commutative (α := Int64) (· ||| ·) := ⟨Int64.or_comm⟩
instance : Std.Commutative (α := ISize) (· ||| ·) := ⟨ISize.or_comm⟩
@[simp] theorem Int8.or_self {a : Int8} : a ||| a = a := Int8.toBitVec_inj.1 BitVec.or_self
@[simp] theorem Int16.or_self {a : Int16} : a ||| a = a := Int16.toBitVec_inj.1 BitVec.or_self
@[simp] theorem Int32.or_self {a : Int32} : a ||| a = a := Int32.toBitVec_inj.1 BitVec.or_self
@[simp] theorem Int64.or_self {a : Int64} : a ||| a = a := Int64.toBitVec_inj.1 BitVec.or_self
@[simp] theorem ISize.or_self {a : ISize} : a ||| a = a := ISize.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem Int8.or_self {a : Int8} : a ||| a = a := Int8.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem Int16.or_self {a : Int16} : a ||| a = a := Int16.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem Int32.or_self {a : Int32} : a ||| a = a := Int32.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem Int64.or_self {a : Int64} : a ||| a = a := Int64.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem ISize.or_self {a : ISize} : a ||| a = a := ISize.toBitVec_inj.1 BitVec.or_self
instance : Std.IdempotentOp (α := Int8) (· ||| ·) := ⟨fun _ => Int8.or_self⟩
instance : Std.IdempotentOp (α := Int16) (· ||| ·) := ⟨fun _ => Int16.or_self⟩
@ -288,17 +288,17 @@ instance : Std.IdempotentOp (α := Int32) (· ||| ·) := ⟨fun _ => Int32.or_se
instance : Std.IdempotentOp (α := Int64) (· ||| ·) := ⟨fun _ => Int64.or_self⟩
instance : Std.IdempotentOp (α := ISize) (· ||| ·) := ⟨fun _ => ISize.or_self⟩
@[simp] theorem Int8.or_zero {a : Int8} : a ||| 0 = a := Int8.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem Int16.or_zero {a : Int16} : a ||| 0 = a := Int16.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem Int32.or_zero {a : Int32} : a ||| 0 = a := Int32.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem Int64.or_zero {a : Int64} : a ||| 0 = a := Int64.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem ISize.or_zero {a : ISize} : a ||| 0 = a := ISize.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem Int8.or_zero {a : Int8} : a ||| 0 = a := Int8.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem Int16.or_zero {a : Int16} : a ||| 0 = a := Int16.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem Int32.or_zero {a : Int32} : a ||| 0 = a := Int32.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem Int64.or_zero {a : Int64} : a ||| 0 = a := Int64.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem ISize.or_zero {a : ISize} : a ||| 0 = a := ISize.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem Int8.zero_or {a : Int8} : 0 ||| a = a := Int8.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem Int16.zero_or {a : Int16} : 0 ||| a = a := Int16.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem Int32.zero_or {a : Int32} : 0 ||| a = a := Int32.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem Int64.zero_or {a : Int64} : 0 ||| a = a := Int64.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem ISize.zero_or {a : ISize} : 0 ||| a = a := ISize.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem Int8.zero_or {a : Int8} : 0 ||| a = a := Int8.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem Int16.zero_or {a : Int16} : 0 ||| a = a := Int16.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem Int32.zero_or {a : Int32} : 0 ||| a = a := Int32.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem Int64.zero_or {a : Int64} : 0 ||| a = a := Int64.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem ISize.zero_or {a : ISize} : 0 ||| a = a := ISize.toBitVec_inj.1 BitVec.zero_or
instance : Std.LawfulCommIdentity (α := Int8) (· ||| ·) 0 where
right_id _ := Int8.or_zero
@ -327,11 +327,11 @@ instance : Std.LawfulCommIdentity (α := ISize) (· ||| ·) 0 where
rw [← ISize.toBitVec_inj, ISize.toBitVec_or, ISize.toBitVec_neg, ISize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
@[simp] theorem Int8.or_neg_one {a : Int8} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem Int16.or_neg_one {a : Int16} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem Int32.or_neg_one {a : Int32} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem Int64.or_neg_one {a : Int64} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem ISize.or_neg_one {a : ISize} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem Int8.or_neg_one {a : Int8} : a ||| -1 = -1 := by rw [Int8.or_comm, neg_one_or]
@[simp] theorem Int16.or_neg_one {a : Int16} : a ||| -1 = -1 := by rw [Int16.or_comm, neg_one_or]
@[simp] theorem Int32.or_neg_one {a : Int32} : a ||| -1 = -1 := by rw [Int32.or_comm, neg_one_or]
@[simp] theorem Int64.or_neg_one {a : Int64} : a ||| -1 = -1 := by rw [Int64.or_comm, neg_one_or]
@[simp] theorem ISize.or_neg_one {a : ISize} : a ||| -1 = -1 := by rw [ISize.or_comm, neg_one_or]
@[simp] theorem Int8.or_eq_zero_iff {a b : Int8} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
simp [← Int8.toBitVec_inj]
@ -344,11 +344,11 @@ instance : Std.LawfulCommIdentity (α := ISize) (· ||| ·) 0 where
@[simp] theorem ISize.or_eq_zero_iff {a b : ISize} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
simp [← ISize.toBitVec_inj]
theorem Int8.and_assoc (a b c : Int8) : a &&& b &&& c = a &&& (b &&& c) := Int8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem Int16.and_assoc (a b c : Int16) : a &&& b &&& c = a &&& (b &&& c) := Int16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem Int32.and_assoc (a b c : Int32) : a &&& b &&& c = a &&& (b &&& c) := Int32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem Int64.and_assoc (a b c : Int64) : a &&& b &&& c = a &&& (b &&& c) := Int64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem ISize.and_assoc (a b c : ISize) : a &&& b &&& c = a &&& (b &&& c) := ISize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem Int8.and_assoc (a b c : Int8) : a &&& b &&& c = a &&& (b &&& c) := Int8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem Int16.and_assoc (a b c : Int16) : a &&& b &&& c = a &&& (b &&& c) := Int16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem Int32.and_assoc (a b c : Int32) : a &&& b &&& c = a &&& (b &&& c) := Int32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem Int64.and_assoc (a b c : Int64) : a &&& b &&& c = a &&& (b &&& c) := Int64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem ISize.and_assoc (a b c : ISize) : a &&& b &&& c = a &&& (b &&& c) := ISize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
instance : Std.Associative (α := Int8) (· &&& ·) := ⟨Int8.and_assoc⟩
instance : Std.Associative (α := Int16) (· &&& ·) := ⟨Int16.and_assoc⟩
@ -356,11 +356,11 @@ instance : Std.Associative (α := Int32) (· &&& ·) := ⟨Int32.and_assoc⟩
instance : Std.Associative (α := Int64) (· &&& ·) := ⟨Int64.and_assoc⟩
instance : Std.Associative (α := ISize) (· &&& ·) := ⟨ISize.and_assoc⟩
theorem Int8.and_comm (a b : Int8) : a &&& b = b &&& a := Int8.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem Int16.and_comm (a b : Int16) : a &&& b = b &&& a := Int16.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem Int32.and_comm (a b : Int32) : a &&& b = b &&& a := Int32.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem Int64.and_comm (a b : Int64) : a &&& b = b &&& a := Int64.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem ISize.and_comm (a b : ISize) : a &&& b = b &&& a := ISize.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem Int8.and_comm (a b : Int8) : a &&& b = b &&& a := Int8.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem Int16.and_comm (a b : Int16) : a &&& b = b &&& a := Int16.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem Int32.and_comm (a b : Int32) : a &&& b = b &&& a := Int32.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem Int64.and_comm (a b : Int64) : a &&& b = b &&& a := Int64.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem ISize.and_comm (a b : ISize) : a &&& b = b &&& a := ISize.toBitVec_inj.1 (BitVec.and_comm _ _)
instance : Std.Commutative (α := Int8) (· &&& ·) := ⟨Int8.and_comm⟩
instance : Std.Commutative (α := Int16) (· &&& ·) := ⟨Int16.and_comm⟩
@ -368,11 +368,11 @@ instance : Std.Commutative (α := Int32) (· &&& ·) := ⟨Int32.and_comm⟩
instance : Std.Commutative (α := Int64) (· &&& ·) := ⟨Int64.and_comm⟩
instance : Std.Commutative (α := ISize) (· &&& ·) := ⟨ISize.and_comm⟩
@[simp] theorem Int8.and_self {a : Int8} : a &&& a = a := Int8.toBitVec_inj.1 BitVec.and_self
@[simp] theorem Int16.and_self {a : Int16} : a &&& a = a := Int16.toBitVec_inj.1 BitVec.and_self
@[simp] theorem Int32.and_self {a : Int32} : a &&& a = a := Int32.toBitVec_inj.1 BitVec.and_self
@[simp] theorem Int64.and_self {a : Int64} : a &&& a = a := Int64.toBitVec_inj.1 BitVec.and_self
@[simp] theorem ISize.and_self {a : ISize} : a &&& a = a := ISize.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem Int8.and_self {a : Int8} : a &&& a = a := Int8.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem Int16.and_self {a : Int16} : a &&& a = a := Int16.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem Int32.and_self {a : Int32} : a &&& a = a := Int32.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem Int64.and_self {a : Int64} : a &&& a = a := Int64.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem ISize.and_self {a : ISize} : a &&& a = a := ISize.toBitVec_inj.1 BitVec.and_self
instance : Std.IdempotentOp (α := Int8) (· &&& ·) := ⟨fun _ => Int8.and_self⟩
instance : Std.IdempotentOp (α := Int16) (· &&& ·) := ⟨fun _ => Int16.and_self⟩
@ -380,17 +380,17 @@ instance : Std.IdempotentOp (α := Int32) (· &&& ·) := ⟨fun _ => Int32.and_s
instance : Std.IdempotentOp (α := Int64) (· &&& ·) := ⟨fun _ => Int64.and_self⟩
instance : Std.IdempotentOp (α := ISize) (· &&& ·) := ⟨fun _ => ISize.and_self⟩
@[simp] theorem Int8.and_zero {a : Int8} : a &&& 0 = 0 := Int8.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem Int16.and_zero {a : Int16} : a &&& 0 = 0 := Int16.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem Int32.and_zero {a : Int32} : a &&& 0 = 0 := Int32.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem Int64.and_zero {a : Int64} : a &&& 0 = 0 := Int64.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem ISize.and_zero {a : ISize} : a &&& 0 = 0 := ISize.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem Int8.and_zero {a : Int8} : a &&& 0 = 0 := Int8.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem Int16.and_zero {a : Int16} : a &&& 0 = 0 := Int16.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem Int32.and_zero {a : Int32} : a &&& 0 = 0 := Int32.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem Int64.and_zero {a : Int64} : a &&& 0 = 0 := Int64.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem ISize.and_zero {a : ISize} : a &&& 0 = 0 := ISize.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem Int8.zero_and {a : Int8} : 0 &&& a = 0 := Int8.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem Int16.zero_and {a : Int16} : 0 &&& a = 0 := Int16.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem Int32.zero_and {a : Int32} : 0 &&& a = 0 := Int32.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem Int64.zero_and {a : Int64} : 0 &&& a = 0 := Int64.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem ISize.zero_and {a : ISize} : 0 &&& a = 0 := ISize.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem Int8.zero_and {a : Int8} : 0 &&& a = 0 := Int8.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem Int16.zero_and {a : Int16} : 0 &&& a = 0 := Int16.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem Int32.zero_and {a : Int32} : 0 &&& a = 0 := Int32.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem Int64.zero_and {a : Int64} : 0 &&& a = 0 := Int64.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem ISize.zero_and {a : ISize} : 0 &&& a = 0 := ISize.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem Int8.neg_one_and {a : Int8} : -1 &&& a = a := by
rw [← Int8.toBitVec_inj, Int8.toBitVec_and, Int8.toBitVec_neg, Int8.toBitVec_one,
@ -408,11 +408,11 @@ instance : Std.IdempotentOp (α := ISize) (· &&& ·) := ⟨fun _ => ISize.and_s
rw [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
@[simp] theorem Int8.and_neg_one {a : Int8} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem Int16.and_neg_one {a : Int16} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem Int32.and_neg_one {a : Int32} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem Int64.and_neg_one {a : Int64} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem ISize.and_neg_one {a : ISize} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem Int8.and_neg_one {a : Int8} : a &&& -1 = a := by rw [Int8.and_comm, neg_one_and]
@[simp] theorem Int16.and_neg_one {a : Int16} : a &&& -1 = a := by rw [Int16.and_comm, neg_one_and]
@[simp] theorem Int32.and_neg_one {a : Int32} : a &&& -1 = a := by rw [Int32.and_comm, neg_one_and]
@[simp] theorem Int64.and_neg_one {a : Int64} : a &&& -1 = a := by rw [Int64.and_comm, neg_one_and]
@[simp] theorem ISize.and_neg_one {a : ISize} : a &&& -1 = a := by rw [ISize.and_comm, neg_one_and]
instance : Std.LawfulCommIdentity (α := Int8) (· &&& ·) (-1) where
right_id _ := Int8.and_neg_one
@ -441,11 +441,11 @@ instance : Std.LawfulCommIdentity (α := ISize) (· &&& ·) (-1) where
simp only [← ISize.toBitVec_inj, ISize.toBitVec_and, ISize.toBitVec_neg, ISize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
theorem Int8.xor_assoc (a b c : Int8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem Int16.xor_assoc (a b c : Int16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem Int32.xor_assoc (a b c : Int32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem Int64.xor_assoc (a b c : Int64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem ISize.xor_assoc (a b c : ISize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := ISize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem Int8.xor_assoc (a b c : Int8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem Int16.xor_assoc (a b c : Int16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem Int32.xor_assoc (a b c : Int32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem Int64.xor_assoc (a b c : Int64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := Int64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem ISize.xor_assoc (a b c : ISize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := ISize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
instance : Std.Associative (α := Int8) (· ^^^ ·) := ⟨Int8.xor_assoc⟩
instance : Std.Associative (α := Int16) (· ^^^ ·) := ⟨Int16.xor_assoc⟩
@ -453,11 +453,11 @@ instance : Std.Associative (α := Int32) (· ^^^ ·) := ⟨Int32.xor_assoc⟩
instance : Std.Associative (α := Int64) (· ^^^ ·) := ⟨Int64.xor_assoc⟩
instance : Std.Associative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_assoc⟩
theorem Int8.xor_comm (a b : Int8) : a ^^^ b = b ^^^ a := Int8.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem Int16.xor_comm (a b : Int16) : a ^^^ b = b ^^^ a := Int16.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem Int32.xor_comm (a b : Int32) : a ^^^ b = b ^^^ a := Int32.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem Int64.xor_comm (a b : Int64) : a ^^^ b = b ^^^ a := Int64.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem ISize.xor_comm (a b : ISize) : a ^^^ b = b ^^^ a := ISize.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem Int8.xor_comm (a b : Int8) : a ^^^ b = b ^^^ a := Int8.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem Int16.xor_comm (a b : Int16) : a ^^^ b = b ^^^ a := Int16.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem Int32.xor_comm (a b : Int32) : a ^^^ b = b ^^^ a := Int32.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem Int64.xor_comm (a b : Int64) : a ^^^ b = b ^^^ a := Int64.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem ISize.xor_comm (a b : ISize) : a ^^^ b = b ^^^ a := ISize.toBitVec_inj.1 (BitVec.xor_comm _ _)
instance : Std.Commutative (α := Int8) (· ^^^ ·) := ⟨Int8.xor_comm⟩
instance : Std.Commutative (α := Int16) (· ^^^ ·) := ⟨Int16.xor_comm⟩
@ -465,23 +465,23 @@ instance : Std.Commutative (α := Int32) (· ^^^ ·) := ⟨Int32.xor_comm⟩
instance : Std.Commutative (α := Int64) (· ^^^ ·) := ⟨Int64.xor_comm⟩
instance : Std.Commutative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_comm⟩
@[simp] theorem Int8.xor_self {a : Int8} : a ^^^ a = 0 := Int8.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem Int16.xor_self {a : Int16} : a ^^^ a = 0 := Int16.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem Int32.xor_self {a : Int32} : a ^^^ a = 0 := Int32.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem Int64.xor_self {a : Int64} : a ^^^ a = 0 := Int64.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem ISize.xor_self {a : ISize} : a ^^^ a = 0 := ISize.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem Int8.xor_self {a : Int8} : a ^^^ a = 0 := Int8.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem Int16.xor_self {a : Int16} : a ^^^ a = 0 := Int16.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem Int32.xor_self {a : Int32} : a ^^^ a = 0 := Int32.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem Int64.xor_self {a : Int64} : a ^^^ a = 0 := Int64.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem ISize.xor_self {a : ISize} : a ^^^ a = 0 := ISize.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem Int8.xor_zero {a : Int8} : a ^^^ 0 = a := Int8.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem Int16.xor_zero {a : Int16} : a ^^^ 0 = a := Int16.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem Int32.xor_zero {a : Int32} : a ^^^ 0 = a := Int32.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem Int64.xor_zero {a : Int64} : a ^^^ 0 = a := Int64.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem ISize.xor_zero {a : ISize} : a ^^^ 0 = a := ISize.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem Int8.xor_zero {a : Int8} : a ^^^ 0 = a := Int8.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem Int16.xor_zero {a : Int16} : a ^^^ 0 = a := Int16.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem Int32.xor_zero {a : Int32} : a ^^^ 0 = a := Int32.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem Int64.xor_zero {a : Int64} : a ^^^ 0 = a := Int64.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem ISize.xor_zero {a : ISize} : a ^^^ 0 = a := ISize.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem Int8.zero_xor {a : Int8} : 0 ^^^ a = a := Int8.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem Int16.zero_xor {a : Int16} : 0 ^^^ a = a := Int16.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem Int32.zero_xor {a : Int32} : 0 ^^^ a = a := Int32.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem Int64.zero_xor {a : Int64} : 0 ^^^ a = a := Int64.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem ISize.zero_xor {a : ISize} : 0 ^^^ a = a := ISize.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem Int8.zero_xor {a : Int8} : 0 ^^^ a = a := Int8.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem Int16.zero_xor {a : Int16} : 0 ^^^ a = a := Int16.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem Int32.zero_xor {a : Int32} : 0 ^^^ a = a := Int32.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem Int64.zero_xor {a : Int64} : 0 ^^^ a = a := Int64.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem ISize.zero_xor {a : ISize} : 0 ^^^ a = a := ISize.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem Int8.neg_one_xor {a : Int8} : -1 ^^^ a = ~~~a := by
rw [← Int8.toBitVec_inj, Int8.toBitVec_xor, Int8.toBitVec_neg, Int8.toBitVec_one,
@ -499,11 +499,11 @@ instance : Std.Commutative (α := ISize) (· ^^^ ·) := ⟨ISize.xor_comm⟩
rw [← ISize.toBitVec_inj, ISize.toBitVec_xor, ISize.toBitVec_neg, ISize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, ISize.toBitVec_not]
@[simp] theorem Int8.xor_neg_one {a : Int8} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem Int16.xor_neg_one {a : Int16} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem Int32.xor_neg_one {a : Int32} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem Int64.xor_neg_one {a : Int64} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem ISize.xor_neg_one {a : ISize} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem Int8.xor_neg_one {a : Int8} : a ^^^ -1 = ~~~a := by rw [Int8.xor_comm, neg_one_xor]
@[simp] theorem Int16.xor_neg_one {a : Int16} : a ^^^ -1 = ~~~a := by rw [Int16.xor_comm, neg_one_xor]
@[simp] theorem Int32.xor_neg_one {a : Int32} : a ^^^ -1 = ~~~a := by rw [Int32.xor_comm, neg_one_xor]
@[simp] theorem Int64.xor_neg_one {a : Int64} : a ^^^ -1 = ~~~a := by rw [Int64.xor_comm, neg_one_xor]
@[simp] theorem ISize.xor_neg_one {a : ISize} : a ^^^ -1 = ~~~a := by rw [ISize.xor_comm, neg_one_xor]
instance : Std.LawfulCommIdentity (α := Int8) (· ^^^ ·) 0 where
right_id _ := Int8.xor_zero

File diff suppressed because it is too large Load diff

View file

@ -27,7 +27,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_add"]
def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
protected def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
/--
Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
@ -35,7 +35,7 @@ via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_sub"]
def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
protected def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
/--
Multiplies two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
@ -43,7 +43,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_mul"]
def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
protected def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
/--
Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
@ -53,7 +53,7 @@ This operation is sometimes called “floor division.” Division by zero is def
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_div"]
def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
protected def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
/--
The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
@ -68,10 +68,10 @@ Examples:
* `UInt8.mod 4 0 = 4`
-/
@[extern "lean_uint8_mod"]
def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
protected def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
set_option linter.missingDocs false in
@[deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩
protected def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩
/--
Bitwise and for 8-bit unsigned integers. Usually accessed via the `&&&` operator.
@ -80,7 +80,7 @@ Each bit of the resulting integer is set if the corresponding bits of both input
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_land"]
def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
protected def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
/--
Bitwise or for 8-bit unsigned integers. Usually accessed via the `|||` operator.
@ -90,7 +90,7 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_lor"]
def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
protected def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
/--
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
@ -100,31 +100,31 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_xor"]
def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
protected def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
/--
Bitwise left shift for 8-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_shift_left"]
def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
protected def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (UInt8.mod b 8).toBitVec⟩
/--
Bitwise right shift for 8-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_shift_right"]
def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
protected def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (UInt8.mod b 8).toBitVec⟩
/--
Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
-/
def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
protected def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
/--
Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
-/
def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
protected def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
instance : Add UInt8 := ⟨UInt8.add⟩
instance : Sub UInt8 := ⟨UInt8.sub⟩
@ -147,7 +147,7 @@ Each bit of the resulting integer is the opposite of the corresponding bit of th
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_complement"]
def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
protected def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
/--
Negation of 8-bit unsigned integers, computed modulo `UInt8.size`.
@ -156,7 +156,7 @@ Negation of 8-bit unsigned integers, computed modulo `UInt8.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_neg"]
def UInt8.neg (a : UInt8) : UInt8 := ⟨-a.toBitVec⟩
protected def UInt8.neg (a : UInt8) : UInt8 := ⟨-a.toBitVec⟩
instance : Complement UInt8 := ⟨UInt8.complement⟩
instance : Neg UInt8 := ⟨UInt8.neg⟩
@ -224,7 +224,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_add"]
def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
protected def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
/--
Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
@ -232,7 +232,7 @@ via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_sub"]
def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
protected def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
/--
Multiplies two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
@ -240,7 +240,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_mul"]
def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
protected def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
/--
Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
@ -250,7 +250,7 @@ This operation is sometimes called “floor division.” Division by zero is def
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_div"]
def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
protected def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
/--
The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
@ -265,10 +265,10 @@ Examples:
* `UInt16.mod 4 0 = 4`
-/
@[extern "lean_uint16_mod"]
def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
protected def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
set_option linter.missingDocs false in
@[deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩
protected def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩
/--
Bitwise and for 16-bit unsigned integers. Usually accessed via the `&&&` operator.
@ -277,7 +277,7 @@ Each bit of the resulting integer is set if the corresponding bits of both input
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_land"]
def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
protected def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
/--
Bitwise or for 16-bit unsigned integers. Usually accessed via the `|||` operator.
@ -287,7 +287,7 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_lor"]
def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
protected def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
/--
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
@ -297,31 +297,31 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_xor"]
def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
protected def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
/--
Bitwise left shift for 16-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_shift_left"]
def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
protected def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (UInt16.mod b 16).toBitVec⟩
/--
Bitwise right shift for 16-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_shift_right"]
def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
protected def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (UInt16.mod b 16).toBitVec⟩
/--
Strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
-/
def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
protected def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
/--
Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
-/
def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
protected def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
instance : Add UInt16 := ⟨UInt16.add⟩
instance : Sub UInt16 := ⟨UInt16.sub⟩
@ -344,7 +344,7 @@ Each bit of the resulting integer is the opposite of the corresponding bit of th
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_complement"]
def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
protected def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
/--
Negation of 16-bit unsigned integers, computed modulo `UInt16.size`.
@ -353,7 +353,7 @@ Negation of 16-bit unsigned integers, computed modulo `UInt16.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_neg"]
def UInt16.neg (a : UInt16) : UInt16 := ⟨-a.toBitVec⟩
protected def UInt16.neg (a : UInt16) : UInt16 := ⟨-a.toBitVec⟩
instance : Complement UInt16 := ⟨UInt16.complement⟩
instance : Neg UInt16 := ⟨UInt16.neg⟩
@ -423,7 +423,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_add"]
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
protected def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
/--
Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
@ -431,7 +431,7 @@ via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_sub"]
def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
protected def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
/--
Multiplies two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
@ -439,7 +439,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_mul"]
def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
protected def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
/--
Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
@ -449,7 +449,7 @@ This operation is sometimes called “floor division.” Division by zero is def
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_div"]
def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
protected def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
/--
The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
@ -464,10 +464,10 @@ Examples:
* `UInt32.mod 4 0 = 4`
-/
@[extern "lean_uint32_mod"]
def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
protected def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
set_option linter.missingDocs false in
@[deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩
protected def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩
/--
Bitwise and for 32-bit unsigned integers. Usually accessed via the `&&&` operator.
@ -476,7 +476,7 @@ Each bit of the resulting integer is set if the corresponding bits of both input
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_land"]
def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
protected def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
/--
Bitwise or for 32-bit unsigned integers. Usually accessed via the `|||` operator.
@ -486,7 +486,7 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_lor"]
def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
protected def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
/--
Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the `^^^` operator.
@ -496,31 +496,31 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_xor"]
def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
protected def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
/--
Bitwise left shift for 32-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_shift_left"]
def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
protected def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (UInt32.mod b 32).toBitVec⟩
/--
Bitwise right shift for 32-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_shift_right"]
def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UInt32.mod b 32).toBitVec⟩
/--
Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
-/
def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
/--
Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
-/
def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
instance : Add UInt32 := ⟨UInt32.add⟩
instance : Sub UInt32 := ⟨UInt32.sub⟩
@ -543,7 +543,7 @@ Each bit of the resulting integer is the opposite of the corresponding bit of th
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_complement"]
def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
protected def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
/--
Negation of 32-bit unsigned integers, computed modulo `UInt32.size`.
@ -552,7 +552,7 @@ Negation of 32-bit unsigned integers, computed modulo `UInt32.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_neg"]
def UInt32.neg (a : UInt32) : UInt32 := ⟨-a.toBitVec⟩
protected def UInt32.neg (a : UInt32) : UInt32 := ⟨-a.toBitVec⟩
instance : Complement UInt32 := ⟨UInt32.complement⟩
instance : Neg UInt32 := ⟨UInt32.neg⟩
@ -584,7 +584,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_add"]
def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
protected def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
/--
Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
@ -592,7 +592,7 @@ via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_sub"]
def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
protected def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
/--
Multiplies two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
@ -600,7 +600,7 @@ operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_mul"]
def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
protected def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
/--
Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
@ -610,7 +610,7 @@ This operation is sometimes called “floor division.” Division by zero is def
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_div"]
def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
protected def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
/--
The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
@ -625,10 +625,10 @@ Examples:
* `UInt64.mod 4 0 = 4`
-/
@[extern "lean_uint64_mod"]
def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
protected def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
set_option linter.missingDocs false in
@[deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩
protected def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩
/--
Bitwise and for 64-bit unsigned integers. Usually accessed via the `&&&` operator.
@ -637,7 +637,7 @@ Each bit of the resulting integer is set if the corresponding bits of both input
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_land"]
def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
protected def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
/--
Bitwise or for 64-bit unsigned integers. Usually accessed via the `|||` operator.
@ -647,7 +647,7 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_lor"]
def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
protected def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
/--
Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the `^^^` operator.
@ -657,31 +657,31 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_xor"]
def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
protected def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
/--
Bitwise left shift for 64-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_shift_left"]
def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
protected def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (UInt64.mod b 64).toBitVec⟩
/--
Bitwise right shift for 64-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_shift_right"]
def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
protected def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (UInt64.mod b 64).toBitVec⟩
/--
Strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
-/
def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
protected def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
/--
Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
-/
def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
protected def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
instance : Add UInt64 := ⟨UInt64.add⟩
instance : Sub UInt64 := ⟨UInt64.sub⟩
@ -704,7 +704,7 @@ Each bit of the resulting integer is the opposite of the corresponding bit of th
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_complement"]
def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
protected def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
/--
Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
@ -713,7 +713,7 @@ Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_neg"]
def UInt64.neg (a : UInt64) : UInt64 := ⟨-a.toBitVec⟩
protected def UInt64.neg (a : UInt64) : UInt64 := ⟨-a.toBitVec⟩
instance : Complement UInt64 := ⟨UInt64.complement⟩
instance : Neg UInt64 := ⟨UInt64.neg⟩
@ -792,7 +792,7 @@ Multiplies two word-sized unsigned integers, wrapping around on overflow. Usual
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_mul"]
def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
protected def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
/--
Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
@ -802,7 +802,7 @@ This operation is sometimes called “floor division.” Division by zero is def
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_div"]
def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
protected def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
/--
The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
@ -817,10 +817,10 @@ Examples:
* `USize.mod 4 0 = 4`
-/
@[extern "lean_usize_mod"]
def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
protected def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
set_option linter.missingDocs false in
@[deprecated USize.mod (since := "2024-09-23")]
def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩
protected def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩
/--
Bitwise and for word-sized unsigned integers. Usually accessed via the `&&&` operator.
@ -829,7 +829,7 @@ Each bit of the resulting integer is set if the corresponding bits of both input
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_land"]
def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
protected def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
/--
Bitwise or for word-sized unsigned integers. Usually accessed via the `|||` operator.
@ -839,7 +839,7 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_lor"]
def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
protected def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
/--
Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the `^^^` operator.
@ -849,21 +849,21 @@ integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_xor"]
def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
protected def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
/--
Bitwise left shift for word-sized unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_shift_left"]
def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
protected def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (USize.mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
/--
Bitwise right shift for word-sized unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_shift_right"]
def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
protected def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (USize.mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
/--
Converts a natural number to a `USize`. Overflow is impossible on any supported platform because
`USize.size` is either `2^32` or `2^64`.
@ -953,14 +953,14 @@ Each bit of the resulting integer is the opposite of the corresponding bit of th
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_complement"]
def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
protected def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
/--
Negation of word-sized unsigned integers, computed modulo `USize.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_neg"]
def USize.neg (a : USize) : USize := ⟨-a.toBitVec⟩
protected def USize.neg (a : USize) : USize := ⟨-a.toBitVec⟩
instance : Complement USize := ⟨USize.complement⟩
instance : Neg USize := ⟨USize.neg⟩

View file

@ -707,11 +707,11 @@ theorem UInt32.not_eq_neg_sub (a : UInt32) : ~~~a = -a - 1 := UInt32.toBitVec_in
theorem UInt64.not_eq_neg_sub (a : UInt64) : ~~~a = -a - 1 := UInt64.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
theorem USize.not_eq_neg_sub (a : USize) : ~~~a = -a - 1 := USize.toBitVec_inj.1 (BitVec.not_eq_neg_add _)
theorem UInt8.or_assoc (a b c : UInt8) : a ||| b ||| c = a ||| (b ||| c) := UInt8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem UInt16.or_assoc (a b c : UInt16) : a ||| b ||| c = a ||| (b ||| c) := UInt16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem UInt32.or_assoc (a b c : UInt32) : a ||| b ||| c = a ||| (b ||| c) := UInt32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem UInt64.or_assoc (a b c : UInt64) : a ||| b ||| c = a ||| (b ||| c) := UInt64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
theorem USize.or_assoc (a b c : USize) : a ||| b ||| c = a ||| (b ||| c) := USize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem UInt8.or_assoc (a b c : UInt8) : a ||| b ||| c = a ||| (b ||| c) := UInt8.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem UInt16.or_assoc (a b c : UInt16) : a ||| b ||| c = a ||| (b ||| c) := UInt16.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem UInt32.or_assoc (a b c : UInt32) : a ||| b ||| c = a ||| (b ||| c) := UInt32.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem UInt64.or_assoc (a b c : UInt64) : a ||| b ||| c = a ||| (b ||| c) := UInt64.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
protected theorem USize.or_assoc (a b c : USize) : a ||| b ||| c = a ||| (b ||| c) := USize.toBitVec_inj.1 (BitVec.or_assoc _ _ _)
instance : Std.Associative (α := UInt8) (· ||| ·) := ⟨UInt8.or_assoc⟩
instance : Std.Associative (α := UInt16) (· ||| ·) := ⟨UInt16.or_assoc⟩
@ -719,11 +719,11 @@ instance : Std.Associative (α := UInt32) (· ||| ·) := ⟨UInt32.or_assoc⟩
instance : Std.Associative (α := UInt64) (· ||| ·) := ⟨UInt64.or_assoc⟩
instance : Std.Associative (α := USize) (· ||| ·) := ⟨USize.or_assoc⟩
theorem UInt8.or_comm (a b : UInt8) : a ||| b = b ||| a := UInt8.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem UInt16.or_comm (a b : UInt16) : a ||| b = b ||| a := UInt16.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem UInt32.or_comm (a b : UInt32) : a ||| b = b ||| a := UInt32.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem UInt64.or_comm (a b : UInt64) : a ||| b = b ||| a := UInt64.toBitVec_inj.1 (BitVec.or_comm _ _)
theorem USize.or_comm (a b : USize) : a ||| b = b ||| a := USize.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem UInt8.or_comm (a b : UInt8) : a ||| b = b ||| a := UInt8.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem UInt16.or_comm (a b : UInt16) : a ||| b = b ||| a := UInt16.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem UInt32.or_comm (a b : UInt32) : a ||| b = b ||| a := UInt32.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem UInt64.or_comm (a b : UInt64) : a ||| b = b ||| a := UInt64.toBitVec_inj.1 (BitVec.or_comm _ _)
protected theorem USize.or_comm (a b : USize) : a ||| b = b ||| a := USize.toBitVec_inj.1 (BitVec.or_comm _ _)
instance : Std.Commutative (α := UInt8) (· ||| ·) := ⟨UInt8.or_comm⟩
instance : Std.Commutative (α := UInt16) (· ||| ·) := ⟨UInt16.or_comm⟩
@ -731,11 +731,11 @@ instance : Std.Commutative (α := UInt32) (· ||| ·) := ⟨UInt32.or_comm⟩
instance : Std.Commutative (α := UInt64) (· ||| ·) := ⟨UInt64.or_comm⟩
instance : Std.Commutative (α := USize) (· ||| ·) := ⟨USize.or_comm⟩
@[simp] theorem UInt8.or_self {a : UInt8} : a ||| a = a := UInt8.toBitVec_inj.1 BitVec.or_self
@[simp] theorem UInt16.or_self {a : UInt16} : a ||| a = a := UInt16.toBitVec_inj.1 BitVec.or_self
@[simp] theorem UInt32.or_self {a : UInt32} : a ||| a = a := UInt32.toBitVec_inj.1 BitVec.or_self
@[simp] theorem UInt64.or_self {a : UInt64} : a ||| a = a := UInt64.toBitVec_inj.1 BitVec.or_self
@[simp] theorem USize.or_self {a : USize} : a ||| a = a := USize.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem UInt8.or_self {a : UInt8} : a ||| a = a := UInt8.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem UInt16.or_self {a : UInt16} : a ||| a = a := UInt16.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem UInt32.or_self {a : UInt32} : a ||| a = a := UInt32.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem UInt64.or_self {a : UInt64} : a ||| a = a := UInt64.toBitVec_inj.1 BitVec.or_self
@[simp] protected theorem USize.or_self {a : USize} : a ||| a = a := USize.toBitVec_inj.1 BitVec.or_self
instance : Std.IdempotentOp (α := UInt8) (· ||| ·) := ⟨fun _ => UInt8.or_self⟩
instance : Std.IdempotentOp (α := UInt16) (· ||| ·) := ⟨fun _ => UInt16.or_self⟩
@ -743,17 +743,17 @@ instance : Std.IdempotentOp (α := UInt32) (· ||| ·) := ⟨fun _ => UInt32.or_
instance : Std.IdempotentOp (α := UInt64) (· ||| ·) := ⟨fun _ => UInt64.or_self⟩
instance : Std.IdempotentOp (α := USize) (· ||| ·) := ⟨fun _ => USize.or_self⟩
@[simp] theorem UInt8.or_zero {a : UInt8} : a ||| 0 = a := UInt8.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem UInt16.or_zero {a : UInt16} : a ||| 0 = a := UInt16.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem UInt32.or_zero {a : UInt32} : a ||| 0 = a := UInt32.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem UInt64.or_zero {a : UInt64} : a ||| 0 = a := UInt64.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem USize.or_zero {a : USize} : a ||| 0 = a := USize.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem UInt8.or_zero {a : UInt8} : a ||| 0 = a := UInt8.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem UInt16.or_zero {a : UInt16} : a ||| 0 = a := UInt16.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem UInt32.or_zero {a : UInt32} : a ||| 0 = a := UInt32.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem UInt64.or_zero {a : UInt64} : a ||| 0 = a := UInt64.toBitVec_inj.1 BitVec.or_zero
@[simp] protected theorem USize.or_zero {a : USize} : a ||| 0 = a := USize.toBitVec_inj.1 BitVec.or_zero
@[simp] theorem UInt8.zero_or {a : UInt8} : 0 ||| a = a := UInt8.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem UInt16.zero_or {a : UInt16} : 0 ||| a = a := UInt16.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem UInt32.zero_or {a : UInt32} : 0 ||| a = a := UInt32.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem UInt64.zero_or {a : UInt64} : 0 ||| a = a := UInt64.toBitVec_inj.1 BitVec.zero_or
@[simp] theorem USize.zero_or {a : USize} : 0 ||| a = a := USize.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem UInt8.zero_or {a : UInt8} : 0 ||| a = a := UInt8.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem UInt16.zero_or {a : UInt16} : 0 ||| a = a := UInt16.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem UInt32.zero_or {a : UInt32} : 0 ||| a = a := UInt32.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem UInt64.zero_or {a : UInt64} : 0 ||| a = a := UInt64.toBitVec_inj.1 BitVec.zero_or
@[simp] protected theorem USize.zero_or {a : USize} : 0 ||| a = a := USize.toBitVec_inj.1 BitVec.zero_or
instance : Std.LawfulCommIdentity (α := UInt8) (· ||| ·) 0 where
right_id _ := UInt8.or_zero
@ -782,11 +782,11 @@ instance : Std.LawfulCommIdentity (α := USize) (· ||| ·) 0 where
rw [← USize.toBitVec_inj, USize.toBitVec_or, USize.toBitVec_neg, USize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_or]
@[simp] theorem UInt8.or_neg_one {a : UInt8} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem UInt16.or_neg_one {a : UInt16} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem UInt32.or_neg_one {a : UInt32} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem UInt64.or_neg_one {a : UInt64} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem USize.or_neg_one {a : USize} : a ||| -1 = -1 := by rw [or_comm, neg_one_or]
@[simp] theorem UInt8.or_neg_one {a : UInt8} : a ||| -1 = -1 := by rw [UInt8.or_comm, neg_one_or]
@[simp] theorem UInt16.or_neg_one {a : UInt16} : a ||| -1 = -1 := by rw [UInt16.or_comm, neg_one_or]
@[simp] theorem UInt32.or_neg_one {a : UInt32} : a ||| -1 = -1 := by rw [UInt32.or_comm, neg_one_or]
@[simp] theorem UInt64.or_neg_one {a : UInt64} : a ||| -1 = -1 := by rw [UInt64.or_comm, neg_one_or]
@[simp] theorem USize.or_neg_one {a : USize} : a ||| -1 = -1 := by rw [USize.or_comm, neg_one_or]
@[simp] theorem UInt8.or_eq_zero_iff {a b : UInt8} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
simp [← UInt8.toBitVec_inj]
@ -799,11 +799,11 @@ instance : Std.LawfulCommIdentity (α := USize) (· ||| ·) 0 where
@[simp] theorem USize.or_eq_zero_iff {a b : USize} : a ||| b = 0 ↔ a = 0 ∧ b = 0 := by
simp [← USize.toBitVec_inj]
theorem UInt8.and_assoc (a b c : UInt8) : a &&& b &&& c = a &&& (b &&& c) := UInt8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem UInt16.and_assoc (a b c : UInt16) : a &&& b &&& c = a &&& (b &&& c) := UInt16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem UInt32.and_assoc (a b c : UInt32) : a &&& b &&& c = a &&& (b &&& c) := UInt32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem UInt64.and_assoc (a b c : UInt64) : a &&& b &&& c = a &&& (b &&& c) := UInt64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
theorem USize.and_assoc (a b c : USize) : a &&& b &&& c = a &&& (b &&& c) := USize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem UInt8.and_assoc (a b c : UInt8) : a &&& b &&& c = a &&& (b &&& c) := UInt8.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem UInt16.and_assoc (a b c : UInt16) : a &&& b &&& c = a &&& (b &&& c) := UInt16.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem UInt32.and_assoc (a b c : UInt32) : a &&& b &&& c = a &&& (b &&& c) := UInt32.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem UInt64.and_assoc (a b c : UInt64) : a &&& b &&& c = a &&& (b &&& c) := UInt64.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
protected theorem USize.and_assoc (a b c : USize) : a &&& b &&& c = a &&& (b &&& c) := USize.toBitVec_inj.1 (BitVec.and_assoc _ _ _)
instance : Std.Associative (α := UInt8) (· &&& ·) := ⟨UInt8.and_assoc⟩
instance : Std.Associative (α := UInt16) (· &&& ·) := ⟨UInt16.and_assoc⟩
@ -811,11 +811,11 @@ instance : Std.Associative (α := UInt32) (· &&& ·) := ⟨UInt32.and_assoc⟩
instance : Std.Associative (α := UInt64) (· &&& ·) := ⟨UInt64.and_assoc⟩
instance : Std.Associative (α := USize) (· &&& ·) := ⟨USize.and_assoc⟩
theorem UInt8.and_comm (a b : UInt8) : a &&& b = b &&& a := UInt8.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem UInt16.and_comm (a b : UInt16) : a &&& b = b &&& a := UInt16.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem UInt32.and_comm (a b : UInt32) : a &&& b = b &&& a := UInt32.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem UInt64.and_comm (a b : UInt64) : a &&& b = b &&& a := UInt64.toBitVec_inj.1 (BitVec.and_comm _ _)
theorem USize.and_comm (a b : USize) : a &&& b = b &&& a := USize.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem UInt8.and_comm (a b : UInt8) : a &&& b = b &&& a := UInt8.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem UInt16.and_comm (a b : UInt16) : a &&& b = b &&& a := UInt16.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem UInt32.and_comm (a b : UInt32) : a &&& b = b &&& a := UInt32.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem UInt64.and_comm (a b : UInt64) : a &&& b = b &&& a := UInt64.toBitVec_inj.1 (BitVec.and_comm _ _)
protected theorem USize.and_comm (a b : USize) : a &&& b = b &&& a := USize.toBitVec_inj.1 (BitVec.and_comm _ _)
instance : Std.Commutative (α := UInt8) (· &&& ·) := ⟨UInt8.and_comm⟩
instance : Std.Commutative (α := UInt16) (· &&& ·) := ⟨UInt16.and_comm⟩
@ -823,11 +823,11 @@ instance : Std.Commutative (α := UInt32) (· &&& ·) := ⟨UInt32.and_comm⟩
instance : Std.Commutative (α := UInt64) (· &&& ·) := ⟨UInt64.and_comm⟩
instance : Std.Commutative (α := USize) (· &&& ·) := ⟨USize.and_comm⟩
@[simp] theorem UInt8.and_self {a : UInt8} : a &&& a = a := UInt8.toBitVec_inj.1 BitVec.and_self
@[simp] theorem UInt16.and_self {a : UInt16} : a &&& a = a := UInt16.toBitVec_inj.1 BitVec.and_self
@[simp] theorem UInt32.and_self {a : UInt32} : a &&& a = a := UInt32.toBitVec_inj.1 BitVec.and_self
@[simp] theorem UInt64.and_self {a : UInt64} : a &&& a = a := UInt64.toBitVec_inj.1 BitVec.and_self
@[simp] theorem USize.and_self {a : USize} : a &&& a = a := USize.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem UInt8.and_self {a : UInt8} : a &&& a = a := UInt8.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem UInt16.and_self {a : UInt16} : a &&& a = a := UInt16.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem UInt32.and_self {a : UInt32} : a &&& a = a := UInt32.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem UInt64.and_self {a : UInt64} : a &&& a = a := UInt64.toBitVec_inj.1 BitVec.and_self
@[simp] protected theorem USize.and_self {a : USize} : a &&& a = a := USize.toBitVec_inj.1 BitVec.and_self
instance : Std.IdempotentOp (α := UInt8) (· &&& ·) := ⟨fun _ => UInt8.and_self⟩
instance : Std.IdempotentOp (α := UInt16) (· &&& ·) := ⟨fun _ => UInt16.and_self⟩
@ -835,17 +835,17 @@ instance : Std.IdempotentOp (α := UInt32) (· &&& ·) := ⟨fun _ => UInt32.and
instance : Std.IdempotentOp (α := UInt64) (· &&& ·) := ⟨fun _ => UInt64.and_self⟩
instance : Std.IdempotentOp (α := USize) (· &&& ·) := ⟨fun _ => USize.and_self⟩
@[simp] theorem UInt8.and_zero {a : UInt8} : a &&& 0 = 0 := UInt8.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem UInt16.and_zero {a : UInt16} : a &&& 0 = 0 := UInt16.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem UInt32.and_zero {a : UInt32} : a &&& 0 = 0 := UInt32.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem UInt64.and_zero {a : UInt64} : a &&& 0 = 0 := UInt64.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem USize.and_zero {a : USize} : a &&& 0 = 0 := USize.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem UInt8.and_zero {a : UInt8} : a &&& 0 = 0 := UInt8.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem UInt16.and_zero {a : UInt16} : a &&& 0 = 0 := UInt16.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem UInt32.and_zero {a : UInt32} : a &&& 0 = 0 := UInt32.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem UInt64.and_zero {a : UInt64} : a &&& 0 = 0 := UInt64.toBitVec_inj.1 BitVec.and_zero
@[simp] protected theorem USize.and_zero {a : USize} : a &&& 0 = 0 := USize.toBitVec_inj.1 BitVec.and_zero
@[simp] theorem UInt8.zero_and {a : UInt8} : 0 &&& a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem UInt16.zero_and {a : UInt16} : 0 &&& a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem UInt32.zero_and {a : UInt32} : 0 &&& a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem UInt64.zero_and {a : UInt64} : 0 &&& a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem USize.zero_and {a : USize} : 0 &&& a = 0 := USize.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem UInt8.zero_and {a : UInt8} : 0 &&& a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem UInt16.zero_and {a : UInt16} : 0 &&& a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem UInt32.zero_and {a : UInt32} : 0 &&& a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem UInt64.zero_and {a : UInt64} : 0 &&& a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_and
@[simp] protected theorem USize.zero_and {a : USize} : 0 &&& a = 0 := USize.toBitVec_inj.1 BitVec.zero_and
@[simp] theorem UInt8.neg_one_and {a : UInt8} : -1 &&& a = a := by
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_and, UInt8.toBitVec_neg, UInt8.toBitVec_one,
@ -863,11 +863,11 @@ instance : Std.IdempotentOp (α := USize) (· &&& ·) := ⟨fun _ => USize.and_s
rw [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_and]
@[simp] theorem UInt8.and_neg_one {a : UInt8} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem UInt16.and_neg_one {a : UInt16} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem UInt32.and_neg_one {a : UInt32} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem UInt64.and_neg_one {a : UInt64} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem USize.and_neg_one {a : USize} : a &&& -1 = a := by rw [and_comm, neg_one_and]
@[simp] theorem UInt8.and_neg_one {a : UInt8} : a &&& -1 = a := by rw [UInt8.and_comm, neg_one_and]
@[simp] theorem UInt16.and_neg_one {a : UInt16} : a &&& -1 = a := by rw [UInt16.and_comm, neg_one_and]
@[simp] theorem UInt32.and_neg_one {a : UInt32} : a &&& -1 = a := by rw [UInt32.and_comm, neg_one_and]
@[simp] theorem UInt64.and_neg_one {a : UInt64} : a &&& -1 = a := by rw [UInt64.and_comm, neg_one_and]
@[simp] theorem USize.and_neg_one {a : USize} : a &&& -1 = a := by rw [USize.and_comm, neg_one_and]
instance : Std.LawfulCommIdentity (α := UInt8) (· &&& ·) (-1) where
right_id _ := UInt8.and_neg_one
@ -896,11 +896,11 @@ instance : Std.LawfulCommIdentity (α := USize) (· &&& ·) (-1) where
simp only [← USize.toBitVec_inj, USize.toBitVec_and, USize.toBitVec_neg, USize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.and_eq_allOnes_iff]
theorem UInt8.xor_assoc (a b c : UInt8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem UInt16.xor_assoc (a b c : UInt16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem UInt32.xor_assoc (a b c : UInt32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem UInt64.xor_assoc (a b c : UInt64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
theorem USize.xor_assoc (a b c : USize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := USize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem UInt8.xor_assoc (a b c : UInt8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt8.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem UInt16.xor_assoc (a b c : UInt16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt16.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem UInt32.xor_assoc (a b c : UInt32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt32.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem UInt64.xor_assoc (a b c : UInt64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := UInt64.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
protected theorem USize.xor_assoc (a b c : USize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := USize.toBitVec_inj.1 (BitVec.xor_assoc _ _ _)
instance : Std.Associative (α := UInt8) (· ^^^ ·) := ⟨UInt8.xor_assoc⟩
instance : Std.Associative (α := UInt16) (· ^^^ ·) := ⟨UInt16.xor_assoc⟩
@ -908,11 +908,11 @@ instance : Std.Associative (α := UInt32) (· ^^^ ·) := ⟨UInt32.xor_assoc⟩
instance : Std.Associative (α := UInt64) (· ^^^ ·) := ⟨UInt64.xor_assoc⟩
instance : Std.Associative (α := USize) (· ^^^ ·) := ⟨USize.xor_assoc⟩
theorem UInt8.xor_comm (a b : UInt8) : a ^^^ b = b ^^^ a := UInt8.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem UInt16.xor_comm (a b : UInt16) : a ^^^ b = b ^^^ a := UInt16.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem UInt32.xor_comm (a b : UInt32) : a ^^^ b = b ^^^ a := UInt32.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem UInt64.xor_comm (a b : UInt64) : a ^^^ b = b ^^^ a := UInt64.toBitVec_inj.1 (BitVec.xor_comm _ _)
theorem USize.xor_comm (a b : USize) : a ^^^ b = b ^^^ a := USize.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem UInt8.xor_comm (a b : UInt8) : a ^^^ b = b ^^^ a := UInt8.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem UInt16.xor_comm (a b : UInt16) : a ^^^ b = b ^^^ a := UInt16.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem UInt32.xor_comm (a b : UInt32) : a ^^^ b = b ^^^ a := UInt32.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem UInt64.xor_comm (a b : UInt64) : a ^^^ b = b ^^^ a := UInt64.toBitVec_inj.1 (BitVec.xor_comm _ _)
protected theorem USize.xor_comm (a b : USize) : a ^^^ b = b ^^^ a := USize.toBitVec_inj.1 (BitVec.xor_comm _ _)
instance : Std.Commutative (α := UInt8) (· ^^^ ·) := ⟨UInt8.xor_comm⟩
instance : Std.Commutative (α := UInt16) (· ^^^ ·) := ⟨UInt16.xor_comm⟩
@ -920,23 +920,23 @@ instance : Std.Commutative (α := UInt32) (· ^^^ ·) := ⟨UInt32.xor_comm⟩
instance : Std.Commutative (α := UInt64) (· ^^^ ·) := ⟨UInt64.xor_comm⟩
instance : Std.Commutative (α := USize) (· ^^^ ·) := ⟨USize.xor_comm⟩
@[simp] theorem UInt8.xor_self {a : UInt8} : a ^^^ a = 0 := UInt8.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem UInt16.xor_self {a : UInt16} : a ^^^ a = 0 := UInt16.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem UInt32.xor_self {a : UInt32} : a ^^^ a = 0 := UInt32.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem UInt64.xor_self {a : UInt64} : a ^^^ a = 0 := UInt64.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem USize.xor_self {a : USize} : a ^^^ a = 0 := USize.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem UInt8.xor_self {a : UInt8} : a ^^^ a = 0 := UInt8.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem UInt16.xor_self {a : UInt16} : a ^^^ a = 0 := UInt16.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem UInt32.xor_self {a : UInt32} : a ^^^ a = 0 := UInt32.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem UInt64.xor_self {a : UInt64} : a ^^^ a = 0 := UInt64.toBitVec_inj.1 BitVec.xor_self
@[simp] protected theorem USize.xor_self {a : USize} : a ^^^ a = 0 := USize.toBitVec_inj.1 BitVec.xor_self
@[simp] theorem UInt8.xor_zero {a : UInt8} : a ^^^ 0 = a := UInt8.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem UInt16.xor_zero {a : UInt16} : a ^^^ 0 = a := UInt16.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem UInt32.xor_zero {a : UInt32} : a ^^^ 0 = a := UInt32.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem UInt64.xor_zero {a : UInt64} : a ^^^ 0 = a := UInt64.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem USize.xor_zero {a : USize} : a ^^^ 0 = a := USize.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem UInt8.xor_zero {a : UInt8} : a ^^^ 0 = a := UInt8.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem UInt16.xor_zero {a : UInt16} : a ^^^ 0 = a := UInt16.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem UInt32.xor_zero {a : UInt32} : a ^^^ 0 = a := UInt32.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem UInt64.xor_zero {a : UInt64} : a ^^^ 0 = a := UInt64.toBitVec_inj.1 BitVec.xor_zero
@[simp] protected theorem USize.xor_zero {a : USize} : a ^^^ 0 = a := USize.toBitVec_inj.1 BitVec.xor_zero
@[simp] theorem UInt8.zero_xor {a : UInt8} : 0 ^^^ a = a := UInt8.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem UInt16.zero_xor {a : UInt16} : 0 ^^^ a = a := UInt16.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem UInt32.zero_xor {a : UInt32} : 0 ^^^ a = a := UInt32.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem UInt64.zero_xor {a : UInt64} : 0 ^^^ a = a := UInt64.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem USize.zero_xor {a : USize} : 0 ^^^ a = a := USize.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem UInt8.zero_xor {a : UInt8} : 0 ^^^ a = a := UInt8.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem UInt16.zero_xor {a : UInt16} : 0 ^^^ a = a := UInt16.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem UInt32.zero_xor {a : UInt32} : 0 ^^^ a = a := UInt32.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem UInt64.zero_xor {a : UInt64} : 0 ^^^ a = a := UInt64.toBitVec_inj.1 BitVec.zero_xor
@[simp] protected theorem USize.zero_xor {a : USize} : 0 ^^^ a = a := USize.toBitVec_inj.1 BitVec.zero_xor
@[simp] theorem UInt8.neg_one_xor {a : UInt8} : -1 ^^^ a = ~~~a := by
rw [← UInt8.toBitVec_inj, UInt8.toBitVec_xor, UInt8.toBitVec_neg, UInt8.toBitVec_one,
@ -954,11 +954,11 @@ instance : Std.Commutative (α := USize) (· ^^^ ·) := ⟨USize.xor_comm⟩
rw [← USize.toBitVec_inj, USize.toBitVec_xor, USize.toBitVec_neg, USize.toBitVec_one,
BitVec.negOne_eq_allOnes, BitVec.allOnes_xor, USize.toBitVec_not]
@[simp] theorem UInt8.xor_neg_one {a : UInt8} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem UInt16.xor_neg_one {a : UInt16} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem UInt32.xor_neg_one {a : UInt32} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem UInt64.xor_neg_one {a : UInt64} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem USize.xor_neg_one {a : USize} : a ^^^ -1 = ~~~a := by rw [xor_comm, neg_one_xor]
@[simp] theorem UInt8.xor_neg_one {a : UInt8} : a ^^^ -1 = ~~~a := by rw [UInt8.xor_comm, neg_one_xor]
@[simp] theorem UInt16.xor_neg_one {a : UInt16} : a ^^^ -1 = ~~~a := by rw [UInt16.xor_comm, neg_one_xor]
@[simp] theorem UInt32.xor_neg_one {a : UInt32} : a ^^^ -1 = ~~~a := by rw [UInt32.xor_comm, neg_one_xor]
@[simp] theorem UInt64.xor_neg_one {a : UInt64} : a ^^^ -1 = ~~~a := by rw [UInt64.xor_comm, neg_one_xor]
@[simp] theorem USize.xor_neg_one {a : USize} : a ^^^ -1 = ~~~a := by rw [USize.xor_comm, neg_one_xor]
instance : Std.LawfulCommIdentity (α := UInt8) (· ^^^ ·) 0 where
right_id _ := UInt8.xor_zero

View file

@ -75,12 +75,12 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
@[int_toBitVec] theorem le_iff_toBitVec_le {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
@[deprecated le_iff_toBitVec_le (since := "2025-03-20")]
theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
protected theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
@[int_toBitVec] theorem lt_iff_toBitVec_lt {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
@[deprecated lt_iff_toBitVec_lt (since := "2025-03-20")]
theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
protected theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
theorem le_iff_toNat_le {a b : $typeName} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
@ -182,7 +182,7 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
· apply toNat_lt_size
· simpa using h2
open $typeName (toNat_mod_lt) in
open $typeName (toNat_mod_lt modn) in
set_option linter.deprecated false in
@[deprecated toNat_mod_lt (since := "2024-09-24")]
protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
@ -347,11 +347,11 @@ theorem USize.le_ofNat_iff {n : USize} {m : Nat} (h : m < size) : n ≤ ofNat m
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)
protected 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)
protected 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)
protected 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)
protected 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)
protected 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
@ -1864,17 +1864,17 @@ theorem USize.le_iff_toFin_le {a b : USize} : a ≤ b ↔ a.toFin ≤ b.toFin :=
@[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 _ _)
protected theorem UInt8.sub_eq_add_neg (a b : UInt8) : a - b = a + (-b) := UInt8.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
protected theorem UInt16.sub_eq_add_neg (a b : UInt16) : a - b = a + (-b) := UInt16.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
protected theorem UInt32.sub_eq_add_neg (a b : UInt32) : a - b = a + (-b) := UInt32.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
protected theorem UInt64.sub_eq_add_neg (a b : UInt64) : a - b = a + (-b) := UInt64.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
protected theorem USize.sub_eq_add_neg (a b : USize) : a - b = a + (-b) := USize.toBitVec_inj.1 (BitVec.sub_toAdd _ _)
theorem UInt8.add_neg_eq_sub {a b : UInt8} : a + -b = a - b := UInt8.toBitVec_inj.1 BitVec.add_neg_eq_sub
theorem UInt16.add_neg_eq_sub {a b : UInt16} : a + -b = a - b := UInt16.toBitVec_inj.1 BitVec.add_neg_eq_sub
theorem UInt32.add_neg_eq_sub {a b : UInt32} : a + -b = a - b := UInt32.toBitVec_inj.1 BitVec.add_neg_eq_sub
theorem UInt64.add_neg_eq_sub {a b : UInt64} : a + -b = a - b := UInt64.toBitVec_inj.1 BitVec.add_neg_eq_sub
theorem USize.add_neg_eq_sub {a b : USize} : a + -b = a - b := USize.toBitVec_inj.1 BitVec.add_neg_eq_sub
protected theorem UInt8.add_neg_eq_sub {a b : UInt8} : a + -b = a - b := UInt8.toBitVec_inj.1 BitVec.add_neg_eq_sub
protected theorem UInt16.add_neg_eq_sub {a b : UInt16} : a + -b = a - b := UInt16.toBitVec_inj.1 BitVec.add_neg_eq_sub
protected theorem UInt32.add_neg_eq_sub {a b : UInt32} : a + -b = a - b := UInt32.toBitVec_inj.1 BitVec.add_neg_eq_sub
protected theorem UInt64.add_neg_eq_sub {a b : UInt64} : a + -b = a - b := UInt64.toBitVec_inj.1 BitVec.add_neg_eq_sub
protected theorem USize.add_neg_eq_sub {a b : USize} : a + -b = a - b := USize.toBitVec_inj.1 BitVec.add_neg_eq_sub
theorem UInt8.neg_one_eq : (-1 : UInt8) = 255 := rfl
theorem UInt16.neg_one_eq : (-1 : UInt16) = 65535 := rfl
@ -1912,15 +1912,15 @@ theorem USize.neg_eq_neg_one_mul (a : USize) : -a = -1 * a := by
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]
rw [UInt8.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]
rw [UInt16.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]
rw [UInt32.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]
rw [UInt64.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]
rw [USize.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)
@ -1929,28 +1929,28 @@ theorem USize.sub_eq_add_mul (a b : USize) : a - b = a + USize.ofNatLT (USize.si
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 [UInt16.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 [UInt32.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 [UInt32.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 [UInt64.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 [UInt64.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 [UInt64.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 [UInt64.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 [USize.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 [USize.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 [USize.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]
@ -2132,11 +2132,11 @@ theorem USize.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : USize) : USize.ofNat a =
@[simp] theorem UInt64.ofBitVec_sub (a b : BitVec 64) : UInt64.ofBitVec (a - b) = UInt64.ofBitVec a - UInt64.ofBitVec b := rfl
@[simp] theorem USize.ofBitVec_sub (a b : BitVec System.Platform.numBits) : USize.ofBitVec (a - b) = USize.ofBitVec a - USize.ofBitVec b := rfl
theorem UInt8.add_sub_cancel (a b : UInt8) : a + b - b = a := UInt8.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
theorem UInt16.add_sub_cancel (a b : UInt16) : a + b - b = a := UInt16.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
theorem UInt32.add_sub_cancel (a b : UInt32) : a + b - b = a := UInt32.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
theorem UInt64.add_sub_cancel (a b : UInt64) : a + b - b = a := UInt64.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
theorem USize.add_sub_cancel (a b : USize) : a + b - b = a := USize.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
@[simp] protected theorem UInt8.add_sub_cancel (a b : UInt8) : a + b - b = a := UInt8.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
@[simp] protected theorem UInt16.add_sub_cancel (a b : UInt16) : a + b - b = a := UInt16.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
@[simp] protected theorem UInt32.add_sub_cancel (a b : UInt32) : a + b - b = a := UInt32.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
@[simp] protected theorem UInt64.add_sub_cancel (a b : UInt64) : a + b - b = a := UInt64.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
@[simp] protected theorem USize.add_sub_cancel (a b : USize) : a + b - b = a := USize.toBitVec_inj.1 (BitVec.add_sub_cancel _ _)
theorem UInt8.ofNat_sub {a b : Nat} (hab : b ≤ a) : UInt8.ofNat (a - b) = UInt8.ofNat a - UInt8.ofNat b := by
rw [(Nat.sub_add_cancel hab ▸ UInt8.ofNat_add (a - b) b :), UInt8.add_sub_cancel]
@ -2301,15 +2301,15 @@ theorem UInt32.zero_ne_one : (0 : UInt32) ≠ 1 := by simp
theorem UInt64.zero_ne_one : (0 : UInt64) ≠ 1 := by simp
theorem USize.zero_ne_one : (0 : USize) ≠ 1 := by simp [← USize.toNat_inj]
theorem UInt8.add_assoc (a b c : UInt8) : a + b + c = a + (b + c) :=
protected theorem UInt8.add_assoc (a b c : UInt8) : a + b + c = a + (b + c) :=
UInt8.toBitVec_inj.1 (BitVec.add_assoc _ _ _)
theorem UInt16.add_assoc (a b c : UInt16) : a + b + c = a + (b + c) :=
protected theorem UInt16.add_assoc (a b c : UInt16) : a + b + c = a + (b + c) :=
UInt16.toBitVec_inj.1 (BitVec.add_assoc _ _ _)
theorem UInt32.add_assoc (a b c : UInt32) : a + b + c = a + (b + c) :=
protected theorem UInt32.add_assoc (a b c : UInt32) : a + b + c = a + (b + c) :=
UInt32.toBitVec_inj.1 (BitVec.add_assoc _ _ _)
theorem UInt64.add_assoc (a b c : UInt64) : a + b + c = a + (b + c) :=
protected theorem UInt64.add_assoc (a b c : UInt64) : a + b + c = a + (b + c) :=
UInt64.toBitVec_inj.1 (BitVec.add_assoc _ _ _)
theorem USize.add_assoc (a b c : USize) : a + b + c = a + (b + c) :=
protected theorem USize.add_assoc (a b c : USize) : a + b + c = a + (b + c) :=
USize.toBitVec_inj.1 (BitVec.add_assoc _ _ _)
instance : Std.Associative (α := UInt8) (· + ·) := ⟨UInt8.add_assoc⟩
@ -2318,11 +2318,11 @@ instance : Std.Associative (α := UInt32) (· + ·) := ⟨UInt32.add_assoc⟩
instance : Std.Associative (α := UInt64) (· + ·) := ⟨UInt64.add_assoc⟩
instance : Std.Associative (α := USize) (· + ·) := ⟨USize.add_assoc⟩
theorem UInt8.add_comm (a b : UInt8) : a + b = b + a := UInt8.toBitVec_inj.1 (BitVec.add_comm _ _)
theorem UInt16.add_comm (a b : UInt16) : a + b = b + a := UInt16.toBitVec_inj.1 (BitVec.add_comm _ _)
theorem UInt32.add_comm (a b : UInt32) : a + b = b + a := UInt32.toBitVec_inj.1 (BitVec.add_comm _ _)
theorem UInt64.add_comm (a b : UInt64) : a + b = b + a := UInt64.toBitVec_inj.1 (BitVec.add_comm _ _)
theorem USize.add_comm (a b : USize) : a + b = b + a := USize.toBitVec_inj.1 (BitVec.add_comm _ _)
protected theorem UInt8.add_comm (a b : UInt8) : a + b = b + a := UInt8.toBitVec_inj.1 (BitVec.add_comm _ _)
protected theorem UInt16.add_comm (a b : UInt16) : a + b = b + a := UInt16.toBitVec_inj.1 (BitVec.add_comm _ _)
protected theorem UInt32.add_comm (a b : UInt32) : a + b = b + a := UInt32.toBitVec_inj.1 (BitVec.add_comm _ _)
protected theorem UInt64.add_comm (a b : UInt64) : a + b = b + a := UInt64.toBitVec_inj.1 (BitVec.add_comm _ _)
protected theorem USize.add_comm (a b : USize) : a + b = b + a := USize.toBitVec_inj.1 (BitVec.add_comm _ _)
instance : Std.Commutative (α := UInt8) (· + ·) := ⟨UInt8.add_comm⟩
instance : Std.Commutative (α := UInt16) (· + ·) := ⟨UInt16.add_comm⟩
@ -2330,17 +2330,17 @@ instance : Std.Commutative (α := UInt32) (· + ·) := ⟨UInt32.add_comm⟩
instance : Std.Commutative (α := UInt64) (· + ·) := ⟨UInt64.add_comm⟩
instance : Std.Commutative (α := USize) (· + ·) := ⟨USize.add_comm⟩
@[simp] theorem UInt8.add_zero (a : UInt8) : a + 0 = a := UInt8.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] theorem UInt16.add_zero (a : UInt16) : a + 0 = a := UInt16.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] theorem UInt32.add_zero (a : UInt32) : a + 0 = a := UInt32.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] theorem UInt64.add_zero (a : UInt64) : a + 0 = a := UInt64.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] theorem USize.add_zero (a : USize) : a + 0 = a := USize.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] protected theorem UInt8.add_zero (a : UInt8) : a + 0 = a := UInt8.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] protected theorem UInt16.add_zero (a : UInt16) : a + 0 = a := UInt16.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] protected theorem UInt32.add_zero (a : UInt32) : a + 0 = a := UInt32.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] protected theorem UInt64.add_zero (a : UInt64) : a + 0 = a := UInt64.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] protected theorem USize.add_zero (a : USize) : a + 0 = a := USize.toBitVec_inj.1 (BitVec.add_zero _)
@[simp] theorem UInt8.zero_add (a : UInt8) : 0 + a = a := UInt8.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] theorem UInt16.zero_add (a : UInt16) : 0 + a = a := UInt16.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] theorem UInt32.zero_add (a : UInt32) : 0 + a = a := UInt32.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] theorem UInt64.zero_add (a : UInt64) : 0 + a = a := UInt64.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] theorem USize.zero_add (a : USize) : 0 + a = a := USize.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] protected theorem UInt8.zero_add (a : UInt8) : 0 + a = a := UInt8.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] protected theorem UInt16.zero_add (a : UInt16) : 0 + a = a := UInt16.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] protected theorem UInt32.zero_add (a : UInt32) : 0 + a = a := UInt32.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] protected theorem UInt64.zero_add (a : UInt64) : 0 + a = a := UInt64.toBitVec_inj.1 (BitVec.zero_add _)
@[simp] protected theorem USize.zero_add (a : USize) : 0 + a = a := USize.toBitVec_inj.1 (BitVec.zero_add _)
instance : Std.LawfulIdentity (α := UInt8) (· + ·) 0 where
left_id := UInt8.zero_add
@ -2358,146 +2358,146 @@ instance : Std.LawfulIdentity (α := USize) (· + ·) 0 where
left_id := USize.zero_add
right_id := USize.add_zero
@[simp] theorem UInt8.sub_zero (a : UInt8) : a - 0 = a := UInt8.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] theorem UInt16.sub_zero (a : UInt16) : a - 0 = a := UInt16.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] theorem UInt32.sub_zero (a : UInt32) : a - 0 = a := UInt32.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] theorem UInt64.sub_zero (a : UInt64) : a - 0 = a := UInt64.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] theorem USize.sub_zero (a : USize) : a - 0 = a := USize.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] protected theorem UInt8.sub_zero (a : UInt8) : a - 0 = a := UInt8.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] protected theorem UInt16.sub_zero (a : UInt16) : a - 0 = a := UInt16.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] protected theorem UInt32.sub_zero (a : UInt32) : a - 0 = a := UInt32.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] protected theorem UInt64.sub_zero (a : UInt64) : a - 0 = a := UInt64.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] protected theorem USize.sub_zero (a : USize) : a - 0 = a := USize.toBitVec_inj.1 (BitVec.sub_zero _)
@[simp] theorem UInt8.zero_sub (a : UInt8) : 0 - a = -a := UInt8.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] theorem UInt16.zero_sub (a : UInt16) : 0 - a = -a := UInt16.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] theorem UInt32.zero_sub (a : UInt32) : 0 - a = -a := UInt32.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] theorem UInt64.zero_sub (a : UInt64) : 0 - a = -a := UInt64.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] theorem USize.zero_sub (a : USize) : 0 - a = -a := USize.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] protected theorem UInt8.zero_sub (a : UInt8) : 0 - a = -a := UInt8.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] protected theorem UInt16.zero_sub (a : UInt16) : 0 - a = -a := UInt16.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] protected theorem UInt32.zero_sub (a : UInt32) : 0 - a = -a := UInt32.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] protected theorem UInt64.zero_sub (a : UInt64) : 0 - a = -a := UInt64.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] protected theorem USize.zero_sub (a : USize) : 0 - a = -a := USize.toBitVec_inj.1 (BitVec.zero_sub _)
@[simp] theorem UInt8.sub_self (a : UInt8) : a - a = 0 := UInt8.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] theorem UInt16.sub_self (a : UInt16) : a - a = 0 := UInt16.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] theorem UInt32.sub_self (a : UInt32) : a - a = 0 := UInt32.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] theorem UInt64.sub_self (a : UInt64) : a - a = 0 := UInt64.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] theorem USize.sub_self (a : USize) : a - a = 0 := USize.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] protected theorem UInt8.sub_self (a : UInt8) : a - a = 0 := UInt8.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] protected theorem UInt16.sub_self (a : UInt16) : a - a = 0 := UInt16.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] protected theorem UInt32.sub_self (a : UInt32) : a - a = 0 := UInt32.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] protected theorem UInt64.sub_self (a : UInt64) : a - a = 0 := UInt64.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] protected theorem USize.sub_self (a : USize) : a - a = 0 := USize.toBitVec_inj.1 (BitVec.sub_self _)
@[simp] theorem UInt8.neg_zero : -(0 : UInt8) = 0 := rfl
@[simp] theorem UInt16.neg_zero : -(0 : UInt16) = 0 := rfl
@[simp] theorem UInt32.neg_zero : -(0 : UInt32) = 0 := rfl
@[simp] theorem UInt64.neg_zero : -(0 : UInt64) = 0 := rfl
@[simp] theorem USize.neg_zero : -(0 : USize) = 0 := USize.toBitVec_inj.1 (BitVec.neg_zero _)
@[simp] protected theorem UInt8.neg_zero : -(0 : UInt8) = 0 := rfl
@[simp] protected theorem UInt16.neg_zero : -(0 : UInt16) = 0 := rfl
@[simp] protected theorem UInt32.neg_zero : -(0 : UInt32) = 0 := rfl
@[simp] protected theorem UInt64.neg_zero : -(0 : UInt64) = 0 := rfl
@[simp] protected theorem USize.neg_zero : -(0 : USize) = 0 := USize.toBitVec_inj.1 (BitVec.neg_zero _)
@[simp] theorem UInt8.sub_add_cancel (a b : UInt8) : a - b + b = a :=
@[simp] protected theorem UInt8.sub_add_cancel (a b : UInt8) : a - b + b = a :=
UInt8.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
@[simp] theorem UInt16.sub_add_cancel (a b : UInt16) : a - b + b = a :=
@[simp] protected theorem UInt16.sub_add_cancel (a b : UInt16) : a - b + b = a :=
UInt16.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
@[simp] theorem UInt32.sub_add_cancel (a b : UInt32) : a - b + b = a :=
@[simp] protected theorem UInt32.sub_add_cancel (a b : UInt32) : a - b + b = a :=
UInt32.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
@[simp] theorem UInt64.sub_add_cancel (a b : UInt64) : a - b + b = a :=
@[simp] protected theorem UInt64.sub_add_cancel (a b : UInt64) : a - b + b = a :=
UInt64.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
@[simp] theorem USize.sub_add_cancel (a b : USize) : a - b + b = a :=
@[simp] protected theorem USize.sub_add_cancel (a b : USize) : a - b + b = a :=
USize.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
theorem UInt8.eq_sub_iff_add_eq {a b c : UInt8} : a = c - b ↔ a + b = c := by
protected theorem UInt8.eq_sub_iff_add_eq {a b c : UInt8} : a = c - b ↔ a + b = c := by
simpa [← UInt8.toBitVec_inj] using BitVec.eq_sub_iff_add_eq
theorem UInt16.eq_sub_iff_add_eq {a b c : UInt16} : a = c - b ↔ a + b = c := by
protected theorem UInt16.eq_sub_iff_add_eq {a b c : UInt16} : a = c - b ↔ a + b = c := by
simpa [← UInt16.toBitVec_inj] using BitVec.eq_sub_iff_add_eq
theorem UInt32.eq_sub_iff_add_eq {a b c : UInt32} : a = c - b ↔ a + b = c := by
protected theorem UInt32.eq_sub_iff_add_eq {a b c : UInt32} : a = c - b ↔ a + b = c := by
simpa [← UInt32.toBitVec_inj] using BitVec.eq_sub_iff_add_eq
theorem UInt64.eq_sub_iff_add_eq {a b c : UInt64} : a = c - b ↔ a + b = c := by
protected theorem UInt64.eq_sub_iff_add_eq {a b c : UInt64} : a = c - b ↔ a + b = c := by
simpa [← UInt64.toBitVec_inj] using BitVec.eq_sub_iff_add_eq
theorem USize.eq_sub_iff_add_eq {a b c : USize} : a = c - b ↔ a + b = c := by
protected theorem USize.eq_sub_iff_add_eq {a b c : USize} : a = c - b ↔ a + b = c := by
simpa [← USize.toBitVec_inj] using BitVec.eq_sub_iff_add_eq
theorem UInt8.sub_eq_iff_eq_add {a b c : UInt8} : a - b = c ↔ a = c + b := by
protected theorem UInt8.sub_eq_iff_eq_add {a b c : UInt8} : a - b = c ↔ a = c + b := by
simpa [← UInt8.toBitVec_inj] using BitVec.sub_eq_iff_eq_add
theorem UInt16.sub_eq_iff_eq_add {a b c : UInt16} : a - b = c ↔ a = c + b := by
protected theorem UInt16.sub_eq_iff_eq_add {a b c : UInt16} : a - b = c ↔ a = c + b := by
simpa [← UInt16.toBitVec_inj] using BitVec.sub_eq_iff_eq_add
theorem UInt32.sub_eq_iff_eq_add {a b c : UInt32} : a - b = c ↔ a = c + b := by
protected theorem UInt32.sub_eq_iff_eq_add {a b c : UInt32} : a - b = c ↔ a = c + b := by
simpa [← UInt32.toBitVec_inj] using BitVec.sub_eq_iff_eq_add
theorem UInt64.sub_eq_iff_eq_add {a b c : UInt64} : a - b = c ↔ a = c + b := by
protected theorem UInt64.sub_eq_iff_eq_add {a b c : UInt64} : a - b = c ↔ a = c + b := by
simpa [← UInt64.toBitVec_inj] using BitVec.sub_eq_iff_eq_add
theorem USize.sub_eq_iff_eq_add {a b c : USize} : a - b = c ↔ a = c + b := by
protected theorem USize.sub_eq_iff_eq_add {a b c : USize} : a - b = c ↔ a = c + b := by
simpa [← USize.toBitVec_inj] using BitVec.sub_eq_iff_eq_add
@[simp] theorem UInt8.neg_neg {a : UInt8} : - -a = a := UInt8.toBitVec_inj.1 BitVec.neg_neg
@[simp] theorem UInt16.neg_neg {a : UInt16} : - -a = a := UInt16.toBitVec_inj.1 BitVec.neg_neg
@[simp] theorem UInt32.neg_neg {a : UInt32} : - -a = a := UInt32.toBitVec_inj.1 BitVec.neg_neg
@[simp] theorem UInt64.neg_neg {a : UInt64} : - -a = a := UInt64.toBitVec_inj.1 BitVec.neg_neg
@[simp] theorem USize.neg_neg {a : USize} : - -a = a := USize.toBitVec_inj.1 BitVec.neg_neg
@[simp] protected theorem UInt8.neg_neg {a : UInt8} : - -a = a := UInt8.toBitVec_inj.1 BitVec.neg_neg
@[simp] protected theorem UInt16.neg_neg {a : UInt16} : - -a = a := UInt16.toBitVec_inj.1 BitVec.neg_neg
@[simp] protected theorem UInt32.neg_neg {a : UInt32} : - -a = a := UInt32.toBitVec_inj.1 BitVec.neg_neg
@[simp] protected theorem UInt64.neg_neg {a : UInt64} : - -a = a := UInt64.toBitVec_inj.1 BitVec.neg_neg
@[simp] protected theorem USize.neg_neg {a : USize} : - -a = a := USize.toBitVec_inj.1 BitVec.neg_neg
@[simp] theorem UInt8.neg_inj {a b : UInt8} : -a = -b ↔ a = b := by simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.neg_inj {a b : UInt16} : -a = -b ↔ a = b := by simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.neg_inj {a b : UInt32} : -a = -b ↔ a = b := by simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.neg_inj {a b : UInt64} : -a = -b ↔ a = b := by simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.neg_inj {a b : USize} : -a = -b ↔ a = b := by simp [← USize.toBitVec_inj]
@[simp] protected theorem UInt8.neg_inj {a b : UInt8} : -a = -b ↔ a = b := by simp [← UInt8.toBitVec_inj]
@[simp] protected theorem UInt16.neg_inj {a b : UInt16} : -a = -b ↔ a = b := by simp [← UInt16.toBitVec_inj]
@[simp] protected theorem UInt32.neg_inj {a b : UInt32} : -a = -b ↔ a = b := by simp [← UInt32.toBitVec_inj]
@[simp] protected theorem UInt64.neg_inj {a b : UInt64} : -a = -b ↔ a = b := by simp [← UInt64.toBitVec_inj]
@[simp] protected theorem USize.neg_inj {a b : USize} : -a = -b ↔ a = b := by simp [← USize.toBitVec_inj]
@[simp] theorem UInt8.neg_ne_zero {a : UInt8} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.neg_ne_zero {a : UInt16} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.neg_ne_zero {a : UInt32} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.neg_ne_zero {a : UInt64} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.neg_ne_zero {a : USize} : -a ≠ 0 ↔ a ≠ 0 := by simp [← USize.toBitVec_inj]
@[simp] protected theorem UInt8.neg_ne_zero {a : UInt8} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt8.toBitVec_inj]
@[simp] protected theorem UInt16.neg_ne_zero {a : UInt16} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt16.toBitVec_inj]
@[simp] protected theorem UInt32.neg_ne_zero {a : UInt32} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt32.toBitVec_inj]
@[simp] protected theorem UInt64.neg_ne_zero {a : UInt64} : -a ≠ 0 ↔ a ≠ 0 := by simp [← UInt64.toBitVec_inj]
@[simp] protected theorem USize.neg_ne_zero {a : USize} : -a ≠ 0 ↔ a ≠ 0 := by simp [← USize.toBitVec_inj]
theorem UInt8.neg_add {a b : UInt8} : - (a + b) = -a - b := UInt8.toBitVec_inj.1 BitVec.neg_add
theorem UInt16.neg_add {a b : UInt16} : - (a + b) = -a - b := UInt16.toBitVec_inj.1 BitVec.neg_add
theorem UInt32.neg_add {a b : UInt32} : - (a + b) = -a - b := UInt32.toBitVec_inj.1 BitVec.neg_add
theorem UInt64.neg_add {a b : UInt64} : - (a + b) = -a - b := UInt64.toBitVec_inj.1 BitVec.neg_add
theorem USize.neg_add {a b : USize} : - (a + b) = -a - b := USize.toBitVec_inj.1 BitVec.neg_add
protected theorem UInt8.neg_add {a b : UInt8} : - (a + b) = -a - b := UInt8.toBitVec_inj.1 BitVec.neg_add
protected theorem UInt16.neg_add {a b : UInt16} : - (a + b) = -a - b := UInt16.toBitVec_inj.1 BitVec.neg_add
protected theorem UInt32.neg_add {a b : UInt32} : - (a + b) = -a - b := UInt32.toBitVec_inj.1 BitVec.neg_add
protected theorem UInt64.neg_add {a b : UInt64} : - (a + b) = -a - b := UInt64.toBitVec_inj.1 BitVec.neg_add
protected theorem USize.neg_add {a b : USize} : - (a + b) = -a - b := USize.toBitVec_inj.1 BitVec.neg_add
@[simp] theorem UInt8.sub_neg {a b : UInt8} : a - -b = a + b := UInt8.toBitVec_inj.1 BitVec.sub_neg
@[simp] theorem UInt16.sub_neg {a b : UInt16} : a - -b = a + b := UInt16.toBitVec_inj.1 BitVec.sub_neg
@[simp] theorem UInt32.sub_neg {a b : UInt32} : a - -b = a + b := UInt32.toBitVec_inj.1 BitVec.sub_neg
@[simp] theorem UInt64.sub_neg {a b : UInt64} : a - -b = a + b := UInt64.toBitVec_inj.1 BitVec.sub_neg
@[simp] theorem USize.sub_neg {a b : USize} : a - -b = a + b := USize.toBitVec_inj.1 BitVec.sub_neg
@[simp] protected theorem UInt8.sub_neg {a b : UInt8} : a - -b = a + b := UInt8.toBitVec_inj.1 BitVec.sub_neg
@[simp] protected theorem UInt16.sub_neg {a b : UInt16} : a - -b = a + b := UInt16.toBitVec_inj.1 BitVec.sub_neg
@[simp] protected theorem UInt32.sub_neg {a b : UInt32} : a - -b = a + b := UInt32.toBitVec_inj.1 BitVec.sub_neg
@[simp] protected theorem UInt64.sub_neg {a b : UInt64} : a - -b = a + b := UInt64.toBitVec_inj.1 BitVec.sub_neg
@[simp] protected theorem USize.sub_neg {a b : USize} : a - -b = a + b := USize.toBitVec_inj.1 BitVec.sub_neg
@[simp] theorem UInt8.neg_sub {a b : UInt8} : -(a - b) = b - a := by
rw [sub_eq_add_neg, neg_add, sub_neg, add_comm, ← sub_eq_add_neg]
@[simp] theorem UInt16.neg_sub {a b : UInt16} : -(a - b) = b - a := by
rw [sub_eq_add_neg, neg_add, sub_neg, add_comm, ← sub_eq_add_neg]
@[simp] theorem UInt32.neg_sub {a b : UInt32} : -(a - b) = b - a := by
rw [sub_eq_add_neg, neg_add, sub_neg, add_comm, ← sub_eq_add_neg]
@[simp] theorem UInt64.neg_sub {a b : UInt64} : -(a - b) = b - a := by
rw [sub_eq_add_neg, neg_add, sub_neg, add_comm, ← sub_eq_add_neg]
@[simp] theorem USize.neg_sub {a b : USize} : -(a - b) = b - a := by
rw [sub_eq_add_neg, neg_add, sub_neg, add_comm, ← sub_eq_add_neg]
@[simp] protected theorem UInt8.neg_sub {a b : UInt8} : -(a - b) = b - a := by
rw [UInt8.sub_eq_add_neg, UInt8.neg_add, UInt8.sub_neg, UInt8.add_comm, ← UInt8.sub_eq_add_neg]
@[simp] protected theorem UInt16.neg_sub {a b : UInt16} : -(a - b) = b - a := by
rw [UInt16.sub_eq_add_neg, UInt16.neg_add, UInt16.sub_neg, UInt16.add_comm, ← UInt16.sub_eq_add_neg]
@[simp] protected theorem UInt32.neg_sub {a b : UInt32} : -(a - b) = b - a := by
rw [UInt32.sub_eq_add_neg, UInt32.neg_add, UInt32.sub_neg, UInt32.add_comm, ← UInt32.sub_eq_add_neg]
@[simp] protected theorem UInt64.neg_sub {a b : UInt64} : -(a - b) = b - a := by
rw [UInt64.sub_eq_add_neg, UInt64.neg_add, UInt64.sub_neg, UInt64.add_comm, ← UInt64.sub_eq_add_neg]
@[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] theorem UInt8.add_left_inj {a b : UInt8} (c : UInt8) : (a + c = b + c) ↔ a = b := by
@[simp] protected theorem UInt8.add_left_inj {a b : UInt8} (c : UInt8) : (a + c = b + c) ↔ a = b := by
simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.add_left_inj {a b : UInt16} (c : UInt16) : (a + c = b + c) ↔ a = b := by
@[simp] protected theorem UInt16.add_left_inj {a b : UInt16} (c : UInt16) : (a + c = b + c) ↔ a = b := by
simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.add_left_inj {a b : UInt32} (c : UInt32) : (a + c = b + c) ↔ a = b := by
@[simp] protected theorem UInt32.add_left_inj {a b : UInt32} (c : UInt32) : (a + c = b + c) ↔ a = b := by
simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.add_left_inj {a b : UInt64} (c : UInt64) : (a + c = b + c) ↔ a = b := by
@[simp] protected theorem UInt64.add_left_inj {a b : UInt64} (c : UInt64) : (a + c = b + c) ↔ a = b := by
simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.add_left_inj {a b : USize} (c : USize) : (a + c = b + c) ↔ a = b := by
@[simp] protected theorem USize.add_left_inj {a b : USize} (c : USize) : (a + c = b + c) ↔ a = b := by
simp [← USize.toBitVec_inj]
@[simp] theorem UInt8.add_right_inj {a b : UInt8} (c : UInt8) : (c + a = c + b) ↔ a = b := by
@[simp] protected theorem UInt8.add_right_inj {a b : UInt8} (c : UInt8) : (c + a = c + b) ↔ a = b := by
simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.add_right_inj {a b : UInt16} (c : UInt16) : (c + a = c + b) ↔ a = b := by
@[simp] protected theorem UInt16.add_right_inj {a b : UInt16} (c : UInt16) : (c + a = c + b) ↔ a = b := by
simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.add_right_inj {a b : UInt32} (c : UInt32) : (c + a = c + b) ↔ a = b := by
@[simp] protected theorem UInt32.add_right_inj {a b : UInt32} (c : UInt32) : (c + a = c + b) ↔ a = b := by
simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.add_right_inj {a b : UInt64} (c : UInt64) : (c + a = c + b) ↔ a = b := by
@[simp] protected theorem UInt64.add_right_inj {a b : UInt64} (c : UInt64) : (c + a = c + b) ↔ a = b := by
simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.add_right_inj {a b : USize} (c : USize) : (c + a = c + b) ↔ a = b := by
@[simp] protected theorem USize.add_right_inj {a b : USize} (c : USize) : (c + a = c + b) ↔ a = b := by
simp [← USize.toBitVec_inj]
@[simp] theorem UInt8.sub_left_inj {a b : UInt8} (c : UInt8) : (a - c = b - c) ↔ a = b := by
@[simp] protected theorem UInt8.sub_left_inj {a b : UInt8} (c : UInt8) : (a - c = b - c) ↔ a = b := by
simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.sub_left_inj {a b : UInt16} (c : UInt16) : (a - c = b - c) ↔ a = b := by
@[simp] protected theorem UInt16.sub_left_inj {a b : UInt16} (c : UInt16) : (a - c = b - c) ↔ a = b := by
simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.sub_left_inj {a b : UInt32} (c : UInt32) : (a - c = b - c) ↔ a = b := by
@[simp] protected theorem UInt32.sub_left_inj {a b : UInt32} (c : UInt32) : (a - c = b - c) ↔ a = b := by
simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.sub_left_inj {a b : UInt64} (c : UInt64) : (a - c = b - c) ↔ a = b := by
@[simp] protected theorem UInt64.sub_left_inj {a b : UInt64} (c : UInt64) : (a - c = b - c) ↔ a = b := by
simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.sub_left_inj {a b : USize} (c : USize) : (a - c = b - c) ↔ a = b := by
@[simp] protected theorem USize.sub_left_inj {a b : USize} (c : USize) : (a - c = b - c) ↔ a = b := by
simp [← USize.toBitVec_inj]
@[simp] theorem UInt8.sub_right_inj {a b : UInt8} (c : UInt8) : (c - a = c - b) ↔ a = b := by
@[simp] protected theorem UInt8.sub_right_inj {a b : UInt8} (c : UInt8) : (c - a = c - b) ↔ a = b := by
simp [← UInt8.toBitVec_inj]
@[simp] theorem UInt16.sub_right_inj {a b : UInt16} (c : UInt16) : (c - a = c - b) ↔ a = b := by
@[simp] protected theorem UInt16.sub_right_inj {a b : UInt16} (c : UInt16) : (c - a = c - b) ↔ a = b := by
simp [← UInt16.toBitVec_inj]
@[simp] theorem UInt32.sub_right_inj {a b : UInt32} (c : UInt32) : (c - a = c - b) ↔ a = b := by
@[simp] protected theorem UInt32.sub_right_inj {a b : UInt32} (c : UInt32) : (c - a = c - b) ↔ a = b := by
simp [← UInt32.toBitVec_inj]
@[simp] theorem UInt64.sub_right_inj {a b : UInt64} (c : UInt64) : (c - a = c - b) ↔ a = b := by
@[simp] protected theorem UInt64.sub_right_inj {a b : UInt64} (c : UInt64) : (c - a = c - b) ↔ a = b := by
simp [← UInt64.toBitVec_inj]
@[simp] theorem USize.sub_right_inj {a b : USize} (c : USize) : (c - a = c - b) ↔ a = b := by
@[simp] protected theorem USize.sub_right_inj {a b : USize} (c : USize) : (c - a = c - b) ↔ a = b := by
simp [← USize.toBitVec_inj]
@[simp] theorem UInt8.add_eq_right {a b : UInt8} : a + b = b ↔ a = 0 := by
@ -2544,11 +2544,11 @@ theorem USize.neg_add {a b : USize} : - (a + b) = -a - b := USize.toBitVec_inj.1
@[simp] theorem USize.left_eq_add {a b : USize} : a = a + b ↔ b = 0 := by
simp [← USize.toBitVec_inj]
theorem UInt8.mul_comm (a b : UInt8) : a * b = b * a := UInt8.toBitVec_inj.1 (BitVec.mul_comm _ _)
theorem UInt16.mul_comm (a b : UInt16) : a * b = b * a := UInt16.toBitVec_inj.1 (BitVec.mul_comm _ _)
theorem UInt32.mul_comm (a b : UInt32) : a * b = b * a := UInt32.toBitVec_inj.1 (BitVec.mul_comm _ _)
theorem UInt64.mul_comm (a b : UInt64) : a * b = b * a := UInt64.toBitVec_inj.1 (BitVec.mul_comm _ _)
theorem USize.mul_comm (a b : USize) : a * b = b * a := USize.toBitVec_inj.1 (BitVec.mul_comm _ _)
protected theorem UInt8.mul_comm (a b : UInt8) : a * b = b * a := UInt8.toBitVec_inj.1 (BitVec.mul_comm _ _)
protected theorem UInt16.mul_comm (a b : UInt16) : a * b = b * a := UInt16.toBitVec_inj.1 (BitVec.mul_comm _ _)
protected theorem UInt32.mul_comm (a b : UInt32) : a * b = b * a := UInt32.toBitVec_inj.1 (BitVec.mul_comm _ _)
protected theorem UInt64.mul_comm (a b : UInt64) : a * b = b * a := UInt64.toBitVec_inj.1 (BitVec.mul_comm _ _)
protected theorem USize.mul_comm (a b : USize) : a * b = b * a := USize.toBitVec_inj.1 (BitVec.mul_comm _ _)
instance : Std.Commutative (α := UInt8) (· * ·) := ⟨UInt8.mul_comm⟩
instance : Std.Commutative (α := UInt16) (· * ·) := ⟨UInt16.mul_comm⟩
@ -2556,11 +2556,11 @@ instance : Std.Commutative (α := UInt32) (· * ·) := ⟨UInt32.mul_comm⟩
instance : Std.Commutative (α := UInt64) (· * ·) := ⟨UInt64.mul_comm⟩
instance : Std.Commutative (α := USize) (· * ·) := ⟨USize.mul_comm⟩
theorem UInt8.mul_assoc (a b c : UInt8) : a * b * c = a * (b * c) := UInt8.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
theorem UInt16.mul_assoc (a b c : UInt16) : a * b * c = a * (b * c) := UInt16.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
theorem UInt32.mul_assoc (a b c : UInt32) : a * b * c = a * (b * c) := UInt32.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
theorem UInt64.mul_assoc (a b c : UInt64) : a * b * c = a * (b * c) := UInt64.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
theorem USize.mul_assoc (a b c : USize) : a * b * c = a * (b * c) := USize.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
protected theorem UInt8.mul_assoc (a b c : UInt8) : a * b * c = a * (b * c) := UInt8.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
protected theorem UInt16.mul_assoc (a b c : UInt16) : a * b * c = a * (b * c) := UInt16.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
protected theorem UInt32.mul_assoc (a b c : UInt32) : a * b * c = a * (b * c) := UInt32.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
protected theorem UInt64.mul_assoc (a b c : UInt64) : a * b * c = a * (b * c) := UInt64.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
protected theorem USize.mul_assoc (a b c : USize) : a * b * c = a * (b * c) := USize.toBitVec_inj.1 (BitVec.mul_assoc _ _ _)
instance : Std.Associative (α := UInt8) (· * ·) := ⟨UInt8.mul_assoc⟩
instance : Std.Associative (α := UInt16) (· * ·) := ⟨UInt16.mul_assoc⟩
@ -2603,92 +2603,92 @@ instance : Std.LawfulCommIdentity (α := USize) (· * ·) 1 where
@[simp] theorem UInt64.zero_mul {a : UInt64} : 0 * a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_mul
@[simp] theorem USize.zero_mul {a : USize} : 0 * a = 0 := USize.toBitVec_inj.1 BitVec.zero_mul
theorem UInt8.mul_add {a b c : UInt8} : a * (b + c) = a * b + a * c :=
protected theorem UInt8.mul_add {a b c : UInt8} : a * (b + c) = a * b + a * c :=
UInt8.toBitVec_inj.1 BitVec.mul_add
theorem UInt16.mul_add {a b c : UInt16} : a * (b + c) = a * b + a * c :=
protected theorem UInt16.mul_add {a b c : UInt16} : a * (b + c) = a * b + a * c :=
UInt16.toBitVec_inj.1 BitVec.mul_add
theorem UInt32.mul_add {a b c : UInt32} : a * (b + c) = a * b + a * c :=
protected theorem UInt32.mul_add {a b c : UInt32} : a * (b + c) = a * b + a * c :=
UInt32.toBitVec_inj.1 BitVec.mul_add
theorem UInt64.mul_add {a b c : UInt64} : a * (b + c) = a * b + a * c :=
protected theorem UInt64.mul_add {a b c : UInt64} : a * (b + c) = a * b + a * c :=
UInt64.toBitVec_inj.1 BitVec.mul_add
theorem USize.mul_add {a b c : USize} : a * (b + c) = a * b + a * c :=
protected theorem USize.mul_add {a b c : USize} : a * (b + c) = a * b + a * c :=
USize.toBitVec_inj.1 BitVec.mul_add
theorem UInt8.add_mul {a b c : UInt8} : (a + b) * c = a * c + b * c := by
rw [mul_comm, mul_add, mul_comm a c, mul_comm c b]
theorem UInt16.add_mul {a b c : UInt16} : (a + b) * c = a * c + b * c := by
rw [mul_comm, mul_add, mul_comm a c, mul_comm c b]
theorem UInt32.add_mul {a b c : UInt32} : (a + b) * c = a * c + b * c := by
rw [mul_comm, mul_add, mul_comm a c, mul_comm c b]
theorem UInt64.add_mul {a b c : UInt64} : (a + b) * c = a * c + b * c := by
rw [mul_comm, mul_add, mul_comm a c, mul_comm c b]
theorem USize.add_mul {a b c : USize} : (a + b) * c = a * c + b * c := by
rw [mul_comm, mul_add, mul_comm a c, mul_comm c b]
protected theorem UInt8.add_mul {a b c : UInt8} : (a + b) * c = a * c + b * c := by
rw [UInt8.mul_comm, UInt8.mul_add, UInt8.mul_comm a c, UInt8.mul_comm c b]
protected theorem UInt16.add_mul {a b c : UInt16} : (a + b) * c = a * c + b * c := by
rw [UInt16.mul_comm, UInt16.mul_add, UInt16.mul_comm a c, UInt16.mul_comm c b]
protected theorem UInt32.add_mul {a b c : UInt32} : (a + b) * c = a * c + b * c := by
rw [UInt32.mul_comm, UInt32.mul_add, UInt32.mul_comm a c, UInt32.mul_comm c b]
protected theorem UInt64.add_mul {a b c : UInt64} : (a + b) * c = a * c + b * c := by
rw [UInt64.mul_comm, UInt64.mul_add, UInt64.mul_comm a c, UInt64.mul_comm c b]
protected theorem USize.add_mul {a b c : USize} : (a + b) * c = a * c + b * c := by
rw [USize.mul_comm, USize.mul_add, USize.mul_comm a c, USize.mul_comm c b]
theorem UInt8.mul_succ {a b : UInt8} : a * (b + 1) = a * b + a := by simp [mul_add]
theorem UInt16.mul_succ {a b : UInt16} : a * (b + 1) = a * b + a := by simp [mul_add]
theorem UInt32.mul_succ {a b : UInt32} : a * (b + 1) = a * b + a := by simp [mul_add]
theorem UInt64.mul_succ {a b : UInt64} : a * (b + 1) = a * b + a := by simp [mul_add]
theorem USize.mul_succ {a b : USize} : a * (b + 1) = a * b + a := by simp [mul_add]
protected theorem UInt8.mul_succ {a b : UInt8} : a * (b + 1) = a * b + a := by simp [UInt8.mul_add]
protected theorem UInt16.mul_succ {a b : UInt16} : a * (b + 1) = a * b + a := by simp [UInt16.mul_add]
protected theorem UInt32.mul_succ {a b : UInt32} : a * (b + 1) = a * b + a := by simp [UInt32.mul_add]
protected theorem UInt64.mul_succ {a b : UInt64} : a * (b + 1) = a * b + a := by simp [UInt64.mul_add]
protected theorem USize.mul_succ {a b : USize} : a * (b + 1) = a * b + a := by simp [USize.mul_add]
theorem UInt8.succ_mul {a b : UInt8} : (a + 1) * b = a * b + b := by simp [add_mul]
theorem UInt16.succ_mul {a b : UInt16} : (a + 1) * b = a * b + b := by simp [add_mul]
theorem UInt32.succ_mul {a b : UInt32} : (a + 1) * b = a * b + b := by simp [add_mul]
theorem UInt64.succ_mul {a b : UInt64} : (a + 1) * b = a * b + b := by simp [add_mul]
theorem USize.succ_mul {a b : USize} : (a + 1) * b = a * b + b := by simp [add_mul]
protected theorem UInt8.succ_mul {a b : UInt8} : (a + 1) * b = a * b + b := by simp [UInt8.add_mul]
protected theorem UInt16.succ_mul {a b : UInt16} : (a + 1) * b = a * b + b := by simp [UInt16.add_mul]
protected theorem UInt32.succ_mul {a b : UInt32} : (a + 1) * b = a * b + b := by simp [UInt32.add_mul]
protected theorem UInt64.succ_mul {a b : UInt64} : (a + 1) * b = a * b + b := by simp [UInt64.add_mul]
protected theorem USize.succ_mul {a b : USize} : (a + 1) * b = a * b + b := by simp [USize.add_mul]
theorem UInt8.two_mul {a : UInt8} : 2 * a = a + a := UInt8.toBitVec_inj.1 BitVec.two_mul
theorem UInt16.two_mul {a : UInt16} : 2 * a = a + a := UInt16.toBitVec_inj.1 BitVec.two_mul
theorem UInt32.two_mul {a : UInt32} : 2 * a = a + a := UInt32.toBitVec_inj.1 BitVec.two_mul
theorem UInt64.two_mul {a : UInt64} : 2 * a = a + a := UInt64.toBitVec_inj.1 BitVec.two_mul
theorem USize.two_mul {a : USize} : 2 * a = a + a := USize.toBitVec_inj.1 BitVec.two_mul
protected theorem UInt8.two_mul {a : UInt8} : 2 * a = a + a := UInt8.toBitVec_inj.1 BitVec.two_mul
protected theorem UInt16.two_mul {a : UInt16} : 2 * a = a + a := UInt16.toBitVec_inj.1 BitVec.two_mul
protected theorem UInt32.two_mul {a : UInt32} : 2 * a = a + a := UInt32.toBitVec_inj.1 BitVec.two_mul
protected theorem UInt64.two_mul {a : UInt64} : 2 * a = a + a := UInt64.toBitVec_inj.1 BitVec.two_mul
protected theorem USize.two_mul {a : USize} : 2 * a = a + a := USize.toBitVec_inj.1 BitVec.two_mul
theorem UInt8.mul_two {a : UInt8} : a * 2 = a + a := UInt8.toBitVec_inj.1 BitVec.mul_two
theorem UInt16.mul_two {a : UInt16} : a * 2 = a + a := UInt16.toBitVec_inj.1 BitVec.mul_two
theorem UInt32.mul_two {a : UInt32} : a * 2 = a + a := UInt32.toBitVec_inj.1 BitVec.mul_two
theorem UInt64.mul_two {a : UInt64} : a * 2 = a + a := UInt64.toBitVec_inj.1 BitVec.mul_two
theorem USize.mul_two {a : USize} : a * 2 = a + a := USize.toBitVec_inj.1 BitVec.mul_two
protected theorem UInt8.mul_two {a : UInt8} : a * 2 = a + a := UInt8.toBitVec_inj.1 BitVec.mul_two
protected theorem UInt16.mul_two {a : UInt16} : a * 2 = a + a := UInt16.toBitVec_inj.1 BitVec.mul_two
protected theorem UInt32.mul_two {a : UInt32} : a * 2 = a + a := UInt32.toBitVec_inj.1 BitVec.mul_two
protected theorem UInt64.mul_two {a : UInt64} : a * 2 = a + a := UInt64.toBitVec_inj.1 BitVec.mul_two
protected theorem USize.mul_two {a : USize} : a * 2 = a + a := USize.toBitVec_inj.1 BitVec.mul_two
theorem UInt8.neg_mul (a b : UInt8) : -a * b = -(a * b) := UInt8.toBitVec_inj.1 (BitVec.neg_mul _ _)
theorem UInt16.neg_mul (a b : UInt16) : -a * b = -(a * b) := UInt16.toBitVec_inj.1 (BitVec.neg_mul _ _)
theorem UInt32.neg_mul (a b : UInt32) : -a * b = -(a * b) := UInt32.toBitVec_inj.1 (BitVec.neg_mul _ _)
theorem UInt64.neg_mul (a b : UInt64) : -a * b = -(a * b) := UInt64.toBitVec_inj.1 (BitVec.neg_mul _ _)
theorem USize.neg_mul (a b : USize) : -a * b = -(a * b) := USize.toBitVec_inj.1 (BitVec.neg_mul _ _)
protected theorem UInt8.neg_mul (a b : UInt8) : -a * b = -(a * b) := UInt8.toBitVec_inj.1 (BitVec.neg_mul _ _)
protected theorem UInt16.neg_mul (a b : UInt16) : -a * b = -(a * b) := UInt16.toBitVec_inj.1 (BitVec.neg_mul _ _)
protected theorem UInt32.neg_mul (a b : UInt32) : -a * b = -(a * b) := UInt32.toBitVec_inj.1 (BitVec.neg_mul _ _)
protected theorem UInt64.neg_mul (a b : UInt64) : -a * b = -(a * b) := UInt64.toBitVec_inj.1 (BitVec.neg_mul _ _)
protected theorem USize.neg_mul (a b : USize) : -a * b = -(a * b) := USize.toBitVec_inj.1 (BitVec.neg_mul _ _)
theorem UInt8.mul_neg (a b : UInt8) : a * -b = -(a * b) := UInt8.toBitVec_inj.1 (BitVec.mul_neg _ _)
theorem UInt16.mul_neg (a b : UInt16) : a * -b = -(a * b) := UInt16.toBitVec_inj.1 (BitVec.mul_neg _ _)
theorem UInt32.mul_neg (a b : UInt32) : a * -b = -(a * b) := UInt32.toBitVec_inj.1 (BitVec.mul_neg _ _)
theorem UInt64.mul_neg (a b : UInt64) : a * -b = -(a * b) := UInt64.toBitVec_inj.1 (BitVec.mul_neg _ _)
theorem USize.mul_neg (a b : USize) : a * -b = -(a * b) := USize.toBitVec_inj.1 (BitVec.mul_neg _ _)
protected theorem UInt8.mul_neg (a b : UInt8) : a * -b = -(a * b) := UInt8.toBitVec_inj.1 (BitVec.mul_neg _ _)
protected theorem UInt16.mul_neg (a b : UInt16) : a * -b = -(a * b) := UInt16.toBitVec_inj.1 (BitVec.mul_neg _ _)
protected theorem UInt32.mul_neg (a b : UInt32) : a * -b = -(a * b) := UInt32.toBitVec_inj.1 (BitVec.mul_neg _ _)
protected theorem UInt64.mul_neg (a b : UInt64) : a * -b = -(a * b) := UInt64.toBitVec_inj.1 (BitVec.mul_neg _ _)
protected theorem USize.mul_neg (a b : USize) : a * -b = -(a * b) := USize.toBitVec_inj.1 (BitVec.mul_neg _ _)
theorem UInt8.neg_mul_neg (a b : UInt8) : -a * -b = a * b := UInt8.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
theorem UInt16.neg_mul_neg (a b : UInt16) : -a * -b = a * b := UInt16.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
theorem UInt32.neg_mul_neg (a b : UInt32) : -a * -b = a * b := UInt32.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
theorem UInt64.neg_mul_neg (a b : UInt64) : -a * -b = a * b := UInt64.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
theorem USize.neg_mul_neg (a b : USize) : -a * -b = a * b := USize.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
protected theorem UInt8.neg_mul_neg (a b : UInt8) : -a * -b = a * b := UInt8.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
protected theorem UInt16.neg_mul_neg (a b : UInt16) : -a * -b = a * b := UInt16.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
protected theorem UInt32.neg_mul_neg (a b : UInt32) : -a * -b = a * b := UInt32.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
protected theorem UInt64.neg_mul_neg (a b : UInt64) : -a * -b = a * b := UInt64.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
protected theorem USize.neg_mul_neg (a b : USize) : -a * -b = a * b := USize.toBitVec_inj.1 (BitVec.neg_mul_neg _ _)
theorem UInt8.neg_mul_comm (a b : UInt8) : -a * b = a * -b := UInt8.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
theorem UInt16.neg_mul_comm (a b : UInt16) : -a * b = a * -b := UInt16.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
theorem UInt32.neg_mul_comm (a b : UInt32) : -a * b = a * -b := UInt32.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
theorem UInt64.neg_mul_comm (a b : UInt64) : -a * b = a * -b := UInt64.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
theorem USize.neg_mul_comm (a b : USize) : -a * b = a * -b := USize.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
protected theorem UInt8.neg_mul_comm (a b : UInt8) : -a * b = a * -b := UInt8.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
protected theorem UInt16.neg_mul_comm (a b : UInt16) : -a * b = a * -b := UInt16.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
protected theorem UInt32.neg_mul_comm (a b : UInt32) : -a * b = a * -b := UInt32.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
protected theorem UInt64.neg_mul_comm (a b : UInt64) : -a * b = a * -b := UInt64.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
protected theorem USize.neg_mul_comm (a b : USize) : -a * b = a * -b := USize.toBitVec_inj.1 (BitVec.neg_mul_comm _ _)
theorem UInt8.mul_sub {a b c : UInt8} : a * (b - c) = a * b - a * c := UInt8.toBitVec_inj.1 BitVec.mul_sub
theorem UInt16.mul_sub {a b c : UInt16} : a * (b - c) = a * b - a * c := UInt16.toBitVec_inj.1 BitVec.mul_sub
theorem UInt32.mul_sub {a b c : UInt32} : a * (b - c) = a * b - a * c := UInt32.toBitVec_inj.1 BitVec.mul_sub
theorem UInt64.mul_sub {a b c : UInt64} : a * (b - c) = a * b - a * c := UInt64.toBitVec_inj.1 BitVec.mul_sub
theorem USize.mul_sub {a b c : USize} : a * (b - c) = a * b - a * c := USize.toBitVec_inj.1 BitVec.mul_sub
protected theorem UInt8.mul_sub {a b c : UInt8} : a * (b - c) = a * b - a * c := UInt8.toBitVec_inj.1 BitVec.mul_sub
protected theorem UInt16.mul_sub {a b c : UInt16} : a * (b - c) = a * b - a * c := UInt16.toBitVec_inj.1 BitVec.mul_sub
protected theorem UInt32.mul_sub {a b c : UInt32} : a * (b - c) = a * b - a * c := UInt32.toBitVec_inj.1 BitVec.mul_sub
protected theorem UInt64.mul_sub {a b c : UInt64} : a * (b - c) = a * b - a * c := UInt64.toBitVec_inj.1 BitVec.mul_sub
protected theorem USize.mul_sub {a b c : USize} : a * (b - c) = a * b - a * c := USize.toBitVec_inj.1 BitVec.mul_sub
theorem UInt8.sub_mul {a b c : UInt8} : (a - b) * c = a * c - b * c := by
rw [mul_comm, mul_sub, mul_comm, mul_comm c]
theorem UInt16.sub_mul {a b c : UInt16} : (a - b) * c = a * c - b * c := by
rw [mul_comm, mul_sub, mul_comm, mul_comm c]
theorem UInt32.sub_mul {a b c : UInt32} : (a - b) * c = a * c - b * c := by
rw [mul_comm, mul_sub, mul_comm, mul_comm c]
theorem UInt64.sub_mul {a b c : UInt64} : (a - b) * c = a * c - b * c := by
rw [mul_comm, mul_sub, mul_comm, mul_comm c]
theorem USize.sub_mul {a b c : USize} : (a - b) * c = a * c - b * c := by
rw [mul_comm, mul_sub, mul_comm, mul_comm c]
protected theorem UInt8.sub_mul {a b c : UInt8} : (a - b) * c = a * c - b * c := by
rw [UInt8.mul_comm, UInt8.mul_sub, UInt8.mul_comm, UInt8.mul_comm c]
protected theorem UInt16.sub_mul {a b c : UInt16} : (a - b) * c = a * c - b * c := by
rw [UInt16.mul_comm, UInt16.mul_sub, UInt16.mul_comm, UInt16.mul_comm c]
protected theorem UInt32.sub_mul {a b c : UInt32} : (a - b) * c = a * c - b * c := by
rw [UInt32.mul_comm, UInt32.mul_sub, UInt32.mul_comm, UInt32.mul_comm c]
protected theorem UInt64.sub_mul {a b c : UInt64} : (a - b) * c = a * c - b * c := by
rw [UInt64.mul_comm, UInt64.mul_sub, UInt64.mul_comm, UInt64.mul_comm c]
protected theorem USize.sub_mul {a b c : USize} : (a - b) * c = a * c - b * c := by
rw [USize.mul_comm, USize.mul_sub, USize.mul_comm, USize.mul_comm c]
theorem UInt8.neg_add_mul_eq_mul_not {a b : UInt8} : -(a + a * b) = a * ~~~b :=
UInt8.toBitVec_inj.1 BitVec.neg_add_mul_eq_mul_not
@ -2712,236 +2712,236 @@ theorem UInt64.neg_mul_not_eq_add_mul {a b : UInt64} : -(a * ~~~b) = a + a * b :
theorem USize.neg_mul_not_eq_add_mul {a b : USize} : -(a * ~~~b) = a + a * b :=
USize.toBitVec_inj.1 BitVec.neg_mul_not_eq_add_mul
theorem UInt8.le_of_lt {a b : UInt8} : a < b → a ≤ b := by
protected theorem UInt8.le_of_lt {a b : UInt8} : a < b → a ≤ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le] using Nat.le_of_lt
theorem UInt16.le_of_lt {a b : UInt16} : a < b → a ≤ b := by
protected theorem UInt16.le_of_lt {a b : UInt16} : a < b → a ≤ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le] using Nat.le_of_lt
theorem UInt32.le_of_lt {a b : UInt32} : a < b → a ≤ b := by
protected theorem UInt32.le_of_lt {a b : UInt32} : a < b → a ≤ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le] using Nat.le_of_lt
theorem UInt64.le_of_lt {a b : UInt64} : a < b → a ≤ b := by
protected theorem UInt64.le_of_lt {a b : UInt64} : a < b → a ≤ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le] using Nat.le_of_lt
theorem USize.le_of_lt {a b : USize} : a < b → a ≤ b := by
protected theorem USize.le_of_lt {a b : USize} : a < b → a ≤ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le] using Nat.le_of_lt
theorem UInt8.lt_of_le_of_ne {a b : UInt8} : a ≤ b → a ≠ b → a < b := by
protected theorem UInt8.lt_of_le_of_ne {a b : UInt8} : a ≤ b → a ≠ b → a < b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt8.toNat_inj] using Nat.lt_of_le_of_ne
theorem UInt16.lt_of_le_of_ne {a b : UInt16} : a ≤ b → a ≠ b → a < b := by
protected theorem UInt16.lt_of_le_of_ne {a b : UInt16} : a ≤ b → a ≠ b → a < b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt16.toNat_inj] using Nat.lt_of_le_of_ne
theorem UInt32.lt_of_le_of_ne {a b : UInt32} : a ≤ b → a ≠ b → a < b := by
protected theorem UInt32.lt_of_le_of_ne {a b : UInt32} : a ≤ b → a ≠ b → a < b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt32.toNat_inj] using Nat.lt_of_le_of_ne
theorem UInt64.lt_of_le_of_ne {a b : UInt64} : a ≤ b → a ≠ b → a < b := by
protected theorem UInt64.lt_of_le_of_ne {a b : UInt64} : a ≤ b → a ≠ b → a < b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt64.toNat_inj] using Nat.lt_of_le_of_ne
theorem USize.lt_of_le_of_ne {a b : USize} : a ≤ b → a ≠ b → a < b := by
protected theorem USize.lt_of_le_of_ne {a b : USize} : a ≤ b → a ≠ b → a < b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← USize.toNat_inj] using Nat.lt_of_le_of_ne
theorem UInt8.lt_iff_le_and_ne {a b : UInt8} : a < b ↔ a ≤ b ∧ a ≠ b := by
protected theorem UInt8.lt_iff_le_and_ne {a b : UInt8} : a < b ↔ a ≤ b ∧ a ≠ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt8.toNat_inj] using Nat.lt_iff_le_and_ne
theorem UInt16.lt_iff_le_and_ne {a b : UInt16} : a < b ↔ a ≤ b ∧ a ≠ b := by
protected theorem UInt16.lt_iff_le_and_ne {a b : UInt16} : a < b ↔ a ≤ b ∧ a ≠ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt16.toNat_inj] using Nat.lt_iff_le_and_ne
theorem UInt32.lt_iff_le_and_ne {a b : UInt32} : a < b ↔ a ≤ b ∧ a ≠ b := by
protected theorem UInt32.lt_iff_le_and_ne {a b : UInt32} : a < b ↔ a ≤ b ∧ a ≠ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt32.toNat_inj] using Nat.lt_iff_le_and_ne
theorem UInt64.lt_iff_le_and_ne {a b : UInt64} : a < b ↔ a ≤ b ∧ a ≠ b := by
protected theorem UInt64.lt_iff_le_and_ne {a b : UInt64} : a < b ↔ a ≤ b ∧ a ≠ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← UInt64.toNat_inj] using Nat.lt_iff_le_and_ne
theorem USize.lt_iff_le_and_ne {a b : USize} : a < b ↔ a ≤ b ∧ a ≠ b := by
protected theorem USize.lt_iff_le_and_ne {a b : USize} : a < b ↔ a ≤ b ∧ a ≠ b := by
simpa [lt_iff_toNat_lt, le_iff_toNat_le, ← USize.toNat_inj] using Nat.lt_iff_le_and_ne
@[simp] theorem UInt8.not_lt_zero {a : UInt8} : ¬a < 0 := by simp [UInt8.lt_iff_toBitVec_lt]
@[simp] theorem UInt16.not_lt_zero {a : UInt16} : ¬a < 0 := by simp [UInt16.lt_iff_toBitVec_lt]
@[simp] theorem UInt32.not_lt_zero {a : UInt32} : ¬a < 0 := by simp [UInt32.lt_iff_toBitVec_lt]
@[simp] theorem UInt64.not_lt_zero {a : UInt64} : ¬a < 0 := by simp [UInt64.lt_iff_toBitVec_lt]
@[simp] theorem USize.not_lt_zero {a : USize} : ¬a < 0 := by simp [USize.lt_iff_toBitVec_lt]
@[simp] protected theorem UInt8.not_lt_zero {a : UInt8} : ¬a < 0 := by simp [UInt8.lt_iff_toBitVec_lt]
@[simp] protected theorem UInt16.not_lt_zero {a : UInt16} : ¬a < 0 := by simp [UInt16.lt_iff_toBitVec_lt]
@[simp] protected theorem UInt32.not_lt_zero {a : UInt32} : ¬a < 0 := by simp [UInt32.lt_iff_toBitVec_lt]
@[simp] protected theorem UInt64.not_lt_zero {a : UInt64} : ¬a < 0 := by simp [UInt64.lt_iff_toBitVec_lt]
@[simp] protected theorem USize.not_lt_zero {a : USize} : ¬a < 0 := by simp [USize.lt_iff_toBitVec_lt]
@[simp] theorem UInt8.zero_le {a : UInt8} : 0 ≤ a := by simp [← UInt8.not_lt]
@[simp] theorem UInt16.zero_le {a : UInt16} : 0 ≤ a := by simp [← UInt16.not_lt]
@[simp] theorem UInt32.zero_le {a : UInt32} : 0 ≤ a := by simp [← UInt32.not_lt]
@[simp] theorem UInt64.zero_le {a : UInt64} : 0 ≤ a := by simp [← UInt64.not_lt]
@[simp] theorem USize.zero_le {a : USize} : 0 ≤ a := by simp [← USize.not_lt]
@[simp] protected theorem UInt8.zero_le {a : UInt8} : 0 ≤ a := by simp [← UInt8.not_lt]
@[simp] protected theorem UInt16.zero_le {a : UInt16} : 0 ≤ a := by simp [← UInt16.not_lt]
@[simp] protected theorem UInt32.zero_le {a : UInt32} : 0 ≤ a := by simp [← UInt32.not_lt]
@[simp] protected theorem UInt64.zero_le {a : UInt64} : 0 ≤ a := by simp [← UInt64.not_lt]
@[simp] protected theorem USize.zero_le {a : USize} : 0 ≤ a := by simp [← USize.not_lt]
@[simp] theorem UInt8.le_zero_iff {a : UInt8} : a ≤ 0 ↔ a = 0 := by
@[simp] protected theorem UInt8.le_zero_iff {a : UInt8} : a ≤ 0 ↔ a = 0 := by
simp [UInt8.le_iff_toBitVec_le, ← UInt8.toBitVec_inj]
@[simp] theorem UInt16.le_zero_iff {a : UInt16} : a ≤ 0 ↔ a = 0 := by
@[simp] protected theorem UInt16.le_zero_iff {a : UInt16} : a ≤ 0 ↔ a = 0 := by
simp [UInt16.le_iff_toBitVec_le, ← UInt16.toBitVec_inj]
@[simp] theorem UInt32.le_zero_iff {a : UInt32} : a ≤ 0 ↔ a = 0 := by
@[simp] protected theorem UInt32.le_zero_iff {a : UInt32} : a ≤ 0 ↔ a = 0 := by
simp [UInt32.le_iff_toBitVec_le, ← UInt32.toBitVec_inj]
@[simp] theorem UInt64.le_zero_iff {a : UInt64} : a ≤ 0 ↔ a = 0 := by
@[simp] protected theorem UInt64.le_zero_iff {a : UInt64} : a ≤ 0 ↔ a = 0 := by
simp [UInt64.le_iff_toBitVec_le, ← UInt64.toBitVec_inj]
@[simp] theorem USize.le_zero_iff {a : USize} : a ≤ 0 ↔ a = 0 := by
@[simp] protected theorem USize.le_zero_iff {a : USize} : a ≤ 0 ↔ a = 0 := by
simp [USize.le_iff_toBitVec_le, ← USize.toBitVec_inj]
@[simp] theorem UInt8.lt_one_iff {a : UInt8} : a < 1 ↔ a = 0 := by
@[simp] protected theorem UInt8.lt_one_iff {a : UInt8} : a < 1 ↔ a = 0 := by
simp [UInt8.lt_iff_toBitVec_lt, ← UInt8.toBitVec_inj]
@[simp] theorem UInt16.lt_one_iff {a : UInt16} : a < 1 ↔ a = 0 := by
@[simp] protected theorem UInt16.lt_one_iff {a : UInt16} : a < 1 ↔ a = 0 := by
simp [UInt16.lt_iff_toBitVec_lt, ← UInt16.toBitVec_inj]
@[simp] theorem UInt32.lt_one_iff {a : UInt32} : a < 1 ↔ a = 0 := by
@[simp] protected theorem UInt32.lt_one_iff {a : UInt32} : a < 1 ↔ a = 0 := by
simp [UInt32.lt_iff_toBitVec_lt, ← UInt32.toBitVec_inj]
@[simp] theorem UInt64.lt_one_iff {a : UInt64} : a < 1 ↔ a = 0 := by
@[simp] protected theorem UInt64.lt_one_iff {a : UInt64} : a < 1 ↔ a = 0 := by
simp [UInt64.lt_iff_toBitVec_lt, ← UInt64.toBitVec_inj]
@[simp] theorem USize.lt_one_iff {a : USize} : a < 1 ↔ a = 0 := by
@[simp] protected theorem USize.lt_one_iff {a : USize} : a < 1 ↔ a = 0 := by
simp [USize.lt_iff_toBitVec_lt, ← USize.toBitVec_inj]
@[simp] theorem UInt8.zero_div {a : UInt8} : 0 / a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_udiv
@[simp] theorem UInt16.zero_div {a : UInt16} : 0 / a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_udiv
@[simp] theorem UInt32.zero_div {a : UInt32} : 0 / a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_udiv
@[simp] theorem UInt64.zero_div {a : UInt64} : 0 / a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_udiv
@[simp] theorem USize.zero_div {a : USize} : 0 / a = 0 := USize.toBitVec_inj.1 BitVec.zero_udiv
@[simp] protected theorem UInt8.zero_div {a : UInt8} : 0 / a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_udiv
@[simp] protected theorem UInt16.zero_div {a : UInt16} : 0 / a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_udiv
@[simp] protected theorem UInt32.zero_div {a : UInt32} : 0 / a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_udiv
@[simp] protected theorem UInt64.zero_div {a : UInt64} : 0 / a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_udiv
@[simp] protected theorem USize.zero_div {a : USize} : 0 / a = 0 := USize.toBitVec_inj.1 BitVec.zero_udiv
@[simp] theorem UInt8.div_zero {a : UInt8} : a / 0 = 0 := UInt8.toBitVec_inj.1 BitVec.udiv_zero
@[simp] theorem UInt16.div_zero {a : UInt16} : a / 0 = 0 := UInt16.toBitVec_inj.1 BitVec.udiv_zero
@[simp] theorem UInt32.div_zero {a : UInt32} : a / 0 = 0 := UInt32.toBitVec_inj.1 BitVec.udiv_zero
@[simp] theorem UInt64.div_zero {a : UInt64} : a / 0 = 0 := UInt64.toBitVec_inj.1 BitVec.udiv_zero
@[simp] theorem USize.div_zero {a : USize} : a / 0 = 0 := USize.toBitVec_inj.1 BitVec.udiv_zero
@[simp] protected theorem UInt8.div_zero {a : UInt8} : a / 0 = 0 := UInt8.toBitVec_inj.1 BitVec.udiv_zero
@[simp] protected theorem UInt16.div_zero {a : UInt16} : a / 0 = 0 := UInt16.toBitVec_inj.1 BitVec.udiv_zero
@[simp] protected theorem UInt32.div_zero {a : UInt32} : a / 0 = 0 := UInt32.toBitVec_inj.1 BitVec.udiv_zero
@[simp] protected theorem UInt64.div_zero {a : UInt64} : a / 0 = 0 := UInt64.toBitVec_inj.1 BitVec.udiv_zero
@[simp] protected theorem USize.div_zero {a : USize} : a / 0 = 0 := USize.toBitVec_inj.1 BitVec.udiv_zero
@[simp] theorem UInt8.div_one {a : UInt8} : a / 1 = a := UInt8.toBitVec_inj.1 BitVec.udiv_one
@[simp] theorem UInt16.div_one {a : UInt16} : a / 1 = a := UInt16.toBitVec_inj.1 BitVec.udiv_one
@[simp] theorem UInt32.div_one {a : UInt32} : a / 1 = a := UInt32.toBitVec_inj.1 BitVec.udiv_one
@[simp] theorem UInt64.div_one {a : UInt64} : a / 1 = a := UInt64.toBitVec_inj.1 BitVec.udiv_one
@[simp] theorem USize.div_one {a : USize} : a / 1 = a := USize.toBitVec_inj.1 BitVec.udiv_one
@[simp] protected theorem UInt8.div_one {a : UInt8} : a / 1 = a := UInt8.toBitVec_inj.1 BitVec.udiv_one
@[simp] protected theorem UInt16.div_one {a : UInt16} : a / 1 = a := UInt16.toBitVec_inj.1 BitVec.udiv_one
@[simp] protected theorem UInt32.div_one {a : UInt32} : a / 1 = a := UInt32.toBitVec_inj.1 BitVec.udiv_one
@[simp] protected theorem UInt64.div_one {a : UInt64} : a / 1 = a := UInt64.toBitVec_inj.1 BitVec.udiv_one
@[simp] protected theorem USize.div_one {a : USize} : a / 1 = a := USize.toBitVec_inj.1 BitVec.udiv_one
theorem UInt8.div_self {a : UInt8} : a / a = if a = 0 then 0 else 1 := by
protected theorem UInt8.div_self {a : UInt8} : a / a = if a = 0 then 0 else 1 := by
simp [← UInt8.toBitVec_inj, apply_ite]
theorem UInt16.div_self {a : UInt16} : a / a = if a = 0 then 0 else 1 := by
protected theorem UInt16.div_self {a : UInt16} : a / a = if a = 0 then 0 else 1 := by
simp [← UInt16.toBitVec_inj, apply_ite]
theorem UInt32.div_self {a : UInt32} : a / a = if a = 0 then 0 else 1 := by
protected theorem UInt32.div_self {a : UInt32} : a / a = if a = 0 then 0 else 1 := by
simp [← UInt32.toBitVec_inj, apply_ite]
theorem UInt64.div_self {a : UInt64} : a / a = if a = 0 then 0 else 1 := by
protected theorem UInt64.div_self {a : UInt64} : a / a = if a = 0 then 0 else 1 := by
simp [← UInt64.toBitVec_inj, apply_ite]
theorem USize.div_self {a : USize} : a / a = if a = 0 then 0 else 1 := by
protected theorem USize.div_self {a : USize} : a / a = if a = 0 then 0 else 1 := by
simp [← USize.toNat_inj]
split
· simp_all
· simpa using Nat.div_self (by omega)
@[simp] theorem UInt8.mod_zero {a : UInt8} : a % 0 = a := UInt8.toBitVec_inj.1 BitVec.umod_zero
@[simp] theorem UInt16.mod_zero {a : UInt16} : a % 0 = a := UInt16.toBitVec_inj.1 BitVec.umod_zero
@[simp] theorem UInt32.mod_zero {a : UInt32} : a % 0 = a := UInt32.toBitVec_inj.1 BitVec.umod_zero
@[simp] theorem UInt64.mod_zero {a : UInt64} : a % 0 = a := UInt64.toBitVec_inj.1 BitVec.umod_zero
@[simp] theorem USize.mod_zero {a : USize} : a % 0 = a := USize.toBitVec_inj.1 BitVec.umod_zero
@[simp] protected theorem UInt8.mod_zero {a : UInt8} : a % 0 = a := UInt8.toBitVec_inj.1 BitVec.umod_zero
@[simp] protected theorem UInt16.mod_zero {a : UInt16} : a % 0 = a := UInt16.toBitVec_inj.1 BitVec.umod_zero
@[simp] protected theorem UInt32.mod_zero {a : UInt32} : a % 0 = a := UInt32.toBitVec_inj.1 BitVec.umod_zero
@[simp] protected theorem UInt64.mod_zero {a : UInt64} : a % 0 = a := UInt64.toBitVec_inj.1 BitVec.umod_zero
@[simp] protected theorem USize.mod_zero {a : USize} : a % 0 = a := USize.toBitVec_inj.1 BitVec.umod_zero
@[simp] theorem UInt8.zero_mod {a : UInt8} : 0 % a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_umod
@[simp] theorem UInt16.zero_mod {a : UInt16} : 0 % a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_umod
@[simp] theorem UInt32.zero_mod {a : UInt32} : 0 % a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_umod
@[simp] theorem UInt64.zero_mod {a : UInt64} : 0 % a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_umod
@[simp] theorem USize.zero_mod {a : USize} : 0 % a = 0 := USize.toBitVec_inj.1 BitVec.zero_umod
@[simp] protected theorem UInt8.zero_mod {a : UInt8} : 0 % a = 0 := UInt8.toBitVec_inj.1 BitVec.zero_umod
@[simp] protected theorem UInt16.zero_mod {a : UInt16} : 0 % a = 0 := UInt16.toBitVec_inj.1 BitVec.zero_umod
@[simp] protected theorem UInt32.zero_mod {a : UInt32} : 0 % a = 0 := UInt32.toBitVec_inj.1 BitVec.zero_umod
@[simp] protected theorem UInt64.zero_mod {a : UInt64} : 0 % a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_umod
@[simp] protected theorem USize.zero_mod {a : USize} : 0 % a = 0 := USize.toBitVec_inj.1 BitVec.zero_umod
@[simp] theorem UInt8.mod_one {a : UInt8} : a % 1 = 0 := UInt8.toBitVec_inj.1 BitVec.umod_one
@[simp] theorem UInt16.mod_one {a : UInt16} : a % 1 = 0 := UInt16.toBitVec_inj.1 BitVec.umod_one
@[simp] theorem UInt32.mod_one {a : UInt32} : a % 1 = 0 := UInt32.toBitVec_inj.1 BitVec.umod_one
@[simp] theorem UInt64.mod_one {a : UInt64} : a % 1 = 0 := UInt64.toBitVec_inj.1 BitVec.umod_one
@[simp] theorem USize.mod_one {a : USize} : a % 1 = 0 := USize.toBitVec_inj.1 BitVec.umod_one
@[simp] protected theorem UInt8.mod_one {a : UInt8} : a % 1 = 0 := UInt8.toBitVec_inj.1 BitVec.umod_one
@[simp] protected theorem UInt16.mod_one {a : UInt16} : a % 1 = 0 := UInt16.toBitVec_inj.1 BitVec.umod_one
@[simp] protected theorem UInt32.mod_one {a : UInt32} : a % 1 = 0 := UInt32.toBitVec_inj.1 BitVec.umod_one
@[simp] protected theorem UInt64.mod_one {a : UInt64} : a % 1 = 0 := UInt64.toBitVec_inj.1 BitVec.umod_one
@[simp] protected theorem USize.mod_one {a : USize} : a % 1 = 0 := USize.toBitVec_inj.1 BitVec.umod_one
@[simp] theorem UInt8.mod_self {a : UInt8} : a % a = 0 := UInt8.toBitVec_inj.1 BitVec.umod_self
@[simp] theorem UInt16.mod_self {a : UInt16} : a % a = 0 := UInt16.toBitVec_inj.1 BitVec.umod_self
@[simp] theorem UInt32.mod_self {a : UInt32} : a % a = 0 := UInt32.toBitVec_inj.1 BitVec.umod_self
@[simp] theorem UInt64.mod_self {a : UInt64} : a % a = 0 := UInt64.toBitVec_inj.1 BitVec.umod_self
@[simp] theorem USize.mod_self {a : USize} : a % a = 0 := USize.toBitVec_inj.1 BitVec.umod_self
@[simp] protected theorem UInt8.mod_self {a : UInt8} : a % a = 0 := UInt8.toBitVec_inj.1 BitVec.umod_self
@[simp] protected theorem UInt16.mod_self {a : UInt16} : a % a = 0 := UInt16.toBitVec_inj.1 BitVec.umod_self
@[simp] protected theorem UInt32.mod_self {a : UInt32} : a % a = 0 := UInt32.toBitVec_inj.1 BitVec.umod_self
@[simp] protected theorem UInt64.mod_self {a : UInt64} : a % a = 0 := UInt64.toBitVec_inj.1 BitVec.umod_self
@[simp] protected theorem USize.mod_self {a : USize} : a % a = 0 := USize.toBitVec_inj.1 BitVec.umod_self
theorem UInt8.pos_iff_ne_zero {a : UInt8} : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, Eq.comm]
theorem UInt16.pos_iff_ne_zero {a : UInt16} : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, Eq.comm]
theorem UInt32.pos_iff_ne_zero {a : UInt32} : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, Eq.comm]
theorem UInt64.pos_iff_ne_zero {a : UInt64} : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, Eq.comm]
theorem USize.pos_iff_ne_zero {a : USize} : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, Eq.comm]
protected theorem UInt8.pos_iff_ne_zero {a : UInt8} : 0 < a ↔ a ≠ 0 := by simp [UInt8.lt_iff_le_and_ne, Eq.comm]
protected theorem UInt16.pos_iff_ne_zero {a : UInt16} : 0 < a ↔ a ≠ 0 := by simp [UInt16.lt_iff_le_and_ne, Eq.comm]
protected theorem UInt32.pos_iff_ne_zero {a : UInt32} : 0 < a ↔ a ≠ 0 := by simp [UInt32.lt_iff_le_and_ne, Eq.comm]
protected theorem UInt64.pos_iff_ne_zero {a : UInt64} : 0 < a ↔ a ≠ 0 := by simp [UInt64.lt_iff_le_and_ne, Eq.comm]
protected theorem USize.pos_iff_ne_zero {a : USize} : 0 < a ↔ a ≠ 0 := by simp [USize.lt_iff_le_and_ne, Eq.comm]
theorem UInt8.lt_of_le_of_lt {a b c : UInt8} : a ≤ b → b < c → a < c := by
protected theorem UInt8.lt_of_le_of_lt {a b c : UInt8} : a ≤ b → b < c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_le_of_lt
theorem UInt16.lt_of_le_of_lt {a b c : UInt16} : a ≤ b → b < c → a < c := by
protected theorem UInt16.lt_of_le_of_lt {a b c : UInt16} : a ≤ b → b < c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_le_of_lt
theorem UInt32.lt_of_le_of_lt {a b c : UInt32} : a ≤ b → b < c → a < c := by
protected theorem UInt32.lt_of_le_of_lt {a b c : UInt32} : a ≤ b → b < c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_le_of_lt
theorem UInt64.lt_of_le_of_lt {a b c : UInt64} : a ≤ b → b < c → a < c := by
protected theorem UInt64.lt_of_le_of_lt {a b c : UInt64} : a ≤ b → b < c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_le_of_lt
theorem USize.lt_of_le_of_lt {a b c : USize} : a ≤ b → b < c → a < c := by
protected theorem USize.lt_of_le_of_lt {a b c : USize} : a ≤ b → b < c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_le_of_lt
theorem UInt8.lt_of_lt_of_le {a b c : UInt8} : a < b → b ≤ c → a < c := by
protected theorem UInt8.lt_of_lt_of_le {a b c : UInt8} : a < b → b ≤ c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_lt_of_le
theorem UInt16.lt_of_lt_of_le {a b c : UInt16} : a < b → b ≤ c → a < c := by
protected theorem UInt16.lt_of_lt_of_le {a b c : UInt16} : a < b → b ≤ c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_lt_of_le
theorem UInt32.lt_of_lt_of_le {a b c : UInt32} : a < b → b ≤ c → a < c := by
protected theorem UInt32.lt_of_lt_of_le {a b c : UInt32} : a < b → b ≤ c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_lt_of_le
theorem UInt64.lt_of_lt_of_le {a b c : UInt64} : a < b → b ≤ c → a < c := by
protected theorem UInt64.lt_of_lt_of_le {a b c : UInt64} : a < b → b ≤ c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_lt_of_le
theorem USize.lt_of_lt_of_le {a b c : USize} : a < b → b ≤ c → a < c := by
protected theorem USize.lt_of_lt_of_le {a b c : USize} : a < b → b ≤ c → a < c := by
simpa [le_iff_toNat_le, lt_iff_toNat_lt] using Nat.lt_of_lt_of_le
theorem UInt8.lt_or_lt_of_ne {a b : UInt8} : a ≠ b → a < b b < a := by
protected theorem UInt8.lt_or_lt_of_ne {a b : UInt8} : a ≠ b → a < b b < a := by
simpa [lt_iff_toNat_lt, ← UInt8.toNat_inj] using Nat.lt_or_lt_of_ne
theorem UInt16.lt_or_lt_of_ne {a b : UInt16} : a ≠ b → a < b b < a := by
protected theorem UInt16.lt_or_lt_of_ne {a b : UInt16} : a ≠ b → a < b b < a := by
simpa [lt_iff_toNat_lt, ← UInt16.toNat_inj] using Nat.lt_or_lt_of_ne
theorem UInt32.lt_or_lt_of_ne {a b : UInt32} : a ≠ b → a < b b < a := by
protected theorem UInt32.lt_or_lt_of_ne {a b : UInt32} : a ≠ b → a < b b < a := by
simpa [lt_iff_toNat_lt, ← UInt32.toNat_inj] using Nat.lt_or_lt_of_ne
theorem UInt64.lt_or_lt_of_ne {a b : UInt64} : a ≠ b → a < b b < a := by
protected theorem UInt64.lt_or_lt_of_ne {a b : UInt64} : a ≠ b → a < b b < a := by
simpa [lt_iff_toNat_lt, ← UInt64.toNat_inj] using Nat.lt_or_lt_of_ne
theorem USize.lt_or_lt_of_ne {a b : USize} : a ≠ b → a < b b < a := by
protected theorem USize.lt_or_lt_of_ne {a b : USize} : a ≠ b → a < b b < a := by
simpa [lt_iff_toNat_lt, ← USize.toNat_inj] using Nat.lt_or_lt_of_ne
theorem UInt8.lt_or_le (a b : UInt8) : a < b b ≤ a := by
protected theorem UInt8.lt_or_le (a b : UInt8) : a < b b ≤ a := by
simp [lt_iff_toNat_lt, le_iff_toNat_le]; omega
theorem UInt16.lt_or_le (a b : UInt16) : a < b b ≤ a := by
protected theorem UInt16.lt_or_le (a b : UInt16) : a < b b ≤ a := by
simp [lt_iff_toNat_lt, le_iff_toNat_le]; omega
theorem UInt32.lt_or_le (a b : UInt32) : a < b b ≤ a := by
protected theorem UInt32.lt_or_le (a b : UInt32) : a < b b ≤ a := by
simp [lt_iff_toNat_lt, le_iff_toNat_le]; omega
theorem UInt64.lt_or_le (a b : UInt64) : a < b b ≤ a := by
protected theorem UInt64.lt_or_le (a b : UInt64) : a < b b ≤ a := by
simp [lt_iff_toNat_lt, le_iff_toNat_le]; omega
theorem USize.lt_or_le (a b : USize) : a < b b ≤ a := by
protected theorem USize.lt_or_le (a b : USize) : a < b b ≤ a := by
simp [lt_iff_toNat_lt, le_iff_toNat_le]; omega
theorem UInt8.le_or_lt (a b : UInt8) : a ≤ b b < a := (b.lt_or_le a).symm
theorem UInt16.le_or_lt (a b : UInt16) : a ≤ b b < a := (b.lt_or_le a).symm
theorem UInt32.le_or_lt (a b : UInt32) : a ≤ b b < a := (b.lt_or_le a).symm
theorem UInt64.le_or_lt (a b : UInt64) : a ≤ b b < a := (b.lt_or_le a).symm
theorem USize.le_or_lt (a b : USize) : a ≤ b b < a := (b.lt_or_le a).symm
protected theorem UInt8.le_or_lt (a b : UInt8) : a ≤ b b < a := (b.lt_or_le a).symm
protected theorem UInt16.le_or_lt (a b : UInt16) : a ≤ b b < a := (b.lt_or_le a).symm
protected theorem UInt32.le_or_lt (a b : UInt32) : a ≤ b b < a := (b.lt_or_le a).symm
protected theorem UInt64.le_or_lt (a b : UInt64) : a ≤ b b < a := (b.lt_or_le a).symm
protected theorem USize.le_or_lt (a b : USize) : a ≤ b b < a := (b.lt_or_le a).symm
theorem UInt8.le_of_eq {a b : UInt8} : a = b → a ≤ b := (· ▸ UInt8.le_rfl)
theorem UInt16.le_of_eq {a b : UInt16} : a = b → a ≤ b := (· ▸ UInt16.le_rfl)
theorem UInt32.le_of_eq {a b : UInt32} : a = b → a ≤ b := (· ▸ UInt32.le_rfl)
theorem UInt64.le_of_eq {a b : UInt64} : a = b → a ≤ b := (· ▸ UInt64.le_rfl)
theorem USize.le_of_eq {a b : USize} : a = b → a ≤ b := (· ▸ USize.le_rfl)
protected theorem UInt8.le_of_eq {a b : UInt8} : a = b → a ≤ b := (· ▸ UInt8.le_rfl)
protected theorem UInt16.le_of_eq {a b : UInt16} : a = b → a ≤ b := (· ▸ UInt16.le_rfl)
protected theorem UInt32.le_of_eq {a b : UInt32} : a = b → a ≤ b := (· ▸ UInt32.le_rfl)
protected theorem UInt64.le_of_eq {a b : UInt64} : a = b → a ≤ b := (· ▸ UInt64.le_rfl)
protected theorem USize.le_of_eq {a b : USize} : a = b → a ≤ b := (· ▸ USize.le_rfl)
theorem UInt8.le_iff_lt_or_eq {a b : UInt8} : a ≤ b ↔ a < b a = b := by
protected theorem UInt8.le_iff_lt_or_eq {a b : UInt8} : a ≤ b ↔ a < b a = b := by
simpa [← UInt8.toNat_inj, le_iff_toNat_le, lt_iff_toNat_lt] using Nat.le_iff_lt_or_eq
theorem UInt16.le_iff_lt_or_eq {a b : UInt16} : a ≤ b ↔ a < b a = b := by
protected theorem UInt16.le_iff_lt_or_eq {a b : UInt16} : a ≤ b ↔ a < b a = b := by
simpa [← UInt16.toNat_inj, le_iff_toNat_le, lt_iff_toNat_lt] using Nat.le_iff_lt_or_eq
theorem UInt32.le_iff_lt_or_eq {a b : UInt32} : a ≤ b ↔ a < b a = b := by
protected theorem UInt32.le_iff_lt_or_eq {a b : UInt32} : a ≤ b ↔ a < b a = b := by
simpa [← UInt32.toNat_inj, le_iff_toNat_le, lt_iff_toNat_lt] using Nat.le_iff_lt_or_eq
theorem UInt64.le_iff_lt_or_eq {a b : UInt64} : a ≤ b ↔ a < b a = b := by
protected theorem UInt64.le_iff_lt_or_eq {a b : UInt64} : a ≤ b ↔ a < b a = b := by
simpa [← UInt64.toNat_inj, le_iff_toNat_le, lt_iff_toNat_lt] using Nat.le_iff_lt_or_eq
theorem USize.le_iff_lt_or_eq {a b : USize} : a ≤ b ↔ a < b a = b := by
protected theorem USize.le_iff_lt_or_eq {a b : USize} : a ≤ b ↔ a < b a = b := by
simpa [← USize.toNat_inj, le_iff_toNat_le, lt_iff_toNat_lt] using Nat.le_iff_lt_or_eq
theorem UInt8.lt_or_eq_of_le {a b : UInt8} : a ≤ b → a < b a = b := UInt8.le_iff_lt_or_eq.mp
theorem UInt16.lt_or_eq_of_le {a b : UInt16} : a ≤ b → a < b a = b := UInt16.le_iff_lt_or_eq.mp
theorem UInt32.lt_or_eq_of_le {a b : UInt32} : a ≤ b → a < b a = b := UInt32.le_iff_lt_or_eq.mp
theorem UInt64.lt_or_eq_of_le {a b : UInt64} : a ≤ b → a < b a = b := UInt64.le_iff_lt_or_eq.mp
theorem USize.lt_or_eq_of_le {a b : USize} : a ≤ b → a < b a = b := USize.le_iff_lt_or_eq.mp
protected theorem UInt8.lt_or_eq_of_le {a b : UInt8} : a ≤ b → a < b a = b := UInt8.le_iff_lt_or_eq.mp
protected theorem UInt16.lt_or_eq_of_le {a b : UInt16} : a ≤ b → a < b a = b := UInt16.le_iff_lt_or_eq.mp
protected theorem UInt32.lt_or_eq_of_le {a b : UInt32} : a ≤ b → a < b a = b := UInt32.le_iff_lt_or_eq.mp
protected theorem UInt64.lt_or_eq_of_le {a b : UInt64} : a ≤ b → a < b a = b := UInt64.le_iff_lt_or_eq.mp
protected theorem USize.lt_or_eq_of_le {a b : USize} : a ≤ b → a < b a = b := USize.le_iff_lt_or_eq.mp
theorem UInt8.sub_le {a b : UInt8} (hab : b ≤ a) : a - b ≤ a := by
protected theorem UInt8.sub_le {a b : UInt8} (hab : b ≤ a) : a - b ≤ a := by
simp [le_iff_toNat_le, UInt8.toNat_sub_of_le _ _ hab]
theorem UInt16.sub_le {a b : UInt16} (hab : b ≤ a) : a - b ≤ a := by
protected theorem UInt16.sub_le {a b : UInt16} (hab : b ≤ a) : a - b ≤ a := by
simp [le_iff_toNat_le, UInt16.toNat_sub_of_le _ _ hab]
theorem UInt32.sub_le {a b : UInt32} (hab : b ≤ a) : a - b ≤ a := by
protected theorem UInt32.sub_le {a b : UInt32} (hab : b ≤ a) : a - b ≤ a := by
simp [le_iff_toNat_le, UInt32.toNat_sub_of_le _ _ hab]
theorem UInt64.sub_le {a b : UInt64} (hab : b ≤ a) : a - b ≤ a := by
protected theorem UInt64.sub_le {a b : UInt64} (hab : b ≤ a) : a - b ≤ a := by
simp [le_iff_toNat_le, UInt64.toNat_sub_of_le _ _ hab]
theorem USize.sub_le {a b : USize} (hab : b ≤ a) : a - b ≤ a := by
protected theorem USize.sub_le {a b : USize} (hab : b ≤ a) : a - b ≤ a := by
simp [le_iff_toNat_le, USize.toNat_sub_of_le _ _ hab]
theorem UInt8.sub_lt {a b : UInt8} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
protected theorem UInt8.sub_lt {a b : UInt8} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
rw [lt_iff_toNat_lt, UInt8.toNat_sub_of_le _ _ hab]
refine Nat.sub_lt ?_ (UInt8.lt_iff_toNat_lt.1 hb)
exact UInt8.lt_iff_toNat_lt.1 (UInt8.lt_of_lt_of_le hb hab)
theorem UInt16.sub_lt {a b : UInt16} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
protected theorem UInt16.sub_lt {a b : UInt16} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
rw [lt_iff_toNat_lt, UInt16.toNat_sub_of_le _ _ hab]
refine Nat.sub_lt ?_ (UInt16.lt_iff_toNat_lt.1 hb)
exact UInt16.lt_iff_toNat_lt.1 (UInt16.lt_of_lt_of_le hb hab)
theorem UInt32.sub_lt {a b : UInt32} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
protected theorem UInt32.sub_lt {a b : UInt32} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
rw [lt_iff_toNat_lt, UInt32.toNat_sub_of_le _ _ hab]
refine Nat.sub_lt ?_ (UInt32.lt_iff_toNat_lt.1 hb)
exact UInt32.lt_iff_toNat_lt.1 (UInt32.lt_of_lt_of_le hb hab)
theorem UInt64.sub_lt {a b : UInt64} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
protected theorem UInt64.sub_lt {a b : UInt64} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
rw [lt_iff_toNat_lt, UInt64.toNat_sub_of_le _ _ hab]
refine Nat.sub_lt ?_ (UInt64.lt_iff_toNat_lt.1 hb)
exact UInt64.lt_iff_toNat_lt.1 (UInt64.lt_of_lt_of_le hb hab)
theorem USize.sub_lt {a b : USize} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
protected theorem USize.sub_lt {a b : USize} (hb : 0 < b) (hab : b ≤ a) : a - b < a := by
rw [lt_iff_toNat_lt, USize.toNat_sub_of_le _ _ hab]
refine Nat.sub_lt ?_ (USize.lt_iff_toNat_lt.1 hb)
exact USize.lt_iff_toNat_lt.1 (USize.lt_of_lt_of_le hb hab)