1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Encoding
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Prototypes.Computability.BitTree.Scanner public import Mathlib.Data.W.Basic
set_option doc.verso true

Binary trees with bitstrings at the leaves

The W-type of the polynomial X ↦ List Bool + X × X has a direct binary encoding. A fork is 1, a leaf starts with 0, each payload bit b is escaped as 1b, and 0 terminates the payload.

Main definitions

  • Tree is the W-type, with constructors leaf and fork.

  • encode serializes a tree.

  • validBool scans a word once, retaining a mode and a pending-tree count.

Main statements

  • validBool_iff characterizes acceptance by existence of an encoded tree.

  • encode_injective states uniqueness of the encoded tree.

  • length_encode counts the bits in the representation.

Tags

binary tree, bitstring, encoding, recognizer, W-type

@[expose] public sectionnamespace Geb.BitTree

Node shapes: a labelled leaf or a binary fork.

abbrev Shape := Option (List Bool)

Leaves have no children; forks have two children indexed by booleans.

def Arity : Shape → Type | some _ => Empty | none => Bool

The initial algebra of X ↦ List Bool + X × X.

abbrev Tree := WType Arity

A leaf carrying a bitstring.

def leaf (s : List Bool) : Tree := WType.mk (some s) Empty.elim

A binary fork, with the left child indexed by false.

def fork (l r : Tree) : Tree := WType.mk none fun b : Bool ↦ if b then r else l

The two-constructor induction principle of the underlying W-type.

theorem tree_ind {P : Tree → Prop} (hl : ∀ s, P (leaf s)) (hf : ∀ l r, P l → P r → P (fork l r)) : ∀ t, P t := WType.rec fun a f ih ↦ P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)a:Shapef:Arity a → WType Arityih:∀ (a : Arity a), P (f a)⊢ P (WType.mk a f) cases a with P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)s:List Boolf:Arity (some s) → WType Arityih:∀ (a : Arity (some s)), P (f a)⊢ P (WType.mk (some s) f) P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)s:List Boolf:Arity (some s) → WType Arityih:∀ (a : Arity (some s)), P (f a)h:f = Empty.elim⊢ P (WType.mk (some s) f) P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)s:List Boolih:∀ (a : Arity (some s)), P (Empty.elim a)⊢ P (WType.mk (some s) Empty.elim) All goals completed! 🐙 P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)f:Arity none → WType Arityih:∀ (a : Arity none), P (f a)⊢ P (WType.mk none f) P:Tree → Prophl:∀ (s : List Bool), P (leaf s)hf:∀ (l r : Tree), P l → P r → P (fork l r)f:Arity none → WType Arityih:∀ (a : Arity none), P (f a)h:(fun b ↦ if b = true then f true else f false) = f⊢ P (WType.mk none f) All goals completed! 🐙

Escape payload bits and terminate the string.

def encodeString (s : List Bool) : List Bool := s.foldr (fun b w ↦ true :: b :: w) [false]
@[simp] theorem encodeString_nil : encodeString [] = [false] := rfl@[simp] theorem encodeString_cons (b : Bool) (s : List Bool) : encodeString (b :: s) = true :: b :: encodeString s := rfl

Preorder encoding with a mode-dependent code for leaves and their payloads.

def encode : Tree → List Bool := WType.elim (List Bool) fun x ↦ match x with | ⟨some s, _⟩ => false :: encodeString s | ⟨none, f⟩ => true :: (f false ++ f true)
@[simp] theorem encode_leaf (s : List Bool) : encode (leaf s) = false :: encodeString s := rfl@[simp] theorem encode_fork (l r : Tree) : encode (fork l r) = true :: (encode l ++ encode r) := rfl

Scanning an escaped string completes one pending tree.

theorem foldl_encodeString (s : List Bool) (n : Nat) : (encodeString s).foldl step (.string, n) = finish n := List.rec rfl (fun b s ih ↦ s✝:List Booln:ℕb:Bools:List Boolih:List.foldl step (Mode.string, n) (encodeString s) = finish n⊢ List.foldl step (Mode.string, n) (encodeString (b :: s)) = finish n All goals completed! 🐙) s

Scanning one encoded tree completes exactly one pending tree.

