Partial label maps on rose trees

RoseTree.filterMap (f : α → Option β) relabels a rose tree along f, recursively dropping every subtree whose root label maps to none; the result is none iff the root itself is dropped. The rose-tree analogue of List.filterMap, with UnorderedTree.filterMap its descent through the Perm quotient.

Main definitions

• RoseTree.filterMap, RoseTree.filterMapList — the mutual tree / children-list partial maps.
• UnorderedTree.filterMap — the descent through the Perm quotient.

Main results

• RoseTree.filterMap_map — filterMap f (map g t) = filterMap (f ∘ g) t.
• RoseTree.filterMap_some — a total map drops nothing: filterMap (fun a => some (g a)) t = some (map g t).

def RoseTree.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) : RoseTree α → Option (RoseTree β)

Partially relabel a rose tree: subtrees whose root label maps to none are dropped, recursively; none iff the root itself is dropped.

Equations

• RoseTree.filterMap f (RoseTree.node a cs) = Option.map (fun (b : β) => RoseTree.node b (RoseTree.filterMapList f cs)) (f a)

def RoseTree.filterMapList {α : Type u_1} {β : Type u_2} (f : α → Option β) : List (RoseTree α) → List (RoseTree β)

Children-list companion of RoseTree.filterMap: partial map over a list of trees, dropping the none results.

Equations

• RoseTree.filterMapList f [] = []
• RoseTree.filterMapList f (c :: cs) = match RoseTree.filterMap f c with | none => RoseTree.filterMapList f cs | some t => t :: RoseTree.filterMapList f cs

@[simp]

theorem RoseTree.filterMap_node {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : α) (cs : List (RoseTree α)) : filterMap f (node a cs) = Option.map (fun (b : β) => node b (filterMapList f cs)) (f a)

@[simp]

theorem RoseTree.filterMapList_nil {α : Type u_1} {β : Type u_2} (f : α → Option β) : filterMapList f [] = []

theorem RoseTree.filterMapList_singleton {α : Type u_1} {β : Type u_2} (f : α → Option β) (t : RoseTree α) : filterMapList f [t] = (filterMap f t).toList

filterMapList on a singleton: the head's partial map as a list.

theorem RoseTree.filterMapList_eq_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (cs : List (RoseTree α)) : filterMapList f cs = List.filterMap (filterMap f) cs

RoseTree.filterMapList agrees with List.filterMap of the per-tree partial map.

theorem RoseTree.filterMapList_append {α : Type u_1} {β : Type u_2} (f : α → Option β) (l₁ l₂ : List (RoseTree α)) : filterMapList f (l₁ ++ l₂) = filterMapList f l₁ ++ filterMapList f l₂

RoseTree.filterMapList distributes over list concatenation.

Composition with total maps

theorem RoseTree.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → Option γ) (g : α → β) (t : RoseTree α) : filterMap f (map g t) = filterMap (f ∘ g) t

Partial-after-total composition: filterMap f after map g is filterMap (f ∘ g).

theorem RoseTree.filterMapList_mapList {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → Option γ) (g : α → β) (cs : List (RoseTree α)) : filterMapList f (List.map (map g) cs) = filterMapList (f ∘ g) cs

Children-list companion of RoseTree.filterMap_map.

theorem RoseTree.filterMap_some {α : Type u_1} {β : Type u_2} (g : α → β) (t : RoseTree α) : filterMap (fun (a : α) => some (g a)) t = some (map g t)

A total map drops nothing: filterMap (some ∘ g) is some ∘ map g.

theorem RoseTree.filterMapList_some {α : Type u_1} {β : Type u_2} (g : α → β) (cs : List (RoseTree α)) : filterMapList (fun (a : α) => some (g a)) cs = List.map (map g) cs

Children-list companion of RoseTree.filterMap_some.

Descent to UnorderedTree

RoseTree.filterMap f ∘ UnorderedTree.mk is well-defined modulo Perm: Perm permutes children, filterMapList commutes with permutations up to List.Perm, and child-list order collapses at the UnorderedTree.mk level.

def UnorderedTree.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) : UnorderedTree α → Option (UnorderedTree β)

Partially relabel a UnorderedTree tree, dropping subtrees whose root label maps to none.

Equations

• UnorderedTree.filterMap f = Quotient.lift (filterMapQuotient✝ f) ⋯

@[simp]

theorem UnorderedTree.filterMap_mk {α : Type u_1} {β : Type u_2} (f : α → Option β) (t : RoseTree α) : filterMap f (mk t) = Option.map mk (RoseTree.filterMap f t)

The Sum.getLeft? roundtrip

@[simp]

theorem RoseTree.filterMap_getLeft?_map_inl {α : Type u_1} {β : Type u_2} (t : RoseTree α) : filterMap Sum.getLeft? (map Sum.inl t) = some t

Left injection followed by Sum.getLeft?-filtering is the identity.

@[simp]

theorem UnorderedTree.filterMap_getLeft?_map_inl {α : Type u_1} {β : Type u_2} (T : UnorderedTree α) : filterMap Sum.getLeft? (map Sum.inl T) = some T

UnorderedTree version of RoseTree.filterMap_getLeft?_map_inl.