Double-tree approximation for metric TSP

StructureMetric cost function#✓fully proved

A cost function \(d\) assigning to each pair of vertices a value in a linearly ordered additive commutative monoid is metric when, for all vertices \(x\), \(y\), \(z\), it is symmetric, \(d(x, y) = d(y, x)\), zero on the diagonal, \(d(x, x) = 0\), nonnegative, \(0 \le d(x, y)\), and satisfies the triangle inequality \(d(x, z) \le d(x, y) + d(y, z)\).

structure IsMetricCost (d : α → α → R) : Prop where
  symm : ∀ x y, d x y = d y x
  self : ∀ x, d x x = 0
  nonneg : ∀ x y, 0 ≤ d x y
  triangle : ∀ x y z, d x z ≤ d x y + d y z
Used by 8
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · Shortcutting a closed walk through its base point · Rerouting the end of a walk · Changing the starting vertex of a walk · The closed preorder walk below a vertex costs at most twice the forest · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · The preorder tour costs at most twice the tree · A minimum spanning tree costs at most any tour

DefinitionCost of a walk#✓fully proved

Let \(d\) be a cost function on the vertices with values in an additive commutative monoid. For a vertex \(x\) and a list \(L = [y_1, \dots, y_n]\) of vertices, the cost of the walk from \(x\) through \(L\) is \(d(x, y_1) + d(y_1, y_2) + \dots + d(y_{n-1}, y_n)\), and \(0\) when \(L\) is empty.

def pathFrom (d : α → α → R) : α → List α → R
  | _, [] => 0
  | x, y :: L => d x y + pathFrom d y L
Used by 7
Used byShortcutting a closed walk through its base point · Rerouting the end of a walk · Changing the starting vertex of a walk · The closed preorder walk below a vertex costs at most twice the forest · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Cost of a closed tour · A minimum spanning tree costs at most any tour

DefinitionCost of a closed tour#✓fully proved

For a cost function \(d\) on the vertices with values in an additive commutative monoid, the cost of the closed tour that visits \(x_0, x_1, \dots, x_k\) in order and returns to its first vertex is \(\sum_{i=1}^{k} d(x_{i-1}, x_i) + d(x_k, x_0)\). The empty tour costs \(0\).

def tourCost (d : α → α → R) : List α → R
  | [] => 0
  | h :: t => pathFrom d h (t ++ [h])
Uses 1 · Used by 4
Statement usesCost of a walk
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · The preorder tour costs at most twice the tree · A minimum spanning tree costs at most any tour

InductiveRooted forest in left-child right-sibling form#✓fully proved

A rooted forest with vertices in \(\alpha\) is either empty, or consists of a first tree with root \(v\), whose subtrees form a forest (the children of \(v\)), followed by a forest of the remaining trees (the siblings of \(v\)).

inductive Forest (α : Type u) where
  | nil : Forest α
  | cons (v : α) (children siblings : Forest α) : Forest α
Used by 22
Used byThe APPROX-TSP-TOUR algorithm · The approximate TSP tour is a tour · Running time of APPROX-TSP-TOUR · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · Forest of a parent array below a vertex · Path as a forest · Minimum spanning tree of a vertex list · Rooted spanning tree of a vertex list · The forest of a parent tree spans all vertices · The closed preorder walk below a vertex costs at most twice the forest · Preorder of a forest · Preorder of a path · Preorder walk · Preorder walk with an accumulator · Result of the preorder walk with an accumulator · Forest of Prim's tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Edge sums over a parent tree · The preorder tour costs at most twice the tree · Weight of a forest below a vertex · Weight of the forest built from a parent array · A minimum spanning tree costs at most any tour

DefinitionPreorder of a forest#✓fully proved

The list of the vertices of a forest in preorder: empty for the empty forest, and for a forest with first root \(v\), children forest \(C\) and sibling forest \(S\), the vertex \(v\), followed by the preorder of \(C\), followed by the preorder of \(S\).

The preorder walk computes this list without appending lists.

def preorder : Forest α → List α
  | nil => []
  | cons v ch sib => v :: ch.preorder ++ sib.preorder
Uses 1 · Used by 13
Statement usesRooted forest in left-child right-sibling form
Used byThe approximate TSP tour is a tour · Running time of APPROX-TSP-TOUR · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · Rooted spanning tree of a vertex list · The forest of a parent tree spans all vertices · The closed preorder walk below a vertex costs at most twice the forest · Preorder of a path · Result of the preorder walk with an accumulator · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Edge sums over a parent tree · The preorder tour costs at most twice the tree · Weight of the forest built from a parent array · A minimum spanning tree costs at most any tour

DefinitionWeight of a forest below a vertex#✓fully proved

For a cost function \(d\) and a vertex \(p\), the weight of a forest hanging below \(p\) is the total cost of its tree edges: each top-level vertex \(v\) is joined to \(p\) by an edge of cost \(d(p, v)\), and each vertex \(u\) is joined to each of its children \(c\) by an edge of cost \(d(u, c)\). The empty forest has weight \(0\).

def weight (d : α → α → R) (p : α) : Forest α → R
  | nil => 0
  | cons v ch sib => d p v + ch.weight d v + sib.weight d p
