Rose trees under Gorn addresses

A Gorn address is a List ℕ path of child indices from the root, and subtreeAt navigates a rose tree by one. The addresses inside a tree are its positions (validPaths), a prefix-closed set of TreePaths, and the subtrees are the trees reached by descending through children (IsSubtree). Navigation recurses on the address, not on the tree. This file also shows that relabelling commutes with navigation, that a subtree is no larger than its tree and that a tree of height above k descends k steps. It defines vertices, which enumerates the addresses, and replaceAt, which replaces the subtree at an address.

Unlike BinaryTree.get (indexed by a PosNum left/right path) there is no indexOf: that is a binary-search-tree lookup, which has no analogue for a general rose tree.

Main declarations

• RoseTree.subtreeAt, RoseTree.validPaths: the subtree at an address, and the addresses inside a tree, prefix-closed (validPaths_prefix_closed).
• RoseTree.IsSubtree: the subtree relation, the subtrees being the values of subtreeAt (isSubtree_iff_exists_subtreeAt). It is a partial order (IsSubtree.antisymm).
• RoseTree.subtrees: the subtrees in preorder, exactly those of IsSubtree (mem_subtrees), which decides it.
• RoseTree.subtreeAt_map: relabelling commutes with navigation.
• RoseTree.exists_subtreeAt_height_sub: a maximal descent from a tree of height above k.
• RoseTree.numNodes_le_of_subtreeAt: a subtree is no larger than its tree.
• RoseTree.vertices: the addresses in preorder, one per vertex (length_vertices, nodup_vertices) and exactly those inside the tree (mem_vertices); RoseTree.positionedSubtrees pairs each with its subtree (mem_positionedSubtrees).
• RoseTree.positionedLeaves: the leaves with their addresses, exactly the leaf addresses (subtreeAt_of_mem_positionedLeaves, mem_positionedLeaves_of_subtreeAt) in the order of the frontier (map_snd_positionedLeaves), which is precedence (pairwise_precedes_positionedLeaves).
• RoseTree.replaceAt: replacement at an address, leaving the subtrees away from it unchanged (subtreeAt_replaceAt_of_not_prefix) and those above it holding the replacement (subtreeAt_replaceAt_of_prefix) and shrinking the tree when the new subtree is smaller (numNodes_replaceAt_lt). Its effect on the frontier is in RoseTree/Span.lean.

Navigation by address

def RoseTree.subtreeAt {α : Type u_1} (t : RoseTree α) : List ℕ → Option (RoseTree α)

The subtree at a Gorn address, none if the address leaves the tree.

Equations

• t.subtreeAt [] = some t
• t.subtreeAt (i :: rest) = t.children[i]?.bind fun (c : RoseTree α) => c.subtreeAt rest

@[simp]

theorem RoseTree.subtreeAt_nil {α : Type u_1} (t : RoseTree α) : t.subtreeAt [] = some t

@[simp]

theorem RoseTree.subtreeAt_cons {α : Type u_1} (t : RoseTree α) (i : ℕ) (rest : List ℕ) : t.subtreeAt (i :: rest) = t.children[i]?.bind fun (c : RoseTree α) => c.subtreeAt rest

theorem RoseTree.subtreeAt_append {α : Type u_1} (t : RoseTree α) (p q : List ℕ) : t.subtreeAt (p ++ q) = (t.subtreeAt p).bind fun (x : RoseTree α) => x.subtreeAt q

Descending along p ++ q is descending along p, then along q from there.

theorem RoseTree.subtreeAt_cons_eq_some_iff {α : Type u_1} {t s : RoseTree α} {i : ℕ} {p : List ℕ} : t.subtreeAt (i :: p) = some s ↔ ∃ (c : RoseTree α), t.children[i]? = some c ∧ c.subtreeAt p = some s

theorem RoseTree.subtreeAt_take_isSome {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) (k : ℕ) : (t.subtreeAt (List.take k p)).isSome = true

Every prefix of an address inside the tree is inside the tree.

