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.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_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.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_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.