64-bit two's complement integers

Arithmetic wraps, so beware (not really, our uses are formally checked).

@[instance_reducible]

instance instCoeInt64Int_interval : Coe Int64 ℤ

The ℤ that an Int64 represents

Equations

• instCoeInt64Int_interval = { coe := fun (x : Int64) => ↑x }

@[instance_reducible]

noncomputable instance instCoeInt64ZModHPowNatOfNat_interval : Coe Int64 (ZMod (2 ^ 64))

The ZMod (2^64) that an Int64 represents

Equations

• instCoeInt64ZModHPowNatOfNat_interval = { coe := fun (x : Int64) => ↑x.toUInt64.toNat }

theorem Int64.ext_iff (x y : Int64) : x = y ↔ x.toUInt64 = y.toUInt64

Reduce Int64 equality to UInt64 equality

theorem Int64.zero_def : 0 = UInt64.toInt64 0

theorem Int64.one_def : 1 = UInt64.toInt64 1

theorem Int64.neg_def (x : Int64) : -x = (-x.toUInt64).toInt64

theorem Int64.add_def (x y : Int64) : x + y = (x.toUInt64 + y.toUInt64).toInt64

theorem Int64.sub_def (x y : Int64) : x - y = (x.toUInt64 - y.toUInt64).toInt64

theorem Int64.mul_def (x y : Int64) : x * y = (x.toUInt64 * y.toUInt64).toInt64

@[simp]

theorem Int64.n_zero : toUInt64 0 = 0

@[simp]

theorem Int64.isNeg_zero : ¬0 < 0

@[simp]

theorem Int64.n_min : minValue.toUInt64 = 2 ^ 63

@[simp]

theorem Int64.toNat_min : minValue.toUInt64.toNat = 2 ^ 63

@[simp]

theorem Int64.toInt_min : ↑minValue = -2 ^ 63

@[simp]

theorem Int64.toBitVec_min : minValue.toBitVec = 2 ^ 63

@[simp]

theorem Int64.isNeg_min : minValue < 0

@[simp]

theorem Int64.neg_min : -minValue = minValue

@[simp]

theorem Int64.zero_undef : UInt64.toInt64 0 = 0

@[instance_reducible]

instance instNatCastInt64_interval : NatCast Int64

Fast conversion from ℕ

Equations

• instNatCastInt64_interval = { natCast := fun (n : ℕ) => (UInt64.ofNat n).toInt64 }

@[instance_reducible]

instance instIntCastInt64_interval : IntCast Int64

Fast conversion from ℤ

Equations

• instIntCastInt64_interval = { intCast := fun (n : ℤ) => Int64.ofInt n }

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

theorem Int64.toBitVec_intCast (n : ℤ) : (↑n).toBitVec = ↑n

theorem Int64.apply_ite_toInt (c : Prop) {d : Decidable c} (x y : Int64) : ↑(if c then x else y) = if c then ↑x else ↑y

theorem Int64.toUInt64_natCast (n : ℕ) : (↑n).toUInt64 = UInt64.ofNat n

theorem Int64.induction_bitvec {p : Int64 → Prop} (h : ∀ (x : BitVec 64), p (ofBitVec x)) (x : Int64) : p x

theorem Int64.toBitVec_ofUInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec

@[simp]

theorem Int64.toInt64_ofNat (n : ℕ) : (UInt64.ofNat n).toInt64 = ofNat n

theorem Int64.toInt_natCast (n : ℕ) : ↑↑n = if 2 * (n % 2 ^ 64) < 2 ^ 64 then ↑n % 2 ^ 64 else ↑n % 2 ^ 64 - 2 ^ 64

theorem Int64.coe_ofNat (n : ℕ) : ↑(ofNat n) = (↑n).bmod size

@[simp]

theorem BitVec.ofNat_mod_64 (n : ℕ) : BitVec.ofNat 64 (n % 2 ^ 64) = BitVec.ofNat 64 n

@[instance_reducible]

instance instCommRingInt64_interval : CommRing Int64

Int64 is a commutative ring. We don't use CommRing.ofMinimalAxioms, since we want our own Sub` instance.

Equations

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

@[instance_reducible]

instance decidableLT : DecidableRel fun (x1 x2 : Int64) => x1 < x2

Int64 < is decidable

Equations

• decidableLT x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance decidableLE : DecidableRel fun (x1 x2 : Int64) => x1 ≤ x2

Int64 ≤ is decidable

Equations

• decidableLE x✝¹ x✝ = id inferInstance

@[simp]