theorem RoseTree.subtreeAt_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) (p : List ℕ) : (map f t).subtreeAt p = Option.map (map f) (t.subtreeAt p)

Relabelling commutes with subtree access.

Positions

def RoseTree.validPaths {α : Type u_1} (t : RoseTree α) : Set Core.Order.TreePath

The positions of t are the addresses inside it. Node identity is the position, never the subtree, since identical subtrees occur at several positions, so orders and graphs live on positions.

Equations

• t.validPaths = {p : Core.Order.TreePath | (t.subtreeAt p.toList).isSome = true}

theorem RoseTree.bot_mem_validPaths {α : Type u_1} (t : RoseTree α) : ⊥ ∈ t.validPaths

theorem RoseTree.mem_validPaths_cons {α : Type u_1} {t : RoseTree α} {i : ℕ} {rest : List ℕ} : { toList := i :: rest } ∈ t.validPaths ↔ ∃ (c : RoseTree α), t.children[i]? = some c ∧ { toList := rest } ∈ c.validPaths

A non-root position descends to one child and is a position there.

theorem RoseTree.validPaths_prefix_closed {α : Type u_1} {t : RoseTree α} {p q : Core.Order.TreePath} (hq : q ∈ t.validPaths) (hpq : p ≤ q) : p ∈ t.validPaths

Positions are closed under prefixes, so they inherit the rooted-tree order of TreePath.

theorem RoseTree.isLowerSet_validPaths {α : Type u_1} (t : RoseTree α) : IsLowerSet t.validPaths

theorem RoseTree.mem_validPaths_append_singleton_iff {α : Type u_1} {t : RoseTree α} {p : List ℕ} {i : ℕ} : { toList := p ++ [i] } ∈ t.validPaths ↔ ∃ (s : RoseTree α), t.subtreeAt p = some s ∧ i < s.children.length

The daughters of a position are its extensions by an index below the arity of its subtree.

Height and size along addresses

theorem RoseTree.exists_mem_children_height_add_one {α : Type u_1} {t : RoseTree α} (h : 1 < t.height) : ∃ c ∈ t.children, c.height + 1 = t.height

A node of height above 1 has a child one shorter.

theorem RoseTree.exists_subtreeAt_height_sub {α : Type u_1} (t : RoseTree α) (k : ℕ) (hk : k < t.height) : ∃ (p : List ℕ), p.length = k ∧ ∀ i ≤ k, ∃ (s : RoseTree α), t.subtreeAt (List.take i p) = some s ∧ s.height = t.height - i

A tree of height above k has a maximal descent of length k, along which the subtree at the prefix of length i has height t.height - i.

theorem RoseTree.numNodes_lt_of_mem {α : Type u_1} {t c : RoseTree α} (h : c ∈ t.children) : c.numNodes < t.numNodes

theorem RoseTree.numNodes_le_of_subtreeAt {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) : s.numNodes ≤ t.numNodes

theorem RoseTree.numNodes_lt_of_subtreeAt_cons {α : Type u_1} {t s : RoseTree α} {i : ℕ} {p : List ℕ} (h : t.subtreeAt (i :: p) = some s) : s.numNodes < t.numNodes

Subtrees

def RoseTree.IsSubtree {α : Type u_1} (s t : RoseTree α) : Prop

IsSubtree s t holds when s is the subtree of t rooted at one of its nodes, reached from t by descending through children.

Equations

• s.IsSubtree t = Relation.ReflTransGen (fun (c u : RoseTree α) => c ∈ u.children) s t

theorem RoseTree.IsSubtree.refl {α : Type u_1} (t : RoseTree α) : t.IsSubtree t

theorem RoseTree.IsSubtree.trans {α : Type u_1} {r s t : RoseTree α} (h₁ : r.IsSubtree s) (h₂ : s.IsSubtree t) : r.IsSubtree t

@[instance_reducible]

instance RoseTree.instTransIsSubtree {α : Type u_1} : Trans IsSubtree IsSubtree IsSubtree

Equations

