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.Encoding
public import Geb.Prototypes.Computability.BitTree.Elias.Code

set_option doc.verso true

Binary trees with length-prefixed leaf payloads

The tree shape retains one tag per node. Leaf payloads are preceded by their lengths, so payload bits are stored without escaping.

Main definitions

lengths lists the payload lengths in left-to-right leaf order.
encode uses one tag per node and a delta length header per leaf.
decode reads a complete tree; validBool tests whether it succeeds.

Main statements

length_encode counts node tags, raw payload bits and length headers.
readTree_encode_append proves the fuel-bounded parser's prefix roundtrip.
validBool_iff_existsUnique characterizes the recognized language.

Tags

binary tree, bitstring, length prefix, encoding

@[expose] public sectionnamespace Geb.BitTree.Elias

Payload lengths in left-to-right leaf order.

def lengths : Tree → List ℕ := WType.elim (List ℕ) fun x ↦
  match x with
  | ⟨some s, _⟩ => [s.length]
  | ⟨none, f⟩ => f false ++ f true

@[simp] theorem lengths_leaf (s : List Bool) : lengths (leaf s) = [s.length] := rfl@[simp] theorem lengths_fork (l r : Tree) : lengths (fork l r) = lengths l ++ lengths r := rfl

There is one payload length per leaf.

theorem length_lengths (t : Tree) : (lengths t).length = (counts t).2.1 :=
  tree_ind (P := fun t ↦ (lengths t).length = (counts t).2.1)
    (fun _ ↦ rfl)
    (fun l r hl hr ↦ byt:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (lengths (fork l r)).length = (counts (fork l r)).2.1
      rw [lengths_fork,t:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (lengths l ++ lengths r).length = (counts (fork l r)).2.1 List.length_append,t:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (lengths l).length + (lengths r).length = (counts (fork l r)).2.1 hl,t:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (counts l).2.1 + (lengths r).length = (counts (fork l r)).2.1 hrt:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (counts l).2.1 + (counts r).2.1 = (counts (fork l r)).2.1]t:Treel:Treer:Treehl:(lengths l).length = (counts l).2.1hr:(lengths r).length = (counts r).2.1⊢ (counts l).2.1 + (counts r).2.1 = (counts (fork l r)).2.1
      rflAll goals completed! 🐙) t

The sum of the lengths is the total number of payload bits.

theorem sum_lengths (t : Tree) : (lengths t).sum = (counts t).2.2 :=
  tree_ind (P := fun t ↦ (lengths t).sum = (counts t).2.2)
    (fun _ ↦ Nat.add_zero _)
    (fun l r hl hr ↦ byt:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (lengths (fork l r)).sum = (counts (fork l r)).2.2
      rw [lengths_fork,t:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (lengths l ++ lengths r).sum = (counts (fork l r)).2.2 List.sum_append,t:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (lengths l).sum + (lengths r).sum = (counts (fork l r)).2.2 hl,t:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (counts l).2.2 + (lengths r).sum = (counts (fork l r)).2.2 hrt:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (counts l).2.2 + (counts r).2.2 = (counts (fork l r)).2.2]t:Treel:Treer:Treehl:(lengths l).sum = (counts l).2.2hr:(lengths r).sum = (counts r).2.2⊢ (counts l).2.2 + (counts r).2.2 = (counts (fork l r)).2.2
      rflAll goals completed! 🐙) t

Read a payload of the specified length, rejecting truncated input.

def readPayload (n : ℕ) (w : List Bool) : Option (List Bool × List Bool) :=
  if n ≤ w.length then some (w.take n, w.drop n) else none

Reading a payload preserves the unconsumed suffix.

theorem readPayload_append (s rest : List Bool) :
    readPayload s.length (s ++ rest) = some (s, rest) := bys:List Boolrest:List Bool⊢ readPayload s.length (s ++ rest) = some (s, rest)
  simp only [readPayload, List.length_append, Nat.le_add_right, ↓reduceIte,
    List.take_left, List.drop_left]All goals completed! 🐙