Uses 1 · Used by 7
Statement usesRooted forest in left-child right-sibling form
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · Minimum spanning tree of a vertex list · The closed preorder walk below a vertex costs at most twice the forest · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · The preorder tour costs at most twice the tree · Weight of the forest built from a parent array · A minimum spanning tree costs at most any tour

DefinitionPath as a forest#✓fully proved

The forest of a list \(x_1, x_2, \dots, x_n\) of vertices is the path \(x_1, x_2, \dots, x_n\): \(x_1\) is its only top-level vertex and each \(x_{i+1}\) is the only child of \(x_i\). The empty list gives the empty forest.

def chain : List α → Forest α
  | [] => nil
  | x :: xs => cons x (chain xs) nil
Uses 1 · Used by 2
Statement usesRooted forest in left-child right-sibling form
Used byPreorder of a path · A minimum spanning tree costs at most any tour

DefinitionPreorder walk with an accumulator#✓fully proved

For a forest \(F\) and a list \(a\) of vertices, this is the timed computation defined as follows. On the empty forest it returns \(a\) at no cost. On a forest with first root \(v\), children forest \(C\) and sibling forest \(S\), it charges one time unit, walks \(S\) with accumulator \(a\) to get a list \(b\), walks \(C\) with accumulator \(b\) to get a list \(c\), and returns \(v\) followed by \(c\). It thus returns the vertices of \(F\) in preorder followed by \(a\), at one time unit per vertex of \(F\).

The accumulator means no list is ever appended, so the untimed work is linear as well.

def preorderWalkAux : Forest α → List α → TimeM ℕ (List α)
  | .nil, acc => pure acc
  | .cons v ch sib, acc => do
      ✓
      let b ← preorderWalkAux sib acc
      let a ← preorderWalkAux ch b
      pure (v :: a)
Uses 1 · Used by 6
Statement usesRooted forest in left-child right-sibling form
Used byThe approximate TSP tour is a tour · Running time of APPROX-TSP-TOUR · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · Preorder walk · Result of the preorder walk with an accumulator · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

DefinitionPreorder walk#✓fully proved

For a forest \(F\), the preorder walk of \(F\) is the preorder walk of \(F\) with the empty list as accumulator: a timed computation that returns the vertices of \(F\) in preorder, at one time unit per vertex.

def preorderWalk (F : Forest α) : TimeM ℕ (List α) := preorderWalkAux F []
Uses 2 · Used by 5
Statement usesRooted forest in left-child right-sibling form · Preorder walk with an accumulator
Used byThe APPROX-TSP-TOUR algorithm · The approximate TSP tour is a tour · Running time of APPROX-TSP-TOUR · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

DefinitionThe APPROX-TSP-TOUR algorithm#✓fully proved

CLRS APPROX-TSP-TOUR, steps 3 and 4: given a root \(r\) and a forest \(F\) (the subtrees of a spanning tree with root \(r\)), return the tour that lists \(r\) followed by the vertices of \(F\) in preorder. As a timed computation it charges one unit for \(r\) and one unit for each vertex visited by the preorder walk of \(F\).

def approxTSPTour (r : α) (F : Forest α) : TimeM ℕ (List α) := do
  ✓
  let w ← preorderWalk F
  pure (r :: w)
Uses 2 · Used by 5
Statement usesRooted forest in left-child right-sibling form · Preorder walk
Used byThe approximate TSP tour is a tour · Running time of APPROX-TSP-TOUR · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · APPROX-TSP-TOUR with Prim's tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremResult of the preorder walk with an accumulator#✓fully proved

For every forest \(F\) and every list \(a\) of vertices, the preorder walk of \(F\) with accumulator \(a\) returns the vertices of \(F\) in preorder followed by \(a\).

theorem preorderWalkAux_ret (F : Forest α) (acc : List α) :
    (preorderWalkAux F acc).ret = F.preorder ++ acc
Uses 3 · Used by 3
Statement usesRooted forest in left-child right-sibling form · Preorder of a forest · Preorder walk with an accumulator
Used byThe approximate TSP tour is a tour · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremRunning time of APPROX-TSP-TOUR#✓fully proved

For every root \(r\) and forest \(F\), the running time of APPROX-TSP-TOUR on \(r\) and \(F\) equals the length of the list of \(r\) followed by the vertices of \(F\) in preorder: one unit per vertex of the returned tour.

@[simp]
theorem approxTSPTour_time (r : α) (F : Forest α) :
    (approxTSPTour r F).time = (r :: F.preorder).length
Uses 5
Statement usesRooted forest in left-child right-sibling form · Preorder of a forest · The APPROX-TSP-TOUR algorithm
Proof usesPreorder walk · Preorder walk with an accumulator

TheoremChanging the starting vertex of a walk#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid, which is symmetric, zero on the diagonal, nonnegative, and satisfies the triangle inequality. For vertices \(q\), \(p\) and a list \(L\) of vertices, the cost of the walk from \(q\) through \(L\) is at most \(d(q, p)\) plus the cost of the walk from \(p\) through \(L\).

theorem pathFrom_le_add (hd : IsMetricCost d) (q p : α) (L : List α) :
    pathFrom d q L ≤ d q p + pathFrom d p L
