Multi-tree insertion on rose trees

This file defines the insertion of several guest trees into a host. For a host T and guests gs, insertion T gs is the multiset, over all assignments of the guests to vertices of T, of the trees obtained by grafting every guest at its vertex at once (multiGraft); insertionForest does the same for a host forest. This is the Guin–Oudom extension of the grafting pre-Lie product to several guests, in the form Foissy gives for decorated trees.

Main definitions

• insertion, insertionForest: multi-tree insertion into a tree and into a forest.

Main results

• insertion_node, insertionForest_cons, insertionForest_append: the guests split between the root and the children, or between two parts of the host forest.
• insertionForest_bind_revzip_sublists': splitting an output forest splits the hosts and the guests, each guest following its host.
• insertion_node_msform, insertionForest_cons_msform: the two recursions read through UnorderedTree.mk.

References

• [Foi21]
• [Foi]

Assignments of guests to vertices

An assignment of n guests to the vertices xs is a section of replicate n xs, a word of length n over xs.

insertion: single-tree host

def RoseTree.insertion {α : Type u_1} (T : RoseTree α) (Ts : List (RoseTree α)) : Multiset (RoseTree α)

insertion T [T₁, …, Tₙ] is the multiset, over (v₁, …, vₙ) ∈ V(T)ⁿ, of multiGraft T [(v₁, T₁), …, (vₙ, Tₙ)].

Equations

• T.insertion Ts = ↑(List.map (fun (choice : List (List ℕ)) => T.multiGraft (choice.zip Ts)) (List.replicate Ts.length T.vertices).sections)

theorem RoseTree.insertion_def {α : Type u_1} (T : RoseTree α) (Ts : List (RoseTree α)) : T.insertion Ts = ↑(List.map (fun (choice : List (List ℕ)) => T.multiGraft (choice.zip Ts)) (List.replicate Ts.length T.vertices).sections)

insertionForest: forest host

def RoseTree.insertionForest {α : Type u_1} (cs gs : List (RoseTree α)) : Multiset (List (RoseTree α))

insertionForest cs gs is the multiset, over assignments of the guests gs to vertices of the forest cs, of the simultaneous grafts multiGraftChildren.

Equations

• RoseTree.insertionForest cs gs = ↑(List.map (fun (ch : List (List ℕ)) => RoseTree.multiGraftChildren cs (ch.zip gs)) (List.replicate gs.length (RoseTree.verticesList cs)).sections)

theorem RoseTree.insertionForest_def {α : Type u_1} (cs gs : List (RoseTree α)) : insertionForest cs gs = ↑(List.map (fun (ch : List (List ℕ)) => multiGraftChildren cs (ch.zip gs)) (List.replicate gs.length (verticesList cs)).sections)

@[simp]

theorem RoseTree.insertionForest_nil_nil {α : Type u_1} : insertionForest [] [] = {[]}

@[simp]

theorem RoseTree.insertionForest_empty_host_nonempty_guests {α : Type u_1} (T_g : RoseTree α) (Ts : List (RoseTree α)) : insertionForest [] (T_g :: Ts) = 0

@[simp]

theorem RoseTree.insertionForest_cons_host_nil_guests {α : Type u_1} (T : RoseTree α) (F : List (RoseTree α)) : insertionForest (T :: F) [] = {T :: F}

theorem RoseTree.insertionForest_nil_guests {α : Type u_1} (F : List (RoseTree α)) : insertionForest F [] = {F}

theorem RoseTree.value_of_mem_insertion {α : Type u_1} {T T' : RoseTree α} {gs : List (RoseTree α)} (h : T' ∈ T.insertion gs) : T'.value = T.value

Every output of insertion T gs has the root value of T.

theorem RoseTree.length_of_mem_insertionForest {α : Type u_1} {cs gs L : List (RoseTree α)} (h : L ∈ insertionForest cs gs) : L.length = cs.length

Every output of insertionForest cs gs has as many trees as cs.

