Simultaneous grafting on rose trees

This file defines multiGraft T pairs, which grafts several trees onto T at once. Each pair (p, S) names a vertex of T by its address p and a tree S to become a new child of that vertex; every address is read in the original T, as in Foissy's multiple grafting. Trees grafted at the same vertex are prepended in the order of the pair list, so multiGraft depends on that order, and Insertion.lean recovers independence of it once children are unordered.

Main definitions

• multiGraft, multiGraftChildren: simultaneous grafting into a tree and into a forest.
• rootPrependFilter, headChildFilter, tailChildFilter: the pairs aimed at the root, at the first child, and at the later children, with the addresses shortened accordingly.

Main results

• filterMap_rootPrependFilter, filterMap_headChildFilter, filterMap_tailChildFilter: each filter is a List.filter on the address followed by a projection.
• multiGraft_nil: grafting nothing leaves the tree unchanged.

Implementation notes

The three filters are top-level definitions rather than inline match expressions so that every caller elaborates the same matcher, which lets their filterMap equations rewrite across files.

References

• [Foi21]
• [Foi]

Routing the pairs

def RoseTree.rootPrependFilter {α : Type u_1} (pair : List ℕ × RoseTree α) : Option (RoseTree α)

A pair aimed at the root yields its tree.

Equations

• RoseTree.rootPrependFilter pair = match pair.1 with | [] => some pair.2 | head :: tail => none

@[simp]

theorem RoseTree.rootPrependFilter_of_nil {α : Type u_1} (T : RoseTree α) : rootPrependFilter ([], T) = some T

@[simp]

theorem RoseTree.rootPrependFilter_of_cons {α : Type u_1} (i : ℕ) (rest : List ℕ) (T : RoseTree α) : rootPrependFilter (i :: rest, T) = none

def RoseTree.headChildFilter {α : Type u_1} (pair : List ℕ × RoseTree α) : Option (List ℕ × RoseTree α)

A pair aimed inside the first child yields the pair with the leading index removed.

Equations

• RoseTree.headChildFilter pair = match pair.1 with | 0 :: rest => some (rest, pair.2) | x => none

@[simp]

theorem RoseTree.headChildFilter_of_nil {α : Type u_1} (T : RoseTree α) : headChildFilter ([], T) = none

@[simp]

theorem RoseTree.headChildFilter_of_zero_cons {α : Type u_1} (rest : List ℕ) (T : RoseTree α) : headChildFilter (0 :: rest, T) = some (rest, T)

@[simp]

theorem RoseTree.headChildFilter_of_succ_cons {α : Type u_1} (k : ℕ) (rest : List ℕ) (T : RoseTree α) : headChildFilter ((k + 1) :: rest, T) = none

def RoseTree.tailChildFilter {α : Type u_1} (pair : List ℕ × RoseTree α) : Option (List ℕ × RoseTree α)

A pair aimed inside a later child yields the pair with the leading index decremented.

Equations

• RoseTree.tailChildFilter pair = match pair.1 with | k.succ :: rest => some (k :: rest, pair.2) | x => none

@[simp]

theorem RoseTree.tailChildFilter_of_nil {α : Type u_1} (T : RoseTree α) : tailChildFilter ([], T) = none

@[simp]

theorem RoseTree.tailChildFilter_of_zero_cons {α : Type u_1} (rest : List ℕ) (T : RoseTree α) : tailChildFilter (0 :: rest, T) = none

@[simp]

theorem RoseTree.tailChildFilter_of_succ_cons {α : Type u_1} (k : ℕ) (rest : List ℕ) (T : RoseTree α) : tailChildFilter ((k + 1) :: rest, T) = some (k :: rest, T)

Simultaneous grafting

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

multiGraft T pairs grafts the tree of each pair at the vertex its address names. The trees aimed at the root are prepended to its children in pair-list order; the other pairs descend into the child their first index names.

Equations

• (RoseTree.node a cs).multiGraft x✝ = RoseTree.node a (List.filterMap RoseTree.rootPrependFilter x✝ ++ RoseTree.multiGraftChildren cs x✝)

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

multiGraftChildren cs pairs grafts into the forest cs, where the first index of each address names a tree of cs.