theorem Int64.neg_eq_min {x : Int64} : -x = minValue ↔ x = minValue

Negation preserves min

@[simp]

theorem Int64.min_ne_zero : minValue ≠ 0

minValue ≠ 0

@[simp]

theorem Int64.zero_ne_min : 0 ≠ minValue

0 ≠ minValue

theorem Int64.coe_of_nonneg {x : Int64} (h : 0 ≤ x) : ↑x = ↑x.toUInt64.toNat

theorem Int64.coe_of_neg {x : Int64} (h : x < 0) : ↑x = ↑x.toUInt64.toNat - ↑(2 ^ 64)

theorem Int64.neg_natCast (n : ℕ) : -↑n = ↑(-↑n)

theorem Int64.toUInt64_intCast (n : ℤ) : (↑n).toUInt64 = UInt64.ofInt n

theorem Int64.isNeg_eq_le (x : Int64) : x < 0 ↔ 2 ^ 63 ≤ x.toUInt64.toNat

isNeg in terms of ≤ over ℕ

@[simp]

theorem Int64.coe_lt_coe (x y : Int64) : ↑x < ↑y ↔ x < y

The ordering is consistent with ℤ

@[simp]

theorem Int64.coe_lt_pow (x : Int64) : ↑x < 2 ^ 63

Converting to ℤ is under 2^63

@[simp]

theorem Int64.pow_le_coe (x : Int64) : -2 ^ 63 ≤ ↑x

Converting to ℤ is at least -2^63

@[simp]

theorem Int64.coe_min' : ↑minValue = -2 ^ 63

@[simp]

theorem Int64.coe_le_coe (x y : Int64) : ↑x ≤ ↑y ↔ x ≤ y

The ordering is consistent with ℤ

@[instance_reducible]

instance instReprInt64_interval : Repr Int64

We print Int64s as signed integers

Equations

• instReprInt64_interval = { reprPrec := fun (x : Int64) (p : ℕ) => reprPrec (↑x) p }

theorem Int64.eq_zero_iff_n_eq_zero (x : Int64) : x = 0 ↔ x.toUInt64 = 0

theorem Int64.ne_zero_iff_n_ne_zero (x : Int64) : x ≠ 0 ↔ x.toUInt64 ≠ 0

theorem Int64.coe_neg {x : Int64} : ↑(-x) = if ↑x = -2 ^ 63 then -2 ^ 63 else -↑x

Expand negation into something omega can handle

theorem Int64.coe_add {x y : Int64} : ↑(x + y) = have s := ↑x + ↑y; if s < -2 ^ 63 then s + 2 ^ 64 else if 2 ^ 63 ≤ s then s - 2 ^ 64 else s

Expand addition into something omega can handle

theorem Int64.coe_sub {x y : Int64} : ↑(x - y) = have s := ↑x - ↑y; if s < -2 ^ 63 then s + 2 ^ 64 else if 2 ^ 63 ≤ s then s - 2 ^ 64 else s

Expand subtraction into something omega can handle

@[simp]

theorem Int64.coe_zero : ↑0 = 0

@[simp]

theorem Int64.coe_one : ↑1 = 1

@[simp]

theorem Int64.coe_eq_coe (x y : Int64) : ↑x = ↑y ↔ x = y

Equality is consistent with ℤ

@[simp]

theorem Int64.coe_ne_coe (x y : Int64) : ↑x ≠ ↑y ↔ x ≠ y

Equality is consistent with ℤ

@[simp]

theorem Int64.coe_eq_zero (x : Int64) : ↑x = 0 ↔ x = 0

@[simp]

theorem Int64.pow_lt_coe {x : Int64} (n : x ≠ minValue) : -2 ^ 63 < ↑x

Converting to ℤ is more than -2^63 if we're not minValue

theorem Int64.isNeg_neg {x : Int64} (x0 : x ≠ 0) (xn : x ≠ minValue) : -x < 0 ↔ 0 ≤ x

Negation flips .isNeg, except at 0 and .minValue

theorem UInt64.coe_toInt64 (x : UInt64) : ↑x.toInt64 = if x < 2 ^ 63 then x.toInt else x.toInt - 2 ^ 64

Conditions for ℤ conversion to commute with arithmetic

theorem Int64.coe_neg' {x : Int64} (xn : x ≠ minValue) : ↑(-x) = -↑x

Int64.neg usually commutes with ℤ conversion

theorem Int64.coe_add_eq {x y : Int64} (h : x + y < 0 ↔ x < 0) : ↑(x + y) = ↑x + ↑y