A successful payload read gives its length and the exact input decomposition.

theorem readPayload_eq_some {n : ℕ} {w s rest : List Bool}
    (h : readPayload n w = some (s, rest)) : s.length = n ∧ w = s ++ rest := byn:ℕw:List Bools:List Boolrest:List Boolh:readPayload n w = some (s, rest)⊢ s.length = n ∧ w = s ++ rest
  unfold readPayload at hn:ℕw:List Bools:List Boolrest:List Boolh:(if n ≤ w.length then some (List.take n w, List.drop n w) else none) = some (s, rest)⊢ s.length = n ∧ w = s ++ rest
  split at hisTruen:ℕw:List Bools:List Boolrest:List Boolh✝:n ≤ w.lengthh:some (List.take n w, List.drop n w) = some (s, rest)⊢ s.length = n ∧ w = s ++ restisFalsen:ℕw:List Bools:List Boolrest:List Boolh✝:¬n ≤ w.lengthh:none = some (s, rest)⊢ s.length = n ∧ w = s ++ rest
  next hn =>n:ℕw:List Bools:List Boolrest:List Boolhn:n ≤ w.lengthh:some (List.take n w, List.drop n w) = some (s, rest)⊢ s.length = n ∧ w = s ++ rest
    cases hrefln:ℕw:List Boolhn:n ≤ w.length⊢ (List.take n w).length = n ∧ w = List.take n w ++ List.drop n w
    exact ⟨List.length_take_of_le hn, (List.take_append_drop n w).symm⟩All goals completed! 🐙
  next =>n:ℕw:List Bools:List Boolrest:List Boolh✝:¬n ≤ w.lengthh:none = some (s, rest)⊢ s.length = n ∧ w = s ++ rest cases hAll goals completed! 🐙

Preorder tree tags with a delta-coded length followed by each leaf's raw payload.

def encode : Tree → List Bool := WType.elim (List Bool) fun x ↦
  match x with
  | ⟨some s, _⟩ => false :: (encodeNat s.length ++ s)
  | ⟨none, f⟩ => true :: (f false ++ f true)

@[simp] theorem encode_leaf (s : List Bool) :
    encode (leaf s) = false :: (encodeNat s.length ++ s) := rfl

@[simp] theorem encode_fork (l r : Tree) :
    encode (fork l r) = true :: (encode l ++ encode r) := rfl

The exact representation length separates node tags, raw bits and length headers.

theorem length_encode (t : Tree) :
    (encode t).length = 2 * (counts t).1 + 1 + (counts t).2.2 +
      ((lengths t).map fun n ↦ (encodeNat n).length).sum :=
  tree_ind (P := fun t ↦ (encode t).length = 2 * (counts t).1 + 1 + (counts t).2.2 +
      ((lengths t).map fun n ↦ (encodeNat n).length).sum)
    (fun s ↦ byt:Trees:List Bool⊢ (encode (leaf s)).length =
  2 * (counts (leaf s)).1 + 1 + (counts (leaf s)).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths (leaf s))).sum
      simp only [encode_leaf, List.length_cons, List.length_append, counts_leaf, lengths_leaf,
        List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]t:Trees:List Bool⊢ (encodeNat s.length).length + s.length + 1 = 2 * 0 + 1 + s.length + ((encodeNat s.length).length + 0)
      omegaAll goals completed! 🐙)
    (fun l r hl hr ↦ byt:Treel:Treer:Treehl:(encode l).length = 2 * (counts l).1 + 1 + (counts l).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths l)).sumhr:(encode r).length = 2 * (counts r).1 + 1 + (counts r).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths r)).sum⊢ (encode (fork l r)).length =
  2 * (counts (fork l r)).1 + 1 + (counts (fork l r)).2.2 +
    (List.map (fun n ↦ (encodeNat n).length) (lengths (fork l r))).sum
      simp only [encode_fork, List.length_cons, List.length_append, counts_fork, lengths_fork,
        List.map_append, List.sum_append]t:Treel:Treer:Treehl:(encode l).length = 2 * (counts l).1 + 1 + (counts l).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths l)).sumhr:(encode r).length = 2 * (counts r).1 + 1 + (counts r).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths r)).sum⊢ (encode l).length + (encode r).length + 1 =
  2 * ((counts l).1 + (counts r).1 + 1) + 1 + ((counts l).2.2 + (counts r).2.2) +
    ((List.map (fun n ↦ (encodeNat n).length) (lengths l)).sum +
      (List.map (fun n ↦ (encodeNat n).length) (lengths r)).sum)
      omegaAll goals completed! 🐙) t

