Finite plane trees

A plane tree is a finite rooted tree whose children are ordered. We use Mathlib's WType, with Fin n indexing the children of a vertex of outdegree n. PlaneTree.node and PlaneTree.children provide the list interface. The induction and cases tactics produce a single node ts case, and PlaneTree.fold defines functions by bottom-up recursion, so the WType encoding is not used outside this file.

Addresses are zero-based lists of child indices; the root has address []. These are implementation coordinates, independent of the paper's one-based numbering of vertices in depth-first order. Size counts vertices, including the root.

def BGW.PlaneTree : Type

Finite rooted ordered trees, with no vertex labels.

Equations

• BGW.PlaneTree = WType fun (n : ℕ) => Fin n

@[instance_reducible]

instance BGW.instEncodablePlaneTree : Encodable PlaneTree

Equations

• BGW.instEncodablePlaneTree = { encode := BGW.instEncodablePlaneTree._aux_1, decode := BGW.instEncodablePlaneTree._aux_3, encodek := BGW.instEncodablePlaneTree._proof_5 }

@[reducible, inline]

abbrev BGW.PlaneForest : Type

Finite ordered forests. The empty forest is allowed.

Equations

• BGW.PlaneForest = List BGW.PlaneTree

def BGW.PlaneTree.equivChildren : PlaneTree ≃ List PlaneTree

A tree is determined by the ordered list of subtrees attached to its root.

Equations

• BGW.PlaneTree.equivChildren = (WType.equivSigma fun (n : ℕ) => Fin n).trans List.equivSigmaTuple.symm

def BGW.PlaneTree.node (ts : List PlaneTree) : PlaneTree

Attach an ordered list of trees to a new root.

Equations

• BGW.PlaneTree.node ts = BGW.PlaneTree.equivChildren.symm ts

def BGW.PlaneTree.children (t : PlaneTree) : List PlaneTree

The ordered subtrees attached to the root.

Equations

• t.children = BGW.PlaneTree.equivChildren t

theorem BGW.PlaneTree.ext {s t : PlaneTree} (h : s.children = t.children) : s = t

Two plane trees are equal when their ordered lists of root subtrees agree.

theorem BGW.PlaneTree.ext_iff {s t : PlaneTree} : s = t ↔ s.children = t.children

@[simp]

theorem BGW.PlaneTree.children_node (ts : List PlaneTree) : (node ts).children = ts

@[simp]

theorem BGW.PlaneTree.node_children (t : PlaneTree) : node t.children = t

@[simp]

theorem BGW.PlaneTree.node_inj {ts ss : List PlaneTree} : node ts = node ss ↔ ts = ss

theorem BGW.PlaneTree.induction_on {motive : PlaneTree → Prop} (t : PlaneTree) (node : ∀ (ts : List PlaneTree), (∀ s ∈ ts, motive s) → motive (node ts)) : motive t

Induction over all the children of a root. This is the default induction principle.

def BGW.PlaneTree.casesOn {motive : PlaneTree → Sort u_1} (t : PlaneTree) (node : (ts : List PlaneTree) → motive (node ts)) : motive t

Case analysis on the children of the root. This is the default cases principle.

Equations

• BGW.PlaneTree.casesOn t node = cast ⋯ (node t.children)

@[simp]

theorem BGW.PlaneTree.casesOn_node {motive : PlaneTree → Sort u_1} (ts : List PlaneTree) (node : (ts : List PlaneTree) → motive (node ts)) : casesOn (PlaneTree.node ts) node = node ts

def BGW.PlaneTree.fold {β : Type u_1} (g : List β → β) : PlaneTree → β

Bottom-up recursion: fold g applies g to the values already computed at the children of the root, in child order.

Equations

• BGW.PlaneTree.fold g = WType.elim β fun (x : (a : ℕ) × (Fin a → β)) => match x with | ⟨fst, f⟩ => g (List.ofFn f)

@[simp]

theorem BGW.PlaneTree.fold_node {β : Type u_1} (g : List β → β) (ts : List PlaneTree) : fold g (node ts) = g (List.map (fold g) ts)

def BGW.PlaneTree.leaf : PlaneTree

The tree consisting only of its root.

Equations

• BGW.PlaneTree.leaf = BGW.PlaneTree.node []

def BGW.PlaneTree.rootDegree (t : PlaneTree) : ℕ

The number of children of the root.

Equations

• t.rootDegree = t.children.length

def BGW.PlaneTree.size : PlaneTree → ℕ

The number of vertices, including the root.

Equations

• BGW.PlaneTree.size = BGW.PlaneTree.fold fun (ns : List ℕ) => 1 + ns.sum

@[simp]

theorem BGW.PlaneTree.size_node (ts : List PlaneTree) : (node ts).size = 1 + (List.map size ts).sum

@[simp]

theorem BGW.PlaneTree.children_leaf : leaf.children = []

@[simp]

theorem BGW.PlaneTree.size_leaf : leaf.size = 1

@[simp]

theorem BGW.PlaneTree.rootDegree_node (ts : List PlaneTree) : (node ts).rootDegree = ts.length

theorem BGW.PlaneTree.size_pos (t : PlaneTree) : 0 < t.size

def BGW.PlaneTree.fringe? : PlaneTree → List ℕ → Option PlaneTree

Lookup of a fringe subtree. none means that the address is not a vertex. The returned tree is re-rooted: its addresses start at [] again.

Equations

• x✝.fringe? [] = some x✝
• x✝.fringe? (i :: u) = x✝.children[i]?.bind fun (s : BGW.PlaneTree) => s.fringe? u

def BGW.PlaneTree.IsVertex (t : PlaneTree) (u : List ℕ) : Prop

An address belongs to the tree exactly when fringe lookup succeeds.

Equations

• t.IsVertex u = ∃ (s : BGW.PlaneTree), t.fringe? u = some s

def BGW.PlaneTree.IsLeaf (t : PlaneTree) (u : List ℕ) : Prop

A leaf is a vertex whose fringe subtree consists only of its root.

Equations

• t.IsLeaf u = (t.fringe? u = some BGW.PlaneTree.leaf)

@[simp]

theorem BGW.PlaneTree.fringe?_nil (t : PlaneTree) : t.fringe? [] = some t

@[simp]

theorem BGW.PlaneTree.fringe?_cons (t : PlaneTree) (i : ℕ) (u : List ℕ) : t.fringe? (i :: u) = t.children[i]?.bind fun (s : PlaneTree) => s.fringe? u

theorem BGW.PlaneTree.fringe?_node_cons (ts : List PlaneTree) (i : ℕ) (u : List ℕ) : (node ts).fringe? (i :: u) = ts[i]?.bind fun (s : PlaneTree) => s.fringe? u