Permutation of rose trees

RoseTree.Perm t s says that t and s agree up to reordering the children of every node. It is the counterpart for rose trees of List.Perm, and UnorderedTree is the quotient by it. As for List.Perm, transitivity is a constructor and reflexivity and symmetry are theorems. The relation is mutually inductive with PermList, which is List.Perm with elements compared by Perm in place of equality.

Main declarations

• RoseTree.Perm, RoseTree.PermList: the mutual permutation relations.
• RoseTree.isSetoid: the setoid of which UnorderedTree is the quotient.

Main results

• RoseTree.permList_iff_rel: PermList is Multiset.Rel Perm on the coerced lists, so its theory is that of Multiset.Rel.
• RoseTree.perm_node_iff: two nodes are related exactly when their labels are equal and their children are related by Multiset.Rel Perm.

inductive RoseTree.Perm {α : Type u_1} : RoseTree α → RoseTree α → Prop

Two rose trees are equal up to reordering the children of every vertex. Transitivity is a constructor (as in List.Perm); reflexivity and symmetry are theorems.

• node {α : Type u_1} {a : α} {cs ds : List (RoseTree α)} : PermList cs ds → (RoseTree.node a cs).Perm (RoseTree.node a ds)

  Equal labels over permuted, componentwise-related children.

• trans {α : Type u_1} {t s u : RoseTree α} : t.Perm s → s.Perm u → t.Perm u

  Composition of permutations.

inductive RoseTree.PermList {α : Type u_1} : List (RoseTree α) → List (RoseTree α) → Prop

List.Perm with corresponding elements related by Perm instead of Eq.

• nil {α : Type u_1} : PermList [] []

  Empty lists are related.

• cons {α : Type u_1} {c d : RoseTree α} {cs ds : List (RoseTree α)} : c.Perm d → PermList cs ds → PermList (c :: cs) (d :: ds)

  Related heads over related tails.

• swap {α : Type u_1} (c d : RoseTree α) (cs : List (RoseTree α)) : PermList (d :: c :: cs) (c :: d :: cs)

  Swap the first two elements.

• trans {α : Type u_1} {cs ds es : List (RoseTree α)} : PermList cs ds → PermList ds es → PermList cs es

  Composition of permutations.

def RoseTree.«term_~_» : Lean.TrailingParserDescr

Two rose trees are equal up to reordering the children of every vertex. Transitivity is a constructor (as in List.Perm); reflexivity and symmetry are theorems.

Equations