Equations

• RoseTree.multiGraftChildren [] x✝ = []
• RoseTree.multiGraftChildren (c :: cs) x✝ = c.multiGraft (List.filterMap RoseTree.headChildFilter x✝) :: RoseTree.multiGraftChildren cs (List.filterMap RoseTree.tailChildFilter x✝)

@[simp]

theorem RoseTree.multiGraft_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) (pairs : List (List ℕ × RoseTree α)) : (node a cs).multiGraft pairs = node a (List.filterMap rootPrependFilter pairs ++ multiGraftChildren cs pairs)

@[simp]

theorem RoseTree.multiGraftChildren_nil_cs {α : Type u_1} (pairs : List (List ℕ × RoseTree α)) : multiGraftChildren [] pairs = []

@[simp]

theorem RoseTree.multiGraftChildren_cons_cs {α : Type u_1} (c : RoseTree α) (cs : List (RoseTree α)) (pairs : List (List ℕ × RoseTree α)) : multiGraftChildren (c :: cs) pairs = c.multiGraft (List.filterMap headChildFilter pairs) :: multiGraftChildren cs (List.filterMap tailChildFilter pairs)

Filter characterizations

Each pair filter is a List.filter on the address followed by a projection, so Insertion.lean can split the pair lists by a predicate on addresses.

theorem RoseTree.filterMap_rootPrependFilter {α : Type u_1} (pairs : List (List ℕ × RoseTree α)) : List.filterMap rootPrependFilter pairs = List.map Prod.snd (List.filter (fun (p : List ℕ × RoseTree α) => decide (p.1 = [])) pairs)

theorem RoseTree.filterMap_headChildFilter {α : Type u_1} (pairs : List (List ℕ × RoseTree α)) : List.filterMap headChildFilter pairs = List.map (Prod.map List.tail id) (List.filter (fun (p : List ℕ × RoseTree α) => decide (p.1.head? = some 0)) pairs)

theorem RoseTree.filterMap_tailChildFilter {α : Type u_1} (pairs : List (List ℕ × RoseTree α)) (h : ∀ p ∈ pairs, p.1 ≠ []) : List.filterMap tailChildFilter pairs = List.map (Prod.map (List.modifyHead fun (x : ℕ) => x - 1) id) (List.filter (fun (p : List ℕ × RoseTree α) => decide ¬p.1.head? = some 0) pairs)

@[simp]

theorem RoseTree.value_multiGraft {α : Type u_1} (T : RoseTree α) (pairs : List (List ℕ × RoseTree α)) : (T.multiGraft pairs).value = T.value

Grafting keeps the root value.

theorem RoseTree.multiGraftChildren_congr {α : Type u_1} {cs : List (RoseTree α)} {pairs₁ pairs₂ : List (List ℕ × RoseTree α)} (h₁ : List.filterMap headChildFilter pairs₁ = List.filterMap headChildFilter pairs₂) (h₂ : List.filterMap tailChildFilter pairs₁ = List.filterMap tailChildFilter pairs₂) : multiGraftChildren cs pairs₁ = multiGraftChildren cs pairs₂

multiGraftChildren depends on its pair list only through the two child filters.

theorem RoseTree.multiGraftChildren_filter_ne_nil {α : Type u_1} (cs : List (RoseTree α)) (pairs : List (List ℕ × RoseTree α)) : multiGraftChildren cs (List.filter (fun (p : List ℕ × RoseTree α) => decide ¬p.1 = []) pairs) = multiGraftChildren cs pairs

Root pairs never reach the children.

theorem RoseTree.multiGraftChildren_length {α : Type u_1} (cs : List (RoseTree α)) (pairs : List (List ℕ × RoseTree α)) : (multiGraftChildren cs pairs).length = cs.length

multiGraftChildren cs pairs has the same length as cs.

theorem RoseTree.multiGraft_nil {α : Type u_1} (T : RoseTree α) : T.multiGraft [] = T

Grafting nothing leaves a tree unchanged.

theorem RoseTree.multiGraftChildren_nil_pairs {α : Type u_1} (cs : List (RoseTree α)) : multiGraftChildren cs [] = cs

Grafting nothing leaves a forest unchanged.