theorem foldl_encode (t : Tree) : ∀ n, 0 < n → (encode t).foldl step (.tree, n) = finish n := tree_ind (P := fun t ↦ ∀ n, 0 < n → (encode t).foldl step (.tree, n) = finish n) (fun s n _ ↦ t:Trees:List Booln:ℕx✝:0 < n⊢ List.foldl step (Mode.tree, n) (encode (leaf s)) = finish n All goals completed! 🐙) (fun l r ihl ihr n hn ↦ t:Treel:Treer:Treeihl:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode l) = finish nihr:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode r) = finish nn:ℕhn:0 < n⊢ List.foldl step (Mode.tree, n) (encode (fork l r)) = finish n t:Treel:Treer:Treeihl:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode l) = finish nihr:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode r) = finish nn:ℕhn:0 < n⊢ List.foldl step (List.foldl step (Mode.tree, n + 1) (encode l)) (encode r) = finish n t:Treel:Treer:Treeihl:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode l) = finish nihr:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode r) = finish nn:ℕhn:0 < n⊢ List.foldl step (finish (n + 1)) (encode r) = finish n t:Treel:Treer:Treeihl:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode l) = finish nihr:∀ (n : ℕ), 0 < n → List.foldl step (Mode.tree, n) (encode r) = finish nn:ℕhn:0 < nh:finish (n + 1) = (Mode.tree, n)⊢ List.foldl step (finish (n + 1)) (encode r) = finish n All goals completed! 🐙) t

Every encoded tree is accepted.

@[simp] theorem validBool_encode (t : Tree) : validBool (encode t) = true := t:Tree⊢ validBool (encode t) = true All goals completed! 🐙

An escaped string can be cancelled from a prefix without losing its boundary.

theorem encodeString_append_injective (s : List Bool) : ∀ t u v, encodeString s ++ u = encodeString t ++ v → s = t ∧ u = v := List.rec (fun t u v h ↦ s:List Boolt:List Boolu:List Boolv:List Boolh:encodeString [] ++ u = encodeString t ++ v⊢ [] = t ∧ u = v cases t with s:List Boolu:List Boolv:List Boolh:encodeString [] ++ u = encodeString [] ++ v⊢ [] = [] ∧ u = v All goals completed! 🐙 s:List Boolu:List Boolv:List Boolhead✝:Booltail✝:List Boolh:encodeString [] ++ u = encodeString (head✝ :: tail✝) ++ v⊢ [] = head✝ :: tail✝ ∧ u = v All goals completed! 🐙) (fun b s ih t u v h ↦ s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vt:List Boolu:List Boolv:List Boolh:encodeString (b :: s) ++ u = encodeString t ++ v⊢ b :: s = t ∧ u = v cases t with s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vu:List Boolv:List Boolh:encodeString (b :: s) ++ u = encodeString [] ++ v⊢ b :: s = [] ∧ u = v All goals completed! 🐙 s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vu:List Boolv:List Boolc:Boolt:List Boolh:encodeString (b :: s) ++ u = encodeString (c :: t) ++ v⊢ b :: s = c :: t ∧ u = v s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vu:List Boolv:List Boolc:Boolt:List Boolh:encodeString (b :: s) ++ u = encodeString (c :: t) ++ vhbc:b = chrest:(List.foldr (fun b w ↦ true :: b :: w) [false] s).append u = (List.foldr (fun b w ↦ true :: b :: w) [false] t).append v⊢ b :: s = c :: t ∧ u = v s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vu:List Boolv:List Boolc:Boolt:List Boolh:encodeString (b :: s) ++ u = encodeString (c :: t) ++ vhbc:b = chrest:(List.foldr (fun b w ↦ true :: b :: w) [false] s).append u = (List.foldr (fun b w ↦ true :: b :: w) [false] t).append vhst:s = thuv:u = v⊢ b :: s = c :: t ∧ u = v exact ⟨s✝:List Boolb:Bools:List Boolih:∀ (t u v : List Bool), encodeString s ++ u = encodeString t ++ v → s = t ∧ u = vu:List Boolv:List Boolc:Boolt:List Boolh:encodeString (b :: s) ++ u = encodeString (c :: t) ++ vhbc:b = chrest:(List.foldr (fun b w ↦ true :: b :: w) [false] s).append u = (List.foldr (fun b w ↦ true :: b :: w) [false] t).append vhst:s = thuv:u = v⊢ b :: s = c :: t All goals completed! 🐙, huv⟩) s

