Bitwise operations on integers

Possibly only of archaeological significance.

Recursors

• Int.bitCasesOn: Parity disjunction. Something is true/defined on ℤ if it's true/defined for even and for odd values.

def Int.div2 : ℤ → ℤ

div2 n = n/2

Equations

• (Int.ofNat n).div2 = ↑n.div2
• (Int.negSucc n).div2 = Int.negSucc n.div2

def Int.bodd : ℤ → Bool

bodd n returns true if n is odd

Equations

• (Int.ofNat n).bodd = n.bodd
• (Int.negSucc n).bodd = !n.bodd

def Int.bit (b : Bool) : ℤ → ℤ

bit b appends the digit b to the binary representation of its integer input.

Equations

• Int.bit b = bif b then fun (x : ℤ) => 2 * x + 1 else fun (x : ℤ) => 2 * x

def Int.natBitwise (f : Bool → Bool → Bool) (m n : ℕ) : ℤ

Int.natBitwise is an auxiliary definition for Int.bitwise.

Equations

• Int.natBitwise f m n = bif f false false then Int.negSucc (Nat.bitwise (fun (x y : Bool) => !f x y) m n) else ↑(Nat.bitwise f m n)

def Int.bitwise (f : Bool → Bool → Bool) : ℤ → ℤ → ℤ

Int.bitwise applies the function f to pairs of bits in the same position in the binary representations of its inputs.

Equations

• Int.bitwise f (Int.ofNat m) (Int.ofNat n) = Int.natBitwise f m n
• Int.bitwise f (Int.ofNat m) (Int.negSucc n) = Int.natBitwise (fun (x y : Bool) => f x !y) m n
• Int.bitwise f (Int.negSucc m) (Int.ofNat n) = Int.natBitwise (fun (x y : Bool) => f (!x) y) m n
• Int.bitwise f (Int.negSucc m) (Int.negSucc n) = Int.natBitwise (fun (x y : Bool) => f (!x) !y) m n

def Int.lnot : ℤ → ℤ

lnot flips all the bits in the binary representation of its input

Equations

• (Int.ofNat n).lnot = Int.negSucc n
• (Int.negSucc n).lnot = ↑n

def Int.lor : ℤ → ℤ → ℤ

lor takes two integers and returns their bitwise or

Equations

• (Int.ofNat m).lor (Int.ofNat n) = ↑(m ||| n)
• (Int.ofNat m).lor (Int.negSucc n) = Int.negSucc (n.ldiff m)
• (Int.negSucc m).lor (Int.ofNat n) = Int.negSucc (m.ldiff n)
• (Int.negSucc m).lor (Int.negSucc n) = Int.negSucc (m &&& n)

def Int.land : ℤ → ℤ → ℤ

land takes two integers and returns their bitwise and

Equations

• (Int.ofNat m).land (Int.ofNat n) = ↑(m &&& n)
• (Int.ofNat m).land (Int.negSucc n) = ↑(m.ldiff n)
• (Int.negSucc m).land (Int.ofNat n) = ↑(n.ldiff m)
• (Int.negSucc m).land (Int.negSucc n) = Int.negSucc (m ||| n)

def Int.ldiff : ℤ → ℤ → ℤ

ldiff a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

Equations

• (Int.ofNat m).ldiff (Int.ofNat n) = ↑(m.ldiff n)
• (Int.ofNat m).ldiff (Int.negSucc n) = ↑(m &&& n)
• (Int.negSucc m).ldiff (Int.ofNat n) = Int.negSucc (m ||| n)
• (Int.negSucc m).ldiff (Int.negSucc n) = ↑(n.ldiff m)

def Int.xor : ℤ → ℤ → ℤ

xor computes the bitwise xor of two natural numbers

Equations

• (Int.ofNat m).xor (Int.ofNat n) = ↑(m ^^^ n)
• (Int.ofNat m).xor (Int.negSucc n) = Int.negSucc (m ^^^ n)
• (Int.negSucc m).xor (Int.ofNat n) = Int.negSucc (m ^^^ n)
• (Int.negSucc m).xor (Int.negSucc n) = ↑(m ^^^ n)

instance Int.instShiftLeft_mathlib : ShiftLeft ℤ

m <<< n produces an integer whose binary representation is obtained by left-shifting the binary representation of m by n places

Equations

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

instance Int.instShiftRight_mathlib : ShiftRight ℤ

m >>> n produces an integer whose binary representation is obtained by right-shifting the binary representation of m by n places

Equations

• Int.instShiftRight_mathlib = { shiftRight := fun (m n : ℤ) => m <<< (-n) }

bitwise ops

@[simp]

theorem Int.bodd_zero : bodd 0 = false

@[simp]

theorem Int.bodd_one : bodd 1 = true

theorem Int.bodd_two : bodd 2 = false

@[simp]

theorem Int.bodd_coe (n : ℕ) : (↑n).bodd = n.bodd

@[simp]

