Int128: 128-bit signed integers

structure Int128 : Type

128-bit twos complement signed integers

• n : UInt128

theorem Int128.ext {x y : Int128} (n : x.n = y.n) : x = y

theorem Int128.ext_iff {x y : Int128} : x = y ↔ x.n = y.n

@[instance_reducible]

instance instDecidableEqInt128 : DecidableEq Int128

Equations

• instDecidableEqInt128 = instDecidableEqInt128.decEq

def instDecidableEqInt128.decEq (x✝ x✝¹ : Int128) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqInt128.decEq { n := a } { n := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instBEqInt128 : BEq Int128

Equations

• instBEqInt128 = { beq := instBEqInt128.beq }

def instBEqInt128.beq : Int128 → Int128 → Bool

Equations

• instBEqInt128.beq { n := a } { n := b } = (a == b)
• instBEqInt128.beq x✝¹ x✝ = false

@[irreducible]

def Int128.isNeg (x : Int128) : Bool

Equations

• x.isNeg = decide (9223372036854775808 ≤ x.n.hi)

@[irreducible]

def Int128.min : Int128

Equations

• Int128.min = { n := { lo := 0, hi := 9223372036854775808 } }

@[instance_reducible]

instance Int128.instZero : Zero Int128

Equations

• Int128.instZero = { zero := { n := 0 } }

@[simp]

theorem Int128.n_zero : n 0 = 0

theorem Int128.isNeg_eq_le_toNat (x : Int128) : x.isNeg = decide (2 ^ 127 ≤ x.n.toNat)

Alternative isNeg characterization in terms of n.toNat

Conversion from other integer types

def Int128.of_lo (x : UInt64) : Int128

Equations

• ↑x = { n := { lo := x, hi := 0 } }

@[instance_reducible]

instance Int128.instCoeUInt64 : Coe UInt64 Int128

UInt64 coerces to Int128

Equations

• Int128.instCoeUInt64 = { coe := Int128.of_lo }

@[irreducible]

def Int128.ofNat (x : ℕ) : Int128

Wrap around conversion from ℕ

Equations

• Int128.ofNat x = { n := UInt128.ofNat x }

@[irreducible]

def Int128.ofInt (x : ℤ) : Int128

Wrap around conversion from ℤ

Equations

• Int128.ofInt x = { n := UInt128.ofInt x }

theorem Int128.n_ofInt (x : ℤ) : (ofInt x).n = UInt128.ofInt x

ℤ conversion

def Int128.toInt (x : Int128) : ℤ

The ℤ that an Int128 represents

Equations

• ↑x = ↑x.n.toNat - bif x.isNeg then 2 ^ 128 else 0

@[instance_reducible]

instance Int128.instCoeInt : Coe Int128 ℤ

The ℤ that an Int64 represents

Equations

• Int128.instCoeInt = { coe := fun (x : Int128) => ↑x }

@[simp]

theorem Int128.coe_of_hi_eq_zero {x : Int128} (h0 : x.n.hi = 0) : ↑x.n.lo.toNat = ↑x

If hi = 0, conversion is just lo

@[simp]

theorem Int128.isNeg_iff {x : Int128} : x.isNeg = decide (↑x < 0)

isNeg is nicer in terms of integers

@[simp]

theorem Int128.ofInt_coe (x : Int128) : ofInt ↑x = x

Int128 → ℤ → Int128 is the identity

theorem Int128.coe_ofInt (x : ℤ) : ↑(ofInt x) = (x + 2 ^ 127) % 2 ^ 128 - 2 ^ 127

ℤ → Int128 → ℤ almost roundtrips

@[simp]

theorem Int128.ofInt_ofUInt64 (x : UInt64) : ofInt ↑x.toNat = ↑x

ofInt_coe if we start with UInt64

Additive group operations: negation, addition, subtraction

@[instance_reducible]

instance Int128.instNeg : Neg Int128

Equations

• Int128.instNeg = { neg := fun (x : Int128) => { n := -x.n } }

@[instance_reducible]

instance Int128.instAdd : Add Int128

Equations

• Int128.instAdd = { add := fun (x y : Int128) => { n := x.n + y.n } }

@[instance_reducible]

instance Int128.instSub : Sub Int128

Equations

• Int128.instSub = { sub := fun (x y : Int128) => { n := x.n - y.n } }

theorem Int128.n_neg (x : Int128) : (-x).n = -x.n

theorem Int128.n_add (x y : Int128) : (x + y).n = x.n + y.n

theorem Int128.n_sub (x y : Int128) : (x - y).n = x.n - y.n

@[simp]

theorem Int128.neg_ofInt (x : ℤ) : ofInt (-x) = -ofInt x

ofInt commutes with -

@[simp]

theorem Int128.add_ofInt (x y : ℤ) : ofInt (x + y) = ofInt x + ofInt y

ofInt commutes with +

@[simp]

theorem Int128.sub_ofInt (x y : ℤ) : ofInt (x - y) = ofInt x - ofInt y

ofInt commutes with -

@[instance_reducible]

instance Int128.instAddCommGroup : AddCommGroup Int128

Int128 inherits the additive group structure from UInt128

Equations

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

ℤ → Int128 is injective for small integers

theorem Int128.coe_ofInt_of_abs_lt {x : ℤ} (sx : x ∈ Set.Ico (-2 ^ 127) (2 ^ 127)) : ↑(ofInt x) = x

Small integers roundtrip through ℤ → Int128 → ℤ

theorem Int128.eq_of_ofInt_eq {x y : ℤ} (e : ofInt x = ofInt y) (sx : x ∈ Set.Ico (-2 ^ 127) (2 ^ 127)) (sy : y ∈ Set.Ico (-2 ^ 127) (2 ^ 127)) : x = y

Small integers are equal if their 128-bit wraps are equal

theorem Int128.coe_small {x : Int128} : ↑x ∈ Set.Ico (-2 ^ 127) (2 ^ 127)

coe is small