The total header cost is logarithmic in each shifted payload length.

theorem length_encode_le (t : Tree) :
    (encode t).length ≤ 2 * (counts t).1 + 1 + (counts t).2.2 +
      3 * ((lengths t).map fun n ↦ (n + 1).size).sum :=
  tree_ind (P := fun t ↦ (encode t).length ≤ 2 * (counts t).1 + 1 + (counts t).2.2 +
      3 * ((lengths t).map fun n ↦ (n + 1).size).sum)
    (fun s ↦ byt:Trees:List Bool⊢ (encode (leaf s)).length ≤
  2 * (counts (leaf s)).1 + 1 + (counts (leaf s)).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths (leaf s))).sum
      have h := length_encodeNat_le s.lengtht:Trees:List Boolh:(encodeNat s.length).length ≤ 3 * (s.length + 1).size⊢ (encode (leaf s)).length ≤
  2 * (counts (leaf s)).1 + 1 + (counts (leaf s)).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths (leaf s))).sum
      simp only [encode_leaf, List.length_cons, List.length_append, counts_leaf, lengths_leaf,
        List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]t:Trees:List Boolh:(encodeNat s.length).length ≤ 3 * (s.length + 1).size⊢ (encodeNat s.length).length + s.length + 1 ≤ 2 * 0 + 1 + s.length + 3 * ((s.length + 1).size + 0)
      omegaAll goals completed! 🐙)
    (fun l r hl hr ↦ byt:Treel:Treer:Treehl:(encode l).length ≤ 2 * (counts l).1 + 1 + (counts l).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths l)).sumhr:(encode r).length ≤ 2 * (counts r).1 + 1 + (counts r).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths r)).sum⊢ (encode (fork l r)).length ≤
  2 * (counts (fork l r)).1 + 1 + (counts (fork l r)).2.2 +
    3 * (List.map (fun n ↦ (n + 1).size) (lengths (fork l r))).sum
      simp only [encode_fork, List.length_cons, List.length_append, counts_fork, lengths_fork,
        List.map_append, List.sum_append]t:Treel:Treer:Treehl:(encode l).length ≤ 2 * (counts l).1 + 1 + (counts l).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths l)).sumhr:(encode r).length ≤ 2 * (counts r).1 + 1 + (counts r).2.2 + 3 * (List.map (fun n ↦ (n + 1).size) (lengths r)).sum⊢ (encode l).length + (encode r).length + 1 ≤
  2 * ((counts l).1 + (counts r).1 + 1) + 1 + ((counts l).2.2 + (counts r).2.2) +
    3 * ((List.map (fun n ↦ (n + 1).size) (lengths l)).sum + (List.map (fun n ↦ (n + 1).size) (lengths r)).sum)
      omegaAll goals completed! 🐙) t

There is enough input length to bound every recursive descent in the tree parser.

theorem forks_lt_length_encode (t : Tree) : (counts t).1 < (encode t).length := byt:Tree⊢ (counts t).1 < (encode t).length
  rw [length_encodet:Tree⊢ (counts t).1 < 2 * (counts t).1 + 1 + (counts t).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths t)).sum]t:Tree⊢ (counts t).1 < 2 * (counts t).1 + 1 + (counts t).2.2 + (List.map (fun n ↦ (encodeNat n).length) (lengths t)).sum
  omegaAll goals completed! 🐙