Uses 2 · Used by 1
Statement usesMetric cost function · Cost of a walk
Used byShortcutting a closed walk through its base point

TheoremShortcutting a closed walk through its base point#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid, which is symmetric, zero on the diagonal, nonnegative, and satisfies the triangle inequality. For a vertex \(p\) and lists \(A\), \(B\) of vertices, the cost of the walk that starts at \(p\), visits \(A\) and then \(B\) in order and returns to \(p\) is at most the cost of the walk from \(p\) through \(A\) back to \(p\) plus the cost of the walk from \(p\) through \(B\) back to \(p\).

theorem pathFrom_append_append_le (hd : IsMetricCost d) (p : α) (A B : List α) :
    pathFrom d p (A ++ B ++ [p]) ≤ pathFrom d p (A ++ [p]) + pathFrom d p (B ++ [p])
Uses 3 · Used by 1
Statement usesMetric cost function · Cost of a walk
Proof usesChanging the starting vertex of a walk
Used byThe closed preorder walk below a vertex costs at most twice the forest

TheoremRerouting the end of a walk#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid, which is symmetric, zero on the diagonal, nonnegative, and satisfies the triangle inequality. For vertices \(v\), \(p\) and a list \(C\) of vertices, the cost of the walk from \(v\) through \(C\) ending at \(p\) is at most the cost of the walk from \(v\) through \(C\) ending back at \(v\), plus \(d(v, p)\).

theorem pathFrom_append_singleton_le (hd : IsMetricCost d) (v p : α) (C : List α) :
    pathFrom d v (C ++ [p]) ≤ pathFrom d v (C ++ [v]) + d v p
Uses 2 · Used by 1
Statement usesMetric cost function · Cost of a walk
Used byThe closed preorder walk below a vertex costs at most twice the forest

TheoremThe closed preorder walk below a vertex costs at most twice the forest#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid, which is symmetric, zero on the diagonal, nonnegative, and satisfies the triangle inequality. For a forest \(F\) and a vertex \(p\), let \(w\) be the weight of \(F\) hanging below \(p\): the total cost of the edges joining \(p\) to the top-level vertices of \(F\) and each vertex of \(F\) to its children. Then the cost of the walk that starts at \(p\), visits the vertices of \(F\) in preorder and returns to \(p\) is at most \(w + w\).

theorem pathFrom_preorder_le (hd : IsMetricCost d) (F : Forest α) (p : α) :
    pathFrom d p (F.preorder ++ [p]) ≤ F.weight d p + F.weight d p
Uses 7 · Used by 1
Statement usesRooted forest in left-child right-sibling form · Preorder of a forest · Weight of a forest below a vertex · Metric cost function · Cost of a walk
Proof usesShortcutting a closed walk through its base point · Rerouting the end of a walk
Used byThe preorder tour costs at most twice the tree

TheoremThe preorder tour costs at most twice the tree#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid that is symmetric, zero on the diagonal, nonnegative and satisfies the triangle inequality. Let \(T\) be a rooted tree with root \(r\), given by the forest \(F\) of the subtrees of \(r\), and let \(w(T)\) be its weight, the total cost of its edges. Then the closed tour that visits \(r\), then the vertices of \(F\) in preorder, and returns to \(r\) costs at most \(2\,w(T)\).

theorem tourCost_preorder_le (hd : IsMetricCost d) (r : α) (F : Forest α) :
    tourCost d (r :: F.preorder) ≤ 2 • F.weight d r
Sources
  • CLRS Theorem 35.2, first half.
Uses 6 · Used by 2
Statement usesRooted forest in left-child right-sibling form · Preorder of a forest · Weight of a forest below a vertex · Metric cost function · Cost of a closed tour
Proof usesThe closed preorder walk below a vertex costs at most twice the forest
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremPreorder of a path#✓fully proved

For every list \(L\) of vertices, the preorder of the forest of \(L\) (the path through the vertices of \(L\) in order) is \(L\) itself.

@[simp]
theorem Forest.preorder_chain (xs : List α) : (Forest.chain xs).preorder = xs
Uses 3 · Used by 1
Statement usesPath as a forest · Preorder of a forest
Proof usesRooted forest in left-child right-sibling form
Used byA minimum spanning tree costs at most any tour

DefinitionRooted spanning tree of a vertex list#✓fully proved

The tree with root \(r\) and subtree forest \(F\) is a spanning tree of a list \(V\) of vertices when the vertices of \(V\) are distinct and the list of \(r\) followed by the vertices of \(F\) in preorder is a permutation of \(V\): the vertices of the tree are those of \(V\), each exactly once.

def IsSpanning (V : List α) (r : α) (F : Forest α) : Prop := V.Nodup ∧ (r :: F.preorder).Perm V
Uses 2 · Used by 5
Statement usesRooted forest in left-child right-sibling form · Preorder of a forest
Used byThe approximate TSP tour is a tour · Minimum spanning tree of a vertex list · The forest of a parent tree spans all vertices · Prim's forest spans all vertices · A minimum spanning tree costs at most any tour