An encoded tree determines both its value and its boundary in a longer word.

theorem encode_append_injective (t : Tree) : ∀ t' u v, encode t ++ u = encode t' ++ v → t = t' ∧ u = v := tree_ind (P := fun t ↦ ∀ t' u v, encode t ++ u = encode t' ++ v → t = t' ∧ u = v) (fun s t' ↦ tree_ind (P := fun t' ↦ ∀ u v, encode (leaf s) ++ u = encode t' ++ v → leaf s = t' ∧ u = v) (fun s' u v h ↦ t:Trees:List Boolt':Trees':List Boolu:List Boolv:List Boolh:encode (leaf s) ++ u = encode (leaf s') ++ v⊢ leaf s = leaf s' ∧ u = v t:Trees:List Boolt':Trees':List Boolu:List Boolv:List Boolh:encode (leaf s) ++ u = encode (leaf s') ++ vhs:s = s'huv:u = v⊢ leaf s = leaf s' ∧ u = v All goals completed! 🐙) (fun _ _ _ _ u v h ↦ t:Trees:List Boolt':Treex✝³:Treex✝²:Treex✝¹:∀ (u v : List Bool), encode (leaf s) ++ u = encode x✝³ ++ v → leaf s = x✝³ ∧ u = vx✝:∀ (u v : List Bool), encode (leaf s) ++ u = encode x✝² ++ v → leaf s = x✝² ∧ u = vu:List Boolv:List Boolh:encode (leaf s) ++ u = encode (fork x✝³ x✝²) ++ v⊢ leaf s = fork x✝³ x✝² ∧ u = v All goals completed! 🐙) t') (fun l r ihl ihr t' ↦ tree_ind (P := fun t' ↦ ∀ u v, encode (fork l r) ++ u = encode t' ++ v → fork l r = t' ∧ u = v) (fun _ u v h ↦ t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treex✝:List Boolu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (leaf x✝) ++ v⊢ fork l r = leaf x✝ ∧ u = v All goals completed! 🐙) (fun l' r' _ _ u v h ↦ t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treel':Treer':Treex✝¹:∀ (u v : List Bool), encode (fork l r) ++ u = encode l' ++ v → fork l r = l' ∧ u = vx✝:∀ (u v : List Bool), encode (fork l r) ++ u = encode r' ++ v → fork l r = r' ∧ u = vu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (fork l' r') ++ v⊢ fork l r = fork l' r' ∧ u = v t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treel':Treer':Treex✝¹:∀ (u v : List Bool), encode (fork l r) ++ u = encode l' ++ v → fork l r = l' ∧ u = vx✝:∀ (u v : List Bool), encode (fork l r) ++ u = encode r' ++ v → fork l r = r' ∧ u = vu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (fork l' r') ++ vhe:encode l ++ (encode r ++ u) = encode l' ++ (encode r' ++ v)⊢ fork l r = fork l' r' ∧ u = v t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treel':Treer':Treex✝¹:∀ (u v : List Bool), encode (fork l r) ++ u = encode l' ++ v → fork l r = l' ∧ u = vx✝:∀ (u v : List Bool), encode (fork l r) ++ u = encode r' ++ v → fork l r = r' ∧ u = vu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (fork l' r') ++ vhe:encode l ++ (encode r ++ u) = encode l' ++ (encode r' ++ v)hl:l = l'hr:encode r ++ u = encode r' ++ v⊢ fork l r = fork l' r' ∧ u = v t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treel':Treer':Treex✝¹:∀ (u v : List Bool), encode (fork l r) ++ u = encode l' ++ v → fork l r = l' ∧ u = vx✝:∀ (u v : List Bool), encode (fork l r) ++ u = encode r' ++ v → fork l r = r' ∧ u = vu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (fork l' r') ++ vhe:encode l ++ (encode r ++ u) = encode l' ++ (encode r' ++ v)hl:l = l'hr:encode r ++ u = encode r' ++ vhr':r = r'huv:u = v⊢ fork l r = fork l' r' ∧ u = v exact ⟨t:Treel:Treer:Treeihl:∀ (t' : Tree) (u v : List Bool), encode l ++ u = encode t' ++ v → l = t' ∧ u = vihr:∀ (t' : Tree) (u v : List Bool), encode r ++ u = encode t' ++ v → r = t' ∧ u = vt':Treel':Treer':Treex✝¹:∀ (u v : List Bool), encode (fork l r) ++ u = encode l' ++ v → fork l r = l' ∧ u = vx✝:∀ (u v : List Bool), encode (fork l r) ++ u = encode r' ++ v → fork l r = r' ∧ u = vu:List Boolv:List Boolh:encode (fork l r) ++ u = encode (fork l' r') ++ vhe:encode l ++ (encode r ++ u) = encode l' ++ (encode r' ++ v)hl:l = l'hr:encode r ++ u = encode r' ++ vhr':r = r'huv:u = v⊢ fork l r = fork l' r' All goals completed! 🐙, huv⟩) t') t

