Permutation of rose trees

RoseTree.Perm t s says the trees agree up to reordering the children of every vertex — the n-ary tree analogue of List.Perm, and the identity criterion of the unordered quotient (Nonplanar, built downstream). Mirroring List.Perm, transitivity is a constructor while reflexivity and symmetry are theorems, and the list-level companion PermList (List.Perm with elements compared by Perm instead of Eq) is mutually inductive with it, in the fold/foldList pattern.

Main declarations

• RoseTree.Perm, RoseTree.PermList: the mutual permutation relations.
• RoseTree.isSetoid: the setoid the nonplanar quotient is taken over.

Main results

• RoseTree.permList_iff_rel: PermList cs ds ↔ Multiset.Rel Perm (↑cs : Multiset (RoseTree α)) ↑ds — the list companion is Multiset.Rel in list clothing, so its theory is inherited.
• RoseTree.perm_node_iff: node inversion, Perm (node a cs) (node b ds) ↔ a = b ∧ Multiset.Rel Perm (↑cs : Multiset (RoseTree α)) ↑ds.

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

@[implicit_reducible]

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

Equations

• RoseTree.instTransPerm = { trans := ⋯ }

@[implicit_reducible]

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

Equations

• RoseTree.instTransListPermList = { trans := ⋯ }

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

@[implicit_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

Componentwise-related children give related nodes.

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

A plain List.Perm of children gives related nodes.

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

Multiset.Rel Perm between coerced children lists gives PermList: the bridge feeding fold_rel at S := Perm.

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)

A plain List.Perm of the children relates the nodes.

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)

Componentwise-related children relate the nodes.

theorem RoseTree.Perm.congr_child {α : Type u_1} {a : α} (pre post : List (RoseTree α)) {old new : RoseTree α} (h : old.Perm new) : (RoseTree.node a (pre ++ old :: post)).Perm (RoseTree.node a (pre ++ new :: post))

Rewriting a single child by a Perm-related tree relates the nodes.

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 in list clothing: its theory is inherited from the Multiset.Rel API.

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

Node inversion: related trees have equal labels and Multiset.Rel-related children.

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

The label is a Perm-invariant.

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

The children, up to Multiset.Rel Perm, are a Perm-invariant.

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

Prepending a shared child preserves relatedness of nodes.

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

PermList-related lists have equal length.

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

Inversion at singletons: PermList [c] [d] is just Perm c 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_3} {S : β → β → Prop} {g : α → List β → β} (hrefl : ∀ (b : β), S b b) (htrans : ∀ {b₁ b₂ b₃ : β}, S b₁ b₂ → S b₂ b₃ → S b₁ b₃) (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)

A fold whose algebra is congruent along Multiset.Rel S carries Perm to any reflexive transitive S.

theorem RoseTree.foldList_rel {α : Type u_1} {β : Type u_3} {S : β → β → Prop} {g : α → List β → β} (hrefl : ∀ (b : β), S b b) (htrans : ∀ {b₁ b₂ b₃ : β}, S b₁ b₂ → S b₂ b₃ → S b₁ b₃) (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)

Folded children of PermList-related lists are Multiset.Rel S-related.

theorem RoseTree.fold_perm {α : Type u_1} {β : Type u_3} {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

A fold with a permutation-invariant algebra is Perm-invariant.

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

numNodes is a Perm-invariant (List.Perm.sum_eq).

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

numLeaves is a Perm-invariant.

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

depth is a Perm-invariant (List.Perm.foldr_eq, max being commutative).

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

Arity (root child count) is a Perm-invariant.

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

Leaf-ness is a Perm-invariant.