• RoseTree.instTransIsSubtree = { trans := ⋯ }

theorem RoseTree.IsSubtree.of_mem_children {α : Type u_1} {c t : RoseTree α} (h : c ∈ t.children) : c.IsSubtree t

theorem RoseTree.isSubtree_iff_exists_subtreeAt {α : Type u_1} {s t : RoseTree α} : s.IsSubtree t ↔ ∃ (p : List ℕ), t.subtreeAt p = some s

The subtrees of t are exactly the values of subtreeAt t at addresses inside t.

theorem RoseTree.isSubtree_node_iff {α : Type u_1} {s : RoseTree α} {a : α} {cs : List (RoseTree α)} : s.IsSubtree (node a cs) ↔ s = node a cs ∨ ∃ c ∈ cs, s.IsSubtree c

@[simp]

theorem RoseTree.isSubtree_leaf_iff {α : Type u_1} {s : RoseTree α} {a : α} : s.IsSubtree (leaf a) ↔ s = leaf a

theorem RoseTree.IsSubtree.numNodes_le {α : Type u_1} {s t : RoseTree α} (h : s.IsSubtree t) : s.numNodes ≤ t.numNodes

A subtree is no larger than its tree.

theorem RoseTree.IsSubtree.eq_of_numNodes_le {α : Type u_1} {s t : RoseTree α} (h : s.IsSubtree t) (hn : t.numNodes ≤ s.numNodes) : s = t

A subtree as large as its tree is the tree.

theorem RoseTree.IsSubtree.antisymm {α : Type u_1} {s t : RoseTree α} (h₁ : s.IsSubtree t) (h₂ : t.IsSubtree s) : s = t

def RoseTree.subtrees {α : Type u_1} : RoseTree α → List (RoseTree α)

subtrees t lists the subtrees of t in preorder, t first, one per vertex.

Equations

• (RoseTree.node value cs).subtrees = RoseTree.node value cs :: RoseTree.subtreesList cs

def RoseTree.subtreesList {α : Type u_1} : List (RoseTree α) → List (RoseTree α)

subtreesList cs lists the subtrees of the trees of cs.

Equations

• RoseTree.subtreesList [] = []
• RoseTree.subtreesList (c :: cs) = c.subtrees ++ RoseTree.subtreesList cs

theorem RoseTree.subtreesList_eq {α : Type u_1} (cs : List (RoseTree α)) : subtreesList cs = List.flatMap subtrees cs

@[simp]

theorem RoseTree.subtrees_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).subtrees = node a cs :: List.flatMap subtrees cs

theorem RoseTree.mem_subtrees {α : Type u_1} {s t : RoseTree α} : s ∈ t.subtrees ↔ s.IsSubtree t

The listed subtrees are exactly the subtrees.

theorem RoseTree.self_mem_subtrees {α : Type u_1} (t : RoseTree α) : t ∈ t.subtrees

@[instance_reducible]

instance RoseTree.instDecidableIsSubtreeOfDecidableEq {α : Type u_1} [DecidableEq α] (s t : RoseTree α) : Decidable (s.IsSubtree t)

Equations

• s.instDecidableIsSubtreeOfDecidableEq t = decidable_of_iff (s ∈ t.subtrees) ⋯

Enumerating the addresses

def RoseTree.vertices {α : Type u_1} : RoseTree α → List (List ℕ)

vertices t lists the addresses of the vertices of t in preorder, the root [] first.

Equations

• (RoseTree.node value cs).vertices = [] :: RoseTree.verticesList cs

def RoseTree.verticesList {α : Type u_1} : List (RoseTree α) → List (List ℕ)

verticesList cs lists the addresses of the vertices of the forest cs, each starting with the index of its tree.

Equations

• RoseTree.verticesList [] = []
• RoseTree.verticesList (c :: cs) = List.map (fun (x : List ℕ) => 0 :: x) c.vertices ++ List.map (List.modifyHead fun (x : ℕ) => x + 1) (RoseTree.verticesList cs)

@[simp]