The direct binary encoding is injective.

theorem encode_injective : Function.Injective encode := fun t t' h ↦ (encode_append_injective t t' [] [] (t:Treet':Treeh:encode t = encode t'⊢ encode t ++ [] = encode t' ++ [] All goals completed! 🐙)).1

Forest encoding is the concatenation of its component encodings.

def encodeForest (ts : List Tree) : List Bool := ts.flatMap encode

The grammar of the remaining suffix in each scanner mode.

def Completion (s : State) (w : List Bool) : Prop := match s.1 with | .tree => ∃ ts, ts.length = s.2 ∧ w = encodeForest ts | .string => ∃ bs ts, ts.length + 1 = s.2 ∧ w = encodeString bs ++ encodeForest ts | .bit => ∃ b bs ts, ts.length + 1 = s.2 ∧ w = b :: (encodeString bs ++ encodeForest ts) | .done => w = [] | .dead => False

A successful scan supplies a grammatical decomposition of its whole suffix.

theorem completion_of_accept (w : List Bool) : ∀ s, Active s → (w.foldl step s).1 = .done → Completion s w := List.rec (fun s _ h ↦ w:List Bools:Statex✝:Active sh:(List.foldl step s []).1 = Mode.done⊢ Completion s [] w:List Boolm:Moden:ℕx✝:Active (m, n)h:(List.foldl step (m, n) []).1 = Mode.done⊢ Completion (m, n) []; w:List Booln:ℕx✝:Active (Mode.tree, n)h:(List.foldl step (Mode.tree, n) []).1 = Mode.done⊢ Completion (Mode.tree, n) []w:List Booln:ℕx✝:Active (Mode.string, n)h:(List.foldl step (Mode.string, n) []).1 = Mode.done⊢ Completion (Mode.string, n) []w:List Booln:ℕx✝:Active (Mode.bit, n)h:(List.foldl step (Mode.bit, n) []).1 = Mode.done⊢ Completion (Mode.bit, n) []w:List Booln:ℕx✝:Active (Mode.done, n)h:(List.foldl step (Mode.done, n) []).1 = Mode.done⊢ Completion (Mode.done, n) []w:List Booln:ℕx✝:Active (Mode.dead, n)h:(List.foldl step (Mode.dead, n) []).1 = Mode.done⊢ Completion (Mode.dead, n) [] w:List Booln:ℕx✝:Active (Mode.tree, n)h:(List.foldl step (Mode.tree, n) []).1 = Mode.done⊢ Completion (Mode.tree, n) []w:List Booln:ℕx✝:Active (Mode.string, n)h:(List.foldl step (Mode.string, n) []).1 = Mode.done⊢ Completion (Mode.string, n) []w:List Booln:ℕx✝:Active (Mode.bit, n)h:(List.foldl step (Mode.bit, n) []).1 = Mode.done⊢ Completion (Mode.bit, n) []w:List Booln:ℕx✝:Active (Mode.done, n)h:(List.foldl step (Mode.done, n) []).1 = Mode.done⊢ Completion (Mode.done, n) []w:List Booln:ℕx✝:Active (Mode.dead, n)h:(List.foldl step (Mode.dead, n) []).1 = Mode.done⊢ Completion (Mode.dead, n) [] All goals completed! 🐙) (fun b w ih s hs ha ↦ w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s ws:Statehs:Active sha:(List.foldl step s (b :: w)).1 = Mode.done⊢ Completion s (b :: w) w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s ws:Statehs:Active sha:(List.foldl step s (b :: w)).1 = Mode.donehc:Completion (step s b) w⊢ Completion s (b :: w) w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wm:Moden:ℕhs:Active (m, n)ha:(List.foldl step (m, n) (b :: w)).1 = Mode.donehc:Completion (step (m, n) b) w⊢ Completion (m, n) (b :: w) cases m with w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)ha:(List.foldl step (Mode.tree, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.tree, n) b) w⊢ Completion (Mode.tree, n) (b :: w) w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)ha:(List.foldl step (Mode.tree, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.tree, n) b) whn:0 < n⊢ Completion (Mode.tree, n) (b :: w) cases b with w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.tree, n) false) w⊢ Completion (Mode.tree, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (false :: w)).1 = Mode.donebs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.tree, n) false).2hw:w = encodeString bs ++ encodeForest ts⊢ Completion (Mode.tree, n) (false :: w) exact ⟨leaf bs :: ts, ht, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (false :: w)).1 = Mode.donebs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.tree, n) false).2hw:w = encodeString bs ++ encodeForest ts⊢ false :: w = encodeForest (leaf bs :: ts) All goals completed! 🐙⟩ w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donehc:Completion (step (Mode.tree, n) true) w⊢ Completion (Mode.tree, n) (true :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donehc:∃ ts, ts.length = n + 1 ∧ w = encodeForest ts⊢ Completion (Mode.tree, n) (true :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donets:List Treeht:ts.length = n + 1hw:w = encodeForest ts⊢ Completion (Mode.tree, n) (true :: w) cases ts with w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.doneht:[].length = n + 1hw:w = encodeForest []⊢ Completion (Mode.tree, n) (true :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.doneht:[].length = n + 1hw:w = encodeForest []⊢ False w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donehw:w = encodeForest []ht:0 = n + 1⊢ False All goals completed! 🐙 w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treets:List Treeht:(l :: ts).length = n + 1hw:w = encodeForest (l :: ts)⊢ Completion (Mode.tree, n) (true :: w) cases ts with w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treeht:[l].length = n + 1hw:w = encodeForest [l]⊢ Completion (Mode.tree, n) (true :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treeht:[l].length = n + 1hw:w = encodeForest [l]⊢ False w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treehw:w = encodeForest [l]ht:1 = n + 1⊢ False All goals completed! 🐙 w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treer:Treets:List Treeht:(l :: r :: ts).length = n + 1hw:w = encodeForest (l :: r :: ts)⊢ Completion (Mode.tree, n) (true :: w) refine ⟨fork l r :: ts, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treer:Treets:List Treeht:(l :: r :: ts).length = n + 1hw:w = encodeForest (l :: r :: ts)⊢ (fork l r :: ts).length = (Mode.tree, n).2 w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.tree, n)hn:0 < nha:(List.foldl step (Mode.tree, n) (true :: w)).1 = Mode.donel:Treer:Treets:List Treeht:ts.length + 1 + 1 = n + 1hw:w = encodeForest (l :: r :: ts)⊢ ts.length + 1 = n; All goals completed! 🐙, ?_⟩ All goals completed! 🐙 w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) b) w⊢ Completion (Mode.string, n) (b :: w) cases b with w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) w⊢ Completion (Mode.string, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:n = 1⊢ Completion (Mode.string, n) (false :: w)w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1⊢ Completion (Mode.string, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:n = 1⊢ Completion (Mode.string, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:n = 1hw:w = []⊢ Completion (Mode.string, n) (false :: w) exact ⟨[], [], w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:n = 1hw:w = []⊢ [].length + 1 = (Mode.string, n).2 All goals completed! 🐙, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:n = 1hw:w = []⊢ false :: w = encodeString [] ++ encodeForest [] All goals completed! 🐙⟩ w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1⊢ Completion (Mode.string, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1ts:List Treeht:ts.length = n - 1hw:w = encodeForest ts⊢ Completion (Mode.string, n) (false :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1ts:List Treeht:ts.length = n - 1hw:w = encodeForest tshp:0 < (Mode.string, n).2⊢ Completion (Mode.string, n) (false :: w) exact ⟨[], ts, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1ts:List Treeht:ts.length = n - 1hw:w = encodeForest tshp:0 < (Mode.string, n).2⊢ ts.length + 1 = (Mode.string, n).2 All goals completed! 🐙, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (false :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) false) whn:¬n = 1ts:List Treeht:ts.length = n - 1hw:w = encodeForest tshp:0 < (Mode.string, n).2⊢ false :: w = encodeString [] ++ encodeForest ts All goals completed! 🐙⟩ w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (true :: w)).1 = Mode.donehc:Completion (step (Mode.string, n) true) w⊢ Completion (Mode.string, n) (true :: w) w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (true :: w)).1 = Mode.donec:Boolbs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.string, n) true).2hw:w = c :: (encodeString bs ++ encodeForest ts)⊢ Completion (Mode.string, n) (true :: w) exact ⟨c :: bs, ts, ht, w✝:List Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.string, n)ha:(List.foldl step (Mode.string, n) (true :: w)).1 = Mode.donec:Boolbs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.string, n) true).2hw:w = c :: (encodeString bs ++ encodeForest ts)⊢ true :: w = encodeString (c :: bs) ++ encodeForest ts All goals completed! 🐙⟩ w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.bit, n)ha:(List.foldl step (Mode.bit, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.bit, n) b) w⊢ Completion (Mode.bit, n) (b :: w) w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.bit, n)ha:(List.foldl step (Mode.bit, n) (b :: w)).1 = Mode.donebs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.bit, n) b).2hw:w = encodeString bs ++ encodeForest ts⊢ Completion (Mode.bit, n) (b :: w) exact ⟨b, bs, ts, ht, w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.bit, n)ha:(List.foldl step (Mode.bit, n) (b :: w)).1 = Mode.donebs:List Boolts:List Treeht:ts.length + 1 = (step (Mode.bit, n) b).2hw:w = encodeString bs ++ encodeForest ts⊢ b :: w = b :: (encodeString bs ++ encodeForest ts) All goals completed! 🐙⟩ w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.done, n)ha:(List.foldl step (Mode.done, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.done, n) b) w⊢ Completion (Mode.done, n) (b :: w) All goals completed! 🐙 w✝:List Boolb:Boolw:List Boolih:∀ (s : State), Active s → (List.foldl step s w).1 = Mode.done → Completion s wn:ℕhs:Active (Mode.dead, n)ha:(List.foldl step (Mode.dead, n) (b :: w)).1 = Mode.donehc:Completion (step (Mode.dead, n) b) w⊢ Completion (Mode.dead, n) (b :: w) All goals completed! 🐙) w