One tree-parser layer: a leaf payload or two recursively read children.

def readTreeStep (readChild : List Bool → Option (Tree × List Bool))
    (w : List Bool) : Option (Tree × List Bool) :=
  match w with
  | [] => none
  | false :: suffix => (readNat suffix).bind fun p ↦
      (readPayload p.1 p.2).map fun q ↦ (leaf q.1, q.2)
  | true :: suffix => (readChild suffix).bind fun p ↦
      (readChild p.2).map fun q ↦ (fork p.1 q.1, q.2)

A fuel-bounded tree parser, with the bound controlling recursive tree descent.

def readTree : ℕ → List Bool → Option (Tree × List Bool) :=
  Nat.rec (fun _ ↦ none) fun _ readChild ↦ readTreeStep readChild

The parser's successor-fuel equation.

theorem readTree_succ (fuel : ℕ) (w : List Bool) :
    readTree (fuel + 1) w = readTreeStep (readTree fuel) w := rfl

A bound larger than the number of forks suffices for every encoded tree.

theorem readTree_encode_append (t : Tree) : ∀ fuel, (counts t).1 + 1 ≤ fuel →
    ∀ rest, readTree fuel (encode t ++ rest) = some (t, rest) :=
  tree_ind (P := fun t ↦ ∀ fuel, (counts t).1 + 1 ≤ fuel →
      ∀ rest, readTree fuel (encode t ++ rest) = some (t, rest))
    (fun s fuel hf rest ↦ byt:Trees:List Boolfuel:ℕhf:(counts (leaf s)).1 + 1 ≤ fuelrest:List Bool⊢ readTree fuel (encode (leaf s) ++ rest) = some (leaf s, rest)
      cases fuel with
      | zero =>zerot:Trees:List Boolrest:List Boolhf:(counts (leaf s)).1 + 1 ≤ 0⊢ readTree 0 (encode (leaf s) ++ rest) = some (leaf s, rest)
        exfalsozerot:Trees:List Boolrest:List Boolhf:(counts (leaf s)).1 + 1 ≤ 0⊢ False
        have hh : 0 + 1 ≤ 0 := hfzerot:Trees:List Boolrest:List Boolhf:(counts (leaf s)).1 + 1 ≤ 0hh:0 + 1 ≤ 0⊢ False
        omegaAll goals completed! 🐙
      | succ fuel =>succt:Trees:List Boolrest:List Boolfuel:ℕhf:(counts (leaf s)).1 + 1 ≤ fuel + 1⊢ readTree (fuel + 1) (encode (leaf s) ++ rest) = some (leaf s, rest)
        simp only [encode_leaf, List.cons_append, readTree_succ, readTreeStep,
          List.append_assoc, readNat_encodeNat_append, Option.bind_some, readPayload_append,
          Option.map_some]All goals completed! 🐙)
    (fun l r hl hr fuel hf rest ↦ byt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)fuel:ℕhf:(counts (fork l r)).1 + 1 ≤ fuelrest:List Bool⊢ readTree fuel (encode (fork l r) ++ rest) = some (fork l r, rest)
      cases fuel with
      | zero =>zerot:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolhf:(counts (fork l r)).1 + 1 ≤ 0⊢ readTree 0 (encode (fork l r) ++ rest) = some (fork l r, rest) exfalsozerot:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolhf:(counts (fork l r)).1 + 1 ≤ 0⊢ False; omegaAll goals completed! 🐙
      | succ fuel =>succt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:(counts (fork l r)).1 + 1 ≤ fuel + 1⊢ readTree (fuel + 1) (encode (fork l r) ++ rest) = some (fork l r, rest)
        rw [counts_forksucct:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ readTree (fuel + 1) (encode (fork l r) ++ rest) = some (fork l r, rest)] at hfsucct:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ readTree (fuel + 1) (encode (fork l r) ++ rest) = some (fork l r, rest)
        simp only [encode_fork, List.cons_append, readTree_succ, readTreeStep,
          List.append_assoc]succt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ ((readTree fuel (encode l ++ (encode r ++ rest))).bind fun p ↦
    Option.map (fun q ↦ (fork p.1 q.1, q.2)) (readTree fuel p.2)) =
  some (fork l r, rest)
        rw [hl fuel (byt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ (counts l).1 + 1 ≤ fuel omegaAll goals completed! 🐙), Option.bind_some,succt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ Option.map (fun q ↦ (fork (l, encode r ++ rest).1 q.1, q.2)) (readTree fuel (l, encode r ++ rest).2) =
  some (fork l r, rest) hr fuel (byt:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ (counts r).1 + 1 ≤ fuel omegaAll goals completed! 🐙), Option.map_somesucct:Treel:Treer:Treehl:∀ (fuel : ℕ), (counts l).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode l ++ rest) = some (l, rest)hr:∀ (fuel : ℕ), (counts r).1 + 1 ≤ fuel → ∀ (rest : List Bool), readTree fuel (encode r ++ rest) = some (r, rest)rest:List Boolfuel:ℕhf:((counts l).1 + (counts r).1 + 1, (counts l).2.1 + (counts r).2.1, (counts l).2.2 + (counts r).2.2).1 + 1 ≤ fuel + 1⊢ some (fork (l, encode r ++ rest).1 (r, rest).1, (r, rest).2) = some (fork l r, rest)]All goals completed! 🐙) t

