Counting binary phylogenetic trees

InductivePlanar rooted binary tree with labeled leaves#✓fully proved

A planar rooted binary tree with leaves labeled by α: a leaf leaf a, or an internal vertex node l r with left subtree l and right subtree r (the children are ordered).

inductive PlaneTree (α : Type u) where
  /-- A leaf labeled `a`. -/
  | leaf : α → PlaneTree α
  /-- An internal vertex with left subtree `l` and right subtree `r`. -/
  | node : PlaneTree α → PlaneTree α → PlaneTree α
  deriving DecidableEq

Used by 8

Used byTopology of a species tree · Leaf labels of a planar binary tree · Every planar binary tree has a leaf · The number of binary hierarchies · Schröder's count of rooted binary phylogenetic trees · Planar drawings of rooted binary trees on a taxon set · Rooted binary phylogenetic tree · Swap of the children of an internal vertex

DefinitionLeaf labels of a planar binary tree#✓fully proved

The multiset of leaf labels.

def leaves : PlaneTree α → Multiset α
  | leaf a => {a}
  | node l r => leaves l + leaves r

Uses 1 · Used by 5

Statement usesPlanar rooted binary tree with labeled leaves

Used byEvery planar binary tree has a leaf · The number of binary hierarchies · Schröder's count of rooted binary phylogenetic trees · Planar drawings of rooted binary trees on a taxon set · Rooted binary phylogenetic tree

TheoremEvery planar binary tree has a leaf#✓fully proved

Every planar tree has at least one leaf.

theorem leaves_ne_zero : ∀ t : PlaneTree α, t.leaves ≠ 0

Uses 2 · Used by 1

Statement usesPlanar rooted binary tree with labeled leaves · Leaf labels of a planar binary tree

Used byThe number of binary hierarchies

InductiveSwap of the children of an internal vertex#✓fully proved

One swap: exchange the two children of one internal vertex (anywhere in the tree).

