Reconstruction from depth-first outdegrees

Read a natural degree word from right to left. At a vertex of degree d, the first d trees already reconstructed become its ordered children. The decoder fails if fewer than d trees are available. A tree word must leave exactly one tree; an empty word represents the empty forest only.

def BGW.PlaneForest.degrees (ts : PlaneForest) : List ℕ

Concatenate the degree words in component order.

Equations

• ts.degrees = (List.map BGW.PlaneTree.degrees ts).flatten

@[simp]

theorem BGW.PlaneForest.degrees_nil : degrees [] = []

@[simp]

theorem BGW.PlaneForest.degrees_cons (t : PlaneTree) (ts : PlaneForest) : degrees (t :: ts) = t.degrees ++ ts.degrees

theorem BGW.PlaneForest.degrees_append (ts ss : PlaneForest) : (ts ++ ss).degrees = ts.degrees ++ ss.degrees

def BGW.PlaneForest.ofDegrees? : List ℕ → Option PlaneForest

Reconstruct an ordered forest from its depth-first outdegrees.

Equations

• One or more equations did not get rendered due to their size.
• BGW.PlaneForest.ofDegrees? [] = some []

@[simp]

theorem BGW.PlaneForest.ofDegrees?_nil : ofDegrees? [] = some []

theorem BGW.PlaneForest.ofDegrees?_cons (d : ℕ) (ds : List ℕ) : ofDegrees? (d :: ds) = (ofDegrees? ds).bind fun (ts : PlaneForest) => if d ≤ List.length ts then some (PlaneTree.node (List.take d ts) :: List.drop d ts) else none

theorem BGW.PlaneForest.ofDegrees?_tree_degrees_append (t : PlaneTree) (ds : List ℕ) : ofDegrees? (t.degrees ++ ds) = Option.map (fun (ts : List PlaneTree) => t :: ts) (ofDegrees? ds)

Prepending one complete tree word adds that tree to any decoded suffix.

theorem BGW.PlaneForest.ofDegrees?_degrees_append (ts : PlaneForest) (ds : List ℕ) : ofDegrees? (ts.degrees ++ ds) = Option.map (fun (ss : PlaneForest) => ts ++ ss) (ofDegrees? ds)

The parser respects concatenation with any suffix word, valid or invalid.

@[simp]

theorem BGW.PlaneForest.ofDegrees?_degrees (ts : PlaneForest) : ofDegrees? ts.degrees = some ts

theorem BGW.PlaneForest.degrees_of_ofDegrees?_eq_some {ds : List ℕ} {ts : PlaneForest} (h : ofDegrees? ds = some ts) : ts.degrees = ds

A successful parse reproduces exactly the input degree word.

theorem BGW.PlaneForest.ofDegrees?_eq_some_iff {ds : List ℕ} {ts : PlaneForest} : ofDegrees? ds = some ts ↔ ts.degrees = ds

Successful parsing is exactly membership in the range of the forest encoder.

theorem BGW.PlaneForest.degrees_injective : Function.Injective degrees

theorem BGW.PlaneForest.length_add_sum_degrees (ts : PlaneForest) : List.length ts + ts.degrees.sum = ts.degrees.length

The number of roots is the deficit between word length and total degree.

theorem BGW.PlaneForest.length_add_sum_of_ofDegrees?_eq_some {ds : List ℕ} {ts : PlaneForest} (h : ofDegrees? ds = some ts) : List.length ts + ds.sum = ds.length

def BGW.PlaneTree.ofDegrees? (ds : List ℕ) : Option PlaneTree

Reconstruct a single tree, rejecting failed parses and nonsingleton forests.

Equations

• BGW.PlaneTree.ofDegrees? ds = match BGW.PlaneForest.ofDegrees? ds with | some [t] => some t | x => none

theorem BGW.PlaneTree.ofDegrees?_eq_some_iff_forest {ds : List ℕ} {t : PlaneTree} : ofDegrees? ds = some t ↔ PlaneForest.ofDegrees? ds = some [t]

A single-tree parse is precisely a forest parse with one component.

theorem BGW.PlaneTree.ofDegrees?_eq_some_iff {ds : List ℕ} {t : PlaneTree} : ofDegrees? ds = some t ↔ t.degrees = ds

Both reconstruction identities, with failure explicit for other words.

@[simp]

theorem BGW.PlaneTree.ofDegrees?_degrees (t : PlaneTree) : ofDegrees? t.degrees = some t

theorem BGW.PlaneTree.degrees_injective : Function.Injective degrees