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.

instance USize.instSMulNat : SMul ℕ USize

Equations

• USize.instSMulNat = { smul := fun (n : ℕ) (a : USize) => { toBitVec := { toFin := n • a.val } } }

theorem UInt64.zsmul_def (z : ℤ) (a : UInt64) : z • a = { toBitVec := { toFin := z • a.val } }

theorem UInt64.natCast_def (n : ℕ) : ↑n = { toBitVec := ↑n }

instance UInt32.instNonUnitalCommRing : NonUnitalCommRing UInt32

Equations

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

theorem UInt32.pow_def (a : UInt32) (n : ℕ) : a ^ n = { toBitVec := { toFin := a.val ^ n } }

instance UInt16.instPowNat_mathlib : Pow UInt16 ℕ

Equations

• UInt16.instPowNat_mathlib = { pow := fun (a : UInt16) (n : ℕ) => { toBitVec := { toFin := a.val ^ n } } }

theorem USize.toBitVec_injective : Function.Injective toBitVec

theorem USize.nsmul_def (n : ℕ) (a : USize) : n • a = { toBitVec := { toFin := n • a.val } }

def UInt32.instNatCast : NatCast UInt32

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

See the module docstring for an explanation

Equations

• UInt32.instNatCast = { natCast := fun (n : ℕ) => { toBitVec := ↑n } }

instance UInt16.instCommMonoid : CommMonoid UInt16

Equations

• UInt16.instCommMonoid = Function.Injective.commMonoid UInt16.toBitVec UInt16.toBitVec_injective UInt16.instCommMonoid.proof_1 UInt16.instCommMonoid.proof_2 UInt16.instCommMonoid.proof_3

theorem UInt16.pow_def (a : UInt16) (n : ℕ) : a ^ n = { toBitVec := { toFin := a.val ^ n } }

instance UInt64.instPowNat_mathlib : Pow UInt64 ℕ

Equations

• UInt64.instPowNat_mathlib = { pow := fun (a : UInt64) (n : ℕ) => { toBitVec := { toFin := a.val ^ n } } }

theorem UInt8.pow_def (a : UInt8) (n : ℕ) : a ^ n = { toBitVec := { toFin := a.val ^ n } }

instance UInt32.instNeg_mathlib : Neg UInt32

Equations

• UInt32.instNeg_mathlib = { neg := fun (a : UInt32) => { toBitVec := { toFin := -a.val } } }

instance UInt64.instNeg_mathlib : Neg UInt64

Equations

• UInt64.instNeg_mathlib = { neg := fun (a : UInt64) => { toBitVec := { toFin := -a.val } } }

theorem UInt16.val_injective : Function.Injective val

instance UInt32.instCommMonoid : CommMonoid UInt32

Equations

• UInt32.instCommMonoid = Function.Injective.commMonoid UInt32.toBitVec UInt32.toBitVec_injective UInt32.instCommMonoid.proof_1 UInt32.instCommMonoid.proof_2 UInt32.instCommMonoid.proof_3

theorem UInt16.toBitVec_injective : Function.Injective toBitVec

theorem UInt64.toBitVec_injective : Function.Injective toBitVec

theorem UInt16.zsmul_def (z : ℤ) (a : UInt16) : z • a = { toBitVec := { toFin := z • a.val } }

def UInt32.instIntCast : IntCast UInt32

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

See the module docstring for an explanation

Equations

• UInt32.instIntCast = { intCast := fun (z : ℤ) => { toBitVec := ↑z } }

instance UInt8.instCommMonoid : CommMonoid UInt8

Equations

• UInt8.instCommMonoid = Function.Injective.commMonoid UInt8.toBitVec UInt8.toBitVec_injective UInt8.instCommMonoid.proof_1 UInt8.instCommMonoid.proof_2 UInt8.instCommMonoid.proof_3

instance UInt32.instSMulNat : SMul ℕ UInt32

Equations

• UInt32.instSMulNat = { smul := fun (n : ℕ) (a : UInt32) => { toBitVec := { toFin := n • a.val } } }

instance UInt32.instPowNat_mathlib : Pow UInt32 ℕ

Equations

• UInt32.instPowNat_mathlib = { pow := fun (a : UInt32) (n : ℕ) => { toBitVec := { toFin := a.val ^ n } } }