DefinitionMinimum spanning tree of a vertex list#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid. The tree with root \(r\) and subtree forest \(F\) is a minimum spanning tree of a list \(V\) of vertices for \(d\) when it is a spanning tree of \(V\) (the vertices of \(V\) are distinct and the list of \(r\) followed by the vertices of \(F\) in preorder is a permutation of \(V\)) and, for every vertex \(r'\) and forest \(F'\) such that the tree with root \(r'\) and subtree forest \(F'\) is a spanning tree of \(V\), the weight of \(F\) below \(r\) is at most the weight of \(F'\) below \(r'\).

def IsMinSpanning (d : α → α → R) (V : List α) (r : α) (F : Forest α) : Prop :=
  IsSpanning V r F ∧ ∀ r' F', IsSpanning V r' F' → F.weight d r ≤ F'.weight d r'
Uses 3 · Used by 2
Statement usesRooted forest in left-child right-sibling form · Weight of a forest below a vertex · Rooted spanning tree of a vertex list
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · A minimum spanning tree costs at most any tour

DefinitionTour of a vertex list#✓fully proved

A list \(H\) is a tour of a list \(V\) of vertices when the vertices of \(V\) are distinct and \(H\) is a permutation of \(V\): \(H\) lists each vertex of \(V\) exactly once and nothing else.

def IsTour (V H : List α) : Prop := V.Nodup ∧ H.Perm V
Used by 5
Used byThe approximate TSP tour is a tour · APPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour · The tour from Prim's tree is a tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · A minimum spanning tree costs at most any tour

TheoremA minimum spanning tree costs at most any tour#✓fully proved

Let \(d\) be a cost function on the vertices with values in a linearly ordered additive commutative monoid that is symmetric, zero on the diagonal, nonnegative and satisfies the triangle inequality. Let \(V\) be a list of distinct vertices. Let \(T\) be a minimum spanning tree of \(V\) for \(d\): a rooted tree whose vertices are the elements of \(V\), each once, whose weight (the total cost of its edges) is at most that of every such tree. Let \(H\) be a tour of \(V\), a list that is a permutation of \(V\). Then the weight of \(T\) is at most the cost of the closed tour \(H\).

A tour minus its closing edge is a spanning path, which is a spanning tree.

theorem weight_le_tourCost (hd : IsMetricCost d) {V : List α} {r : α} {F : Forest α}
    (hT : IsMinSpanning d V r F) {H : List α} (hH : IsTour V H) :
    F.weight d r ≤ tourCost d H
Sources
  • CLRS Theorem 35.2, second half.
Uses 11 · Used by 1
Statement usesRooted forest in left-child right-sibling form · Weight of a forest below a vertex · Metric cost function · Minimum spanning tree of a vertex list · Tour of a vertex list · Cost of a closed tour
Proof usesPath as a forest · Preorder of a forest · Preorder of a path · Rooted spanning tree of a vertex list · Cost of a walk
Used byAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour

TheoremThe approximate TSP tour is a tour#✓fully proved

Let \(V\) be a list of distinct vertices, and let \(r\) and \(F\) be such that \(r\) followed by the vertices of the forest \(F\) in preorder is a permutation of \(V\) (the tree with root \(r\) and subtree forest \(F\) spans \(V\)). Then the list returned by APPROX-TSP-TOUR on \(r\) and \(F\) is a tour of \(V\): it is a permutation of \(V\).

theorem approxTSPTour_isTour {V : List α} {r : α} {F : Forest α} (hT : IsSpanning V r F) :
    IsTour V (approxTSPTour r F).ret
Uses 8 · Used by 1
Statement usesRooted forest in left-child right-sibling form · Rooted spanning tree of a vertex list · Tour of a vertex list · The APPROX-TSP-TOUR algorithm
Proof usesPreorder of a forest · Preorder walk · Preorder walk with an accumulator · Result of the preorder walk with an accumulator
Used byThe tour from Prim's tree is a tour

TheoremAPPROX-TSP-TOUR on a given minimum spanning tree costs at most twice any tour#✓fully proved

Let \(d\) be a cost function on vertices with values in a linearly ordered additive commutative monoid that is symmetric, zero on the diagonal, nonnegative and satisfies the triangle inequality. Let \(V\) be a list of vertices, let the tree with root \(r\) and subtree forest \(F\) be a minimum spanning tree of \(V\) for \(d\), and let \(H\) be a tour of \(V\). Then the cost under \(d\) of the closed tour returned by APPROX-TSP-TOUR on \(r\) and \(F\) is at most twice the cost under \(d\) of the closed tour \(H\).

theorem approxTSPTour_two_approx (hd : IsMetricCost d) {V : List α} {r : α} {F : Forest α}
    (hT : IsMinSpanning d V r F) {H : List α} (hH : IsTour V H) :
    tourCost d (approxTSPTour r F).ret ≤ 2 • tourCost d H
Sources
  • CLRS, third edition, Theorem 35.2.
Uses 13
Statement usesRooted forest in left-child right-sibling form · Metric cost function · Minimum spanning tree of a vertex list · Tour of a vertex list · The APPROX-TSP-TOUR algorithm · Cost of a closed tour
Proof usesPreorder of a forest · Weight of a forest below a vertex · Preorder walk · Preorder walk with an accumulator · Result of the preorder walk with an accumulator · The preorder tour costs at most twice the tree · A minimum spanning tree costs at most any tour

