Bit operations on natural numbers

Naming convention:

• ..._getBit_1 or _eq_one : the value of getBit is 1 at the specified bit(s)
• getBit_of_... : the value of getBit is the value of the specified bit(s), under some preconditions

@[simp]

theorem ENat.le_floor_NNReal_iff (x : ℕ∞) (y : NNReal) (hx_ne_top : x ≠ ⊤) : x ≤ ↑⌊y⌋₊ ↔ x.toNat ≤ ⌊y⌋₊

theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (↑a)⁻¹ * (↑b)⁻¹ = (↑a * ↑b)⁻¹

theorem ENNReal.coe_le_of_NNRat {a b : ℚ≥0} : ↑a ≤ ↑b ↔ a ≤ b

theorem ENNReal.coe_NNRat_coe_NNReal (x : ℚ≥0) : ↑x = ↑↑x

theorem ENNReal.coe_div_of_NNRat {a b : ℚ≥0} (hb : b ≠ 0) : ↑a / ↑b = ↑(a / b)

theorem ENNReal.coe_Nat_coe_NNRat (x : ℕ) : ↑x = ↑↑x

theorem ENNReal.coe_NNRat_eq_coe_NNRat (x y : ℚ≥0) : ↑x = ↑y ↔ x = y

theorem Nat.max_eq_add_sub {m n : ℕ} : m.max n = m + (n - m)

theorem Nat.sub_add_eq_sub_sub_rev (a b c : ℕ) (h1 : c ≤ b) (h2 : b ≤ a) : a - b + c = a - (b - c)

theorem Nat.cast_gt_Real_one (a : ℕ) (ha : a > 1) : ↑a > 1

theorem Nat.sub_div_two_add_one_le (n k : ℕ) [NeZero n] [NeZero k] (hkn : k ≤ n) : (n - k) / 2 + 1 ≤ n

@[simp]

theorem Nat.lt_add_of_pos_right_of_le (a b c : ℕ) [NeZero c] (h : a ≤ b) : a < b + c

@[simp]

theorem Nat.cast_div_le_div_cast_NNReal (x y : ℕ) : ↑(x / y) ≤ ↑x / ↑y

theorem Nat.two_mul_lt_iff_le_half_of_sub_one (a b : ℕ) (h_b_pos : b > 0) : 2 * a < b ↔ a ≤ (b - 1) / 2

theorem Nat.dvd_of_pow_sub_one_dvd_pow_sub_one {q n d : ℕ} (hq : 1 < q) (h_dvd : q ^ d - 1 ∣ q ^ n - 1) : d ∣ n

Reverse Divisibility of Powers: If q > 1 and q^d - 1 divides q^n - 1, then d must divide n. (This corresponds to the fact that cyclic subgroups are unique).

def Nat.getBit (k n : ℕ) : ℕ

Returns the k-th least significant bit of a natural number n as a natural number (in {0, 1}).

We decompose each number j < 2^ℓ into its binary representation : j = Σ k ∈ Fin ℓ, jₖ * 2ᵏ

theorem Nat.testBit_true_eq_getBit_eq_1 (k n : ℕ) : (n.testBit k = true) = (k.getBit n = 1)

theorem Nat.testBit_eq_getBit (k n : ℕ) : (n.testBit k = true) = (k.getBit n = 1)

theorem Nat.testBit_false_eq_getBit_eq_0 (k n : ℕ) : (n.testBit k = false) = (k.getBit n = 0)

def Nat.popCount (n : ℕ) : ℕ

theorem Nat.getBit_lt_2 {k n : ℕ} : k.getBit n < 2

theorem Nat.getBit_eq_testBit (k n : ℕ) : k.getBit n = if n.testBit k = true then 1 else 0

theorem Nat.getBit_zero_eq_zero {k : ℕ} : k.getBit 0 = 0

theorem Nat.getBit_eq_zero_or_one {k n : ℕ} : k.getBit n = 0 ∨ k.getBit n = 1

theorem Nat.getBit_zero_eq_self {n : ℕ} (h_n : n < 2) : getBit 0 n = n

theorem Nat.getBit_zero_of_two_mul {n : ℕ} : getBit 0 (2 * n) = 0

def Nat.getLowBits (numLowBits n : ℕ) : ℕ

Get the numLowBits least significant bits of n.

theorem Nat.getLowBits_zero_eq_zero {n : ℕ} : getLowBits 0 n = 0

theorem Nat.getLowBits_eq_mod_two_pow {numLowBits : ℕ} (n : ℕ) : numLowBits.getLowBits n = n % 2 ^ numLowBits

theorem Nat.getLowBits_lt_two_pow {n : ℕ} (numLowBits : ℕ) : numLowBits.getLowBits n < 2 ^ numLowBits

theorem Nat.getLowBits_le_self {n : ℕ} (numLowBits : ℕ) : numLowBits.getLowBits n ≤ n

theorem Nat.and_eq_zero_iff {n m : ℕ} : n &&& m = 0 ↔ ∀ (k : ℕ), n >>> k &&& m >>> k = 0