instance USize.instPowNat_mathlib : Pow USize ℕ

Equations

• USize.instPowNat_mathlib = { pow := fun (a : USize) (n : ℕ) => { toBitVec := { toFin := a.val ^ n } } }

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 UInt64.instSMulNat : SMul ℕ UInt64

Equations

• UInt64.instSMulNat = { smul := fun (n : ℕ) (a : UInt64) => { toBitVec := { toFin := n • a.val } } }

theorem USize.intCast_def (z : ℤ) : ↑z = { toBitVec := ↑z }

instance UInt16.instNeg_mathlib : Neg UInt16

Equations

• UInt16.instNeg_mathlib = { neg := fun (a : UInt16) => { toBitVec := { toFin := -a.val } } }

instance UInt16.instSMulInt : SMul ℤ UInt16

Equations

• UInt16.instSMulInt = { smul := fun (z : ℤ) (a : UInt16) => { toBitVec := { toFin := z • a.val } } }

def UInt16.instNatCast : NatCast UInt16

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

See the module docstring for an explanation

Equations

• UInt16.instNatCast = { natCast := fun (n : ℕ) => { toBitVec := ↑n } }

def UInt64.instIntCast : IntCast UInt64

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

See the module docstring for an explanation

Equations

• UInt64.instIntCast = { intCast := fun (z : ℤ) => { toBitVec := ↑z } }

theorem UInt16.intCast_def (z : ℤ) : ↑z = { toBitVec := ↑z }

theorem UInt64.intCast_def (z : ℤ) : ↑z = { toBitVec := ↑z }

theorem UInt32.toBitVec_injective : Function.Injective toBitVec

theorem UInt64.neg_def (a : UInt64) : -a = { toBitVec := { toFin := -a.val } }

theorem UInt32.neg_def (a : UInt32) : -a = { toBitVec := { toFin := -a.val } }

instance UInt8.instNonUnitalCommRing : NonUnitalCommRing UInt8

Equations

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

theorem UInt16.nsmul_def (n : ℕ) (a : UInt16) : n • a = { toBitVec := { toFin := n • a.val } }

def UInt8.instIntCast : IntCast UInt8

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

See the module docstring for an explanation

Equations

• UInt8.instIntCast = { intCast := fun (z : ℤ) => { toBitVec := ↑z } }

instance UInt16.instSMulNat : SMul ℕ UInt16

Equations

• UInt16.instSMulNat = { smul := fun (n : ℕ) (a : UInt16) => { toBitVec := { toFin := n • a.val } } }

instance USize.instSMulInt : SMul ℤ USize

Equations

• USize.instSMulInt = { smul := fun (z : ℤ) (a : USize) => { toBitVec := { toFin := z • a.val } } }

theorem UInt8.intCast_def (z : ℤ) : ↑z = { toBitVec := ↑z }

theorem UInt64.val_injective : Function.Injective val

def USize.instCommRing : CommRing USize

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

See the module docstring for an explanation

Equations

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

theorem USize.natCast_def (n : ℕ) : ↑n = { toBitVec := ↑n }

theorem USize.val_injective : Function.Injective val

instance USize.instNonUnitalCommRing : NonUnitalCommRing USize

Equations

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

theorem UInt16.natCast_def (n : ℕ) : ↑n = { toBitVec := ↑n }

def UInt8.instNatCast : NatCast UInt8

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

See the module docstring for an explanation

Equations

• UInt8.instNatCast = { natCast := fun (n : ℕ) => { toBitVec := ↑n } }

instance UInt64.instNonUnitalCommRing : NonUnitalCommRing UInt64

Equations

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

theorem UInt8.natCast_def (n : ℕ) : ↑n = { toBitVec := ↑n }

theorem USize.zsmul_def (z : ℤ) (a : USize) : z • a = { toBitVec := { toFin := z • a.val } }

instance UInt64.instCommMonoid : CommMonoid UInt64

Equations

• UInt64.instCommMonoid = Function.Injective.commMonoid UInt64.toBitVec UInt64.toBitVec_injective UInt64.instCommMonoid.proof_1 UInt64.instCommMonoid.proof_2 UInt64.instCommMonoid.proof_3

theorem UInt64.pow_def (a : UInt64) (n : ℕ) : a ^ n = { toBitVec := { toFin := a.val ^ n } }