DefinitionOne step up a parent array#✓fully proved

Let \(p\) be a parent array on the vertices \(\{0, \dots, n-1\}\), assigning to each vertex \(v\) either a parent \(p(v)\) or no parent. Then \(\operatorname{up}(v)\) is the parent \(p(v)\) when \(v\) has one, and \(v\) itself otherwise, so a root stays put.

def up (v : Fin n) : Fin n := (par v).getD v
Used by 8
Used byDescendant within \(k\) levels · Every non-root vertex lies below the root · The forest of a parent tree spans all vertices · Parent tree · Prim's parent array is a parent tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Edge sums over a parent tree · Weight of the forest built from a parent array

DefinitionChildren in a parent array#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing. The children of a vertex \(v\) are the vertices \(c\) whose parent \(p(c)\) is \(v\), listed in increasing order.

def children (v : Fin n) : List (Fin n) := (List.finRange n).filter fun c => par c = some v
Used by 4
Used byForest of a parent array below a vertex · The forest of a parent tree spans all vertices · Edge sums over a parent tree · Weight of the forest built from a parent array

DefinitionForest of a parent array below a vertex#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing. For \(k \in \mathbb{N}\) and a vertex \(v\), the forest below \(v\) of depth \(k\) is empty when \(k = 0\). For depth \(k + 1\) it has one tree for each child \(c\) of \(v\) (each vertex whose parent is \(v\)), in increasing order of \(c\), namely \(c\) with the forest below \(c\) of depth \(k\) as its subtrees.

def buildForest : ℕ → Fin n → Forest (Fin n)
  | 0, _ => .nil
  | k + 1, v => (children par v).foldr (fun c acc => .cons c (buildForest k c) acc) .nil
Uses 2 · Used by 5
Statement usesRooted forest in left-child right-sibling form · Children in a parent array
Used byThe forest of a parent tree spans all vertices · Forest of Prim's tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Edge sums over a parent tree · Weight of the forest built from a parent array

StructureParent tree#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing, and let a step up move a vertex to its parent, leaving a vertex without parent in place. The parent array \(p\) is a parent tree with root \(r\) when \(r\) has no parent and every vertex reaches \(r\) after finitely many steps up.

structure ParentTree (root : Fin n) : Prop where
  root_none : par root = none
  reach : ∀ v, ∃ j, (up par)^[j] v = root
Uses 1 · Used by 5
Statement usesOne step up a parent array
Used byEvery non-root vertex lies below the root · The forest of a parent tree spans all vertices · Prim's parent array is a parent tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation · Edge sums over a parent tree

DefinitionDescendant within \(k\) levels#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing, and let a step up move a vertex to its parent, leaving a vertex without parent in place. For \(k \in \mathbb{N}\), a vertex \(u\) lies strictly below a vertex \(v\), at most \(k\) levels down, when for some \(j < k\) the vertex reached from \(u\) after \(j\) steps up has parent \(v\).

def DescK (k : ℕ) (v u : Fin n) : Prop := ∃ j < k, par ((up par)^[j] u) = some v
Uses 1 · Used by 3
Statement usesOne step up a parent array
Used byEvery non-root vertex lies below the root · The forest of a parent tree spans all vertices · Edge sums over a parent tree

TheoremWeight of the forest built from a parent array#✓fully proved

Let \(p\) be a parent array on the vertices \(\{0, \dots, n-1\}\), let \(d\) be a cost on ordered pairs of vertices with values in an additive commutative monoid, and let \(\operatorname{up}(u)\) be the parent of \(u\), or \(u\) itself if \(u\) has no parent. For every \(k \in \mathbb{N}\) and every vertex \(v\), let \(F\) be the forest of the subtrees of the children of \(v\) in \(p\), cut off \(k\) levels below \(v\). Then the weight under \(d\) of \(F\) hanging below \(v\) equals the sum of \(d(\operatorname{up}(u), u)\) over the vertices \(u\) of \(F\) in preorder.

theorem weight_buildForest : ∀ (k : ℕ) (v : Fin n),
    (buildForest par k v).weight d v =
      ((buildForest par k v).preorder.map fun u => d (up par u) u).sum
Uses 6 · Used by 1
Statement usesPreorder of a forest · Weight of a forest below a vertex · Forest of a parent array below a vertex · One step up a parent array
Proof usesRooted forest in left-child right-sibling form · Children in a parent array
Used byAPPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremEvery non-root vertex lies below the root#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing, forming a parent tree with root \(r\), and let a step up move a vertex to its parent, leaving a vertex without parent in place. Then every vertex \(u \ne r\) lies strictly below \(r\), at most \(n\) levels down: for some \(j < n\), the vertex reached from \(u\) after \(j\) steps up has parent \(r\).

theorem descK_root (ht : ParentTree par root) {u : Fin n} (hu : u ≠ root) :
    DescK par n root u
Uses 3 · Used by 2
Statement usesDescendant within \(k\) levels · Parent tree
Proof usesOne step up a parent array
Used byThe forest of a parent tree spans all vertices · Edge sums over a parent tree

