Adds Mathlib specific instances to the UIntX data types.

The CommRing instances (and the NatCast and IntCast instances from which they is built) are scoped in the UIntX.CommRing namespace, rather than available globally. As a result, the ring tactic will not work on UIntX types without open scoped UIntX.Ring.

This is because the presence of these casting operations contradicts assumptions made by the expression tree elaborator, namely that coercions do not form a cycle.

The UInt version also interferes more with software-verification use-cases, which is reason to be more cautious here.

@[simp]

theorem UInt32.toBitVec_intCast (z : ℤ) : (↑z).toBitVec = ↑z

@[simp]

theorem UInt64.toBitVec_natCast (n : ℕ) : (↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_zsmul (z : ℤ) (a : USize) : (z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt32.toBitVec_zsmul (z : ℤ) (a : UInt32) : (z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt64.toBitVec_zsmul (z : ℤ) (a : UInt64) : (z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt32.toBitVec_natCast (n : ℕ) : (↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_natCast (n : ℕ) : (↑n).toBitVec = ↑n

theorem UInt32.toBitVec_nsmul (n : ℕ) (a : UInt32) : (n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt16.toBitVec_zsmul (z : ℤ) (a : UInt16) : (z • a).toBitVec = z • a.toBitVec

theorem UInt64.toBitVec_nsmul (n : ℕ) (a : UInt64) : (n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt8.toBitVec_zsmul (z : ℤ) (a : UInt8) : (z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt8.toBitVec_intCast (z : ℤ) : (↑z).toBitVec = ↑z

@[simp]

theorem UInt16.toBitVec_natCast (n : ℕ) : (↑n).toBitVec = ↑n

theorem USize.toBitVec_nsmul (n : ℕ) (a : USize) : (n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt64.toBitVec_intCast (z : ℤ) : (↑z).toBitVec = ↑z

theorem UInt8.toBitVec_nsmul (n : ℕ) (a : UInt8) : (n • a).toBitVec = n • a.toBitVec

theorem UInt16.toBitVec_nsmul (n : ℕ) (a : UInt16) : (n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt16.toBitVec_intCast (z : ℤ) : (↑z).toBitVec = ↑z

@[simp]

theorem UInt8.toBitVec_natCast (n : ℕ) : (↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_intCast (z : ℤ) : (↑z).toBitVec = ↑z

instance UInt32.instNonUnitalCommRing : NonUnitalCommRing UInt32

Equations

• UInt32.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing UInt32.toBitVec UInt32.toBitVec_injective UInt32.toBitVec_zero ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem UInt8.toFin_injective : Function.Injective toFin

def USize.instCommRing : CommRing USize

To use this instance, use open scoped USize.CommRing.

See the module docstring for an explanation

Equations

• USize.instCommRing = Function.Injective.commRing USize.toBitVec USize.toBitVec_injective USize.toBitVec_zero USize.toBitVec_one ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ USize.toBitVec_natCast USize.toBitVec_intCast

instance UInt8.instCommMonoid : CommMonoid UInt8

Equations

• UInt8.instCommMonoid = Function.Injective.commMonoid UInt8.toBitVec UInt8.toBitVec_injective UInt8.toBitVec_one ⋯ ⋯

instance USize.instNonUnitalCommRing : NonUnitalCommRing USize

Equations

• USize.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing USize.toBitVec USize.toBitVec_injective USize.toBitVec_zero ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem UInt32.toFin_injective : Function.Injective toFin

instance UInt64.instNonUnitalCommRing : NonUnitalCommRing UInt64

Equations

• UInt64.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing UInt64.toBitVec UInt64.toBitVec_injective UInt64.toBitVec_zero ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance UInt64.instCommMonoid : CommMonoid UInt64

Equations

• UInt64.instCommMonoid = Function.Injective.commMonoid UInt64.toBitVec UInt64.toBitVec_injective UInt64.toBitVec_one ⋯ ⋯

instance USize.instCommMonoid : CommMonoid USize

Equations

• USize.instCommMonoid = Function.Injective.commMonoid USize.toBitVec USize.toBitVec_injective USize.toBitVec_one ⋯ ⋯

theorem USize.toBitVec_injective : Function.Injective toBitVec

instance UInt16.instCommMonoid : CommMonoid UInt16

Equations

• UInt16.instCommMonoid = Function.Injective.commMonoid UInt16.toBitVec UInt16.toBitVec_injective UInt16.toBitVec_one ⋯ ⋯

def UInt32.instCommRing : CommRing UInt32

To use this instance, use open scoped UInt32.CommRing.

See the module docstring for an explanation

Equations

• One or more equations did not get rendered due to their size.

def UInt64.instCommRing : CommRing UInt64

To use this instance, use open scoped UInt64.CommRing.

See the module docstring for an explanation

Equations

• One or more equations did not get rendered due to their size.

instance UInt16.instNonUnitalCommRing : NonUnitalCommRing UInt16

Equations

• UInt16.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing UInt16.toBitVec UInt16.toBitVec_injective UInt16.toBitVec_zero ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def UInt8.instCommRing : CommRing UInt8

To use this instance, use open scoped UInt8.CommRing.

See the module docstring for an explanation

Equations

• UInt8.instCommRing = Function.Injective.commRing UInt8.toBitVec UInt8.toBitVec_injective UInt8.toBitVec_zero UInt8.toBitVec_one ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ UInt8.toBitVec_natCast UInt8.toBitVec_intCast

theorem UInt8.toBitVec_injective : Function.Injective toBitVec

instance UInt32.instCommMonoid : CommMonoid UInt32

Equations

• UInt32.instCommMonoid = Function.Injective.commMonoid UInt32.toBitVec UInt32.toBitVec_injective UInt32.toBitVec_one ⋯ ⋯

theorem USize.toFin_injective : Function.Injective toFin

def UInt16.instCommRing : CommRing UInt16

To use this instance, use open scoped UInt16.CommRing.

See the module docstring for an explanation

Equations

• One or more equations did not get rendered due to their size.

theorem UInt32.toBitVec_injective : Function.Injective toBitVec

theorem UInt16.toFin_injective : Function.Injective toFin

theorem UInt16.toBitVec_injective : Function.Injective toBitVec

instance UInt8.instNonUnitalCommRing : NonUnitalCommRing UInt8

Equations

• UInt8.instNonUnitalCommRing = Function.Injective.nonUnitalCommRing UInt8.toBitVec UInt8.toBitVec_injective UInt8.toBitVec_zero ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem UInt64.toFin_injective : Function.Injective toFin

theorem UInt64.toBitVec_injective : Function.Injective toBitVec

def UInt8.isASCIIUpper (c : UInt8) : Bool

Is this an uppercase ASCII letter?

Equations

• c.isASCIIUpper = (decide (c ≥ 65) && decide (c ≤ 90))

def UInt8.isASCIILower (c : UInt8) : Bool

Is this a lowercase ASCII letter?

Equations

• c.isASCIILower = (decide (c ≥ 97) && decide (c ≤ 122))

def UInt8.isASCIIAlpha (c : UInt8) : Bool

Is this an alphabetic ASCII character?

Equations

• c.isASCIIAlpha = (c.isASCIIUpper || c.isASCIILower)

def UInt8.isASCIIDigit (c : UInt8) : Bool

Is this an ASCII digit character?

Equations

• c.isASCIIDigit = (decide (c ≥ 48) && decide (c ≤ 57))

def UInt8.isASCIIAlphanum (c : UInt8) : Bool

Is this an alphanumeric ASCII character?

Equations

• c.isASCIIAlphanum = (c.isASCIIAlpha || c.isASCIIDigit)

def UInt8.toChar (n : UInt8) : Char

The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.

Equations

• n.toChar = { val := n.toUInt32, valid := ⋯ }