theorem UInt16.neg_def (a : UInt16) : -a = { toBitVec := { toFin := -a.val } }

theorem UInt8.toBitVec_injective : Function.Injective toBitVec

theorem USize.pow_def (a : USize) (n : ℕ) : a ^ n = { toBitVec := { toFin := a.val ^ n } }

instance UInt32.instSMulInt : SMul ℤ UInt32

Equations

• UInt32.instSMulInt = { smul := fun (z : ℤ) (a : UInt32) => { toBitVec := { toFin := z • a.val } } }

instance UInt16.instNonUnitalCommRing : NonUnitalCommRing UInt16

Equations

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

theorem UInt8.neg_def (a : UInt8) : -a = { toBitVec := { toFin := -a.val } }

def UInt8.instCommRing : CommRing UInt8

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

See the module docstring for an explanation

Equations

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

theorem UInt8.val_injective : Function.Injective val

theorem UInt32.zsmul_def (z : ℤ) (a : UInt32) : z • a = { toBitVec := { toFin := z • a.val } }

instance UInt8.instPowNat_mathlib : Pow UInt8 ℕ

Equations

• UInt8.instPowNat_mathlib = { pow := fun (a : UInt8) (n : ℕ) => { toBitVec := { toFin := a.val ^ n } } }

def UInt16.instIntCast : IntCast UInt16

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

See the module docstring for an explanation

Equations

• UInt16.instIntCast = { intCast := fun (z : ℤ) => { toBitVec := ↑z } }

instance USize.instCommMonoid : CommMonoid USize

Equations

• USize.instCommMonoid = Function.Injective.commMonoid USize.toBitVec USize.toBitVec_injective USize.instCommMonoid.proof_1 USize.instCommMonoid.proof_2 USize.instCommMonoid.proof_3

theorem UInt32.nsmul_def (n : ℕ) (a : UInt32) : n • a = { toBitVec := { toFin := n • a.val } }

theorem USize.neg_def (a : USize) : -a = { toBitVec := { toFin := -a.val } }

instance UInt8.instNeg_mathlib : Neg UInt8

Equations

• UInt8.instNeg_mathlib = { neg := fun (a : UInt8) => { toBitVec := { toFin := -a.val } } }

instance UInt8.instSMulNat : SMul ℕ UInt8

Equations

• UInt8.instSMulNat = { smul := fun (n : ℕ) (a : UInt8) => { toBitVec := { toFin := n • a.val } } }

instance UInt8.instSMulInt : SMul ℤ UInt8

Equations

• UInt8.instSMulInt = { smul := fun (z : ℤ) (a : UInt8) => { toBitVec := { toFin := z • a.val } } }

theorem UInt32.intCast_def (z : ℤ) : ↑z = { toBitVec := ↑z }

def UInt64.instNatCast : NatCast UInt64

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

See the module docstring for an explanation

Equations

• UInt64.instNatCast = { natCast := fun (n : ℕ) => { toBitVec := ↑n } }

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.

instance UInt64.instSMulInt : SMul ℤ UInt64

Equations

• UInt64.instSMulInt = { smul := fun (z : ℤ) (a : UInt64) => { toBitVec := { toFin := z • a.val } } }

theorem UInt8.zsmul_def (z : ℤ) (a : UInt8) : z • a = { toBitVec := { toFin := z • a.val } }

def USize.instIntCast : IntCast USize

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

See the module docstring for an explanation

Equations

• USize.instIntCast = { intCast := fun (z : ℤ) => { toBitVec := ↑z } }

theorem UInt32.val_injective : Function.Injective val

theorem UInt64.nsmul_def (n : ℕ) (a : UInt64) : n • a = { toBitVec := { toFin := n • a.val } }

theorem UInt8.nsmul_def (n : ℕ) (a : UInt8) : n • a = { toBitVec := { toFin := n • a.val } }

instance USize.instNeg_mathlib : Neg USize

Equations

• USize.instNeg_mathlib = { neg := fun (a : USize) => { toBitVec := { toFin := -a.val } } }

def USize.instNatCast : NatCast USize

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

See the module docstring for an explanation

Equations

• USize.instNatCast = { natCast := fun (n : ℕ) => { toBitVec := ↑n } }

theorem UInt32.natCast_def (n : ℕ) : ↑n = { toBitVec := ↑n }

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 := ⋯ }