Multi-path grafting on RoseTree α

multiGraft T pairs grafts trees onto T at several paths simultaneously, every path read in the original T (Foissy's convention). Several pairs may share a path; their trees are prepended in pair-list order, so multiGraft is order-sensitive, and commutativity is recovered at the multiset level in Insertion.lean.

Main definitions and results

• multiGraft, multiGraftChildren: the mutual recursion. multiGraftChildren descends by shifting path indices: pairs starting 0 :: rest go to the head child as (rest, t), pairs starting (k + 1) :: rest go to the tail as (k :: rest, t).
• rootPrependFilter, headChildFilter, tailChildFilter: the three pair projections, with their List.filter characterizations.
• multiGraft_nil: no pairs, no change.
• multiGraft_singleton: one pair is insertAt.

References

• [foissy-typed-decorated-rooted-trees-2018]
• [Foi]

§1: Filter helpers (top-level for matcher stability)

The multiGraft recursion uses three pair-filtering functions: extracting root-prepends (empty path), extracting head-child pairs (first index 0), and shifting tail-child pairs (first index k+1). Each is defined as a top-level function so that all filterMap callers reference the same elaborated matcher — rw with filter equalities then works cleanly across files. Without this, Lean's inline-match elaboration generates fresh match_N aux constants per scope, blocking unification.

Each helper carries unfolding @[simp] lemmas on every pattern so that simp can reduce them where rfl would otherwise fail.

def RoseTree.Pathed.rootPrependFilter {α : Type u_1} (pair : Path × RoseTree α) : Option (RoseTree α)

Extract pair as root prepend iff its path is empty.

Equations

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

@[simp]

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

@[simp]

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

def RoseTree.Pathed.headChildFilter {α : Type u_1} (pair : Path × RoseTree α) : Option (Path × RoseTree α)

Extract pair as head-child pair iff its path starts with 0, stripping the leading index.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

def RoseTree.Pathed.tailChildFilter {α : Type u_1} (pair : Path × RoseTree α) : Option (Path × RoseTree α)

Extract pair as tail-child pair iff its path starts with k+1, decrementing the leading index by one.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

§2: multiGraft mutual definition

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

multiGraft T pairs: walk T, prepend the trees assigned to each path. Pairs whose path is [] graft at the root (prepended to the children list in pair-list order). Pairs whose path is i :: rest descend into the i-th child with the projected pair (rest, _).

Equations

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

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

Auxiliary: descend pair list into children. Pairs with first index 0 apply to the head child (with the rest of the path); pairs with first index k+1 are forwarded to the tail (with the rest of the list and index decremented).

Equations

• One or more equations did not get rendered due to their size.
• RoseTree.Pathed.multiGraftChildren [] x✝ = []

@[simp]

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

@[simp]

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

@[simp]

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

Filter characterizations

Each pair filter is a List.filter on the path followed by a projection, so pair lists can be bucketed by a predicate on paths (bind_listChoices_filter in Insertion.lean).

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

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

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

theorem RoseTree.Pathed.multiGraftChildren_congr {α : Type u_1} {cs : List (RoseTree α)} {pairs₁ pairs₂ : List (Path × 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.Pathed.multiGraftChildren_filter_ne_nil {α : Type u_1} (cs : List (RoseTree α)) (pairs : List (Path × RoseTree α)) : multiGraftChildren cs (List.filter (fun (p : Path × RoseTree α) => decide ¬p.1 = []) pairs) = multiGraftChildren cs pairs

Root pairs never reach the children.

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

multiGraftChildren cs pairs has the same length as cs.

§3: Nil identity

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

Empty pair list: multiGraft is the identity.

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

Empty pair list: multiGraftChildren is the identity on the children list.

§4: Singleton bridge to insertAt

A single-pair multiGraft is exactly insertAt. The proof splits into:

• §4.1 multiGraftChildren cs [([], T₂)] = cs — the empty path contributes only to root prepends, not to the children.
• §4.2 multiGraftChildren cs [(j :: rest, T₂)] agrees with cs.set j when j < cs.length, else is the identity.
• §4.3 Top-level multiGraft_singleton combines these.

theorem RoseTree.Pathed.multiGraft_singleton {α : Type u_1} (T : RoseTree α) (p : Path) (T₂ : RoseTree α) : multiGraft T [(p, T₂)] = insertAt p T₂ T

Single-pair multiGraft is insertAt. Bridges the multi-graft primitive to the single-vertex insertion in Insert.lean.