Bitwise operations on natural numbers

In the first half of this file, we provide theorems for reasoning about natural numbers from their bitwise properties. In the second half of this file, we show properties of the bitwise operations lor', land' and lxor', which are defined in core.

Main results

• eq_of_testBit_eq: two natural numbers are equal if they have equal bits at every position.
• exists_most_significant_bit: if n ≠ 0, then there is some position i that contains the most significant 1-bit of n.
• lt_of_testBit: if n and m are numbers and i is a position such that the i-th bit of of n is zero, the i-th bit of m is one, and all more significant bits are equal, then n < m.

Future work

There is another way to express bitwise properties of natural number: digits 2. The two ways should be connected.

Keywords

bitwise, and, or, xor

@[simp]

theorem Nat.bit_false : Nat.bit false = bit0

@[simp]

theorem Nat.bit_true : Nat.bit true = bit1

@[simp]

theorem Nat.bit_eq_zero {n : ℕ} {b : Bool} : Nat.bit b n = 0 ↔ n = 0 ∧ b = false

theorem Nat.zero_of_testBit_eq_false {n : ℕ} (h : ∀ (i : ℕ), Nat.testBit n i = false) : n = 0

@[simp]

theorem Nat.zero_testBit (i : ℕ) : Nat.testBit 0 i = false

theorem Nat.testBit_eq_inth (n : ℕ) (i : ℕ) : Nat.testBit n i = List.getI (Nat.bits n) i

The ith bit is the ith element of n.bits.

theorem Nat.eq_of_testBit_eq {n : ℕ} {m : ℕ} (h : ∀ (i : ℕ), Nat.testBit n i = Nat.testBit m i) : n = m

Bitwise extensionality: Two numbers agree if they agree at every bit position.

theorem Nat.exists_most_significant_bit {n : ℕ} (h : n ≠ 0) : ∃ i, Nat.testBit n i = true ∧ ∀ (j : ℕ), i < j → Nat.testBit n j = false

theorem Nat.lt_of_testBit {n : ℕ} {m : ℕ} (i : ℕ) (hn : Nat.testBit n i = false) (hm : Nat.testBit m i = true) (hnm : ∀ (j : ℕ), i < j → Nat.testBit n j = Nat.testBit m j) : n < m

@[simp]

theorem Nat.testBit_two_pow_self (n : ℕ) : Nat.testBit (2 ^ n) n = true

theorem Nat.testBit_two_pow_of_ne {n : ℕ} {m : ℕ} (hm : n ≠ m) : Nat.testBit (2 ^ n) m = false

theorem Nat.testBit_two_pow (n : ℕ) (m : ℕ) : (Nat.testBit (2 ^ n) m = true) = (n = m)

theorem Nat.bitwise'_comm {f : Bool → Bool → Bool} (hf : ∀ (b b' : Bool), f b b' = f b' b) (hf' : f false false = false) (n : ℕ) (m : ℕ) : Nat.bitwise' f n m = Nat.bitwise' f m n

If f is a commutative operation on bools such that f false false = false, then bitwise f is also commutative.

theorem Nat.lor'_comm (n : ℕ) (m : ℕ) : Nat.lor' n m = Nat.lor' m n

theorem Nat.land'_comm (n : ℕ) (m : ℕ) : Nat.land' n m = Nat.land' m n

theorem Nat.lxor'_comm (n : ℕ) (m : ℕ) : Nat.lxor' n m = Nat.lxor' m n

@[simp]

theorem Nat.zero_lxor' (n : ℕ) : Nat.lxor' 0 n = n

@[simp]

theorem Nat.lxor'_zero (n : ℕ) : Nat.lxor' n 0 = n

@[simp]

theorem Nat.zero_land' (n : ℕ) : Nat.land' 0 n = 0

@[simp]

theorem Nat.land'_zero (n : ℕ) : Nat.land' n 0 = 0

@[simp]

theorem Nat.zero_lor' (n : ℕ) : Nat.lor' 0 n = n

@[simp]

theorem Nat.lor'_zero (n : ℕ) : Nat.lor' n 0 = n

def Nat.tacticBitwise_assoc_tac : Lean.ParserDescr

Proving associativity of bitwise operations in general essentially boils down to a huge case distinction, so it is shorter to use this tactic instead of proving it in the general case.

Equations

• Nat.tacticBitwise_assoc_tac = Lean.ParserDescr.node `Nat.tacticBitwise_assoc_tac 1024 (Lean.ParserDescr.nonReservedSymbol "bitwise_assoc_tac" false)

theorem Nat.lxor'_assoc (n : ℕ) (m : ℕ) (k : ℕ) : Nat.lxor' (Nat.lxor' n m) k = Nat.lxor' n (Nat.lxor' m k)

theorem Nat.land'_assoc (n : ℕ) (m : ℕ) (k : ℕ) : Nat.land' (Nat.land' n m) k = Nat.land' n (Nat.land' m k)

theorem Nat.lor'_assoc (n : ℕ) (m : ℕ) (k : ℕ) : Nat.lor' (Nat.lor' n m) k = Nat.lor' n (Nat.lor' m k)

@[simp]

theorem Nat.lxor'_self (n : ℕ) : Nat.lxor' n n = 0

theorem Nat.lxor_cancel_right (n : ℕ) (m : ℕ) : Nat.lxor' (Nat.lxor' m n) n = m

theorem Nat.lxor'_cancel_left (n : ℕ) (m : ℕ) : Nat.lxor' n (Nat.lxor' n m) = m

theorem Nat.lxor'_right_injective {n : ℕ} : Function.Injective (Nat.lxor' n)

theorem Nat.lxor'_left_injective {n : ℕ} : Function.Injective fun m => Nat.lxor' m n

@[simp]

theorem Nat.lxor'_right_inj {n : ℕ} {m : ℕ} {m' : ℕ} : Nat.lxor' n m = Nat.lxor' n m' ↔ m = m'

@[simp]

theorem Nat.lxor'_left_inj {n : ℕ} {m : ℕ} {m' : ℕ} : Nat.lxor' m n = Nat.lxor' m' n ↔ m = m'

@[simp]

theorem Nat.lxor'_eq_zero {n : ℕ} {m : ℕ} : Nat.lxor' n m = 0 ↔ n = m

theorem Nat.lxor'_ne_zero {n : ℕ} {m : ℕ} : Nat.lxor' n m ≠ 0 ↔ n ≠ m

theorem Nat.lxor'_trichotomy {a : ℕ} {b : ℕ} {c : ℕ} (h : a ≠ Nat.lxor' b c) : Nat.lxor' b c < a ∨ Nat.lxor' a c < b ∨ Nat.lxor' a b < c

theorem Nat.lt_lxor'_cases {a : ℕ} {b : ℕ} {c : ℕ} (h : a < Nat.lxor' b c) : Nat.lxor' a c < b ∨ Nat.lxor' a b < c