Fringe subtrees and replacement

Lookup uses zero-based addresses. Replacing the subtree at a valid address identifies the old and new roots; replacement at a leaf is leaf grafting. Replacement at an invalid address leaves the tree unchanged.

theorem BGW.PlaneTree.fringe?_append (t : PlaneTree) (u v : List ℕ) : t.fringe? (u ++ v) = (t.fringe? u).bind fun (s : PlaneTree) => s.fringe? v

Taking a fringe subtree re-roots all its descendant addresses.

@[simp]

theorem BGW.PlaneTree.isVertex_nil (t : PlaneTree) : t.IsVertex []

theorem BGW.PlaneTree.isVertex_append_iff (t : PlaneTree) (u v : List ℕ) : t.IsVertex (u ++ v) ↔ ∃ (s : PlaneTree), t.fringe? u = some s ∧ s.IsVertex v

theorem BGW.PlaneTree.IsVertex.prefix {t : PlaneTree} {u v : List ℕ} (h : t.IsVertex (u ++ v)) : t.IsVertex u

Every prefix of a vertex address is a vertex address.

@[simp]

theorem BGW.PlaneTree.isVertex_singleton_iff (t : PlaneTree) (i : ℕ) : t.IsVertex [i] ↔ i < t.rootDegree

Children form an initial segment, with no gaps.

theorem BGW.PlaneTree.isVertex_append_singleton_iff {t s : PlaneTree} {u : List ℕ} (h : t.fringe? u = some s) (i : ℕ) : t.IsVertex (u ++ [i]) ↔ i < s.rootDegree

The children of any vertex are precisely an initial segment.

theorem BGW.PlaneTree.IsLeaf.isVertex {t : PlaneTree} {u : List ℕ} (h : t.IsLeaf u) : t.IsVertex u

@[simp]

theorem BGW.PlaneTree.isLeaf_nil_iff (t : PlaneTree) : t.IsLeaf [] ↔ t = leaf

def BGW.PlaneTree.graft : PlaneTree → List ℕ → PlaneTree → PlaneTree

Replace the fringe subtree at an address, preserving the ordered context. At a leaf this is the grafting operation used in cut-and-graft arguments.

Equations

• x✝¹.graft [] x✝ = x✝
• x✝¹.graft (i :: u) x✝ = BGW.PlaneTree.node (x✝¹.children.modify i fun (r : BGW.PlaneTree) => r.graft u x✝)

def BGW.PlaneTree.cut (t : PlaneTree) (u : List ℕ) : PlaneTree

Remove strict descendants of an address, retaining that vertex as a leaf.

Equations

• t.cut u = t.graft u BGW.PlaneTree.leaf

@[simp]

theorem BGW.PlaneTree.graft_nil (t s : PlaneTree) : t.graft [] s = s

@[simp]

theorem BGW.PlaneTree.graft_cons (t s : PlaneTree) (i : ℕ) (u : List ℕ) : t.graft (i :: u) s = node (t.children.modify i fun (r : PlaneTree) => r.graft u s)

theorem BGW.PlaneTree.fringe?_graft {t : PlaneTree} {u : List ℕ} (h : t.IsVertex u) (s : PlaneTree) : (t.graft u s).fringe? u = some s

The inserted tree is exactly the fringe subtree at the graft address.

theorem BGW.PlaneTree.graft_fringe {t r : PlaneTree} {u : List ℕ} (h : t.fringe? u = some r) : t.graft u r = t

Replacing a fringe subtree by itself recovers the original tree.

theorem BGW.PlaneTree.graft_graft (t s r : PlaneTree) (u : List ℕ) : (t.graft u s).graft u r = t.graft u r

Repeated replacements at one address keep only the last replacement.

theorem BGW.PlaneTree.isLeaf_cut {t : PlaneTree} {u : List ℕ} (h : t.IsVertex u) : (t.cut u).IsLeaf u

theorem BGW.PlaneTree.graft_cut {t r : PlaneTree} {u : List ℕ} (h : t.fringe? u = some r) : (t.cut u).graft u r = t

Cutting and restoring the removed fringe reconstructs the original tree.

theorem BGW.PlaneTree.size_graft_add {t r : PlaneTree} {u : List ℕ} (h : t.fringe? u = some r) (s : PlaneTree) : (t.graft u s).size + r.size = t.size + s.size

Subtree replacement removes exactly the old fringe and inserts the new one.

theorem BGW.PlaneTree.size_graft_of_isLeaf {t : PlaneTree} {u : List ℕ} (h : t.IsLeaf u) (s : PlaneTree) : (t.graft u s).size + 1 = t.size + s.size

Leaf grafting identifies the leaf with the inserted root.

theorem BGW.PlaneTree.graft_of_fringe?_eq_none {t : PlaneTree} {u : List ℕ} (h : t.fringe? u = none) (s : PlaneTree) : t.graft u s = t

A failed lookup cannot create a new branch by grafting.