theorem Int.bodd_subNatNat (m n : ℕ) : (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

@[simp]

theorem Int.bodd_negOfNat (n : ℕ) : (negOfNat n).bodd = n.bodd

@[simp]

theorem Int.bodd_neg (n : ℤ) : (-n).bodd = n.bodd

@[simp]

theorem Int.bodd_add (m n : ℤ) : (m + n).bodd = (m.bodd ^^ n.bodd)

@[simp]

theorem Int.bodd_mul (m n : ℤ) : (m * n).bodd = (m.bodd && n.bodd)

theorem Int.bodd_add_div2 (n : ℤ) : (bif n.bodd then 1 else 0) + 2 * n.div2 = n

theorem Int.div2_val (n : ℤ) : n.div2 = n / 2

theorem Int.bit_val (b : Bool) (n : ℤ) : bit b n = 2 * n + bif b then 1 else 0

theorem Int.bit_decomp (n : ℤ) : bit n.bodd n.div2 = n

def Int.bitCasesOn {C : ℤ → Sort u} (n : ℤ) (h : (b : Bool) → (n : ℤ) → C (bit b n)) : C n

Defines a function from ℤ conditionally, if it is defined for odd and even integers separately using bit.

Equations

• n.bitCasesOn h = ⋯.mpr (h n.bodd n.div2)

@[simp]

theorem Int.bit_zero : bit false 0 = 0

@[simp]

theorem Int.bit_coe_nat (b : Bool) (n : ℕ) : bit b ↑n = ↑(Nat.bit b n)

@[simp]

theorem Int.bit_negSucc (b : Bool) (n : ℕ) : bit b (negSucc n) = negSucc (Nat.bit (!b) n)

@[simp]

theorem Int.bodd_bit (b : Bool) (n : ℤ) : (bit b n).bodd = b

@[simp]

theorem Int.testBit_bit_zero (b : Bool) (n : ℤ) : (bit b n).testBit 0 = b

@[simp]

theorem Int.testBit_bit_succ (m : ℕ) (b : Bool) (n : ℤ) : (bit b n).testBit m.succ = n.testBit m

theorem Int.bitwise_or : bitwise or = lor

theorem Int.bitwise_and : bitwise and = land

theorem Int.bitwise_diff : (bitwise fun (a b : Bool) => a && !b) = ldiff

theorem Int.bitwise_xor : bitwise xor = Int.xor

@[simp]

theorem Int.bitwise_bit (f : Bool → Bool → Bool) (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) : bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

@[simp]

theorem Int.lor_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) : (bit a m).lor (bit b n) = bit (a || b) (m.lor n)

@[simp]

theorem Int.land_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) : (bit a m).land (bit b n) = bit (a && b) (m.land n)

@[simp]

theorem Int.ldiff_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) : (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

@[simp]

theorem Int.lxor_bit (a : Bool) (m : ℤ) (b : Bool) (n : ℤ) : (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)

@[simp]

theorem Int.lnot_bit (b : Bool) (n : ℤ) : (bit b n).lnot = bit (!b) n.lnot

@[simp]

theorem Int.testBit_bitwise (f : Bool → Bool → Bool) (m n : ℤ) (k : ℕ) : (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

@[simp]

theorem Int.testBit_lor (m n : ℤ) (k : ℕ) : (m.lor n).testBit k = (m.testBit k || n.testBit k)

@[simp]

theorem Int.testBit_land (m n : ℤ) (k : ℕ) : (m.land n).testBit k = (m.testBit k && n.testBit k)

@[simp]

theorem Int.testBit_ldiff (m n : ℤ) (k : ℕ) : (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)

@[simp]

theorem Int.testBit_lxor (m n : ℤ) (k : ℕ) : (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)

@[simp]

theorem Int.testBit_lnot (n : ℤ) (k : ℕ) : n.lnot.testBit k = !n.testBit k

@[simp]

theorem Int.shiftLeft_neg (m n : ℤ) : m <<< (-n) = m >>> n

@[simp]

theorem Int.shiftRight_neg (m n : ℤ) : m >>> (-n) = m <<< n

@[simp]

theorem Int.shiftLeft_coe_nat (m n : ℕ) : ↑m <<< ↑n = ↑(m <<< n)

@[simp]

theorem Int.shiftRight_coe_nat (m n : ℕ) : ↑m >>> ↑n = ↑(m >>> n)

@[simp]

theorem Int.shiftLeft_negSucc (m n : ℕ) : negSucc m <<< ↑n = negSucc (Nat.shiftLeft' true m n)

@[simp]

theorem Int.shiftRight_negSucc (m n : ℕ) : negSucc m >>> ↑n = negSucc (m >>> n)

theorem Int.shiftRight_add' (m : ℤ) (n k : ℕ) : m >>> (↑n + ↑k) = m >>> ↑n >>> ↑k

Compare with Int.shiftRight_add, which doesn't have the coercions ℕ → ℤ.

bitwise ops

theorem Int.shiftLeft_add (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (↑n + k) = m <<< ↑n <<< k

theorem Int.shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (↑n - k) = m <<< ↑n >>> k

theorem Int.shiftLeft_eq_mul_pow (m : ℤ) (n : ℕ) : m <<< ↑n = m * ↑(2 ^ n)

theorem Int.one_shiftLeft (n : ℕ) : 1 <<< ↑n = ↑(2 ^ n)

@[simp]

theorem Int.zero_shiftLeft (n : ℤ) : 0 <<< n = 0

@[simp]

theorem Int.zero_shiftRight' (n : ℤ) : 0 >>> n = 0

Compare with Int.zero_shiftRight, which has n : ℕ.