Every successful tree parse consumes exactly the canonical encoding of its result.

theorem readTree_eq_some (fuel : ℕ) : ∀ w t rest,
    readTree fuel w = some (t, rest) → w = encode t ++ rest :=
  Nat.rec (fun w t rest h ↦ byfuel:ℕw:List Boolt:Treerest:List Boolh:readTree Nat.zero w = some (t, rest)⊢ w = encode t ++ rest cases hAll goals completed! 🐙)
    (fun fuel ih w t rest h ↦ byfuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restw:List Boolt:Treerest:List Boolh:readTree fuel.succ w = some (t, rest)⊢ w = encode t ++ rest
      cases w with
      | nil =>nilfuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolh:readTree fuel.succ [] = some (t, rest)⊢ [] = encode t ++ rest cases hAll goals completed! 🐙
      | cons b suffix =>consfuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolb:Boolsuffix:List Boolh:readTree fuel.succ (b :: suffix) = some (t, rest)⊢ b :: suffix = encode t ++ rest
        cases b with
        | false =>cons.falsefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)⊢ false :: suffix = encode t ++ rest
          cases hn : readNat suffix with
          | none =>cons.false.nonefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)hn:readNat suffix = none⊢ false :: suffix = encode t ++ rest
            simp only [readTree_succ, readTreeStep, hn, Option.bind_none, reduceCtorEq] at hAll goals completed! 🐙
          | some p =>cons.false.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)p:ℕ × List Boolhn:readNat suffix = some p⊢ false :: suffix = encode t ++ rest
            rcases p with ⟨n, input⟩cons.false.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)⊢ false :: suffix = encode t ++ rest
            cases hp : readPayload n input with
            | none =>cons.false.some.nonefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)hp:readPayload n input = none⊢ false :: suffix = encode t ++ rest
              simp only [readTree_succ, readTreeStep, hn, Option.bind_some, hp,
                Option.map_none, reduceCtorEq] at hAll goals completed! 🐙
            | some p =>cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)p:List Bool × List Boolhp:readPayload n input = some p⊢ false :: suffix = encode t ++ rest
              rcases p with ⟨bs, tail⟩cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)⊢ false :: suffix = encode t ++ rest
              have he : (leaf bs, tail) = (t, rest) := Option.some.inj (byfuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)⊢ some (leaf bs, tail) = some (t, rest)
                simpa only [readTree_succ, readTreeStep, hn, Option.bind_some, hp,
                  Option.map_some] using hAll goals completed! 🐙)cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)⊢ false :: suffix = encode t ++ rest
              obtain ⟨ht, hr⟩ := Prod.mk.inj hecons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = rest⊢ false :: suffix = encode t ++ rest
              obtain ⟨hlen, hinput⟩ := readPayload_eq_some hpcons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: suffix = encode t ++ rest
              rw [← ht,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: suffix = encode (leaf bs) ++ rest ← hr,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: suffix = encode (leaf bs) ++ tail encode_leaf,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: suffix = false :: (encodeNat bs.length ++ bs) ++ tail List.cons_append,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: suffix = false :: (encodeNat bs.length ++ bs ++ tail)
                readNat_eq_some suffix n input hn,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: (encodeNat n ++ input) = false :: (encodeNat bs.length ++ bs ++ tail) hinput,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: (encodeNat n ++ (bs ++ tail)) = false :: (encodeNat bs.length ++ bs ++ tail) ← hlen,cons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: (encodeNat bs.length ++ (bs ++ tail)) = false :: (encodeNat bs.length ++ bs ++ tail) List.append_assoccons.false.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (false :: suffix) = some (t, rest)n:ℕinput:List Boolhn:readNat suffix = some (n, input)bs:List Booltail:List Boolhp:readPayload n input = some (bs, tail)he:(leaf bs, tail) = (t, rest)ht:leaf bs = thr:tail = resthlen:bs.length = nhinput:input = bs ++ tail⊢ false :: (encodeNat bs.length ++ (bs ++ tail)) = false :: (encodeNat bs.length ++ (bs ++ tail))]All goals completed! 🐙
        | true =>cons.truefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)⊢ true :: suffix = encode t ++ rest
          cases hl : readTree fuel suffix with
          | none =>cons.true.nonefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)hl:readTree fuel suffix = none⊢ true :: suffix = encode t ++ rest
            simp only [readTree_succ, readTreeStep, hl, Option.bind_none, reduceCtorEq] at hAll goals completed! 🐙
          | some p =>cons.true.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)p:Tree × List Boolhl:readTree fuel suffix = some p⊢ true :: suffix = encode t ++ rest
            rcases p with ⟨l, middle⟩cons.true.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)⊢ true :: suffix = encode t ++ rest
            cases hr : readTree fuel middle with
            | none =>cons.true.some.nonefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)hr:readTree fuel middle = none⊢ true :: suffix = encode t ++ rest
              simp only [readTree_succ, readTreeStep, hl, Option.bind_some, hr,
                Option.map_none, reduceCtorEq] at hAll goals completed! 🐙
            | some p =>cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)p:Tree × List Boolhr:readTree fuel middle = some p⊢ true :: suffix = encode t ++ rest
              rcases p with ⟨r, tail⟩cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)⊢ true :: suffix = encode t ++ rest
              have he : (fork l r, tail) = (t, rest) := Option.some.inj (byfuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)⊢ some (fork l r, tail) = some (t, rest)
                simpa only [readTree_succ, readTreeStep, hl, Option.bind_some, hr,
                  Option.map_some] using hAll goals completed! 🐙)cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)⊢ true :: suffix = encode t ++ rest
              obtain ⟨ht, hs⟩ := Prod.mk.inj hecons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: suffix = encode t ++ rest
              rw [← ht,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: suffix = encode (fork l r) ++ rest ← hs,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: suffix = encode (fork l r) ++ tail encode_fork,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: suffix = true :: (encode l ++ encode r) ++ tail List.cons_append,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: suffix = true :: (encode l ++ encode r ++ tail) ih suffix l middle hl,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: (encode l ++ middle) = true :: (encode l ++ encode r ++ tail)
                ih middle r tail hr,cons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: (encode l ++ (encode r ++ tail)) = true :: (encode l ++ encode r ++ tail) List.append_assoccons.true.some.somefuel✝:ℕfuel:ℕih:∀ (w : List Bool) (t : Tree) (rest : List Bool), readTree fuel w = some (t, rest) → w = encode t ++ restt:Treerest:List Boolsuffix:List Boolh:readTree fuel.succ (true :: suffix) = some (t, rest)l:Treemiddle:List Boolhl:readTree fuel suffix = some (l, middle)r:Treetail:List Boolhr:readTree fuel middle = some (r, tail)he:(fork l r, tail) = (t, rest)ht:fork l r = ths:tail = rest⊢ true :: (encode l ++ (encode r ++ tail)) = true :: (encode l ++ (encode r ++ tail))]All goals completed! 🐙) fuel