ℤ conversion commutes with add if isNeg matches the left argument

theorem Int64.coe_add_eq' {x y : Int64} (h : x + y < 0 ↔ y < 0) : ↑(x + y) = ↑x + ↑y

ℤ conversion commutes with add if isNeg matches the right argument

theorem Int64.coe_add_ne {x y : Int64} (h : ¬(x < 0 ↔ y < 0)) : ↑(x + y) = ↑x + ↑y

ℤ conversion commutes with add if the two arguments have different isNegs

theorem Int64.coe_sub_of_le_of_pos {x y : Int64} (yx : y ≤ x) (h : 0 ≤ x - y) : ↑(x - y) = ↑x - ↑y

ℤ conversion commutes with sub if the result is positive

theorem Int64.toReal_toInt {x : Int64} (h : 0 ≤ x) : ↑↑x = ↑x.toUInt64.toNat

Conversion to ℤ is the same as via ℕ if we're nonnegative

@[simp]

theorem Int64.ofNat_eq_coe (n : ℕ) : (↑n).toUInt64 = UInt64.ofNat n

Conversion from ℕ is secretly the same as conversion to UInt64

@[simp]

theorem Int64.toNat_toBitVec_natCast (n : ℕ) : (↑n).toBitVec.toNat = n % 2 ^ 64

@[simp]

theorem Int64.toNat_toBitVec_intCast (n : ℤ) : (↑n).toBitVec.toNat = (n % 2 ^ 64).toNat

theorem Int64.toInt_ofNat'' {n : ℕ} (h : n < 2 ^ 63) : ↑↑n = ↑n

Conversion ℕ → Int64 → ℤ is the same as direct if we're small

theorem Int64.toInt_ofInt' {n : ℤ} (h : |n| < 2 ^ 63) : ↑↑n = n

Conversion ℤ → Int64 → ℤ is the same as direct if we're small

theorem Int64.toInt_eq_toNat_of_lt {x : Int64} (h : x.toUInt64.toNat < 2 ^ 63) : ↑x = ↑x.toUInt64.toNat

Conversion to ℤ is the same as the underlying toNat if we're small

@[simp]

theorem Int64.coe_log2 (n : UInt64) : ↑n.log2.toInt64 = ↑n.log2.toNat

UInt64.log2 converts to ℤ as toNat

@[simp]

theorem Int64.toNat_add_pow_eq_coe (n : Int64) : ↑(n + 2 ^ 63).toUInt64.toNat = ↑n + 2 ^ 63

Adding 2^63 and converting via UInt64 commutes

Order lemmas

@[instance_reducible]

instance instMinInt64_interval : Min Int64

Int64 min (must be defined before LinearOrder)

Equations

• instMinInt64_interval = { min := fun (x y : Int64) => if x < y then x else y }

@[instance_reducible]

instance instMaxInt64_interval : Max Int64

Int64 max (must be defined before LinearOrder)

Equations

• instMaxInt64_interval = { max := fun (x y : Int64) => if x < y then y else x }

@[instance_reducible]

instance instLinearOrderInt64_interval : LinearOrder Int64

Int64 is a linear order (though not an ordered algebraic structure)

Equations

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

@[simp]

theorem Int64.min_le (x : Int64) : minValue ≤ x

Int64.min is the smallest element

theorem Int64.eq_min_iff_min_lt (x : Int64) : x = minValue ↔ x ≤ minValue

Int64.min is the smallest element

theorem Int64.coe_nonneg {x : Int64} (h : 0 ≤ x) : 0 ≤ ↑x

@[simp]

theorem Int64.coe_nonpos_iff {x : Int64} : ↑x ≤ 0 ↔ x ≤ 0

theorem Int64.coe_lt_zero {x : Int64} (h : x < 0) : ↑x < 0

theorem Int64.coe_lt_zero_iff {x : Int64} : ↑x < 0 ↔ x < 0

@[simp]

theorem Int64.coe_nonneg_iff {x : Int64} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Int64.coe_neg_iff {x : Int64} : ↑x < 0 ↔ x < 0

@[simp]

theorem Int64.coe_pos_iff {x : Int64} : 0 < ↑x ↔ 0 < x

@[simp]

theorem Int64.natAbs_lt_pow_iff {x : Int64} : (↑x).natAbs < 2 ^ 63 ↔ x ≠ minValue

theorem Int64.sub_le' {x y : Int64} (h : minValue + y ≤ x) : x - y ≤ x

A sufficient condition for subtraction to decrease the value