theorem Nat.eq_iff_eq_all_getBits {n m : ℕ} : n = m ↔ ∀ (k : ℕ), k.getBit n = k.getBit m

theorem Nat.shiftRight_and_one_distrib {n m k : ℕ} : k.getBit (n &&& m) = k.getBit n &&& k.getBit m

theorem Nat.and_eq_zero_iff_and_each_getBit_eq_zero {n m : ℕ} : n &&& m = 0 ↔ ∀ (k : ℕ), k.getBit n &&& k.getBit m = 0

theorem Nat.ge_two_pow_of_getBit_1 {n i : ℕ} (h_getBit : i.getBit n = 1) : n ≥ 2 ^ i

theorem Nat.exists_ge_and_getBit_1_of_ge_two_pow {n x : ℕ} (p : x ≥ 2 ^ n) : ∃ i ≥ n, i.getBit x = 1

theorem Nat.getBit_1_of_ge_two_pow_and_lt_two_pow_succ {x i : ℕ} (h_ge_two_pow : x ≥ 2 ^ i) (h_lt_two_pow_succ : x < 2 ^ (i + 1)) : i.getBit x = 1

theorem Nat.getBit_two_pow {i k : ℕ} : k.getBit (2 ^ i) = if (i == k) = true then 1 else 0

theorem Nat.and_two_pow_eq_zero_of_getBit_0 {n i : ℕ} (h_getBit : i.getBit n = 0) : n &&& 2 ^ i = 0

theorem Nat.and_two_pow_eq_two_pow_of_getBit_1 {n i : ℕ} (h_getBit : i.getBit n = 1) : n &&& 2 ^ i = 2 ^ i

theorem Nat.and_two_pow_eq_two_pow_of_getBit_eq_one {n i : ℕ} (h_getBit : i.getBit n = 1) : n &&& 2 ^ i = 2 ^ i

theorem Nat.and_one_eq_of_eq {a b : ℕ} : a = b → a &&& 1 = b &&& 1

theorem Nat.eq_zero_or_eq_one_of_lt_two {n : ℕ} (h_lt : n < 2) : n = 0 ∨ n = 1

theorem Nat.div_2_form {nD2 b : ℕ} (h_b : b < 2) : (nD2 * 2 + b) / 2 = nD2

theorem Nat.and_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2) (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm) : n &&& m = (n1 &&& m1) * 2 + (bn &&& bm)

theorem Nat.xor_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2) (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm) : n ^^^ m = (n1 ^^^ m1) * 2 + (bn ^^^ bm)

theorem Nat.or_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2) (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm) : n ||| m = (n1 ||| m1) * 2 + (bn ||| bm)

theorem Nat.sum_eq_xor_plus_twice_and (n m : ℕ) : n + m = (n ^^^ m) + 2 * (n &&& m)

theorem Nat.add_shiftRight_distrib {n m k : ℕ} (h_and_zero : n &&& m = 0) : (n + m) >>> k = n >>> k + m >>> k

theorem Nat.sum_of_and_eq_zero_is_xor {n m : ℕ} (h_n_AND_m : n &&& m = 0) : n + m = n ^^^ m

theorem Nat.xor_of_and_eq_zero_is_or {n m : ℕ} (h_n_AND_m : n &&& m = 0) : n ^^^ m = n ||| m

theorem Nat.sum_of_and_eq_zero_is_or {n m : ℕ} (h_n_AND_m : n &&& m = 0) : n + m = n ||| m

theorem Nat.xor_eq_sub_iff_submask {n m : ℕ} (h : m ≤ n) : n ^^^ m = n - m ↔ n &&& m = m

theorem Nat.getBit_of_add_distrib {n m k : ℕ} (h_n_AND_m : n &&& m = 0) : k.getBit (n + m) = k.getBit n + k.getBit m

theorem Nat.add_two_pow_of_getBit_eq_zero_lt_two_pow {n m i : ℕ} (h_n : n < 2 ^ m) (h_i : i < m) (h_getBit_at_i_eq_zero : i.getBit n = 0) : n + 2 ^ i < 2 ^ m

theorem Nat.getBit_of_multiple_of_power_of_two {n p : ℕ} (k : ℕ) : k.getBit (2 ^ p * n) = if k < p then 0 else (k - p).getBit n

theorem Nat.getBit_of_shiftLeft {n p : ℕ} (k : ℕ) : k.getBit (n <<< p) = if k < p then 0 else (k - p).getBit n

theorem Nat.getBit_of_shiftRight {n p : ℕ} (k : ℕ) : k.getBit (n >>> p) = (k + p).getBit n

theorem Nat.getBit_of_or {n m k : ℕ} : k.getBit (n ||| m) = k.getBit n ||| k.getBit m

theorem Nat.getBit_of_xor {n m k : ℕ} : k.getBit (n ^^^ m) = k.getBit n ^^^ k.getBit m

theorem Nat.getBit_of_and {n m k : ℕ} : k.getBit (n &&& m) = k.getBit n &&& k.getBit m

theorem Nat.getBit_of_two_pow_sub_one {i k : ℕ} : k.getBit (2 ^ i - 1) = if k < i then 1 else 0

