Node-host decomposition of the multi-graft insertion

For a single-tree host node a cs, the vertex set splits as {root} ⊔ vertices(cs), so the simultaneous multi-graft insertion decomposes by which guests land at the root (they are prepended as new children) versus inside the child forest (a recursive insertionForest). This is the node-level analog of insertionMultiset_add_host's forest-append bucketing (InsertionAddHost.lean).

Main results

• listChoices_alphabet_split: choices over an appended alphabet ys ++ zs enumerate as a boolean mask plus per-bucket choices, recombined by mergeMask.
• insertionForest_eq_multiGraftChildren_choices: the vertex-choice form of insertionForest — grafting into a host forest cs is the sum over verticesAux 0 cs-choices of multiGraftChildren.
• insertion_node_split: the headline RoseTree-level decomposition of insertion (node a cs) gs by root-vs-subtree guest masks.

All three statements are validated computationally on concrete trees (multi-vertex hosts, repeated guests, empty edge cases) prior to proof.

mergeMask — interleave two bucket lists along a boolean mask

def RoseTree.Pathed.mergeMask {X : Type u_2} : List Bool → List X → List X → List X

Interleave us (used at true positions) and ws (used at false positions) along the mask m. Off-length inputs truncate.

Equations

• RoseTree.Pathed.mergeMask [] x✝¹ x✝ = []
• RoseTree.Pathed.mergeMask (true :: m) (u :: us) x✝ = u :: RoseTree.Pathed.mergeMask m us x✝
• RoseTree.Pathed.mergeMask (true :: tail) [] x✝ = []
• RoseTree.Pathed.mergeMask (false :: m) x✝ (w :: ws) = w :: RoseTree.Pathed.mergeMask m x✝ ws
• RoseTree.Pathed.mergeMask (false :: tail) x✝ [] = []

@[simp]

theorem RoseTree.Pathed.mergeMask_nil {X : Type u_2} (us ws : List X) : mergeMask [] us ws = []

@[simp]

theorem RoseTree.Pathed.mergeMask_true_cons {X : Type u_2} (m : List Bool) (u : X) (us ws : List X) : mergeMask (true :: m) (u :: us) ws = u :: mergeMask m us ws

@[simp]

theorem RoseTree.Pathed.mergeMask_false_cons {X : Type u_2} (m : List Bool) (us : List X) (w : X) (ws : List X) : mergeMask (false :: m) us (w :: ws) = w :: mergeMask m us ws

Alphabet split for listChoices

theorem RoseTree.Pathed.listChoices_alphabet_split {X : Type u_2} {γ : Type u_3} (ys zs : List X) (n : ℕ) (g : List X → Multiset γ) : (↑(listChoices (ys ++ zs) n)).bind g = (↑(listChoices [true, false] n)).bind fun (m : List Bool) => (↑(listChoices ys (List.count true m))).bind fun (u : List X) => (↑(listChoices zs (List.count false m))).bind fun (w : List X) => g (mergeMask m u w)

Choices over an appended alphabet enumerate as: a boolean mask over the positions, a choice vector over ys for the true positions, and a choice vector over zs for the false positions, recombined by mergeMask.

theorem RoseTree.Pathed.listChoices_singleton {X : Type u_2} (x : X) (n : ℕ) : listChoices [x] n = [List.replicate n x]

Choices over a singleton alphabet: the constant vector.

Index shift for verticesAux

filterMap plumbing through mergeMask-zips

multiGraft's three pair filters (rootPrependFilter, headChildFilter, tailChildFilter) each kill all pairs from one bucket of a mergeMask-interleaved choice vector; the surviving bucket zips against its own guests.

Vertex-choice form of insertionForest

theorem RoseTree.Pathed.insertionForest_eq_multiGraftChildren_choices {α : Type u_1} (cs gs : List (RoseTree α)) : insertionForest cs gs = ↑(List.map (fun (ch : List Path) => multiGraftChildren cs (ch.zip gs)) (listChoices (verticesAux 0 cs) gs.length))

Grafting a guest list into a host forest, in vertex-choice form: insertionForest cs gs is the sum over assignments of each guest to a forest vertex (a verticesAux 0 cs path) of the simultaneous multiGraftChildren.

The node-host decomposition

theorem RoseTree.Pathed.insertion_node_split {α : Type u_1} (a : α) (cs gs : List (RoseTree α)) : insertion (node a cs) gs = (↑(listChoices [true, false] gs.length)).bind fun (m : List Bool) => Multiset.map (fun (cs' : List (RoseTree α)) => node a (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) (gs.zip m) ++ cs')) (insertionForest cs (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) (gs.zip m)))

Node-host decomposition of the simultaneous multi-graft: guests split by a boolean mask into root-guests (prepended as new children, in guest order) and subtree-guests (an insertionForest into the child forest).