theorem RoseTree.vertices_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).vertices = [] :: verticesList cs

@[simp]

theorem RoseTree.verticesList_nil {α : Type u_1} : verticesList [] = []

@[simp]

theorem RoseTree.verticesList_cons {α : Type u_1} (c : RoseTree α) (cs : List (RoseTree α)) : verticesList (c :: cs) = List.map (fun (x : List ℕ) => 0 :: x) c.vertices ++ List.map (List.modifyHead fun (x : ℕ) => x + 1) (verticesList cs)

theorem RoseTree.mem_verticesList {α : Type u_1} {cs : List (RoseTree α)} {p : List ℕ} : p ∈ verticesList cs ↔ ∃ (j : ℕ) (q : List ℕ) (c : RoseTree α), p = j :: q ∧ cs[j]? = some c ∧ q ∈ c.vertices

theorem RoseTree.exists_cons_of_mem_verticesList {α : Type u_1} {cs : List (RoseTree α)} {p : List ℕ} (hp : p ∈ verticesList cs) : ∃ (j : ℕ) (q : List ℕ), p = j :: q

theorem RoseTree.mem_vertices {α : Type u_1} {t : RoseTree α} {p : List ℕ} : p ∈ t.vertices ↔ (t.subtreeAt p).isSome = true

The addresses listed by vertices t are exactly the addresses inside t.

theorem RoseTree.length_vertices {α : Type u_1} (t : RoseTree α) : t.vertices.length = t.numNodes

theorem RoseTree.length_verticesList {α : Type u_1} (cs : List (RoseTree α)) : (verticesList cs).length = (List.map numNodes cs).sum

theorem RoseTree.nodup_vertices {α : Type u_1} (t : RoseTree α) : t.vertices.Nodup

theorem RoseTree.nodup_verticesList {α : Type u_1} (cs : List (RoseTree α)) : (verticesList cs).Nodup

def RoseTree.positionedSubtrees {α : Type u_1} (t : RoseTree α) : List (Core.Order.TreePath × RoseTree α)

The subtrees of t with their positions, in preorder.

Equations

• t.positionedSubtrees = List.filterMap (fun (p : List ℕ) => Option.map (fun (x : RoseTree α) => ({ toList := p }, x)) (t.subtreeAt p)) t.vertices

theorem RoseTree.mem_positionedSubtrees {α : Type u_1} {t s : RoseTree α} {p : Core.Order.TreePath} : (p, s) ∈ t.positionedSubtrees ↔ t.subtreeAt p.toList = some s

theorem RoseTree.nodup_map_fst_positionedSubtrees {α : Type u_1} (t : RoseTree α) : (List.map Prod.fst t.positionedSubtrees).Nodup

The leaves with their addresses

def RoseTree.positionedLeaves {α : Type u_1} : RoseTree α → List (Core.Order.TreePath × α)

positionedLeaves t lists the leaves of t from left to right, each with its address.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RoseTree.positionedLeaves_leaf {α : Type u_1} (a : α) : (node a []).positionedLeaves = [(⊥, a)]

theorem RoseTree.positionedLeaves_node_of_ne_nil {α : Type u_1} (a : α) {cs : List (RoseTree α)} (h : cs ≠ []) : (node a cs).positionedLeaves = List.flatMap (fun (x : RoseTree α × ℕ) => match x with | (c, i) => List.map (fun (x : Core.Order.TreePath × α) => ({ toList := i :: x.1.toList }, x.2)) c.positionedLeaves) cs.zipIdx

theorem RoseTree.map_snd_positionedLeaves {α : Type u_1} (t : RoseTree α) : List.map Prod.snd t.positionedLeaves = t.leafList

Forgetting the addresses leaves the frontier.

theorem RoseTree.subtreeAt_of_mem_positionedLeaves {α : Type u_1} {t : RoseTree α} {x : Core.Order.TreePath × α} (h : x ∈ t.positionedLeaves) : t.subtreeAt x.1.toList = some (node x.2 [])

Each listed address holds its leaf.