Acceptance is equivalent to being the encoding of a binary tree of bitstrings.

theorem validBool_iff (w : List Bool) : validBool w = true ↔ ∃ t, encode t = w := w:List Bool⊢ validBool w = true ↔ ∃ t, encode t = w w:List Bool⊢ validBool w = true → ∃ t, encode t = ww:List Bool⊢ (∃ t, encode t = w) → validBool w = true w:List Bool⊢ validBool w = true → ∃ t, encode t = w w:List Boolh:validBool w = true⊢ ∃ t, encode t = w w:List Boolh:validBool w = truehc:Completion (Mode.tree, 1) w⊢ ∃ t, encode t = w w:List Boolh:validBool w = truets:List Treeht:ts.length = (Mode.tree, 1).2hw:w = encodeForest ts⊢ ∃ t, encode t = w cases ts with w:List Boolh:validBool w = trueht:[].length = (Mode.tree, 1).2hw:w = encodeForest []⊢ ∃ t, encode t = w All goals completed! 🐙 w:List Boolh:validBool w = truet:Treets:List Treeht:(t :: ts).length = (Mode.tree, 1).2hw:w = encodeForest (t :: ts)⊢ ∃ t, encode t = w w:List Boolh:validBool w = truet:Treets:List Treeht:(t :: ts).length = (Mode.tree, 1).2hw:w = encodeForest (t :: ts)he:ts = []⊢ ∃ t, encode t = w w:List Boolh:validBool w = truet:Treeht:[t].length = (Mode.tree, 1).2hw:w = encodeForest [t]⊢ ∃ t, encode t = w exact ⟨t, w:List Boolh:validBool w = truet:Treeht:[t].length = (Mode.tree, 1).2hw:w = encodeForest [t]⊢ encode t = w All goals completed! 🐙⟩ w:List Bool⊢ (∃ t, encode t = w) → validBool w = true t:Tree⊢ validBool (encode t) = true All goals completed! 🐙