TheoremThe forest of a parent tree spans all vertices#✓fully proved

Let \(p\) assign to each vertex of \(\{0, \dots, n-1\}\) either a parent or nothing, forming a parent tree with root \(r\). Then \(r\) together with the forest below \(r\) of depth \(n\) built from \(p\) is a spanning tree of \(\{0, \dots, n-1\}\): \(r\) followed by the vertices of the forest in preorder lists every vertex exactly once.

theorem isSpanning_buildForest (ht : ParentTree par root) :
    IsSpanning (List.finRange n) root (buildForest par n root)
Uses 9 · Used by 1
Statement usesRooted spanning tree of a vertex list · Parent tree · Forest of a parent array below a vertex
Proof usesDescendant within \(k\) levels · Rooted forest in left-child right-sibling form · Preorder of a forest · Children in a parent array · Every non-root vertex lies below the root · One step up a parent array
Used byPrim's forest spans all vertices

DefinitionComplete graph as an ordered adjacency#✓fully proved

For \(n \in \mathbb{N}\), the complete graph on the vertices \(\{0, \dots, n-1\}\) as a directed adjacency: the vertices are listed in increasing order, and the neighbours of each vertex \(u\) are all vertices other than \(u\), in increasing order.

def completeAdjacency (n : ℕ) : DirectedAdjacency (Fin n) where
  vertices := List.finRange n
  vertices_nodup := List.nodup_finRange n
  vertices_complete := List.mem_finRange
  adjacency u := (List.finRange n).filter (· ≠ u)
Uses 1 · Used by 5
Statement usesDirected adjacency graph
Used byNeighbours in the complete adjacency · Prim's parent array is a parent tree · Prim's parent array on the complete graph · Prim's tree is a minimum spanning tree · Prim's tree is a spanning tree

DefinitionSymmetrized edge weights#✓fully proved

Given costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a type with commutative addition, the weight of an unordered pair \(\{u, v\}\) is \(d(u,v) + d(v,u)\), which does not depend on the order of \(u\) and \(v\). When \(d\) is symmetric this is twice the cost, which leaves minimum spanning trees unchanged.

def symWeight {W : Type*} [Add W] [Std.Commutative (α := W) (· + ·)] (d : Fin n → Fin n → W) :
    Sym2 (Fin n) → W :=
  Sym2.lift ⟨fun u v => d u v + d v u, fun _ _ => Std.Commutative.comm _ _⟩
Used by 5
Used byPrim's parent array is a parent tree · Prim's parent array on the complete graph · Prim's tree is a minimum spanning tree · Prim's tree is a spanning tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

DefinitionPrim's parent array on the complete graph#✓fully proved

Given costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a linearly ordered type with a zero and commutative addition, and a root \(r\), this is the parent array returned by Prim's algorithm run from \(r\) on the complete graph on these vertices, with the weight of the edge \(\{u, v\}\) equal to \(d(u,v) + d(v,u)\): it sends each vertex to its parent, or to no parent.

def primParents {W : Type*} [LinearOrder W] [Zero W] [Add W] [Std.Commutative (α := W) (· + ·)]
    (d : Fin n → Fin n → W) (root : Fin n) : Fin n → Option (Fin n) :=
  let parents := (Prim.prim (completeAdjacency n) (symWeight d) root).ret
  fun v => parents[v]
Uses 3 · Used by 6
Statement usesComplete graph as an ordered adjacency · Symmetrized edge weights · Prim's algorithm with an indexed binary heap
Used byPrim's forest spans all vertices · Prim's parent array is a parent tree · Forest of Prim's tree · Prim's tree · Prim's tree is a minimum spanning tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

DefinitionForest of Prim's tree#✓fully proved

Given costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a linearly ordered type with a zero and commutative addition, and a root \(r\), take Prim's parent array for \(d\) and \(r\) (Prim's algorithm run from \(r\) on the complete graph with edge weights \(d(u,v) + d(v,u)\)). This forest is the forest of the subtrees below \(r\) in that parent array, cut off \(n\) levels below \(r\), in left-child right-sibling form, with the children of each vertex in vertex order.

def primForest {W : Type*} [LinearOrder W] [Zero W] [Add W] [Std.Commutative (α := W) (· + ·)]
    (d : Fin n → Fin n → W) (root : Fin n) : Forest (Fin n) :=
  buildForest (primParents d root) n root
Uses 3 · Used by 4
Statement usesRooted forest in left-child right-sibling form · Forest of a parent array below a vertex · Prim's parent array on the complete graph
Used byPrim's forest spans all vertices · APPROX-TSP-TOUR with Prim's tree · The tour from Prim's tree is a tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

DefinitionAPPROX-TSP-TOUR with Prim's tree#✓fully proved

Given costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a linearly ordered type with a zero and commutative addition, and a root \(r\), the tour is \(r\) followed by the vertices of the forest of Prim's tree below \(r\) in preorder. Its running time counts one unit per vertex of the tour; running Prim's algorithm and building the forest are not counted.

This is CLRS APPROX-TSP-TOUR, with the minimum spanning tree computed by Prim.

