Traversable rose tree

Traversable and LawfulTraversable instances for the n-ary RoseTree, mirroring Mathlib.Data.Tree.Traversable for BinaryTree. The lawfulness lemmas recurse through the child list via traverseList, so each is proved with a small list-level helper fed the per-child induction hypothesis from RoseTree.rec'.

@[implicit_reducible]

instance RoseTree.instTraversable : Traversable RoseTree

Equations

• RoseTree.instTraversable = { map := fun {α β : Type ?u.1} => RoseTree.map, traverse := fun {m : Type ?u.1 → Type ?u.1} [Applicative m] {α β : Type ?u.1} => RoseTree.traverse }

traverse_eq_map_id

theorem RoseTree.traverse_eq_map_id {α β : Type u} (f : α → β) (t : RoseTree α) : traverse (pure ∘ f) t = pure (map f t)

comp_traverse

theorem RoseTree.comp_traverse {α : Type u} {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {β γ : Type u} (f : β → F γ) (g : α → G β) (t : RoseTree α) : traverse (Functor.Comp.mk ∘ (fun (x : G β) => f <$> x) ∘ g) t = Functor.Comp.mk ((fun (x : RoseTree β) => traverse f x) <$> traverse g t)

naturality

theorem RoseTree.naturality {α : Type u} {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {β : Type u} (f : α → F β) (t : RoseTree α) : (fun {α : Type u} => η.app α) (traverse f t) = traverse (η.app β ∘ f) t

instance RoseTree.instLawfulTraversable : LawfulTraversable RoseTree