Decode exactly one complete tree, rejecting trailing or incomplete input.

def decode (w : List Bool) : Option Tree :=
  match readTree w.length w with
  | some (t, []) => some t
  | _ => none

The input length supplies enough parser fuel for every encoded tree.

@[simp] theorem decode_encode (t : Tree) : decode (encode t) = some t := byt:Tree⊢ decode (encode t) = some t
  have h := readTree_encode_append t (encode t).length (forks_lt_length_encode t) []t:Treeh:readTree (encode t).length (encode t ++ []) = some (t, [])⊢ decode (encode t) = some t
  simp only [List.append_nil] at ht:Treeh:readTree (encode t).length (encode t) = some (t, [])⊢ decode (encode t) = some t
  rw [decode,t:Treeh:readTree (encode t).length (encode t) = some (t, [])⊢ (match readTree (encode t).length (encode t) with
  | some (t, []) => some t
  | x => none) =
  some t ht:Treeh:readTree (encode t).length (encode t) = some (t, [])⊢ (match some (t, []) with
  | some (t, []) => some t
  | x => none) =
  some t]All goals completed! 🐙

Successful complete decoding identifies the whole input as the resulting tree's encoding.

theorem decode_eq_some (w : List Bool) (t : Tree) (h : decode w = some t) : encode t = w := byw:List Boolt:Treeh:decode w = some t⊢ encode t = w
  cases hp : readTree w.length w with
  | none =>nonew:List Boolt:Treeh:decode w = some thp:readTree w.length w = none⊢ encode t = w simp only [decode, hp, reduceCtorEq] at hAll goals completed! 🐙
  | some p =>somew:List Boolt:Treeh:decode w = some tp:Tree × List Boolhp:readTree w.length w = some p⊢ encode t = w
    rcases p with ⟨t', rest⟩somew:List Boolt:Treeh:decode w = some tt':Treerest:List Boolhp:readTree w.length w = some (t', rest)⊢ encode t = w
    cases rest with
    | nil =>some.nilw:List Boolt:Treeh:decode w = some tt':Treehp:readTree w.length w = some (t', [])⊢ encode t = w
      have he : t' = t := Option.some.inj (byw:List Boolt:Treeh:decode w = some tt':Treehp:readTree w.length w = some (t', [])⊢ some t' = some t simpa only [decode, hp] using hAll goals completed! 🐙)some.nilw:List Boolt:Treeh:decode w = some tt':Treehp:readTree w.length w = some (t', [])he:t' = t⊢ encode t = w
      rw [hesome.nilw:List Boolt:Treeh:decode w = some tt':Treehp:readTree w.length w = some (t, [])he:t' = t⊢ encode t = w] at hpsome.nilw:List Boolt:Treeh:decode w = some tt':Treehp:readTree w.length w = some (t, [])he:t' = t⊢ encode t = w
      simpa only [List.append_nil] using (readTree_eq_some w.length w t [] hp).symmAll goals completed! 🐙
    | cons _ _ =>some.consw:List Boolt:Treeh:decode w = some tt':Treehead✝:Booltail✝:List Boolhp:readTree w.length w = some (t', head✝ :: tail✝)⊢ encode t = w simp only [decode, hp, reduceCtorEq] at hAll goals completed! 🐙