def primTSPTour {W : Type*} [LinearOrder W] [Zero W] [Add W] [Std.Commutative (α := W) (· + ·)]
    (d : Fin n → Fin n → W) (root : Fin n) : TimeM ℕ (List (Fin n)) :=
  approxTSPTour root (primForest d root)
Uses 2 · Used by 2
Statement usesThe APPROX-TSP-TOUR algorithm · Forest of Prim's tree
Used byThe tour from Prim's tree is a tour · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremNeighbours in the complete adjacency#✓fully proved

For all vertices \(u, v\) of \(\{0, \dots, n-1\}\), \(v\) is listed among the neighbours of \(u\) in the complete graph as an ordered adjacency if and only if \(u\) and \(v\) are adjacent in the complete simple graph on \(\{0, \dots, n-1\}\), that is, \(u \ne v\).

theorem mem_completeAdjacency (u v : Fin n) :
    v ∈ (completeAdjacency n).adjacency u ↔ (⊤ : SimpleGraph (Fin n)).Adj u v
Uses 2 · Used by 2
Statement usesDirected adjacency graph · Complete graph as an ordered adjacency
Used byPrim's tree is a minimum spanning tree · Prim's tree is a spanning tree

AbbreviationPrim's tree#✓fully proved

Given costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a linearly ordered type with a zero and commutative addition, and a root \(r\), Prim's tree is the simple graph on these vertices in which distinct vertices \(u\) and \(v\) are adjacent when one of them is the parent of the other in Prim's parent array for \(d\) and \(r\).

abbrev primTree {W : Type*} [LinearOrder W] [Zero W] [Add W] [Std.Commutative (α := W) (· + ·)]
    (d : Fin n → Fin n → W) (root : Fin n) : SimpleGraph (Fin n) :=
  SimpleGraph.fromRel fun u v => primParents d root v = some u
Uses 1 · Used by 4
Statement usesPrim's parent array on the complete graph
Used byPrim's parent array is a parent tree · Prim's tree is a minimum spanning tree · Prim's tree is a spanning tree · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremPrim's tree is a spanning tree#✓fully proved

For costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in any linearly ordered type with a zero and commutative addition, and any root \(r\), Prim's tree for \(d\) and \(r\) is a tree on all of \(\{0, \dots, n-1\}\), that is, a spanning tree of the complete graph.

theorem primTree_isTree {W : Type*} [LinearOrder W] [Zero W] [Add W]
    [Std.Commutative (α := W) (· + ·)] (d : Fin n → Fin n → W) (root : Fin n) :
    (primTree d root).IsTree
Uses 5 · Used by 1
Statement usesPrim's tree
Proof usesComplete graph as an ordered adjacency · Neighbours in the complete adjacency · Symmetrized edge weights · Prim's algorithm returns a tree
Used byPrim's parent array is a parent tree

TheoremPrim's tree is a minimum spanning tree#✓fully proved

Let \(d(u,v)\) be real costs on the vertices \(\{0, \dots, n-1\}\), let \(r\) be a vertex, and weigh each edge \(\{u, v\}\) by \(d(u,v) + d(v,u)\). Then Prim's tree for \(d\) and \(r\) is a tree, and for every tree \(H\) on these vertices the total weight of the edges of Prim's tree is at most the total weight of the edges of \(H\).

theorem primTree_isMinimumSpanningTree (d : Fin n → Fin n → ℝ) (root : Fin n) :
    (primTree d root).IsTree ∧ ∀ H : SimpleGraph (Fin n), H.IsTree →
      (∑ e ∈ (primTree d root).edgeFinset, symWeight d e) ≤
        ∑ e ∈ H.edgeFinset, symWeight d e
Uses 7 · Used by 1
Statement usesPrim's parent array on the complete graph · Prim's tree · Symmetrized edge weights
Proof usesComplete graph as an ordered adjacency · Neighbours in the complete adjacency · Prim's algorithm with an indexed binary heap · Prim's algorithm returns a minimum spanning tree
Used byAPPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremPrim's parent array is a parent tree#✓fully proved

Let \(W\) be a linearly ordered type with a zero and a commutative addition, let \(d\) assign a weight in \(W\) to each ordered pair of vertices of \(\{0, \dots, n-1\}\), and let \(r\) be a vertex. Then Prim's parent array for \(d\) from \(r\) is a parent tree with root \(r\): \(r\) has no parent, and every vertex reaches \(r\) after finitely many steps up, where a step up moves a vertex to its parent and leaves a vertex without parent in place.

theorem parentTree_primParents {W : Type*} [LinearOrder W] [Zero W] [Add W]
    [Std.Commutative (α := W) (· + ·)] (d : Fin n → Fin n → W) (root : Fin n) :
    ParentTree (primParents d root) root
Uses 9 · Used by 2
Statement usesParent tree · Prim's parent array on the complete graph
Proof usesComplete graph as an ordered adjacency · Prim's tree · Prim's tree is a spanning tree · Symmetrized edge weights · One step up a parent array · Prim's algorithm with an indexed binary heap · The root has no parent in Prim's algorithm
Used byPrim's forest spans all vertices · APPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremPrim's forest spans all vertices#✓fully proved