Every accepted word represents exactly one tree.

theorem validBool_iff_existsUnique (w : List Bool) : validBool w = true ↔ ∃! t, encode t = w := w:List Bool⊢ validBool w = true ↔ ∃! t, encode t = w w:List Bool⊢ (∃ t, encode t = w) ↔ ∃! t, encode t = w w:List Bool⊢ (∃ t, encode t = w) → ∃! t, encode t = ww:List Bool⊢ (∃! t, encode t = w) → ∃ t, encode t = w w:List Bool⊢ (∃ t, encode t = w) → ∃! t, encode t = w w:List Boolt:Treeht:encode t = w⊢ ∃! t, encode t = w All goals completed! 🐙 w:List Bool⊢ (∃! t, encode t = w) → ∃ t, encode t = w w:List Boolt:Treeht:encode t = wright✝:∀ (y : Tree), (fun t ↦ encode t = w) y → y = t⊢ ∃ t, encode t = w All goals completed! 🐙

The number of forks, leaves, and payload bits, respectively.

def counts : Tree → Nat × Nat × Nat := WType.elim (Nat × Nat × Nat) fun x ↦ match x with | ⟨some s, _⟩ => (0, 1, s.length) | ⟨none, f⟩ => (1 + (f false).1 + (f true).1, (f false).2.1 + (f true).2.1, (f false).2.2 + (f true).2.2)
@[simp] theorem counts_leaf (s : List Bool) : counts (leaf s) = (0, 1, s.length) := rfl@[simp] theorem counts_fork (l r : Tree) : counts (fork l r) = ((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2) := l:Treer:Tree⊢ counts (fork l r) = ((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2) l:Treer:Tree⊢ (1 + (counts l).1 + (counts r).1, ((fun b ↦ WType.elim (ℕ × ℕ × ℕ) (fun x ↦ match x with | ⟨some s, snd⟩ => (0, 1, s.length) | ⟨none, f⟩ => (1 + (f false).1 + (f true).1, (f false).2.1 + (f true).2.1, (f false).2.2 + (f true).2.2)) ((fun b ↦ if b = true then r else l) b)) false).2.1 + ((fun b ↦ WType.elim (ℕ × ℕ × ℕ) (fun x ↦ match x with | ⟨some s, snd⟩ => (0, 1, s.length) | ⟨none, f⟩ => (1 + (f false).1 + (f true).1, (f false).2.1 + (f true).2.1, (f false).2.2 + (f true).2.2)) ((fun b ↦ if b = true then r else l) b)) true).2.1, ((fun b ↦ WType.elim (ℕ × ℕ × ℕ) (fun x ↦ match x with | ⟨some s, snd⟩ => (0, 1, s.length) | ⟨none, f⟩ => (1 + (f false).1 + (f true).1, (f false).2.1 + (f true).2.1, (f false).2.2 + (f true).2.2)) ((fun b ↦ if b = true then r else l) b)) false).2.2 + ((fun b ↦ WType.elim (ℕ × ℕ × ℕ) (fun x ↦ match x with | ⟨some s, snd⟩ => (0, 1, s.length) | ⟨none, f⟩ => (1 + (f false).1 + (f true).1, (f false).2.1 + (f true).2.1, (f false).2.2 + (f true).2.2)) ((fun b ↦ if b = true then r else l) b)) true).2.2) = ((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2) l:Treer:Tree⊢ 1 + (counts l).1 + (counts r).1 = (counts l).1 + (counts r).1 + 1 All goals completed! 🐙

A full binary tree has one more leaf than fork.

theorem leaves_eq_forks_add_one (t : Tree) : (counts t).2.1 = (counts t).1 + 1 := tree_ind (P := fun t ↦ (counts t).2.1 = (counts t).1 + 1) (fun s ↦ rfl) (fun l r ihl ihr ↦ t:Treel:Treer:Treeihl:(counts l).2.1 = (counts l).1 + 1ihr:(counts r).2.1 = (counts r).1 + 1⊢ (counts (fork l r)).2.1 = (counts (fork l r)).1 + 1 t:Treel:Treer:Treeihl:(counts l).2.1 = (counts l).1 + 1ihr:(counts r).2.1 = (counts r).1 + 1⊢ (counts l).2.1 + (counts r).2.1 = (counts l).1 + (counts r).1 + 1 + 1; All goals completed! 🐙) t

Escaping uses two bits per payload bit and one terminator.

@[simp] theorem length_encodeString (s : List Bool) : (encodeString s).length = 2 * s.length + 1 := List.rec rfl (fun b s ih ↦ s✝:List Boolb:Bools:List Boolih:(encodeString s).length = 2 * s.length + 1⊢ (encodeString (b :: s)).length = 2 * (b :: s).length + 1 s✝:List Boolb:Bools:List Boolih:(encodeString s).length = 2 * s.length + 1⊢ (encodeString s).length + 1 + 1 = 2 * (s.length + 1) + 1; All goals completed! 🐙) s

The encoding uses one bit per fork, two per leaf, and two per payload bit.

theorem length_encode (t : Tree) : (encode t).length = (counts t).1 + 2 * (counts t).2.1 + 2 * (counts t).2.2 := tree_ind (P := fun t ↦ (encode t).length = (counts t).1 + 2 * (counts t).2.1 + 2 * (counts t).2.2) (fun s ↦ t:Trees:List Bool⊢ (encode (leaf s)).length = (counts (leaf s)).1 + 2 * (counts (leaf s)).2.1 + 2 * (counts (leaf s)).2.2 t:Trees:List Bool⊢ (false :: encodeString s).length = 0 + 2 * 1 + 2 * s.length t:Trees:List Bool⊢ 2 * s.length + 1 + 1 = 2 + 2 * s.length; All goals completed! 🐙) (fun l r ihl ihr ↦ t:Treel:Treer:Treeihl:(encode l).length = (counts l).1 + 2 * (counts l).2.1 + 2 * (counts l).2.2ihr:(encode r).length = (counts r).1 + 2 * (counts r).2.1 + 2 * (counts r).2.2⊢ (encode (fork l r)).length = (counts (fork l r)).1 + 2 * (counts (fork l r)).2.1 + 2 * (counts (fork l r)).2.2 t:Treel:Treer:Treeihl:(encode l).length = (counts l).1 + 2 * (counts l).2.1 + 2 * (counts l).2.2ihr:(encode r).length = (counts r).1 + 2 * (counts r).2.1 + 2 * (counts r).2.2⊢ (encode l).length + (encode r).length + 1 = (counts (fork l r)).1 + 2 * (counts (fork l r)).2.1 + 2 * (counts (fork l r)).2.2 t:Treel:Treer:Treeihl:(encode l).length = (counts l).1 + 2 * (counts l).2.1 + 2 * (counts l).2.2ihr:(encode r).length = (counts r).1 + 2 * (counts r).2.1 + 2 * (counts r).2.2⊢ (encode l).length + (encode r).length + 1 = 1 + (counts l).1 + (counts r).1 + 2 * ((counts l).2.1 + (counts r).2.1) + 2 * ((counts l).2.2 + (counts r).2.2) All goals completed! 🐙) t

Counting leaves through the full-binary-tree identity eliminates one parameter.

theorem length_encode_forks (t : Tree) : (encode t).length = 3 * (counts t).1 + 2 + 2 * (counts t).2.2 := t:Tree⊢ (encode t).length = 3 * (counts t).1 + 2 + 2 * (counts t).2.2 t:Tree⊢ (counts t).1 + 2 * ((counts t).1 + 1) + 2 * (counts t).2.2 = 3 * (counts t).1 + 2 + 2 * (counts t).2.2 All goals completed! 🐙
end Geb.BitTree