theorem RoseTree.mem_positionedLeaves_of_subtreeAt {α : Type u_1} {t : RoseTree α} {p : List ℕ} {a : α} (h : t.subtreeAt p = some (node a [])) : ({ toList := p }, a) ∈ t.positionedLeaves

Every leaf address is listed.

theorem RoseTree.pairwise_precedes_positionedLeaves {α : Type u_1} (t : RoseTree α) : List.Pairwise (fun (x y : Core.Order.TreePath × α) => x.1.Precedes y.1) t.positionedLeaves

The leaf addresses, in the order of the frontier, ascend in precedence.

Replacement at an address

def RoseTree.replaceAt {α : Type u_1} : RoseTree α → List ℕ → RoseTree α → RoseTree α

Replace the subtree at a Gorn address; an address outside the tree leaves it unchanged.

Equations

• x✝¹.replaceAt [] x✝ = x✝
• (RoseTree.node a cs).replaceAt (i :: p) x✝ = RoseTree.node a (cs.modify i fun (x : RoseTree α) => x.replaceAt p x✝)

@[simp]

theorem RoseTree.replaceAt_nil {α : Type u_1} (t new : RoseTree α) : t.replaceAt [] new = new

theorem RoseTree.replaceAt_cons {α : Type u_1} (a : α) (cs : List (RoseTree α)) (i : ℕ) (p : List ℕ) (new : RoseTree α) : (node a cs).replaceAt (i :: p) new = node a (cs.modify i fun (x : RoseTree α) => x.replaceAt p new)

@[simp]

theorem RoseTree.children_replaceAt_cons {α : Type u_1} (t : RoseTree α) (i : ℕ) (p : List ℕ) (new : RoseTree α) : (t.replaceAt (i :: p) new).children = t.children.modify i fun (x : RoseTree α) => x.replaceAt p new

Replacing below the root replaces inside one child.

@[simp]

theorem RoseTree.value_replaceAt_cons {α : Type u_1} (t : RoseTree α) (i : ℕ) (p : List ℕ) (new : RoseTree α) : (t.replaceAt (i :: p) new).value = t.value

theorem RoseTree.value_replaceAt {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) {new : RoseTree α} (hv : new.value = s.value) : (t.replaceAt p new).value = t.value

Replacing a subtree by one with the same root value keeps the root value.

theorem RoseTree.replaceAt_cons_of_getElem? {α : Type u_1} {t c : RoseTree α} {i : ℕ} (hc : t.children[i]? = some c) (p : List ℕ) (new : RoseTree α) : t.replaceAt (i :: p) new = node t.value (t.children.set i (c.replaceAt p new))

theorem RoseTree.subtreeAt_replaceAt_of_not_prefix {α : Type u_1} {t new : RoseTree α} {p q : List ℕ} (hpq : ¬p <+: q) (hqp : ¬q <+: p) : (t.replaceAt p new).subtreeAt q = t.subtreeAt q

Away from the replaced address, at an address neither above nor below it, the subtree is unchanged.

theorem RoseTree.subtreeAt_replaceAt_of_prefix {α : Type u_1} {t new : RoseTree α} {p q : List ℕ} (hqp : q <+: p) : (t.replaceAt p new).subtreeAt q = Option.map (fun (x : RoseTree α) => x.replaceAt (List.drop q.length p) new) (t.subtreeAt q)

At an address above the replaced one, the subtree has the replacement inside it.

theorem RoseTree.subtreeAt_replaceAt_append {α : Type u_1} {t new : RoseTree α} {p : List ℕ} (hp : (t.subtreeAt p).isSome = true) (q : List ℕ) : (t.replaceAt p new).subtreeAt (p ++ q) = new.subtreeAt q

At an address below the replaced one, the subtree is that of the replacement.

theorem RoseTree.numNodes_replaceAt_lt {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) {new : RoseTree α} (hlt : new.numNodes < s.numNodes) : (t.replaceAt p new).numNodes < t.numNodes

Replacing a subtree by a strictly smaller one shrinks the tree.