inductive Swap : PlaneTree α → PlaneTree α → Prop
  /-- Exchange the children of the root. -/
  | root (l r : PlaneTree α) : Swap (node l r) (node r l)
  /-- Swap inside the left subtree. -/
  | left {l l' : PlaneTree α} (r : PlaneTree α) : Swap l l' → Swap (node l r) (node l' r)
  /-- Swap inside the right subtree. -/
  | right (l : PlaneTree α) {r r' : PlaneTree α} : Swap r r' → Swap (node l r) (node l r')

Uses 1 · Used by 3

Statement usesPlanar rooted binary tree with labeled leaves

Used byThe number of binary hierarchies · Schröder's count of rooted binary phylogenetic trees · Rooted binary phylogenetic tree

DefinitionPlanar drawings of rooted binary trees on a taxon set#✓fully proved

The planar drawings of rooted binary trees on the taxa X: planar trees whose leaves are labeled by X, each taxon labeling exactly one leaf.

def On (X : Finset α) : Type u :=
  {t : PlaneTree α // t.leaves = X.val}

Uses 2 · Used by 3

Statement usesPlanar rooted binary tree with labeled leaves · Leaf labels of a planar binary tree

Used byThe number of binary hierarchies · Schröder's count of rooted binary phylogenetic trees · Rooted binary phylogenetic tree

DefinitionRooted binary phylogenetic tree#✓fully proved

The rooted binary phylogenetic trees on the taxa X: planar drawings with leaf set X modulo exchanging the two children of internal vertices, i.e. rooted binary trees with unordered children and leaves labeled bijectively by X, up to label-preserving isomorphism.

def RootedBinaryTree (X : Finset α) : Type u :=
  Quotient (PlaneTree.swapSetoid X)

Uses 4 · Used by 2

Statement usesPlanar rooted binary tree with labeled leaves · Planar drawings of rooted binary trees on a taxon set · Swap of the children of an internal vertex · Leaf labels of a planar binary tree

Used byThe number of binary hierarchies · Schröder's count of rooted binary phylogenetic trees

TheoremSchröder's count of rooted binary phylogenetic trees#✓fully proved

On n ≥ 1 labeled taxa there are (2 n - 3)‼ = 1 · 3 · 5 ⋯ (2 n - 3) rooted binary phylogenetic trees (1 tree for n = 1 and n = 2, 3 for n = 3, 15 for n = 4). For n = 1 the natural-number subtraction gives 2 - 3 = 0 and 0‼ = 1, the conventional value (-1)‼ = 1 of the formula; the empty set of taxa (excluded here) has no tree (isEmpty_rootedBinaryTree_empty).

theorem nat_card_rootedBinaryTree (X : Finset α) (hX : X.Nonempty) :
    Nat.card (RootedBinaryTree X) = (2 * X.card - 3)‼

Sources

• Semple & Steel (2003), Proposition 2.1.4.

Uses 5 · Used by 1

Statement usesRooted binary phylogenetic tree

Proof usesPlanar rooted binary tree with labeled leaves · Planar drawings of rooted binary trees on a taxon set · Swap of the children of an internal vertex · Leaf labels of a planar binary tree

Used byThe number of binary hierarchies

StructureUnrooted binary phylogenetic tree#✓fully proved

An unrooted binary phylogenetic tree on the taxa X: a finite tree G on a vertex type V whose degree-one vertices are labeled bijectively by X (label) and whose other vertices all have degree three.

MathlibExt.Biology.Phylogenetics.UnrootedTreeCount.UnrootedBinaryTree · 15 lines

structure UnrootedBinaryTree (X : Type) : Type 1 where
  /-- The vertex type. -/
  V : Type
  /-- The vertex type is finite. -/
  [fintype : Fintype V]
  /-- The tree. -/
  G : SimpleGraph V
  /-- Adjacency is decidable (so that degrees are defined). -/
  [decRel : DecidableRel G.Adj]
  /-- `G` is a tree. -/
  isTree : G.IsTree
  /-- The bijective labeling of the leaves by the taxa. -/
  label : X ≃ {v : V // G.degree v = 1}
  /-- Every vertex that is not a leaf has degree three. -/
  degree_eq_three : ∀ v, G.degree v ≠ 1 → G.degree v = 3

Used by 55

Used byCluster of a vertex seen from a leaf · Cluster set of a tree seen from a leaf · Isomorphic trees have the same clusters · Every binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy · Isomorphism of unrooted binary phylogenetic trees · Clusters determine an unrooted binary tree · The number of unrooted binary phylogenetic trees · Number of unrooted binary phylogenetic trees · Unrooted binary trees correspond to binary hierarchies · The Branch Length Score · Branch length score of the empty set is zero · Normalized branch length score · Normalized branch length score is at most one for nonnegative lengths · Normalized branch length score is nonnegative for nonnegative lengths · Branch length score is at most the tree length for nonnegative lengths · All species give the whole tree · Monotonicity · Branch length score is nonnegative for nonnegative edge lengths · A single species has BLS 0 · Subadditivity · Sum over darts is twice the sum over edges · The side of a pendant edge is the singleton of its leaf · Nonnegative edge lengths of a tree · Total branch length of a tree · Bootstrap support · Bootstrap support lies in the unit interval · Clusters seen from a leaf are edge sides · Edge splits of a tree are pairwise compatible · Splits computed from a leaf are pairwise compatible · The two sides of a tree edge are complementary · Tree displaying a quartet · Side of a tree edge containing a vertex · Edge splits of a tree · Perfect phylogeny and the four-gamete condition · The majority-rule consensus tree · Perfect phylogeny for a binary character matrix · An unrooted binary tree is determined by its quartets · Majority splits of a family of trees · Majority splits are compatible · Clusters seen from a leaf omit that leaf · Bootstrap support above one half means a majority split · Robinson–Foulds distance · Symmetry of the Robinson–Foulds distance · Isomorphism invariance of the Robinson–Foulds distance · Robinson–Foulds distance is independent of the base leaf · Robinson–Foulds distance vanishes exactly on isomorphic trees · Maximum of the Robinson–Foulds distance · Robinson–Foulds distance from a tree to itself is zero · Triangle inequality for the Robinson–Foulds distance · Split set of a tree computed from a leaf · Split set from any leaf equals the edge splits · The split set does not depend on the leaf used to compute it · Splits-equivalence theorem · Robinson–Foulds distance as half the split symmetric difference

DefinitionIsomorphism of unrooted binary phylogenetic trees#✓fully proved

Two unrooted binary phylogenetic trees are isomorphic when some graph isomorphism maps the leaf with each label to the leaf with the same label.

def UnrootedBinaryTree.Iso {X : Type} (T T' : UnrootedBinaryTree X) : Prop :=
  ∃ e : T.G ≃g T'.G, ∀ x, e (T.label x) = T'.label x

Uses 1 · Used by 8

Statement usesUnrooted binary phylogenetic tree

Used byIsomorphic trees have the same clusters · Clusters determine an unrooted binary tree · The number of unrooted binary phylogenetic trees · Number of unrooted binary phylogenetic trees · Unrooted binary trees correspond to binary hierarchies · An unrooted binary tree is determined by its quartets · Isomorphism invariance of the Robinson–Foulds distance · Robinson–Foulds distance vanishes exactly on isomorphic trees

DefinitionBinary hierarchy on a finite set#✓fully proved

A binary hierarchy on a finite set S: a family of nonempty subsets of S containing S and every singleton, any two members nested or disjoint, and every member with at least two elements the disjoint union of two members. These are the cluster systems of the rooted binary phylogenetic trees on S (Semple & Steel 2003, Section 3.1).

def IsBinaryHierarchy {α : Type*} [DecidableEq α] (S : Finset α) (H : Finset (Finset α)) :
    Prop :=
  S ∈ H ∧ (∀ C ∈ H, C.Nonempty ∧ C ⊆ S) ∧ (∀ x ∈ S, {x} ∈ H) ∧
    (∀ C ∈ H, ∀ D ∈ H, C ⊆ D ∨ D ⊆ C ∨ Disjoint C D) ∧
    ∀ C ∈ H, 1 < C.card → ∃ D₁ ∈ H, ∃ D₂ ∈ H, Disjoint D₁ D₂ ∧ D₁ ∪ D₂ = C

Used by 14

Used byEvery binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy · Binary hierarchy restricted below a member is a binary hierarchy · The number of binary hierarchies · Number of unrooted binary phylogenetic trees · Unrooted binary trees correspond to binary hierarchies · Correctness of BUILD · Number of members of a binary hierarchy · A rooted binary tree is determined by its triplets · Hierarchies are refined by binary trees · The majority-rule consensus tree · A binary hierarchy is a hierarchy · Maximum of the Robinson–Foulds distance · Splits-equivalence theorem

TheoremBinary hierarchy restricted below a member is a binary hierarchy#✓fully proved

The members of a binary hierarchy below a member form a binary hierarchy.

theorem isBinaryHierarchy_filter {α : Type u} [DecidableEq α] {S D : Finset α}
    {H : Finset (Finset α)} (hH : IsBinaryHierarchy S H) (hD : D ∈ H) :
    IsBinaryHierarchy D (H.filter (· ⊆ D))

Uses 1 · Used by 2

Statement usesBinary hierarchy on a finite set

Used byThe number of binary hierarchies · Number of members of a binary hierarchy

TheoremThe number of binary hierarchies#✓fully proved

On a nonempty finite set S there are (2 |S| - 3)‼ binary hierarchies, as many as rooted binary phylogenetic trees on S: a tree corresponds to the leaf sets of its subtrees.

theorem nat_card_binaryHierarchy {α : Type u} [DecidableEq α] (S : Finset α)
    (hS : S.Nonempty) :
    Nat.card {H : Finset (Finset α) // IsBinaryHierarchy S H} = (2 * S.card - 3)‼

Uses 9 · Used by 1

Statement usesBinary hierarchy on a finite set

Proof usesPlanar rooted binary tree with labeled leaves · Planar drawings of rooted binary trees on a taxon set · Swap of the children of an internal vertex · Leaf labels of a planar binary tree · Every planar binary tree has a leaf · Rooted binary phylogenetic tree · Schröder's count of rooted binary phylogenetic trees · Binary hierarchy restricted below a member is a binary hierarchy

Used byNumber of unrooted binary phylogenetic trees

DefinitionCluster of a vertex seen from a leaf#✓fully proved

The cluster of a vertex v seen from the leaf labeled a: the taxa x ≠ a whose leaf lies beyond v, i.e. v is on the path from the leaf a to the leaf x.

noncomputable def cluster {X : Type} [Fintype X] [DecidableEq X] (T : UnrootedBinaryTree X)
    (a : X) (v : T.V) : Finset X :=
  Finset.univ.filter fun x => x ≠ a ∧
    T.G.dist (T.label a) v + T.G.dist v (T.label x) = T.G.dist (T.label a) (T.label x)

Uses 1 · Used by 7

Statement usesUnrooted binary phylogenetic tree

Used byCluster set of a tree seen from a leaf · Isomorphic trees have the same clusters · Every binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy · Clusters determine an unrooted binary tree · Clusters seen from a leaf are edge sides · Split set from any leaf equals the edge splits

DefinitionCluster set of a tree seen from a leaf#✓fully proved

The clusters of all vertices seen from the leaf labeled a. (The cluster of the leaf a itself is the set of all other taxa, which is also the cluster of its neighbor.)

noncomputable def clusterSet {X : Type} [Fintype X] [DecidableEq X] (T : UnrootedBinaryTree X)
    (a : X) : Finset (Finset X) :=
  Finset.univ.image (cluster T a)

Uses 2 · Used by 25

Statement usesUnrooted binary phylogenetic tree · Cluster of a vertex seen from a leaf

Used byIsomorphic trees have the same clusters · Every binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy · Clusters determine an unrooted binary tree · Unrooted binary trees correspond to binary hierarchies · All species give the whole tree · Bootstrap support · Bootstrap support lies in the unit interval · Splits computed from a leaf are pairwise compatible · The majority-rule consensus tree · An unrooted binary tree is determined by its quartets · Majority splits of a family of trees · Majority splits are compatible · Clusters seen from a leaf omit that leaf · Bootstrap support above one half means a majority split · Robinson–Foulds distance · Symmetry of the Robinson–Foulds distance · Isomorphism invariance of the Robinson–Foulds distance · Robinson–Foulds distance vanishes exactly on isomorphic trees · Maximum of the Robinson–Foulds distance · Robinson–Foulds distance from a tree to itself is zero · Triangle inequality for the Robinson–Foulds distance · Split set of a tree computed from a leaf · Splits-equivalence theorem · Robinson–Foulds distance as half the split symmetric difference

TheoremIsomorphic trees have the same clusters#✓fully proved

Isomorphic trees have the same clusters.

theorem clusterSet_eq_of_iso {X : Type} [Fintype X] [DecidableEq X]
    {T T' : UnrootedBinaryTree X} (h : T.Iso T') (a : X) :
    clusterSet T a = clusterSet T' a

Uses 4 · Used by 3

Statement usesUnrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees · Cluster set of a tree seen from a leaf

Proof usesCluster of a vertex seen from a leaf

Used byUnrooted binary trees correspond to binary hierarchies · Isomorphism invariance of the Robinson–Foulds distance · Robinson–Foulds distance vanishes exactly on isomorphic trees

TheoremClusters of an unrooted tree form a binary hierarchy#✓fully proved

The clusters of a tree seen from a leaf form a binary hierarchy on the other taxa (Semple & Steel 2003, Section 3.1).

theorem isBinaryHierarchy_clusterSet {X : Type} [Fintype X] [DecidableEq X]
    (T : UnrootedBinaryTree X) (a : X) :
    IsBinaryHierarchy (Finset.univ.erase a) (clusterSet T a)

Uses 5 · Used by 8

Statement usesBinary hierarchy on a finite set · Unrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Proof usesCluster of a vertex seen from a leaf · Parent vertex towards a root in a connected graph

Used byUnrooted binary trees correspond to binary hierarchies · All species give the whole tree · Splits computed from a leaf are pairwise compatible · The majority-rule consensus tree · An unrooted binary tree is determined by its quartets · Majority splits are compatible · Clusters seen from a leaf omit that leaf · Maximum of the Robinson–Foulds distance

TheoremClusters determine an unrooted binary tree#✓fully proved

Two trees with the same clusters seen from the leaf a are isomorphic: the clusters determine the tree.

theorem iso_of_clusterSet_eq {X : Type} [Fintype X] [DecidableEq X]
    {T T' : UnrootedBinaryTree X} (a : X)
    (h : clusterSet T a = clusterSet T' a) : T.Iso T'

Uses 5 · Used by 3

Statement usesUnrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees · Cluster set of a tree seen from a leaf

Proof usesCluster of a vertex seen from a leaf · Parent vertex towards a root in a connected graph

Used byUnrooted binary trees correspond to binary hierarchies · An unrooted binary tree is determined by its quartets · Robinson–Foulds distance vanishes exactly on isomorphic trees

TheoremEvery binary hierarchy is a cluster set of a tree#✓fully proved

Every binary hierarchy on the taxa other than a is the cluster set, seen from the leaf a, of some unrooted binary phylogenetic tree (vertices: the leaf a and the members of the hierarchy; each member is joined to the smallest member strictly containing it).

theorem exists_clusterSet_eq {X : Type} [Fintype X] [DecidableEq X] (a : X)
    (H : Finset (Finset X)) (hH : IsBinaryHierarchy (Finset.univ.erase a) H) :
    ∃ T : UnrootedBinaryTree X, clusterSet T a = H

Uses 4 · Used by 3

Statement usesBinary hierarchy on a finite set · Unrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Proof usesCluster of a vertex seen from a leaf

Used byUnrooted binary trees correspond to binary hierarchies · The majority-rule consensus tree · Splits-equivalence theorem

DefinitionUnrooted binary trees correspond to binary hierarchies#✓fully proved

Unrooted binary phylogenetic trees up to label-preserving isomorphism correspond to the binary hierarchies on the taxa other than a, by their clusters seen from the leaf a.

MathlibExt.Biology.Phylogenetics.UnrootedTreeCount.quotEquivHierarchy · 15 lines

noncomputable def quotEquivHierarchy {X : Type} [Fintype X] [DecidableEq X] (a : X) :
    Quot (UnrootedBinaryTree.Iso (X := X)) ≃
      {H : Finset (Finset X) // IsBinaryHierarchy (Finset.univ.erase a) H} := by
  refine Equiv.ofBijective
    (Quot.lift (fun T => ⟨clusterSet T a, isBinaryHierarchy_clusterSet T a⟩)
      fun T T' h => Subtype.ext (clusterSet_eq_of_iso h a)) ⟨?_, ?_⟩
  · intro p q hpq
    induction p using Quot.ind with
    | mk T =>
    induction q using Quot.ind with
    | mk T' =>
    exact Quot.sound (iso_of_clusterSet_eq a (congrArg Subtype.val hpq))
  · rintro ⟨H, hH⟩
    obtain ⟨T, hT⟩ := exists_clusterSet_eq a H hH
    exact ⟨Quot.mk _ T, Subtype.ext hT⟩

Uses 8 · Used by 1

Statement usesBinary hierarchy on a finite set · Unrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees · Cluster set of a tree seen from a leaf · Isomorphic trees have the same clusters · Every binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy · Clusters determine an unrooted binary tree

Used byNumber of unrooted binary phylogenetic trees

TheoremNumber of unrooted binary phylogenetic trees#✓fully proved

The count (2 n - 5)‼ of unrooted binary phylogenetic trees holds from n = 2 taxa on: for n = 2 the single tree is one edge and 2 · 2 - 5 = 0 in ℕ, 0‼ = 1 (the conventional value (-1)‼ = 1). For n ≤ 1 there is no tree while the formula gives 1.

theorem nat_card_unrootedBinaryTree_of_two_le (n : ℕ) (hn : 2 ≤ n) :
    Nat.card (Quot (UnrootedBinaryTree.Iso (X := Fin n))) = (2 * n - 5)‼

Uses 5 · Used by 1

Statement usesUnrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees

Proof usesBinary hierarchy on a finite set · The number of binary hierarchies · Unrooted binary trees correspond to binary hierarchies

Used byThe number of unrooted binary phylogenetic trees

TheoremThe number of unrooted binary phylogenetic trees#✓fully proved

On n ≥ 3 labeled taxa there are (2 n - 5)‼ = 1 · 3 ⋯ (2 n - 5) unrooted binary phylogenetic trees up to label-preserving isomorphism.

theorem nat_card_unrootedBinaryTree (n : ℕ) (hn : 3 ≤ n) :
    Nat.card (Quot (UnrootedBinaryTree.Iso (X := Fin n))) = (2 * n - 5)‼

Sources

• Semple & Steel (2003), Proposition 2.1.4. Proves the deferred entry nat_card_unrootedBinaryTree.

Uses 3

Statement usesUnrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees

Proof usesNumber of unrooted binary phylogenetic trees

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.