Foissy 2021 Theorem 5.1 multi-tree insertion (path-based)

[foissy-typed-decorated-rooted-trees-2018] [foissy-introduction-hopf-algebras-trees]

The Foissy 2021 Theorem 5.1 multi-tree multi-vertex insertion operator. Defined as a sum over functions Ts → V(T) of multiGraft, taken as a Multiset to make the sum-over-choices commutative.

Sibling to Graft.lean (path-based multi-graft primitive). Lives under namespace RoseTree.Pathed.

File scope

• §1: listChoices — choice-list enumeration (representation-independent).
• §2: insertion — Foissy 2021 Theorem 5.1, single-tree host.
• §3: insertionForest — forest host + identity/nil lemmas.
• §4: Pair-list Perm-invariance for multiGraft.
• §5: Guest-list invariance for insertion (insertion_permEquiv_guests).
• §5.5: Validity discharge for listChoices-derived pair lists.
• §6: Host invariance via the swapPathAt path-relabel bijection.
• §7: Forest invariance (insertionForest_permEquiv_host, insertionForest_perm_guests).
• §8: Singleton-host insertion.

Status

[UPSTREAM] candidate. Sorry-free.

§1: listChoices enumeration

def RoseTree.Pathed.listChoices {β : Type u_2} : List β → ℕ → List (List β)

All length-n lists with entries from xs (with repetition). The "n-fold list power" used in Foissy 2021 Theorem 5.1's vertex-choice sum. Representation-independent (no Vertex dependence): copied from the legacy Insertion.lean.

Equations

• RoseTree.Pathed.listChoices x✝ 0 = [[]]
• RoseTree.Pathed.listChoices x✝ n.succ = List.flatMap (fun (v : β) => List.map (fun (x : List β) => v :: x) (RoseTree.Pathed.listChoices x✝ n)) x✝

@[simp]

theorem RoseTree.Pathed.listChoices_zero {β : Type u_2} (xs : List β) : listChoices xs 0 = [[]]

@[simp]

theorem RoseTree.Pathed.listChoices_succ {β : Type u_2} (xs : List β) (n : ℕ) : listChoices xs (n + 1) = List.flatMap (fun (v : β) => List.map (fun (x : List β) => v :: x) (listChoices xs n)) xs

§2: insertion — Foissy 2021 Theorem 5.1

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

Foissy 2021 Theorem 5.1 multi-graft on a single-tree host. Sum over (v₁, …, vₙ) ∈ V(T)ⁿ of multiGraft T [(v₁, T₁), …, (vₙ, Tₙ)].

Equations

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

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

§3: insertionForest — forest host

@[irreducible]

def RoseTree.Pathed.insertionForest {α : Type u_1} : List (RoseTree α) → List (RoseTree α) → Multiset (List (RoseTree α))

Multi-graft into a host forest. Disjoint pattern cases for clean auto-generated equation lemmas.

Equations

• One or more equations did not get rendered due to their size.
• RoseTree.Pathed.insertionForest [] [] = {[]}
• RoseTree.Pathed.insertionForest [] (head :: tail) = 0
• RoseTree.Pathed.insertionForest (T :: F) [] = {T :: F}

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem RoseTree.Pathed.insertionForest_cons_cons {α : Type u_1} (T : RoseTree α) (F : List (RoseTree α)) (T_g : RoseTree α) (Ts : List (RoseTree α)) : insertionForest (T :: F) (T_g :: Ts) = (↑(listChoices [true, false] (T_g :: Ts).length)).bind fun (assignment : List Bool) => (insertion T (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then some p.1 else none) ((T_g :: Ts).zip assignment))).bind fun (T' : RoseTree α) => Multiset.map (fun (F' : List (RoseTree α)) => T' :: F') (insertionForest F (List.filterMap (fun (p : RoseTree α × Bool) => if p.2 = true then none else some p.1) ((T_g :: Ts).zip assignment)))

§4: Pair-list Perm invariance for multiGraft

multiGraft T pairs is PermEquiv-invariant under permutation of the pair list: grafts at distinct paths commute, and grafts at the same path are root-list permutations (lift via permEquiv_root_perm).

Path-based reformulation of the legacy multiGraft_perm_pair / multiGraftList_perm_pair.

Forall₂-version of multiGraft_perm_pair

For insertion_permEquiv_guests we need: when Ts ~ᶠ Ts' (Forall₂ PermEquiv) and we zip with the same choice, the resulting pair lists satisfy a Forall₂ relation (same fst, PermEquiv snd). Then this lifts to multiGraft T pairs ~ multiGraft T pairs' (PermEquiv).

Path-based version of the legacy multiGraft_permEquiv_pair_Forall₂.

§5: Guest-list invariance for insertion

pairSum t pre Ts aggregates mk (multiGraft t (pre ++ c.zip Ts)) over all choices c ∈ listChoices (vertices t) |Ts|. The clean recursive equation pairSum t pre (x :: rest) = bind v over vertices of pairSum t (pre ++ [(v, x)]) rest lets us prove Ts-perm invariance by Perm induction.

Path-based reformulation of the legacy pairSum / insertion_perm_guests machinery. The pair type changes from Vertex t × RoseTree α to Path × RoseTree α.