The length-prefixed tree encoding is injective.

theorem encode_injective : Function.Injective encode := by⊢ Function.Injective encode
  intro t t' ht:Treet':Treeh:encode t = encode t'⊢ t = t'
  have he := congrArg decode ht:Treet':Treeh:encode t = encode t'he:decode (encode t) = decode (encode t')⊢ t = t'
  rw [decode_encode,t:Treet':Treeh:encode t = encode t'he:some t = decode (encode t')⊢ t = t' decode_encodet:Treet':Treeh:encode t = encode t'he:some t = some t'⊢ t = t'] at het:Treet':Treeh:encode t = encode t'he:some t = some t'⊢ t = t'
  exact Option.some.inj heAll goals completed! 🐙

The complete decoder decides membership in the encoded-tree language.

def validBool (w : List Bool) : Bool := (decode w).isSome

Every encoded tree is accepted by the complete decoder.

@[simp] theorem validBool_encode (t : Tree) : validBool (encode t) = true := byt:Tree⊢ validBool (encode t) = true
  rw [validBool,t:Tree⊢ (decode (encode t)).isSome = true decode_encodet:Tree⊢ (some t).isSome = true]t:Tree⊢ (some t).isSome = true
  rflAll goals completed! 🐙

Acceptance is exactly existence of an encoded tree.

theorem validBool_iff (w : List Bool) : validBool w = true ↔ ∃ t, encode t = w := byw:List Bool⊢ validBool w = true ↔ ∃ t, encode t = w
  constructormpw:List Bool⊢ validBool w = true → ∃ t, encode t = wmprw:List Bool⊢ (∃ t, encode t = w) → validBool w = true
  ·mpw:List Bool⊢ validBool w = true → ∃ t, encode t = w intro hmpw:List Boolh:validBool w = true⊢ ∃ t, encode t = w
    cases hd : decode w with
    | none =>mp.nonew:List Boolh:validBool w = truehd:decode w = none⊢ ∃ t, encode t = w simp only [validBool, hd, Option.isSome_none, Bool.false_eq_true] at hAll goals completed! 🐙
    | some t =>mp.somew:List Boolh:validBool w = truet:Treehd:decode w = some t⊢ ∃ t, encode t = w exact ⟨t, decode_eq_some w t hd⟩All goals completed! 🐙
  ·mprw:List Bool⊢ (∃ t, encode t = w) → validBool w = true rintro ⟨t, rfl⟩mprt:Tree⊢ validBool (encode t) = true
    exact validBool_encode tAll goals completed! 🐙

Every accepted word represents exactly one tree of bitstrings.

theorem validBool_iff_existsUnique (w : List Bool) :
    validBool w = true ↔ ∃! t, encode t = w := byw:List Bool⊢ validBool w = true ↔ ∃! t, encode t = w
  rw [validBool_iffw:List Bool⊢ (∃ t, encode t = w) ↔ ∃! t, encode t = w]w:List Bool⊢ (∃ t, encode t = w) ↔ ∃! t, encode t = w
  constructormpw:List Bool⊢ (∃ t, encode t = w) → ∃! t, encode t = wmprw:List Bool⊢ (∃! t, encode t = w) → ∃ t, encode t = w
  ·mpw:List Bool⊢ (∃ t, encode t = w) → ∃! t, encode t = w rintro ⟨t, ht⟩mpw:List Boolt:Treeht:encode t = w⊢ ∃! t, encode t = w
    exact ⟨t, ht, fun t' ht' ↦ encode_injective (ht'.trans ht.symm)⟩All goals completed! 🐙
  ·mprw:List Bool⊢ (∃! t, encode t = w) → ∃ t, encode t = w rintro ⟨t, ht, _⟩mprw:List Boolt:Treeht:encode t = wright✝:∀ (y : Tree), (fun t ↦ encode t = w) y → y = t⊢ ∃ t, encode t = w
    exact ⟨t, ht⟩All goals completed! 🐙

end Geb.BitTree.Elias