Substitution of subtrees of a rose tree

RoseTree.modifyIf p f applies f to every outermost subtree satisfying p, and RoseTree.replaceIf p r replaces each by r. The subtrees modified are RoseTree.outerMatches p, those satisfying p among the subtrees reached without passing through one (RoseTree.subtreesUntil p); the first match in preorder is among them, and replacing them trades their leaves for copies of the replacement's.

Main definitions

• RoseTree.modifyIf, RoseTree.replaceIf, RoseTree.subtreesUntil, RoseTree.outerMatches

Main results

• RoseTree.mem_outerMatches_of_find?: the first match in preorder is an outermost one.
• RoseTree.leaves_replaceIf: substitution trades the leaves of the replaced subtrees for those of the replacement.
• RoseTree.filterMap_leaves_replaceIf_add: replacing the copies of a subtree whose leaves occur once trades the leaves of one copy.

def RoseTree.modifyIf {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (f : RoseTree α → RoseTree α) : RoseTree α → RoseTree α

Apply f to every outermost subtree satisfying p, testing each subtree before its children.

Equations

• RoseTree.modifyIf p f (RoseTree.node a cs) = if p (RoseTree.node a cs) then f (RoseTree.node a cs) else RoseTree.node a (RoseTree.modifyIfList p f cs)

def RoseTree.modifyIfList {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (f : RoseTree α → RoseTree α) : List (RoseTree α) → List (RoseTree α)

modifyIf in each tree of a list.

Equations

• RoseTree.modifyIfList p f [] = []
• RoseTree.modifyIfList p f (c :: cs) = RoseTree.modifyIf p f c :: RoseTree.modifyIfList p f cs

theorem RoseTree.modifyIfList_eq {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (f : RoseTree α → RoseTree α) (cs : List (RoseTree α)) : modifyIfList p f cs = List.map (modifyIf p f) cs

theorem RoseTree.modifyIf_node {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (f : RoseTree α → RoseTree α) (a : α) (cs : List (RoseTree α)) : modifyIf p f (node a cs) = if p (node a cs) then f (node a cs) else node a (List.map (modifyIf p f) cs)

def RoseTree.replaceIf {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (r : RoseTree α) : RoseTree α → RoseTree α

Replace every outermost subtree satisfying p by r.

Equations

• RoseTree.replaceIf p r = RoseTree.modifyIf p fun (x : RoseTree α) => r

theorem RoseTree.replaceIf_node {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (r : RoseTree α) (a : α) (cs : List (RoseTree α)) : replaceIf p r (node a cs) = if p (node a cs) then r else node a (List.map (replaceIf p r) cs)

theorem RoseTree.map_replaceIf {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (r : RoseTree α) {β : Type u_2} {g : α → β} {p' : RoseTree β → Prop} [DecidablePred p'] (hp : ∀ (s : RoseTree α), p' (map g s) ↔ p s) (t : RoseTree α) : map g (replaceIf p r t) = replaceIf p' (map g r) (map g t)

def RoseTree.subtreesUntil {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] : RoseTree α → List (RoseTree α)

The subtrees reached in preorder without passing through a subtree satisfying p, those satisfying it included.

Equations

• RoseTree.subtreesUntil p (RoseTree.node a cs) = RoseTree.node a cs :: if p (RoseTree.node a cs) then [] else RoseTree.subtreesUntilList p cs

def RoseTree.subtreesUntilList {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] : List (RoseTree α) → List (RoseTree α)

subtreesUntil of the trees of a list.

Equations

• RoseTree.subtreesUntilList p [] = []
• RoseTree.subtreesUntilList p (c :: cs) = RoseTree.subtreesUntil p c ++ RoseTree.subtreesUntilList p cs

theorem RoseTree.subtreesUntilList_eq {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (cs : List (RoseTree α)) : subtreesUntilList p cs = List.flatMap (subtreesUntil p) cs

theorem RoseTree.subtreesUntil_node {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) : subtreesUntil p (node a cs) = node a cs :: if p (node a cs) then [] else List.flatMap (subtreesUntil p) cs

theorem RoseTree.isSubtree_of_mem_subtreesUntil {α : Type u_1} {p : RoseTree α → Prop} [DecidablePred p] {s t : RoseTree α} (h : s ∈ subtreesUntil p t) : s.IsSubtree t

def RoseTree.outerMatches {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (t : RoseTree α) : List (RoseTree α)

The outermost subtrees satisfying p, in preorder: those modifyIf p modifies.

Equations

• RoseTree.outerMatches p t = List.filter (fun (x : RoseTree α) => decide (p x)) (RoseTree.subtreesUntil p t)

theorem RoseTree.outerMatches_node {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) : outerMatches p (node a cs) = if p (node a cs) then [node a cs] else List.flatMap (outerMatches p) cs

theorem RoseTree.of_mem_outerMatches {α : Type u_1} {p : RoseTree α → Prop} [DecidablePred p] {s t : RoseTree α} (h : s ∈ outerMatches p t) : p s

theorem RoseTree.mem_outerMatches_of_find? {α : Type u_1} {p : RoseTree α → Prop} [DecidablePred p] {s t : RoseTree α} (h : List.find? (fun (u : RoseTree α) => decide (p u)) t.subtrees = some s) : s ∈ outerMatches p t

The first subtree in preorder satisfying p is an outermost one.

theorem RoseTree.leaves_replaceIf {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (r t : RoseTree α) : (replaceIf p r t).leaves + (List.map leaves (outerMatches p t)).sum = t.leaves + (outerMatches p t).length • r.leaves

Substitution trades the leaves of the replaced subtrees for copies of the replacement's.

theorem RoseTree.filterMap_leaves_replaceIf_add {α : Type u_1} (p : RoseTree α → Prop) [DecidablePred p] (r : RoseTree α) {β : Type u_2} [DecidableEq β] {g : α → Option β} {L : Multiset β} {s t : RoseTree α} (hL : ∀ (u : RoseTree α), p u → Multiset.filterMap g u.leaves = L) (hr : Multiset.filterMap g r.leaves = 0) (ht : (Multiset.filterMap g t.leaves).Nodup) (hs : s ∈ outerMatches p t) : Multiset.filterMap g (replaceIf p r t).leaves + Multiset.filterMap g s.leaves = Multiset.filterMap g t.leaves

When the outermost matches all have the same leaves under g, the replacement has none, and no g-value occurs twice among the leaves of t, replacing trades the leaves of one match.