Contracting unary vertices of a rose tree

contractUnary collapses every unary vertex (one with exactly one child) into that child — the series reduction normalizing a rooted tree to one with no unary vertices. Each contracted vertex disappears whole, so the vertex count drops by exactly the number of unary vertices.

Main definitions

• RoseTree.contractUnary, RoseTree.numUnary: the contraction and the unary-vertex count, with descents to the Nonplanar quotient.

Main results

• RoseTree.numUnary_contractUnary: the result has no unary vertices.
• RoseTree.contractUnary_eq_self_iff: the fixed points are exactly the unary-free trees; hence contractUnary_idem.
• RoseTree.numNodes_contractUnary_add_numUnary: each contraction removes one vertex.

[UPSTREAM] candidate alongside the RoseTree carrier.

The contraction

def RoseTree.contractUnary {α : Type u_1} : RoseTree α → RoseTree α

Contract every unary (single-child) vertex into its child.

Equations

• RoseTree.contractUnary = RoseTree.fold RoseTree.contractCombine✝

@[simp]

theorem RoseTree.contractUnary_leaf {α : Type u_1} (a : α) : (node a []).contractUnary = node a []

@[simp]

theorem RoseTree.contractUnary_node_singleton {α : Type u_1} (a : α) (c : RoseTree α) : (node a [c]).contractUnary = c.contractUnary

@[simp]

theorem RoseTree.contractUnary_node_cons₂ {α : Type u_1} (a : α) (c d : RoseTree α) (cs : List (RoseTree α)) : (node a (c :: d :: cs)).contractUnary = node a (List.map contractUnary (c :: d :: cs))

def RoseTree.numUnary {α : Type u_1} : RoseTree α → ℕ

The number of unary (single-child) vertices.

Equations

• RoseTree.numUnary = RoseTree.fold fun (x : α) (ns : List ℕ) => (if ns.length = 1 then 1 else 0) + ns.sum

@[simp]

theorem RoseTree.numUnary_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).numUnary = (if cs.length = 1 then 1 else 0) + (List.map numUnary cs).sum

Vertex-count conservation

theorem RoseTree.numNodes_contractUnary_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : ((node a cs).contractUnary.numNodes + if cs.length = 1 then 1 else 0) = 1 + (List.map (fun (c : RoseTree α) => c.contractUnary.numNodes) cs).sum

The unary tick exactly compensates the root count: at a unary node the root is contracted away and the tick is 1; otherwise the root survives and the tick is 0.

theorem RoseTree.numNodes_contractUnary_add_numUnary {α : Type u_1} (t : RoseTree α) : t.contractUnary.numNodes + t.numUnary = t.numNodes

Each contracted unary vertex removes exactly one vertex.

contractUnary normalizes: no unary vertices remain

theorem RoseTree.numUnary_contractUnary_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).contractUnary.numUnary = (List.map (fun (c : RoseTree α) => c.contractUnary.numUnary) cs).sum

Contraction never creates a unary root: a unary root collapses away, and any other root keeps its arity, so the unary count at a node is the children's total.

@[simp]

theorem RoseTree.numUnary_contractUnary {α : Type u_1} (t : RoseTree α) : t.contractUnary.numUnary = 0

After contraction no unary vertices remain.

theorem RoseTree.contractUnary_eq_self_iff {α : Type u_1} {t : RoseTree α} : t.contractUnary = t ↔ t.numUnary = 0

The fixed points of contractUnary are exactly the unary-free trees.

@[simp]

theorem RoseTree.contractUnary_idem {α : Type u_1} (t : RoseTree α) : t.contractUnary.contractUnary = t.contractUnary

contractUnary is idempotent.

Perm invariance

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

numUnary is a Perm-invariant.

theorem RoseTree.Perm.contractUnary {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.contractUnary.Perm s.contractUnary

contractUnary respects Perm: contraction descends to the nonplanar quotient (fold_rel at S := Perm; the algebra congruence is the inline match).

Descent to Nonplanar

def RootedTree.Nonplanar.numUnary {α : Type u_1} : Nonplanar α → ℕ

The number of unary vertices of a nonplanar tree.

Equations

• RootedTree.Nonplanar.numUnary = RootedTree.Nonplanar.lift RoseTree.numUnary ⋯

@[simp]

theorem RootedTree.Nonplanar.numUnary_mk {α : Type u_1} (t : RoseTree α) : (mk t).numUnary = t.numUnary

def RootedTree.Nonplanar.contractUnary {α : Type u_1} : Nonplanar α → Nonplanar α

Contract every unary vertex into its child.

Equations

• RootedTree.Nonplanar.contractUnary = Quotient.map RoseTree.contractUnary ⋯

@[simp]

theorem RootedTree.Nonplanar.contractUnary_mk {α : Type u_1} (t : RoseTree α) : (mk t).contractUnary = mk t.contractUnary

theorem RootedTree.Nonplanar.numNodes_contractUnary_add_numUnary {α : Type u_1} (t : Nonplanar α) : t.contractUnary.numNodes + t.numUnary = t.numNodes

Each contracted unary vertex removes exactly one vertex.

@[simp]

theorem RootedTree.Nonplanar.numUnary_contractUnary {α : Type u_1} (t : Nonplanar α) : t.contractUnary.numUnary = 0

After contraction no unary vertices remain.

@[simp]

theorem RootedTree.Nonplanar.contractUnary_idem {α : Type u_1} (t : Nonplanar α) : t.contractUnary.contractUnary = t.contractUnary

contractUnary is idempotent.