Fixed-width binary encodings of natural numbers

Big-endian, fixed-width binary encoding Nat.toBits with its exact decoder Nat.fromBits and round-trip lemmas. Values wider than the target width are truncated modulo 2 ^ w.

This file lives in Complexitylib/Mathlib/ because it extends a Mathlib type in its home (root) namespace — the sanctioned exception to the Complexity root-namespace rule. Its contents are candidates for upstreaming to Mathlib.

def Nat.toBits : ℕ → ℕ → List Bool

Encode a natural number as a big-endian binary list of exactly w bits. Numbers larger than 2^w - 1 are truncated (mod 2^w).

Equations

• Nat.toBits 0 x✝ = []
• w.succ.toBits x✝ = (x✝ / 2 ^ w % 2 == 1) :: w.toBits x✝

theorem Nat.length_toBits (w val : ℕ) : (w.toBits val).length = w

def Nat.fromBits : List Bool → ℕ

Decode a big-endian binary list to a natural number.

Equations

• Nat.fromBits [] = 0
• Nat.fromBits (b :: rest) = (if b = true then 1 else 0) * 2 ^ rest.length + Nat.fromBits rest

theorem Nat.fromBits_lt_pow_length (l : List Bool) : fromBits l < 2 ^ l.length

Decoded values are bounded by 2 ^ length.

theorem Nat.fromBits_toBits_mod (w val : ℕ) : fromBits (w.toBits val) = val % 2 ^ w

fromBits ∘ toBits w reduces any input modulo 2 ^ w.

theorem Nat.fromBits_toBits {w val : ℕ} (hv : val < 2 ^ w) : fromBits (w.toBits val) = val

Nat.fromBits is a left inverse of Nat.toBits on values below 2 ^ w.