Recovering a natural number from its binary digits

The digits returned by Nat.bits are least significant first. Folding Nat.bit from the right with initial value zero reconstructs the original number.

Main results

• Nat.bits_eq_nil_iff: a natural has no binary digits exactly when it is zero.
• Nat.foldr_bit_bits: folding Nat.bit over the binary representation of n gives n.
• Nat.foldr_bit_lt, Nat.foldr_bit_testBit: fixed-width little-endian reconstruction.
• Nat.foldr_bit_one_ne_zero, Nat.bits_foldr_bit_one, Nat.foldr_bit_one_lt: reconstruction with base value 1, producing a positive number whose binary digits end in true.
• Nat.foldr_bit_ofFn: reconstruction is the sum of the digits' binary place values.
• Nat.size_div_two_add_one: halving a positive number removes one binary digit.

theorem Nat.bits_eq_nil_iff {n : ℕ} : n.bits = [] ↔ n = 0

The binary digit list of n is empty if and only if n = 0.

theorem Nat.foldr_bit_ofFn {w : ℕ} (bits : Fin w → Bool) : List.foldr bit 0 (List.ofFn bits) = ∑ k : Fin w, (bits k).toNat * 2 ^ ↑k

Reconstructing a finite little-endian word sums the digits' binary place values.

@[simp]

theorem Nat.foldr_bit_bits (n : ℕ) : List.foldr bit 0 n.bits = n

Folding Nat.bit over the binary representation of n gives back n.

theorem Nat.foldr_bit_lt (l : List Bool) : List.foldr bit 0 l < 2 ^ l.length

A little-endian word represents a natural below the power of two given by its length.

theorem Nat.foldr_bit_one_ne_zero (w : List Bool) : List.foldr bit 1 w ≠ 0

Folding Nat.bit with base 1 over any word gives a positive number.

theorem Nat.bits_foldr_bit_one (w : List Bool) : (List.foldr bit 1 w).bits = w ++ [true]

Folding Nat.bit with base 1 appends true to the binary representation.

theorem Nat.foldr_bit_one_lt (w : List Bool) : List.foldr bit 1 w < 2 ^ (w.length + 1)

Folding Nat.bit with base 1 produces a number strictly below 2 ^ (|w| + 1).

theorem Nat.foldr_bit_testBit {n K : ℕ} (h : n.size ≤ K) : List.foldr bit 0 (List.map n.testBit (List.range K)) = n

Reading enough low-order digits recovers the natural, including its leading zero digits.

theorem Nat.size_div_two_add_one {n : ℕ} (hn : n ≠ 0) : (n / 2).size + 1 = n.size

Halving a positive number removes one binary digit.