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 UnorderedTree 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.
• UnorderedTree.IsFullBinary.numUnary_eq_zero: a full binary tree has no unary vertices.

[UPSTREAM] candidate alongside the RoseTree carrier.

The contraction

def RoseTree.contractCombine {α : Type u_1} (a : α) : List (RoseTree α) → RoseTree α

Rebuild a node from already-contracted children: a lone child replaces the node, otherwise the node is kept.

Equations

• RoseTree.contractCombine a [c] = c
• RoseTree.contractCombine a x✝ = RoseTree.node a x✝

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

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

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

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 UnorderedTree

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

The number of unary vertices of a nonplanar tree.

Equations

• UnorderedTree.numUnary = Quotient.lift RoseTree.numUnary ⋯

@[simp]

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

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

Contract every unary vertex into its child.

Equations

• UnorderedTree.contractUnary = Quotient.map RoseTree.contractUnary ⋯

@[simp]

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

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

Each contracted unary vertex removes exactly one vertex.

@[simp]

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

After contraction no unary vertices remain.

@[simp]

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

contractUnary is idempotent.

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

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

theorem UnorderedTree.contractUnary_node_pair {α : Type u_1} (a : α) (s t : UnorderedTree α) : (node a {s, t}).contractUnary = node a {s.contractUnary, t.contractUnary}

A binary node contracts to the node of its contracted children.

theorem UnorderedTree.IsFullBinary.numUnary_eq_zero {α : Type u_1} {u : UnorderedTree α} (hu : u.IsFullBinary) : u.numUnary = 0

A full binary tree has no unary vertices.