theorem RoseTree.insertionForest_cons {α : Type u_1} (T : RoseTree α) (F gs : List (RoseTree α)) : insertionForest (T :: F) gs = (↑gs.sublists'.revzip).bind fun (p : List (RoseTree α) × List (RoseTree α)) => (T.insertion p.1).bind fun (T' : RoseTree α) => Multiset.map (fun (x : List (RoseTree α)) => T' :: x) (insertionForest F p.2)

In a forest host, the first tree takes a sublist of the guests and the other trees take the complement.

theorem RoseTree.insertionForest_append {α : Type u_1} (xs ys gs : List (RoseTree α)) : insertionForest (xs ++ ys) gs = (↑gs.sublists'.revzip).bind fun (p : List (RoseTree α) × List (RoseTree α)) => (insertionForest xs p.1).bind fun (A : List (RoseTree α)) => Multiset.map (fun (x : List (RoseTree α)) => A ++ x) (insertionForest ys p.2)

In a concatenated host, the guests split into a sublist for the left forest and its complement for the right one.

theorem RoseTree.insertionForest_bind_revzip_sublists' {α : Type u_1} {δ : Type u_2} (hs gs : List (RoseTree α)) (K : List (RoseTree α) → List (RoseTree α) → Multiset δ) : ((insertionForest hs gs).bind fun (L : List (RoseTree α)) => (↑L.sublists'.revzip).bind fun (x : List (RoseTree α) × List (RoseTree α)) => K x.1 x.2) = (↑hs.sublists'.revzip).bind fun (h : List (RoseTree α) × List (RoseTree α)) => (↑gs.sublists'.revzip).bind fun (q : List (RoseTree α) × List (RoseTree α)) => (insertionForest h.2 q.2).bind fun (L₂ : List (RoseTree α)) => (insertionForest h.1 q.1).bind fun (L₁ : List (RoseTree α)) => K L₁ L₂

Splits of an output list are splits of the hosts and of the guests, each guest following its host. Stated in continuation form over a function K of the two parts.

theorem RoseTree.insertion_node {α : Type u_1} (a : α) (cs gs : List (RoseTree α)) : (node a cs).insertion gs = (↑gs.sublists'.revzip).bind fun (p : List (RoseTree α) × List (RoseTree α)) => Multiset.map (fun (cs' : List (RoseTree α)) => node a (p.1 ++ cs')) (insertionForest cs p.2)

In a node host, the guests split into a sublist prepended at the root, in guest order, and its complement grafted into the child forest.

Reading the recursion through UnorderedTree.mk

insertion_node and insertionForest_cons with every output read through UnorderedTree.mk, the form in which UnorderedTree.insertion_mk matches them against the nonplanar recursion.

theorem RoseTree.insertionForest_cons_msform {α : Type u_1} (T : RoseTree α) (F gs : List (RoseTree α)) : Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map UnorderedTree.mk L)) (insertionForest (T :: F) gs) = (↑gs.sublists'.revzip).bind fun (p : List (RoseTree α) × List (RoseTree α)) => (Multiset.map UnorderedTree.mk (T.insertion p.1)).bind fun (X : UnorderedTree α) => Multiset.map (fun (x : Multiset (UnorderedTree α)) => X ::ₘ x) (Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map UnorderedTree.mk L)) (insertionForest F p.2))

The host-forest recursion under mk.

theorem RoseTree.insertion_node_msform {α : Type u_1} (a : α) (cs gs : List (RoseTree α)) : Multiset.map UnorderedTree.mk ((node a cs).insertion gs) = (↑gs.sublists'.revzip).bind fun (p : List (RoseTree α) × List (RoseTree α)) => Multiset.map (fun (X : Multiset (UnorderedTree α)) => UnorderedTree.node a (↑(List.map UnorderedTree.mk p.1) + X)) (Multiset.map (fun (L : List (RoseTree α)) => ↑(List.map UnorderedTree.mk L)) (insertionForest cs p.2))

The node-host decomposition under mk.

Singleton hosts and empty guest lists

theorem RoseTree.insertion_nil_guests {α : Type u_1} (T : RoseTree α) : T.insertion [] = {T}

Inserting no guests leaves the host unchanged.

theorem RoseTree.insertionForest_singleton {α : Type u_1} (T : RoseTree α) (gs : List (RoseTree α)) : insertionForest [T] gs = Multiset.map (fun (T' : RoseTree α) => [T']) (T.insertion gs)

Inserting into a one-tree forest is inserting into that tree.