Correctness and size of finite-alphabet codes

Delimited unary parsing is exact. Its codeword lengths are bounded by an alphabet-dependent constant and its palindromic framing commutes with reversal.

theorem Complexity.FiniteAlphabetCode.encode_nil {α : Type} (c : FiniteAlphabetCode α) : c.encode [] = []

theorem Complexity.FiniteAlphabetCode.encode_cons {α : Type} (c : FiniteAlphabetCode α) (a : α) (w : List α) : c.encode (a :: w) = c.symbol a ++ c.encode w

theorem Complexity.FiniteAlphabetCode.symbol_length {α : Type} (c : FiniteAlphabetCode α) (a : α) : (c.symbol a).length = ↑(c.index a) + 2

theorem Complexity.FiniteAlphabetCode.decodeFrom_trues {α : Type} (c : FiniteAlphabetCode α) (i k : ℕ) (h : i + k < c.size) (rest : List Bool) : c.decodeFrom (some i) (List.replicate k true ++ rest) = c.decodeFrom (some (i + k)) rest

theorem Complexity.FiniteAlphabetCode.decodeFrom_symbol {α : Type} (c : FiniteAlphabetCode α) (a : α) (rest : List Bool) : c.decodeFrom none (c.symbol a ++ rest) = Option.map (fun (x : List α) => a :: x) (c.decodeFrom none rest)

theorem Complexity.FiniteAlphabetCode.decode_encode_proof {α : Type} (c : FiniteAlphabetCode α) (w : List α) : c.decode (c.encode w) = some w

theorem Complexity.FiniteAlphabetCode.encode_length_lower {α : Type} (c : FiniteAlphabetCode α) (w : List α) : w.length ≤ (c.encode w).length

theorem Complexity.FiniteAlphabetCode.encode_length_upper {α : Type} (c : FiniteAlphabetCode α) (w : List α) : (c.encode w).length ≤ (c.size + 1) * w.length

theorem Complexity.FiniteAlphabetCode.symbol_reverse {α : Type} (c : FiniteAlphabetCode α) (a : α) : (c.symbol a).reverse = c.symbol a

theorem Complexity.FiniteAlphabetCode.encode_append {α : Type} (c : FiniteAlphabetCode α) (xs ys : List α) : c.encode (xs ++ ys) = c.encode xs ++ c.encode ys

theorem Complexity.FiniteAlphabetCode.encode_reverse {α : Type} (c : FiniteAlphabetCode α) (w : List α) : c.encode w.reverse = (c.encode w).reverse

theorem Complexity.FiniteAlphabetCode.encode_count_false {α : Type} (c : FiniteAlphabetCode α) (w : List α) : List.count false (c.encode w) = 2 * w.length

def Complexity.FiniteAlphabetCode.pendingPrefix : Option ℕ → List Bool

Prefix already consumed when the parser is inside a codeword.

Equations

• Complexity.FiniteAlphabetCode.pendingPrefix none = []
• Complexity.FiniteAlphabetCode.pendingPrefix (some i) = false :: List.replicate i true

theorem Complexity.FiniteAlphabetCode.decodeFrom_exact {α : Type} (c : FiniteAlphabetCode α) (bits : List Bool) (pending : Option ℕ) (w : List α) (h : c.decodeFrom pending bits = some w) : pendingPrefix pending ++ bits = c.encode w

theorem Complexity.FiniteAlphabetCode.encode_decode_proof {α : Type} (c : FiniteAlphabetCode α) {bits : List Bool} {w : List α} (h : c.decode bits = some w) : c.encode w = bits

theorem Complexity.FiniteAlphabetCode.decode_reverse {α : Type} (c : FiniteAlphabetCode α) (bits : List Bool) : c.decode bits.reverse = Option.map List.reverse (c.decode bits)