theorem Int64.toNat_toUInt64 (x : Int64) : x.toUInt64.toNat = (↑x % 2 ^ 64).toNat

Shims for proof backwards compatibility

def Int64.isNeg (x : Int64) : Bool

I now use x < 0 directly in most places, but we record this for backwards compatibility

Equations

• x.isNeg = decide (x < 0)

theorem Int64.toInt_eq_if (x : Int64) : ↑x = ↑x.toUInt64.toNat - ↑(if x < 0 then 2 ^ 64 else 0)

Show that Int64 → ℤ is the same as we used to define it

theorem Int64.abs_def (x : Int64) : x.abs = if x < 0 then -x else x

Alternate definition of (almost) absolute value (maps Int64.min → Int64.min)

theorem Int64.induction_nat (p : Int64 → Prop) (h : ∀ n < 2 ^ 64, p ↑n) (x : Int64) : p x

Prove something about Int64 via ℕ

theorem Int64.toNat_toBitVec' (x : Int64) : x.toBitVec.toNat = (↑x % 2 ^ 64).toNat

Order operations: min, abs

def Int64.uabs (x : Int64) : UInt64

Alterantive abs which is better behaved, by has to change type

Equations

• x.uabs = if x < 0 then -x.toUInt64 else x.toUInt64

@[simp]

theorem Int64.abs_zero : Int64.abs 0 = 0

@[simp]

theorem Int64.uabs_zero : uabs 0 = 0

@[simp]

theorem Int64.abs_min : minValue.abs = minValue

@[simp]

theorem Int64.uabs_min : minValue.uabs = 2 ^ 63

theorem Int64.toNat_abs {x : Int64} : x.abs.toNatClampNeg = if x = minValue then 0 else (↑x).natAbs

.abs is absolute value (ℕ version)

theorem Int64.toNat_uabs {x : Int64} : x.uabs.toNat = (↑x).natAbs

.uabs is absolute value (ℕ version)

theorem Int64.coe_abs {x : Int64} : ↑x.abs = if x = minValue then -2 ^ 63 else |↑x|

.abs is absolute value (ℤ version)

theorem Int64.coe_uabs {x : Int64} : x.uabs.toInt = |↑x|

.uabs is absolute value (ℤ version)

theorem Int64.coe_uabs' {x : Int64} (n : x ≠ minValue) : ↑x.uabs.toInt64 = |↑x|

If we turn uabs back into an Int64, it's abs except at .min

@[simp]

theorem Int64.abs_eq_zero_iff {x : Int64} : x.abs = 0 ↔ x = 0

abs preserves 0

@[simp]

theorem Int64.uabs_eq_zero_iff {x : Int64} : x.uabs = 0 ↔ x = 0

uabs preserves 0

@[simp]

theorem Int64.abs_ne_zero_iff {x : Int64} : x.abs ≠ 0 ↔ x ≠ 0

abs preserves 0

@[simp]

theorem Int64.uabs_ne_zero_iff {x : Int64} : x.uabs ≠ 0 ↔ x ≠ 0

uabs preserves 0

theorem Int64.abs_eq_self' {x : Int64} (h : 0 ≤ x) : x.abs = x

.abs doesn't change if nonneg

theorem Int64.uabs_eq_self' {x : Int64} (h : 0 ≤ x) : x.uabs = x.toUInt64

.uabs doesn't change if nonneg

theorem Int64.ne_minValue_of_nonneg {x : Int64} (h : 0 ≤ x) : x ≠ minValue

theorem Int64.abs_eq_self {x : Int64} (h : 0 ≤ x) : ↑x.abs = ↑x

.abs doesn't change if nonneg

theorem Int64.uabs_eq_self {x : Int64} (h : 0 ≤ x) : x.uabs.toInt = ↑x

.uabs doesn't change if nonneg

theorem Int64.abs_eq_neg' {x : Int64} (n : x < 0) : x.abs = -x

.abs negates if negative

theorem Int64.uabs_eq_neg' {x : Int64} (n : x < 0) : x.uabs = (-x).toUInt64

.uabs negates if negative

theorem Int64.uabs_eq_neg {x : Int64} (n : x < 0) : x.uabs.toInt = -↑x

.uabs negates if negative

theorem Int64.coe_min {x y : Int64} : ↑(min x y) = min ↑x ↑y

.min commutes with coe

theorem Int64.coe_max {x y : Int64} : ↑(max x y) = max ↑x ↑y

.max commutes with coe

@[simp]

theorem Nat.toUInt64_toInt64 (n : ℕ) : n.toInt64.toUInt64 = UInt64.ofInt ↑n