theorem Nat.getBit_of_sub_two_pow_of_bit_1 {n i j : ℕ} (h_getBit_eq_1 : i.getBit n = 1) : j.getBit (n - 2 ^ i) = if j = i then 0 else j.getBit n

theorem Nat.getBit_of_lowBits {n : ℕ} (numLowBits k : ℕ) : k.getBit (numLowBits.getLowBits n) = if k < numLowBits then k.getBit n else 0

theorem Nat.getBit_eq_succ_getBit_of_mul_two {n k : ℕ} : (k + 1).getBit (2 * n) = k.getBit n

theorem Nat.getBit_eq_succ_getBit_of_mul_two_add_one {n k : ℕ} : (k + 1).getBit (2 * n + 1) = k.getBit n

theorem Nat.getBit_eq_pred_getBit_of_div_two {n k : ℕ} (h_k : k > 0) : k.getBit n = (k - 1).getBit (n / 2)

theorem Nat.getBit_repr {ℓ : ℕ} (j : ℕ) : j < 2 ^ ℓ → j = ∑ k ∈ Finset.Icc 0 (ℓ - 1), k.getBit j * 2 ^ k

theorem Nat.getBit_repr_univ {ℓ : ℕ} (j : ℕ) : j < 2 ^ ℓ → j = ∑ k : Fin ℓ, (↑k).getBit j * 2 ^ ↑k

theorem Nat.getLowBits_succ {n : ℕ} (numLowBits : ℕ) : (numLowBits + 1).getLowBits n = numLowBits.getLowBits n + numLowBits.getBit n <<< numLowBits

def Nat.getHighBits_no_shl (numLowBits n : ℕ) : ℕ

This takes a argument for the number of lowBitss to remove from the number

def Nat.getHighBits (numLowBits n : ℕ) : ℕ

theorem Nat.and_highBits_lowBits_eq_zero {n : ℕ} (numLowBits : ℕ) : numLowBits.getHighBits n &&& numLowBits.getLowBits n = 0

theorem Nat.num_eq_highBits_add_lowBits {n : ℕ} (numLowBits : ℕ) : n = numLowBits.getHighBits n + numLowBits.getLowBits n

theorem Nat.num_eq_highBits_xor_lowBits {n : ℕ} (numLowBits : ℕ) : n = numLowBits.getHighBits n ^^^ numLowBits.getLowBits n

theorem Nat.getBit_of_highBits {n : ℕ} (numLowBits k : ℕ) : k.getBit (numLowBits.getHighBits n) = if k < numLowBits then 0 else k.getBit n

theorem Nat.getBit_of_highBits_no_shl {n : ℕ} (numLowBits k : ℕ) : k.getBit (numLowBits.getHighBits_no_shl n) = (k + numLowBits).getBit n

theorem Nat.getBit_of_lt_two_pow {n : ℕ} (a : Fin (2 ^ n)) (k : ℕ) : k.getBit ↑a = if k < n then k.getBit ↑a else 0

theorem Nat.exist_bit_diff_if_diff {n : ℕ} (a b : Fin (2 ^ n)) (h_a_ne_b : a ≠ b) : ∃ (k : Fin n), (↑k).getBit ↑a ≠ (↑k).getBit ↑b

def Nat.binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary : ∀ (j : Fin n), m j ≤ 1) : Fin (2 ^ n)

theorem Nat.getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary : ∀ (j : Fin n), m j ≤ 1) (k : ℕ) : k.getBit ↑(binaryFinMapToNat m h_binary) = if h_k : k < n then m ⟨k, h_k⟩ else 0

def Nat.getMiddleBits (offset len n : ℕ) : ℕ

Middle bits: take len bits starting at offset from n.

theorem Nat.getBit_of_middleBits {n offset len k : ℕ} : k.getBit (offset.getMiddleBits len n) = if k < len then (k + offset).getBit n else 0

Bit-level characterization of middle bits.

theorem Nat.getMiddleBits_lt_two_pow {n offset len : ℕ} : offset.getMiddleBits len n < 2 ^ len

Middle bits are strictly less than 2^len.

theorem Nat.getMiddleBits_eq_mod {n offset len : ℕ} : offset.getMiddleBits len n = n >>> offset % 2 ^ len

Middle bits as a modulus form.

theorem Nat.and_shl_eq_zero_of_lt_two_pow {a n b : ℕ} (hb : b < 2 ^ n) : a <<< n &&& b = 0

def Nat.joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : Fin (2 ^ (m + n))

Concatenate high (length m) and low (length n) using shifts.

theorem Nat.getBit_joinBits {n m k : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : k.getBit ↑(joinBits low high) = if k < n then k.getBit ↑low else (k - n).getBit ↑high

Bit characterization: below cut use low, above cut use high.

theorem Nat.getLowBits_joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : n.getLowBits ↑(joinBits low high) = ↑low

Low n bits of joinBits are exactly low.

theorem Nat.getHighBits_no_shl_joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) : n.getHighBits_no_shl ↑(joinBits low high) = ↑high

Dropping low n bits by shifting right recovers high.