Let \(W\) be a linearly ordered type with a zero and a commutative addition, let \(d\) assign a weight in \(W\) to each ordered pair of vertices of \(\{0, \dots, n-1\}\), and let \(r\) be a vertex. Then \(r\) together with Prim's forest for \(d\) and \(r\) is a spanning tree of \(\{0, \dots, n-1\}\): \(r\) followed by the vertices of the forest in preorder lists every vertex exactly once.

theorem isSpanning_primForest {W : Type*} [LinearOrder W] [Zero W] [Add W]
    [Std.Commutative (α := W) (· + ·)] (d : Fin n → Fin n → W) (root : Fin n) :
    IsSpanning (List.finRange n) root (primForest d root)
Uses 5 · Used by 1
Statement usesRooted spanning tree of a vertex list · Forest of Prim's tree
Proof usesThe forest of a parent tree spans all vertices · Prim's parent array is a parent tree · Prim's parent array on the complete graph
Used byThe tour from Prim's tree is a tour

TheoremThe tour from Prim's tree is a tour#✓fully proved

For costs \(d(u,v)\) on the vertices \(\{0, \dots, n-1\}\) with values in a linearly ordered type with a zero and commutative addition, and any root \(r\), the list returned by APPROX-TSP-TOUR with Prim's tree for \(d\) and \(r\) is a permutation of \(0, 1, \dots, n-1\): it visits every vertex exactly once.

theorem primTSPTour_isTour {W : Type*} [LinearOrder W] [Zero W] [Add W]
    [Std.Commutative (α := W) (· + ·)] (d : Fin n → Fin n → W) (root : Fin n) :
    IsTour (List.finRange n) (primTSPTour d root).ret
Uses 5
Statement usesTour of a vertex list · APPROX-TSP-TOUR with Prim's tree
Proof usesThe approximate TSP tour is a tour · Prim's forest spans all vertices · Forest of Prim's tree

TheoremEdge sums over a parent tree#✓fully proved

Let \(p\) be a parent array on the vertices \(\{0, \dots, n-1\}\) in which the root \(r\) has no parent and every chain of parents reaches \(r\), and let \(w\) assign to each unordered pair \(\{u, v\}\) of vertices (possibly \(u = v\)) a value in a commutative additive monoid. Write \(\hat p(u)\) for the parent of \(u\), or \(u\) itself if \(u\) has no parent. Then the sum of \(w(e)\) over the edges \(e\) of the parent graph (distinct \(u\) and \(v\) are adjacent when one is the parent of the other) equals the sum of \(w(\{\hat p(u), u\})\) over the vertices \(u\) of the forest built from \(p\) below \(r\), \(n\) levels deep, listed in preorder.

theorem sum_edgeFinset_eq {M : Type*} [AddCommMonoid M] (ht : ParentTree par root)
    (w : Sym2 (Fin n) → M) :
    ∑ e ∈ (SimpleGraph.fromRel fun u v => par v = some u).edgeFinset, w e =
      ((buildForest par n root).preorder.map fun u => w s(up par u, u)).sum
Uses 8 · Used by 1
Statement usesPreorder of a forest · Parent tree · Forest of a parent array below a vertex · One step up a parent array
Proof usesDescendant within \(k\) levels · Rooted forest in left-child right-sibling form · Children in a parent array · Every non-root vertex lies below the root
Used byAPPROX-TSP-TOUR with Prim's tree is a 2-approximation

TheoremAPPROX-TSP-TOUR with Prim's tree is a 2-approximation#✓fully proved

Let \(d\) be a real metric cost on the vertices \(\{0, \dots, n-1\}\) (symmetric, zero on the diagonal, nonnegative, and satisfying the triangle inequality), and let \(r\) be a vertex. Then the cost of the closed tour through the list returned by APPROX-TSP-TOUR with Prim's tree for \(d\) and \(r\) is at most twice the cost of the closed tour through \(H\), for every list \(H\) that visits each of \(0, 1, \dots, n-1\) exactly once.

This is CLRS Theorem 35.2, with the minimum spanning tree computed by Prim.

theorem primTSPTour_two_approx {n : ℕ} {d : Fin n → Fin n → ℝ} (hd : IsMetricCost d)
    (root : Fin n) {H : List (Fin n)} (hH : IsTour (List.finRange n) H) :
    tourCost d (primTSPTour d root).ret ≤ 2 * tourCost d H
Uses 24
Statement usesMetric cost function · Tour of a vertex list · APPROX-TSP-TOUR with Prim's tree · Cost of a closed tour
Proof usesRooted forest in left-child right-sibling form · Preorder of a forest · Weight of a forest below a vertex · Parent tree · The APPROX-TSP-TOUR algorithm · Forest of a parent array below a vertex · Prim's parent array is a parent tree · Cost of a walk · Preorder walk · Preorder walk with an accumulator · Result of the preorder walk with an accumulator · Forest of Prim's tree · Prim's parent array on the complete graph · Prim's tree · Prim's tree is a minimum spanning tree · Edge sums over a parent tree · Symmetrized edge weights · The preorder tour costs at most twice the tree · One step up a parent array · Weight of the forest built from a parent array
46 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.