Documentation

Interval.UInt64

`UInt64` lemmas #

theorem UInt64.size_eq_pow :

size = 2 ^ 64

def UInt64.max :

Equations

UInt64.max = UInt64.ofNat UInt64.size - 1

Instances For

theorem UInt64.max_eq_pow_sub_one :

max = 2 ^ 64 - 1

@[simp]

theorem UInt64.toNat_lt_2_pow_64 (n : UInt64) :

n.toNat < 2 ^ 64

@[simp]

theorem UInt64.cast_toNat_lt_2_pow_64 (n : UInt64) :

↑n.toNat < 2 ^ 64

@[simp]

theorem UInt64.toNat_lt_toNat (m n : UInt64) :

m.toNat < n.toNat ↔ m < n

@[simp]

theorem UInt64.toNat_le_toNat (m n : UInt64) :

m.toNat ≤ n.toNat ↔ m ≤ n

theorem UInt64.eq_iff_toNat_eq (m n : UInt64) :

m = n ↔ m.toNat = n.toNat

theorem UInt64.pos_iff_toNat_pos (n : UInt64) :

0 < n ↔ 0 < n.toNat

theorem UInt64.eq_zero_iff_toNat_eq_zero {n : UInt64} :

n = 0 ↔ n.toNat = 0

theorem UInt64.ne_zero_iff_toNat_ne_zero {n : UInt64} :

n ≠ 0 ↔ n.toNat ≠ 0

@[simp]

theorem UInt64.nonneg {n : UInt64} :

0 ≤ n

@[simp]

theorem UInt64.toNat_2_pow_63 :

(2 ^ 63).toNat = 2 ^ 63

@[simp]

theorem UInt64.toNat_2_pow_63' :

toNat 9223372036854775808 = 2 ^ 63

@[simp]

theorem UInt32.size_pos :

@[simp]

theorem UInt32.lt_size (n : UInt32) :

@[simp]

theorem UInt32.le_size (n : UInt32) :

n.toNat ≤ size

@[simp]

theorem UInt64.size_pos :

@[simp]

theorem UInt64.lt_size (n : UInt64) :

@[simp]

theorem UInt64.le_size (n : UInt64) :

n.toNat ≤ size

@[simp]

theorem UInt64.le_size_sub_one (n : UInt64) :

n.toNat ≤ size - 1

@[simp]

theorem UInt64.toNat_neg' (n : UInt64) :

(-n).toNat = if n = 0 then 0 else size - n.toNat

theorem UInt64.toNat_add' (m n : UInt64) :

(m + n).toNat = m.toNat + n.toNat - if m.toNat + n.toNat < size then 0 else size

@[simp]

theorem UInt64.sub_sub_cancel {x y : UInt64} :

x - (x - y) = y

theorem UInt64.add_wrap_iff (m n : UInt64) :

m + n < m ↔ size ≤ m.toNat + n.toNat

theorem UInt64.toNat_add_of_le_add {m n : UInt64} (h : m ≤ m + n) :

(m + n).toNat = m.toNat + n.toNat

If UInt64 doesn't wrap, addition commutes with toNat

theorem UInt64.toNat_add_of_add_lt' {G : Type} [AddGroupWithOne G] {m n : UInt64} (h : m + n < m) :

↑(m + n).toNat = ↑m.toNat + ↑n.toNat - ↑size

If UInt64 wraps, addition and toNat commute except for subtracting size (AddGroupWithOne version)

theorem UInt64.toNat_add_of_add_lt {m n : UInt64} (h : m + n < m) :

(m + n).toNat = m.toNat + n.toNat - size

If UInt64 wraps, addition commutes with toNat except for subtracting size (ℕ version)

theorem UInt64.toNat_sub' {x y : UInt64} :

(x - y).toNat = (x.toNat + (size - y.toNat)) % size

UInt64 subtract wraps around

theorem UInt64.toNat_sub'' {x y : UInt64} (h : y ≤ x) :

(x - y).toNat = x.toNat - y.toNat

If truncation doesn't occur, - commutes with toNat

theorem UInt64.toNat_add_one {m : UInt64} (h : m.toNat ≠ 2 ^ 64 - 1) :

(m + 1).toNat = m.toNat + 1

Adding 1 is usually adding one toNat

theorem UInt64.toNat_add_one' {m : UInt64} (h : m ≠ max) :

(m + 1).toNat = m.toNat + 1

Adding 1 is usually adding one toNat

instance instLinearOrderUInt64_interval :

LinearOrder UInt64

UInt64 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 UInt64.toNat_land {x y : UInt64} :

(x &&& y).toNat = x.toNat &&& y.toNat

UInt64 bitwise and is ℕ bitwise and

@[simp]

theorem UInt64.land_eq_hand {x y : UInt64} :

x.land y = x &&& y

@[simp]

theorem UInt64.zero_land {x : UInt64} :

0 &&& x = 0

theorem UInt64.toNat_shiftLeft' {x s : UInt64} :

(x <<< s).toNat = x.toNat % 2 ^ (64 - s.toNat % 64) * 2 ^ (s.toNat % 64)

