mathlib documentation

data.nat.bitwise

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 #

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]
@[simp]
@[simp]
theorem nat.bit_eq_zero {n : } {b : bool} :
nat.bit b n = 0 n = 0 b = bool.ff
theorem nat.zero_of_test_bit_eq_ff {n : } (h : ∀ (i : ), n.test_bit i = bool.ff) :
n = 0
@[simp]
theorem nat.zero_test_bit (i : ) :
theorem nat.test_bit_eq_inth (n i : ) :

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

theorem nat.eq_of_test_bit_eq {n m : } (h : ∀ (i : ), n.test_bit i = m.test_bit 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 : ), n.test_bit i = bool.tt ∀ (j : ), i < jn.test_bit j = bool.ff
theorem nat.lt_of_test_bit {n m : } (i : ) (hn : n.test_bit i = bool.ff) (hm : m.test_bit i = bool.tt) (hnm : ∀ (j : ), i < jn.test_bit j = m.test_bit j) :
n < m
@[simp]
theorem nat.test_bit_two_pow_self (n : ) :
theorem nat.test_bit_two_pow_of_ne {n m : } (hm : n m) :
theorem nat.test_bit_two_pow (n m : ) :
theorem nat.bitwise_comm {f : boolboolbool} (hf : ∀ (b b' : bool), f b b' = f b' b) (hf' : f bool.ff bool.ff = bool.ff) (n m : ) :

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

theorem nat.lor_comm (n m : ) :
n.lor m = m.lor n
theorem nat.land_comm (n m : ) :
n.land m = m.land n
theorem nat.lxor_comm (n m : ) :
n.lxor m = m.lxor n
@[simp]
theorem nat.zero_lxor (n : ) :
0.lxor n = n
@[simp]
theorem nat.lxor_zero (n : ) :
n.lxor 0 = n
@[simp]
theorem nat.zero_land (n : ) :
0.land n = 0
@[simp]
theorem nat.land_zero (n : ) :
n.land 0 = 0
@[simp]
theorem nat.zero_lor (n : ) :
0.lor n = n
@[simp]
theorem nat.lor_zero (n : ) :
n.lor 0 = n

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.

theorem nat.lxor_assoc (n m k : ) :
(n.lxor m).lxor k = n.lxor (m.lxor k)
theorem nat.land_assoc (n m k : ) :
(n.land m).land k = n.land (m.land k)
theorem nat.lor_assoc (n m k : ) :
(n.lor m).lor k = n.lor (m.lor k)
@[simp]
theorem nat.lxor_self (n : ) :
n.lxor n = 0
theorem nat.lxor_cancel_right (n m : ) :
(m.lxor n).lxor n = m
theorem nat.lxor_cancel_left (n m : ) :
n.lxor (n.lxor m) = m
theorem nat.lxor_left_injective {n : } :
function.injective (λ (m : ), m.lxor n)
@[simp]
theorem nat.lxor_right_inj {n m m' : } :
n.lxor m = n.lxor m' m = m'
@[simp]
theorem nat.lxor_left_inj {n m m' : } :
m.lxor n = m'.lxor n m = m'
@[simp]
theorem nat.lxor_eq_zero {n m : } :
n.lxor m = 0 n = m
theorem nat.lxor_ne_zero {n m : } :
n.lxor m 0 n m
theorem nat.lxor_trichotomy {a b c : } (h : a b.lxor c) :
b.lxor c < a a.lxor c < b a.lxor b < c
theorem nat.lt_lxor_cases {a b c : } (h : a < b.lxor c) :
a.lxor c < b a.lxor b < c