Binary digits by repeated halving

Halving a number n repeatedly and recording the parity of each nonzero intermediate value yields the little-endian binary digits n.bits. A machine that halves a unary counter once per round and emits one bit per round therefore writes n in binary, and stops emitting once the counter reaches zero, so any number of rounds at least n suffices.

Main results

• Nat.bits_of_pos: the binary digits of a positive number are its parity followed by the binary digits of its half.
• Nat.iterate_div: dividing by b i times divides by b ^ i.
• Nat.flatten_map_range_halfBit: for n ≤ m, emitting the parity of every nonzero value among the first m halvings of n produces n.bits.

theorem Nat.bits_of_pos {q : ℕ} (hq : 0 < q) : q.bits = decide (q % 2 = 1) :: (q / 2).bits

The binary digits of a positive number: its remainder by two, then those of its half.

theorem Nat.iterate_div (b n i : ℕ) : (fun (x : ℕ) => x / b)^[i] n = n / b ^ i

Dividing by b i times divides by b ^ i.

def Nat.halfBit (k : ℕ) : List Bool

The bit a halving machine emits at the value k: nothing at zero, else the parity of k.

theorem Nat.flatten_map_range_halfBit {n m : ℕ} (h : n ≤ m) : (List.map (fun (i : ℕ) => ((fun (x : ℕ) => x / 2)^[i] n).halfBit) (List.range m)).flatten = n.bits

Binary digits by repeated halving. If n ≤ m, emitting halfBit of each of the first m values n, n / 2, n / 4, … writes the little-endian binary digits of n.