theorem RoseTree.Pathed.insertion_permEquiv_guests {α : Type u_1} (t : RoseTree α) {Ts Ts' : List (RoseTree α)} (h : List.Forall₂ PermEquiv Ts Ts') : Multiset.map RootedTree.Nonplanar.mk (insertion t Ts) = Multiset.map RootedTree.Nonplanar.mk (insertion t Ts')

Guest-list Forall₂ PermEquiv lifts to insertion mk-equality.

§5.5: Validity discharge for listChoices-derived pair lists

Every element of a listChoices-enumerated choice is a member of the alphabet (mem_of_mem_listChoices), so a pair list of the canonical shape choice.zip Ts automatically satisfies the validity hypothesis that graft operations require (forall_zip_isValidPath_of_listChoices). These utilities are consumed by InsertionNodeDecomp and InsertionCompose.

theorem RoseTree.Pathed.mem_of_mem_listChoices {β : Type u_2} (xs : List β) (n : ℕ) (choice : List β) (h_choice : choice ∈ listChoices xs n) (v : β) (h_v : v ∈ choice) : v ∈ xs

Every element of a choice ∈ listChoices xs n is a member of xs. Lifts membership-in-an-enumerated-choice to membership-in-the-alphabet.

theorem RoseTree.Pathed.forall_zip_isValidPath_of_listChoices {α : Type u_1} (T : RoseTree α) (Ts : List (RoseTree α)) (choice : List Path) (h_choice : choice ∈ listChoices (vertices T) Ts.length) (pair : Path × RoseTree α) (h_pair : pair ∈ choice.zip Ts) : IsValidPath pair.1 T

Every path in a choice.zip Ts pair list is a valid path in T, when choice ∈ listChoices (vertices T) Ts.length. Discharges the validity hypothesis of the graft operations for listChoices-derived pair lists.

§6: Host invariance via path-swap bijection

insertion T Ts is mk-invariant under PermEquiv of the host: the original blocker for the path-based refactor.

Strategy:

1. swapPathAt n — swap the first index n ↔ n+1 in a path.
2. vertices_swap_perm — applying swapPathAt pre.length to vertices of node a (pre ++ l :: r :: post) is a List.Perm of vertices of node a (pre ++ r :: l :: post). Reduces to a List.Perm of two appendable middle blocks, via verticesAux_append + a List.perm_append_comm.
3. multiGraft_swap_permEquiv — the multiGraft results differ only by the swap of l/r in the root children list; lift via PermStep.swapAtRoot.
4. Combine via listChoices Perm-respect → insertion_swap_invariant.
5. Lift via PermStep (recurse case) and PermEquiv = EqvGen PermStep.

§6.2 substrate: pair-relabel + permEquiv prefix-cons-lift

§6.3 substrate for insertion_permEquiv_host

The swapAtRoot case of insertion_permStep_host needs to lift a Perm of vertices into a Perm of choice lists (via listChoices), then combine with multiGraft_swap_permEquiv to get equal mk-mapped insertion outputs. Helpers below build this bridge.

theorem RoseTree.Pathed.listChoices_map {β : Type u_2} {γ : Type u_3} (f : β → γ) (xs : List β) (n : ℕ) : listChoices (List.map f xs) n = List.map (List.map f) (listChoices xs n)

listChoices is compatible with List.map: applying f element-wise to choices in xs.map f gives the same as mapping List.map f over listChoices xs n.

theorem RoseTree.Pathed.insertionForest_permEquiv_host {α : Type u_1} (Ts : List (RoseTree α)) {F F' : List (RoseTree α)} (h : List.Forall₂ PermEquiv F F') : Multiset.map (List.map RootedTree.Nonplanar.mk) (insertionForest F Ts) = Multiset.map (List.map RootedTree.Nonplanar.mk) (insertionForest F' Ts)

Forest host invariance: Forall₂ PermEquiv F F' lifts to mk-equality of insertionForest F Ts and insertionForest F' Ts.

§7.1 substrate for insertionForest_perm_guests

Forest-side analogue of pairSum: a Multiset aggregator that splits the guest list into a pre_T bucket (going to the head host T) and a pre_F bucket (going to the tail forest), then aggregates over all remaining assignments. Used to make Ts-Perm-invariance provable by induction on the Perm structure (the swap case becomes a clean Multiset.bind_bind after lifting to the mk-mapped level).

theorem RoseTree.Pathed.insertionForest_perm_guests {α : Type u_1} (F : List (RoseTree α)) {Ts Ts' : List (RoseTree α)} (h : Ts.Perm Ts') : Multiset.map (List.map RootedTree.Nonplanar.mk) (insertionForest F Ts) = Multiset.map (List.map RootedTree.Nonplanar.mk) (insertionForest F Ts')

Forest guest invariance: List.Perm of guests lifts to mk-equality of insertionForest.

§8: Singleton-host insertion = single-tree insertion lifted to singleton lists

insertionForest [T] gs = (insertion T gs).map (fun T' => [T']) — when the host has exactly one tree, the multi-graft is just the single-tree multi-graft with each output wrapped in a singleton list. Used downstream to handle hostTripleSum T [T'] F patterns at the singleton-F_A level.

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

insertion T [] is the singleton {T} — multi-graft of no guests is the identity.

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

Singleton-host insertion: when the host has exactly one tree, insertionForest reduces to single-tree insertion followed by singleton lift. This lets us match hostTripleSum T [T_other] F patterns by converting (insertionForest [T_other] pre).bind to (insertion T_other pre).bind (via Multiset.bind_map).