theorem Int64.uabs_lt_zero {x : Int64} : ↑x.uabs.toInt64 < 0 ↔ x = minValue

If we turn uabs back into an Int64, it's negative only at .min

@[simp]

theorem Int64.uabs_neg {x : Int64} : (-x).uabs = x.uabs

(-x).uabs = x.uabs

@[simp]

theorem Int64.toNat_neg {x : Int64} (n : x < 0) : ↑(-x).toUInt64.toNat = -↑x

(-t).n.toNat = t when converting negatives to ℤ

@[simp]

theorem Int64.uabs_eq_pow_iff {x : Int64} : x.uabs = 2 ^ 63 ↔ x = minValue

@[simp]

theorem Int64.uabs_uabs {x : Int64} : x.uabs.toInt64.uabs = x.uabs

@[simp]

theorem Int64.isNeg_uabs {x : Int64} (m : x ≠ minValue) : 0 ≤ x.uabs.toInt64

Left shift

@[instance_reducible]

instance instHShiftLeftInt64UInt64_interval : HShiftLeft Int64 UInt64 Int64

Shifting left is shifting the inner UInt64 left

Equations

• instHShiftLeftInt64UInt64_interval = { hShiftLeft := fun (x : Int64) (s : UInt64) => (x.toUInt64 <<< s).toInt64 }

theorem Int64.shiftLeft_def (x : Int64) (s : UInt64) : x <<< s = (x.toUInt64 <<< s).toInt64

theorem Int64.coe_shiftLeft {x : Int64} {s : UInt64} (s64 : s.toNat < 64) (xs : x.uabs.toNat < 2 ^ (63 - s.toNat)) : ↑(x <<< s) = ↑x * 2 ^ s.toNat

Shifting left is multiplying by a power of two, in nice cases

@[simp]

theorem Int64.zero_shiftLeft' (s : UInt64) : 0 <<< s = 0

0 <<< s = 0

Right shift, rounding up or down

@[irreducible]

def Int64.shiftRightRound (x : Int64) (s : UInt64) (up : Bool) : Int64

Shift right, rounding up or down

Equations

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

@[simp]

theorem Int64.zero_shiftRightRound (s : UInt64) (up : Bool) : shiftRightRound 0 s up = 0

0.shiftRightRound = 0

theorem Int64.isNeg_one_shift {s : UInt64} (s64 : s.toNat < 64) : (1 <<< s).toInt64 < 0 ↔ s.toNat = 63

Int64.isNeg for powers of two

theorem Int64.coe_one_shift {s : UInt64} (s63 : s.toNat < 63) : ↑(1 <<< s).toInt64 = 2 ^ s.toNat

ℤ conversion for UInt64 powers of two

theorem Int64.coe_neg_one_shift {s : UInt64} (s63 : s.toNat < 63) : ↑(-(1 <<< s).toInt64) = -2 ^ s.toNat

ℤ conversion for negated Int64 powers of two

theorem Int64.coe_eq_toNat_of_lt {n : UInt64} (h : n.toNat < 2 ^ 63) : ↑n.toInt64 = ↑n.toNat

Negated ℤ conversion for UInt64 values

theorem Int64.coe_neg_eq_neg_toNat_of_lt {n : UInt64} (h : n.toNat < 2 ^ 63) : ↑(-n.toInt64) = -↑n.toNat

Negated ℤ conversion for UInt64 values

theorem Int64.coe_shiftRightRound (x : Int64) (s : UInt64) (up : Bool) : ↑(x.shiftRightRound s up) = (↑x).rdiv (2 ^ s.toNat) up

Int64.shiftRightRound rounds correctly

theorem Int64.abs_shiftRightRound_le (x : Int64) (s : UInt64) (up : Bool) : |↑(x.shiftRightRound s up)| ≤ |↑x|

Int64.shiftRightRound reduces abs

theorem Int64.shiftRightRound_ne_min {x : Int64} (n : x ≠ minValue) (s : UInt64) (up : Bool) : x.shiftRightRound s up ≠ minValue

Int64.shiftRightRound never produces min from scratch

natFloor: An ℕ trying to be less than an Int64

def Int64.natFloor (n : Int64) : ℕ

The greatest natural ≤ n (that is, max 0 n)

Equations

• n.natFloor = if n < 0 then 0 else n.toUInt64.toNat

theorem Int64.natFloor_eq (n : Int64) : n.natFloor = ⌊↑n⌋₊

natFloor in terms of n : ℤ