theorem UInt64.toNat_shiftLeft'' {x s : UInt64} (h : s < 64) :

(x <<< s).toNat = x.toNat % 2 ^ (64 - s.toNat) * 2 ^ s.toNat

theorem UInt64.toNat_shiftLeft''' {x s : UInt64} (h : s.toNat < 64) :

(x <<< s).toNat = x.toNat % 2 ^ (64 - s.toNat) * 2 ^ s.toNat

@[simp]

theorem UInt64.toNat_shiftLeft32 {x : UInt64} :

(x <<< 32).toNat = x.toNat % 2 ^ 32 * 2 ^ 32

theorem UInt64.toNat_shiftRight' {x s : UInt64} :

(x >>> s).toNat = x.toNat / 2 ^ (s.toNat % 64)

theorem UInt64.toNat_shiftRight'' {x s : UInt64} (h : s < 64) :

(x >>> s).toNat = x.toNat / 2 ^ s.toNat

@[simp]

theorem UInt64.testBit_eq_zero {x : UInt64} {i : ℕ} (h : 64 ≤ i) :

x.toNat.testBit i = false

@[simp]

theorem UInt64.toNat_lor {x y : UInt64} :

(x ||| y).toNat = x.toNat ||| y.toNat

theorem UInt64.toNat_lor_shifts {x y s : UInt64} (s0 : s ≠ 0) (s64 : s < 64) :

(x >>> s).toNat ||| (y <<< (64 - s)).toNat = (x >>> s).toNat + (y <<< (64 - s)).toNat

@[simp]

theorem UInt64.toNat_cast (n : ℕ) :

(ofNat n).toNat = n % size

@[simp]

theorem UInt64.cast_toNat (n : UInt64) :

ofNat n.toNat = n

@[simp]

theorem UInt64.toInt_intCast (n : ℤ) :

↑(ofInt n).toNat = n % 2 ^ 64

theorem UInt64.toInt_mem_Ico (n : UInt64) :

↑n.toNat ∈ Set.Ico 0 (2 ^ 64)

@[simp]

theorem UInt64.toNat_log2 (n : UInt64) :

n.log2.toNat = n.toNat.log2

@[simp]

theorem UInt64.log2_zero :

log2 0 = 0

@[simp]

theorem UInt64.log2_lt_64 (n : UInt64) :

n.toNat.log2 < 64

@[simp]

theorem UInt64.log2_lt_64' (n : UInt64) :

n.log2 < 64

theorem UInt64.toNat_add_of_le {x y : UInt64} (h : x ≤ max - y) :

(x + y).toNat = x.toNat + y.toNat

@[simp]

theorem UInt64.toNat_max' :

max.toNat = 2 ^ 64 - 1

@[simp]

theorem UInt64.le_max (n : UInt64) :

@[simp]

theorem UInt64.toNat_le_pow_sub_one (n : UInt64) :

n.toNat ≤ 2 ^ 64 - 1

@[simp]

theorem UInt64.pow_eq_zero :

2 ^ 64 = 0

Conversion from `UInt64` to `ZMod` #

def UInt64.toZMod (x : UInt64) :

Equations

x.toZMod = ↑x.toNat

Instances For

noncomputable instance instCoeUInt64ZModSize_interval :

Coe UInt64 (ZMod UInt64.size)

Equations

instCoeUInt64ZModSize_interval = { coe := fun (x : UInt64) => x.toZMod }

@[simp]

theorem UInt64.toZMod_toNat (x : UInt64) :

↑x.toNat = x.toZMod

@[simp]

theorem UInt64.toZMod_add (x y : UInt64) :

(x + y).toZMod = x.toZMod + y.toZMod

@[simp]

theorem UInt64.toZMod_mul (x y : UInt64) :

(x * y).toZMod = x.toZMod * y.toZMod

@[simp]

theorem UInt64.toZMod_cast (x : ℕ) :

(ofNat x).toZMod = ↑x

@[simp]

theorem UInt64.toZMod_shiftLeft32 (x : UInt64) :

(x <<< 32).toZMod = x.toZMod * 2 ^ 32

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

p x

Prove something about UInt64 via ℕ

theorem UInt64.toNat_ofNat'' (n : ℕ) :

(ofNat n).toNat = n % 2 ^ 64

Add with carry #

def addc (x y : UInt64) :

UInt64 × UInt64

Add with carry, producing the {0,1} value as an UInt64

Equations

addc x y = (x + y, if x + y < x then 1 else 0)

Instances For

theorem addc_eq (x y : UInt64) :

∃ (a0 : ℕ) (a2 : ℕ), a0 < 2 ^ 64 ∧ a2 < 2 ∧ x.toNat + y.toNat = a2 * 2 ^ 64 + a0 ∧ addc x y = (UInt64.ofNat a0, UInt64.ofNat a2)

Decompose an addc

Splitting `UInt64`s into 32-bit halves #

def split (x : UInt64) :

UInt64 × UInt64

Split a UInt64 into low and high 32-bit values, both represented as UInt64

Equations

split x = (x.toUInt32.toUInt64, x >>> 32)

Instances For

@[simp]

theorem UInt64.toNat_shiftRight32 {x : UInt64} :

(x >>> 32).toNat = x.toNat / 2 ^ 32

@[simp]

theorem toNat_split_1 {x : UInt64} :

(split x).1.toNat = x.toNat % 2 ^ 32

@[simp]

theorem toNat_split_2 {x : UInt64} :

(split x).2.toNat = x.toNat / 2 ^ 32

@[simp]

theorem toNat_split_1_lt {x : UInt64} :

(split x).1.toNat < 2 ^ 32

@[simp]

theorem toNat_split_2_lt {x : UInt64} :

(split x).2.toNat < 2 ^ 32

@[simp]

theorem mod_32_mod_64 (x : ℕ) :

x % 2 ^ 32 % 2 ^ 64 = x % 2 ^ 32

theorem UInt64.eq_split (x : UInt64) :

∃ (x0 : ℕ) (x1 : ℕ), x0 < 2 ^ 32 ∧ x1 < 2 ^ 32 ∧ x.toNat = x1 * 2 ^ 32 + x0 ∧ split x = (ofNat x0, ofNat x1)

Decompose a UInt64 via split

`ℤ` conversion #

def UInt64.toInt (x : UInt64) :

Equations

x.toInt = ↑x.toNat

Instances For

theorem UInt64.coe_toNat_sub {x y : UInt64} (h : y ≤ x) :

↑(x - y).toNat = ↑x.toNat - ↑y.toNat

@[simp]

theorem UInt64.toInt_zero :

theorem UInt64.toInt_neg {x : UInt64} :

(-x).toInt = if x = 0 then 0 else 2 ^ 64 - x.toInt

@[simp]

theorem UInt64.toInt_ofNat (n : ℕ) :

(ofNat n).toInt = ↑n % 2 ^ 64

@[simp]

theorem UInt64.toNat_ofInt (n : ℤ) :

(ofInt n).toNat = (n % 2 ^ 64).toNat

@[simp]

theorem UInt64.natCast_toNat (n : UInt64) :

↑n.toNat = n.toInt

@[simp]

theorem UInt64.ofInt_toInt (n : UInt64) :

ofInt n.toInt = n

@[simp]

theorem UInt64.toNat_toInt (n : UInt64) :

n.toInt.toNat = n.toNat

theorem UInt64.toInt_add (a b : UInt64) :

(a + b).toInt = (a.toInt + b.toInt) % 2 ^ 64

theorem UInt64.toInt_shiftLeft' {x s : UInt64} :

(x <<< s).toInt = x.toInt % 2 ^ (64 - s.toNat % 64) * 2 ^ (s.toNat % 64)

theorem UInt64.toInt_one :

theorem UInt64.apply_ite_toInt (c : Prop) {d : Decidable c} (x y : UInt64) :

(if c then x else y).toInt = if c then x.toInt else y.toInt

theorem UInt64.toBitVec_two_pow_63 :

(2 ^ 63).toBitVec = 9223372036854775808

theorem UInt64.induction_bitvec {p : UInt64 → Prop} (h : ∀ (x : BitVec 64), p { toBitVec := x }) (x : UInt64) :

p x

Shift right, rounding up or down #

@[irreducible]

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

Shift right, rounding up or down correctly even for large s

Equations

x.shiftRightRound s up = bif s == 0 then x else bif decide (64 ≤ s) then bif x == 0 || !up then 0 else 1 else have y := x >>> s; bif up && x != y <<< s then y + 1 else y

Instances For

@[simp]

theorem UInt64.zero_shiftRightRound (s : UInt64) (up : Bool) :

shiftRightRound 0 s up = 0

0.shiftRightRound = 0

theorem UInt64.toNat_shiftRightRound {x s : UInt64} {up : Bool} :

(x.shiftRightRound s up).toNat = (x.toNat + if up = true then 2 ^ s.toNat - 1 else 0) / 2 ^ s.toNat

Exact ℕ result of UInt64.shiftRightRound

theorem UInt64.toNat_shiftRightRound' {x s : UInt64} {up : Bool} :

(x.shiftRightRound s up).toNat = if up = true then x.toNat ⌈/⌉ 2 ^ s.toNat else x.toNat / 2 ^ s.toNat

Alternate version using ceilDiv

theorem UInt64.shiftRightRound_le_self {x s : UInt64} {up : Bool} :

(x.shiftRightRound s up).toNat ≤ x.toNat

UInt64.shiftRightRound only makes things smaller

Complement facts #

theorem UInt64.toNat_complement (x : UInt64) :

(~~~x).toNat = 2 ^ 64 - 1 - x.toNat

Kernel-friendly version of `Nat.log2` #

theorem UInt64.fast_log2_lt (n : UInt64) :

(↑n.toFin).log2 < size

@[irreducible]

def UInt64.fast_log2 (n : UInt64) :

Equations

n.fast_log2 = { toBitVec := { toFin := ⟨(↑n.toFin).log2, ⋯⟩ } }

Instances For

@[simp, csimp]

theorem UInt64.fast_log2_eq :

fast_log2 = log2