• RoseTree.«term_~_» = Lean.ParserDescr.trailingNode `RoseTree.«term_~_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

Equivalence

theorem RoseTree.Perm.refl {α : Type u_1} (t : RoseTree α) : t.Perm t

theorem RoseTree.PermList.refl {α : Type u_1} (cs : List (RoseTree α)) : PermList cs cs

theorem RoseTree.Perm.symm {α : Type u_1} {t s : RoseTree α} : t.Perm s → s.Perm t

theorem RoseTree.PermList.symm {α : Type u_1} {cs ds : List (RoseTree α)} : PermList cs ds → PermList ds cs

@[instance_reducible]

instance RoseTree.instTransPerm {α : Type u_1} : Trans Perm Perm Perm

Equations

• RoseTree.instTransPerm = { trans := ⋯ }

@[instance_reducible]

instance RoseTree.instTransListPermList {α : Type u_1} : Trans PermList PermList PermList

Equations

• RoseTree.instTransListPermList = { trans := ⋯ }

instance RoseTree.instIsEquivPerm {α : Type u_1} : IsEquiv (RoseTree α) Perm

theorem RoseTree.Perm.eqv {α : Type u_1} : Equivalence Perm

@[instance_reducible]

instance RoseTree.isSetoid {α : Type u_1} : Setoid (RoseTree α)

The setoid of rose trees up to child reordering; the nonplanar quotient is taken over it.

Equations

• RoseTree.isSetoid = { r := RoseTree.Perm, iseqv := ⋯ }

Constructors from list-level data

theorem RoseTree.PermList.of_forall₂ {α : Type u_1} {cs ds : List (RoseTree α)} (h : List.Forall₂ Perm cs ds) : PermList cs ds

theorem RoseTree.PermList.of_perm {α : Type u_1} {cs ds : List (RoseTree α)} (h : cs.Perm ds) : PermList cs ds

theorem RoseTree.PermList.of_rel {α : Type u_1} {cs ds : List (RoseTree α)} (h : Multiset.Rel Perm ↑cs ↑ds) : PermList cs ds

theorem RoseTree.Perm.node_of_perm {α : Type u_1} {a : α} {cs ds : List (RoseTree α)} (h : cs.Perm ds) : (RoseTree.node a cs).Perm (RoseTree.node a ds)

theorem RoseTree.Perm.node_of_forall₂ {α : Type u_1} {a : α} {cs ds : List (RoseTree α)} (h : List.Forall₂ Perm cs ds) : (RoseTree.node a cs).Perm (RoseTree.node a ds)

The Multiset.Rel characterization

theorem RoseTree.permList_iff_rel {α : Type u_1} {cs ds : List (RoseTree α)} : PermList cs ds ↔ Multiset.Rel Perm ↑cs ↑ds

PermList is Multiset.Rel Perm on the coerced lists.

theorem RoseTree.perm_node_iff {α : Type u_1} {a b : α} {cs ds : List (RoseTree α)} : (node a cs).Perm (node b ds) ↔ a = b ∧ Multiset.Rel Perm ↑cs ↑ds

Two nodes are related exactly when their labels are equal and their children are related by Multiset.Rel Perm.

theorem RoseTree.Perm.value_eq {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.value = s.value

theorem RoseTree.Perm.children_rel {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : Multiset.Rel Perm ↑t.children ↑s.children

theorem RoseTree.PermList.length_eq {α : Type u_1} {cs ds : List (RoseTree α)} (h : PermList cs ds) : cs.length = ds.length

theorem RoseTree.PermList.singleton_inv {α : Type u_1} {c d : RoseTree α} (h : PermList [c] [d]) : c.Perm d

Functoriality

theorem RoseTree.Perm.map {α : Type u_1} {β : Type u_2} (f : α → β) {t s : RoseTree α} : t.Perm s → (RoseTree.map f t).Perm (RoseTree.map f s)

RoseTree.map preserves Perm (cf. List.Perm.map).

theorem RoseTree.PermList.map {α : Type u_1} {β : Type u_2} (f : α → β) {cs ds : List (RoseTree α)} : PermList cs ds → PermList (List.map (RoseTree.map f) cs) (List.map (RoseTree.map f) ds)

List.map ∘ RoseTree.map preserves PermList.

Fold invariance

A fold whose algebra is congruent along Multiset.Rel S of the folded children carries Perm to S (fold_rel): the generic dissolver of per-function invariance inductions, relational so that tree-valued folds descend too. fold_perm is the S := Eq case; the counts below are such folds.

theorem RoseTree.fold_rel {α : Type u_1} {β : Type u_2} {S : β → β → Prop} [IsPreorder β S] {g : α → List β → β} (hg : ∀ (a : α) {l₁ l₂ : List β}, Multiset.Rel S ↑l₁ ↑l₂ → S (g a l₁) (g a l₂)) {t s : RoseTree α} : t.Perm s → S (fold g t) (fold g s)

theorem RoseTree.foldList_rel {α : Type u_1} {β : Type u_2} {S : β → β → Prop} [IsPreorder β S] {g : α → List β → β} (hg : ∀ (a : α) {l₁ l₂ : List β}, Multiset.Rel S ↑l₁ ↑l₂ → S (g a l₁) (g a l₂)) {cs ds : List (RoseTree α)} : PermList cs ds → Multiset.Rel S ↑(List.map (fold g) cs) ↑(List.map (fold g) ds)

theorem RoseTree.fold_perm {α : Type u_1} {β : Type u_2} {g : α → List β → β} (hg : ∀ (a : α) (l₁ l₂ : List β), l₁.Perm l₂ → g a l₁ = g a l₂) {t s : RoseTree α} : t.Perm s → fold g t = fold g s

theorem RoseTree.numNodes_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.numNodes = s.numNodes

theorem RoseTree.numLeaves_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.numLeaves = s.numLeaves

theorem RoseTree.height_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.height = s.height

theorem RoseTree.arity_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.arity = s.arity