Kruskal's algorithm

StructureRaw input edge#✓fully proved

A raw edge is an undirected weighted input edge given by three natural numbers: two endpoints, which are not yet checked to be vertices of the graph, and a weight.

public structure RawEdge where
  /-- First endpoint. -/
  source : Nat
  /-- Second endpoint. -/
  target : Nat
  /-- Nonnegative edge weight. -/
  weight : Nat
deriving DecidableEq, Repr

Used by 4

Used byDecoding a raw edge at an ordinal · Kruskal input graph · Valid edges of an input graph · Validating an edge list from a given ordinal

StructureKruskal input graph#✓fully proved

For a natural number \(n\), an input graph on the vertices \(\{0, \dots, n-1\}\) consists of a list of raw edges, kept in input order; the same pair of endpoints may occur on several edges.

The endpoints of a raw edge are natural numbers and are not required to be below \(n\).

public structure Graph (n : Nat) where
  /-- Input edges in deterministic order. -/
  rawEdges : List RawEdge
deriving DecidableEq, Repr

Uses 1 · Used by 16

Statement usesRaw input edge

Used byGreedy cut property of Kruskal's scan · Ordered spanning forest · Spanning forest of an input graph · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's output is a sorted spanning forest · Kruskal's output is a spanning forest · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Valid edges in Kruskal order · Edge lists spanning a graph · Valid edges of an input graph

StructureWeighted edge#✓fully proved

A weighted edge on the vertices \(\{0, \dots, n-1\}\) consists of an ordinal, a natural number recording its zero-based position in the original input list, two endpoints in \(\{0, \dots, n-1\}\), and a natural-number weight.

public structure WeightedEdge (n : Nat) where
  /-- Zero-based position in the original input list. -/
  ordinal : Nat
  /-- Validated first endpoint. -/
  source : Fin n
  /-- Validated second endpoint. -/
  target : Fin n
  /-- Nonnegative edge weight. -/
  weight : Nat
deriving DecidableEq, Repr

Used by 28

Used byAcyclic edge list · Acyclicity of a newest-first edge list · Connectivity by an edge list · Connectivity by a newest-first edge list · Decoding a raw edge at an ordinal · Greedy cut property of Kruskal's scan · Ordered spanning forest · Spanning forest of an input graph · Sorting key of a weighted edge · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's output is a sorted spanning forest · Kruskal's output is a spanning forest · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Edge lists spanning a graph · Kruskal scan state · One Kruskal step · Total weight of a Kruskal edge list · Valid edges of an input graph · Validating an edge list from a given ordinal

DefinitionSorting key of a weighted edge#✓fully proved

The sorting key of a weighted edge \(e\) is the pair \((w(e), i(e)) \in \mathbb{N} \times \mathbb{N}\) of its weight \(w(e)\) and its input ordinal \(i(e)\), the zero-based position of \(e\) in the original input edge list.

Keys are compared lexicographically.

public def WeightedEdge.key {n : Nat} (edge : WeightedEdge n) : Nat × Nat :=
  (edge.weight, edge.ordinal)

Uses 1 · Used by 10

Statement usesWeighted edge

Used byGreedy cut property of Kruskal's scan · Ordered spanning forest · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's output is a sorted spanning forest · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Sorting edges by weight and input position

DefinitionLexicographic order on edge keys#✓fully proved

For pairs of natural numbers \((w, i)\) and \((w', i')\), \((w, i) \preceq (w', i')\) holds when \(w < w'\), or \(w = w'\) and \(i \le i'\). This is the non-strict lexicographic order on \(\mathbb{N} \times \mathbb{N}\); Kruskal's algorithm applies it to keys (weight, input ordinal).

public def KeyLE (left right : Nat × Nat) : Prop :=
  left.1 < right.1 ∨ (left.1 = right.1 ∧ left.2 ≤ right.2)

Used by 10

Used byGreedy cut property of Kruskal's scan · Ordered spanning forest · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's output is a sorted spanning forest · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Sorting edges by weight and input position

DefinitionDecoding a raw edge at an ordinal#✓fully proved

Given natural numbers \(n\) and \(i\) and a raw edge with source \(s\), target \(t\) and weight \(w\), decoding at ordinal \(i\) returns the validated edge on the vertices \(\{0, \dots, n-1\}\) with ordinal \(i\), source \(s\), target \(t\) and weight \(w\) when \(s < n\) and \(t < n\), and returns no edge otherwise.

public def decodeAt (n ordinal : Nat) (edge : RawEdge) : Option (WeightedEdge n) :=
  if hs : edge.source < n then
    if ht : edge.target < n then
      some {
        ordinal := ordinal
        source := ⟨edge.source, hs⟩
        target := ⟨edge.target, ht⟩
        weight := edge.weight
      }
    else none
  else none

Uses 2 · Used by 1

Statement usesRaw input edge · Weighted edge

Used byValidating an edge list from a given ordinal

DefinitionValidating an edge list from a given ordinal#✓fully proved

Given \(n\), a starting ordinal \(o\) and a list of raw edges \(e_0, e_1, \dots, e_{m-1}\), this returns, in input order, the weighted edges on the vertices \(\{0, \dots, n-1\}\) obtained from those \(e_k\) whose two endpoints are both less than \(n\); each keeps the endpoints and weight of \(e_k\) and carries the ordinal \(o + k\). Edges with an endpoint at least \(n\) are omitted, but they still count towards the ordinals of later edges.

public def validEdgesFrom (n ordinal : Nat) : List RawEdge → List (WeightedEdge n)
  | [] => []
  | edge :: rest =>
      match decodeAt n ordinal edge with
      | none => validEdgesFrom n (ordinal + 1) rest
      | some decoded => decoded :: validEdgesFrom n (ordinal + 1) rest

Uses 3 · Used by 1

Statement usesRaw input edge · Weighted edge · Decoding a raw edge at an ordinal

Used byValid edges of an input graph

DefinitionValid edges of an input graph#✓fully proved

For a graph \(G\) on the vertices \(\{0, \dots, n-1\}\) given by its list of raw edges \(e_0, e_1, \dots, e_{m-1}\), the valid edges of \(G\) are, in input order, the weighted edges obtained from those \(e_k\) whose two endpoints are both less than \(n\); each keeps the endpoints and weight of \(e_k\) and carries its zero-based input ordinal \(k\). Edges with an endpoint at least \(n\) are omitted.

public def validEdges {n : Nat} (graph : Graph n) : List (WeightedEdge n) :=
  validEdgesFrom n 0 graph.rawEdges

Uses 4 · Used by 11

Statement usesKruskal input graph · Raw input edge · Weighted edge · Validating an edge list from a given ordinal

Used byGreedy cut property of Kruskal's scan · Spanning forest of an input graph · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's output is a spanning forest · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Valid edges in Kruskal order · Edge lists spanning a graph

DefinitionSorting edges by weight and input position#✓fully proved

Sorting a list of validated edges is merge sort with the comparison \((w, i) \preceq (w', i')\) if \(w < w'\), or \(w = w'\) and \(i \le i'\), applied to the pairs (weight, input position) of the edges.

public def sortEdges {n : Nat} (edges : List (WeightedEdge n)) : List (WeightedEdge n) :=
  List.mergeSort edges (fun left right => decide (KeyLE left.key right.key))

Uses 3 · Used by 6

Statement usesLexicographic order on edge keys · Weighted edge · Sorting key of a weighted edge

Used byKruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Valid edges in Kruskal order

DefinitionValid edges in Kruskal order#✓fully proved

For a finite weighted multigraph \(G\) on the vertices \(\{0, \dots, n-1\}\), the ordered edges of \(G\) are its valid input edges (those whose endpoints are both less than \(n\)), sorted by merge sort in lexicographic order of (weight, input position): by nondecreasing weight, with edges of equal weight in input order.

public def orderedEdges {n : Nat} (graph : Graph n) : List (WeightedEdge n) :=
  sortEdges (validEdges graph)

Uses 4 · Used by 9

Statement usesKruskal input graph · Weighted edge · Sorting edges by weight and input position · Valid edges of an input graph

Used byGreedy cut property of Kruskal's scan · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph

DefinitionDiscrete parent forest#✓fully proved

The initial forest on the vertices \(\{0, \dots, n-1\}\) is the parent forest in which every vertex is its own parent, so every vertex is a root, and whose depth certificate is \(0\) at every vertex.

public def initialForest (n : Nat) : Forest n where
  parent vertex := vertex
  depth _ := 0
  parent_lt _ h := False.elim (h rfl)

Uses 1 · Used by 9

Statement usesParent forest with a depth certificate

Used byGreedy cut property of Kruskal's scan · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph

DefinitionConnectivity by a newest-first edge list#✓fully proved

Connectivity of vertices \(u\) and \(v\) of \(\{0, \dots, n-1\}\) by a list of validated edges, read newest first, is defined by recursion on the list. By the empty list, \(u\) and \(v\) are connected exactly when \(u = v\). By a list whose first edge \(e\) has source \(a\) and target \(b\) and whose remaining edges form the list \(L\), the vertices \(u\) and \(v\) are connected when \(u\) and \(v\) are connected by \(L\), or \(u\) is connected to \(a\) and \(v\) is connected to \(b\) by \(L\), or \(u\) is connected to \(b\) and \(v\) is connected to \(a\) by \(L\).

public def ConnectedRev {n : Nat} : List (WeightedEdge n) → Fin n → Fin n → Prop
  | [], left, right => left = right
  | edge :: edges, left, right =>
      ConnectedRev edges left right ∨
        (ConnectedRev edges left edge.source ∧
          ConnectedRev edges right edge.target) ∨
        (ConnectedRev edges left edge.target ∧
          ConnectedRev edges right edge.source)

Uses 1 · Used by 6

Statement usesWeighted edge

Used byAcyclicity of a newest-first edge list · Connectivity by an edge list · Kruskal's output is acyclic · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's selected edges span the graph

DefinitionConnectivity by an edge list#✓fully proved

Vertices \(u\) and \(v\) of \(\{0, \dots, n-1\}\) are connected by a list \(e_1, \dots, e_k\) of validated edges when they are connected by the reversed list \(e_k, \dots, e_1\) in the sense of connectivity by a newest-first edge list.

public def Connected {n : Nat} (edges : List (WeightedEdge n))
    (left right : Fin n) : Prop :=
  ConnectedRev edges.reverse left right

Uses 2 · Used by 3

Statement usesConnectivity by a newest-first edge list · Weighted edge

Used byKruskal's algorithm gives a minimum spanning forest · Kruskal's selected edges span the graph · Edge lists spanning a graph

DefinitionAcyclicity of a newest-first edge list#✓fully proved

A list \(e_1, \dots, e_k\) of validated edges on the vertices \(\{0, \dots, n-1\}\), read newest first, is newest-first acyclic when, for every \(i\), the endpoints of \(e_i\) are not connected by the later list \(e_{i+1}, \dots, e_k\) in the sense of connectivity by a newest-first edge list.

public def AcyclicRev {n : Nat} : List (WeightedEdge n) → Prop
  | [] => True
  | edge :: edges =>
      ¬ConnectedRev edges edge.source edge.target ∧ AcyclicRev edges

Uses 2 · Used by 3

Statement usesConnectivity by a newest-first edge list · Weighted edge

Used byAcyclic edge list · Kruskal's output is acyclic · Kruskal's algorithm gives a minimum spanning forest

DefinitionAcyclic edge list#✓fully proved

A list \(e_1, \dots, e_k\) of validated edges on the vertices \(\{0, \dots, n-1\}\) is acyclic when, for every \(i\), the endpoints of \(e_i\) are not connected by the preceding edges \(e_1, \dots, e_{i-1}\), in the sense of connectivity by an edge list.

public def Acyclic {n : Nat} (edges : List (WeightedEdge n)) : Prop :=
  AcyclicRev edges.reverse

Uses 2 · Used by 4

Statement usesAcyclicity of a newest-first edge list · Weighted edge

Used bySpanning forest of an input graph · Kruskal's output is acyclic · Kruskal's output is a spanning forest · Kruskal's algorithm gives a minimum spanning forest

DefinitionEdge lists spanning a graph#✓fully proved

A list \(L\) of validated edges spans a finite weighted multigraph \(G\) on the vertices \(\{0, \dots, n-1\}\) when, for every valid input edge of \(G\) (one whose endpoints are both less than \(n\)), the two endpoints of that edge are connected using the edges of \(L\).

public def Spans {n : Nat} (graph : Graph n) (edges : List (WeightedEdge n)) : Prop :=
  ∀ edge ∈ validEdges graph, Connected edges edge.source edge.target

Uses 4 · Used by 4

Statement usesConnectivity by an edge list · Kruskal input graph · Weighted edge · Valid edges of an input graph

Used bySpanning forest of an input graph · Kruskal's output is a spanning forest · Kruskal's algorithm gives a minimum spanning forest · Kruskal's selected edges span the graph

DefinitionSpanning forest of an input graph#✓fully proved

For an input graph \(G\) on the vertices \(\{0, \dots, n-1\}\), a list \(F\) of validated edges is a spanning forest of \(G\) when every edge of \(F\) is a valid edge of \(G\), \(F\) is acyclic, and \(F\) spans \(G\): for every valid edge of \(G\), its endpoints are connected by \(F\).

public def IsSpanningForest {n : Nat} (graph : Graph n)
    (edges : List (WeightedEdge n)) : Prop :=
  (∀ edge ∈ edges, edge ∈ validEdges graph) ∧ Acyclic edges ∧ Spans graph edges

Uses 5 · Used by 4

Statement usesAcyclic edge list · Kruskal input graph · Edge lists spanning a graph · Weighted edge · Valid edges of an input graph

Used byOrdered spanning forest · Kruskal's output is a sorted spanning forest · Kruskal's output is a spanning forest · Kruskal's algorithm gives a minimum spanning forest

DefinitionOrdered spanning forest#✓fully proved

For an input graph \(G\) on the vertices \(\{0, \dots, n-1\}\), a list \(e_1, \dots, e_k\) of validated edges is an ordered spanning forest of \(G\) when it is a spanning forest of \(G\) and its keys are nondecreasing: for all \(i < j\), the key of \(e_i\) is at most the key of \(e_j\), where the key of an edge with weight \(w\) and input ordinal \(o\) is the pair \((w, o)\) and keys are compared lexicographically.

public def IsOrderedSpanningForest {n : Nat} (graph : Graph n)
    (edges : List (WeightedEdge n)) : Prop :=
  IsSpanningForest graph edges ∧
    edges.Pairwise fun left right => KeyLE left.key right.key

Uses 5 · Used by 1

Statement usesKruskal input graph · Spanning forest of an input graph · Lexicographic order on edge keys · Weighted edge · Sorting key of a weighted edge

Used byKruskal's output is a sorted spanning forest

DefinitionTotal weight of a Kruskal edge list#✓fully proved

The total weight of a list of validated edges is the sum of the weights of its entries, each entry counted once, so parallel edges and repeated entries each contribute their weight.

public def totalWeight {n : Nat} (edges : List (WeightedEdge n)) : Nat :=
  (edges.map WeightedEdge.weight).sum

Uses 1 · Used by 1

Statement usesWeighted edge

Used byKruskal's algorithm gives a minimum spanning forest

StructureKruskal scan state#✓fully proved

A state of the Kruskal scan on the vertices \(\{0, \dots, n-1\}\) consists of a union-find parent forest on these vertices, which records the current partition, and the list of edges accepted so far, newest first.

public structure State (n : Nat) where
  /-- Current endpoint partition. -/
  forest : Forest n
  /-- Accepted edges, newest first. -/
  chosenRev : List (WeightedEdge n)

Uses 2 · Used by 11

Statement usesWeighted edge · Parent forest with a depth certificate

Used byGreedy cut property of Kruskal's scan · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Scanning a list of edges · One Kruskal step

DefinitionOne Kruskal step#✓fully proved

Let \(s\) be a Kruskal scan state and \(e\) a validated edge with endpoints \(u\) and \(v\). If \(u\) and \(v\) are equivalent in the union-find forest of \(s\), processing \(e\) leaves \(s\) unchanged. Otherwise \(e\) is accepted: the new forest is the union of \(u\) and \(v\) in the forest of \(s\), and \(e\) is put at the front of the list of accepted edges.

public def State.step {n : Nat} (state : State n) (edge : WeightedEdge n) : State n :=
  if Equivalent state.forest edge.source edge.target then state
  else {
    forest := union state.forest edge.source edge.target
    chosenRev := edge :: state.chosenRev
  }

Uses 6 · Used by 7

Statement usesKruskal scan state · Weighted edge · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Union in a union-find forest

Used byKruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph · Scanning a list of edges

DefinitionScanning a list of edges#✓fully proved

Starting from a Kruskal scan state \(s\), scanning a list of validated edges \(e_1, \dots, e_k\) applies one Kruskal step to each edge in list order: the scan of the empty list returns \(s\), and the scan of \(e_1, \dots, e_k\) is the scan of \(e_2, \dots, e_k\) from the state obtained by processing \(e_1\) in \(s\).

public def scan {n : Nat} : State n → List (WeightedEdge n) → State n
  | state, [] => state
  | state, edge :: rest => scan (state.step edge) rest

Uses 3 · Used by 9

Statement usesKruskal scan state · One Kruskal step · Weighted edge

Used byGreedy cut property of Kruskal's scan · Kruskal's algorithm · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's greedy cut property · Kruskal accepts light edges · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph

DefinitionGreedy cut property of Kruskal's scan#✓fully proved

Let \(G\) be an input graph on the vertices \(\{0, \dots, n-1\}\), give each valid edge with weight \(w\) and input ordinal \(o\) the key \((w, o)\), and compare keys lexicographically. The graph \(G\) has the greedy cut property when the following holds for every way of splitting the valid edges of \(G\), sorted by key, into an initial segment, an edge \(e\) and a final segment. Let \(P\) be the union-find partition obtained by scanning the initial segment from the discrete parent forest with no accepted edges. If the endpoints of \(e\) lie in different classes of \(P\), then the key of \(e\) is at most the key of every valid edge of \(G\) whose endpoints lie in different classes of \(P\).

public def HasGreedyCutProperty {n : Nat} (graph : Graph n) : Prop :=
  ∀ before edge after,
    orderedEdges graph = before ++ edge :: after →
    ¬Equivalent (scan ⟨initialForest n, []⟩ before).forest edge.source edge.target →
    ∀ candidate ∈ validEdges graph,
      ¬Equivalent (scan ⟨initialForest n, []⟩ before).forest
        candidate.source candidate.target →
      KeyLE edge.key candidate.key

Uses 11 · Used by 1

Statement usesKruskal input graph · Lexicographic order on edge keys · Kruskal scan state · Weighted edge · Sorting key of a weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate

Used byKruskal's greedy cut property

DefinitionKruskal's algorithm#✓fully proved

For a finite weighted multigraph \(G\) on the vertices \(\{0, \dots, n-1\}\), Kruskal's algorithm starts from the partition of the vertices into singletons and processes the valid input edges of \(G\) (those whose endpoints are both less than \(n\)) in lexicographic order of (weight, input position). An edge whose endpoints lie in different classes of the current partition is accepted and its two classes are merged; an edge whose endpoints lie in the same class is skipped. The result is the list of accepted edges in the order in which they were processed.

public def kruskal {n : Nat} (graph : Graph n) : List (WeightedEdge n) :=
  (scan ⟨initialForest n, []⟩ (orderedEdges graph)).chosenRev.reverse

Uses 7 · Used by 7

Statement usesKruskal input graph · Kruskal scan state · Weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Parent forest with a depth certificate

Used byKruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's output is a sorted spanning forest · Kruskal's output is a spanning forest · Kruskal's algorithm gives a minimum spanning forest · Kruskal's output is sorted by key · Kruskal's selected edges span the graph

TheoremKruskal selects only valid input edges#✓fully proved

For every graph \(G\) on \(n\) vertices, every edge in the list returned by Kruskal's algorithm on \(G\) is a valid edge of \(G\): an input edge whose two endpoints are both below \(n\), carrying its input ordinal.

public theorem kruskal_edge_mem_valid {n : Nat} (graph : Graph n)
    {edge : WeightedEdge n} (selected : edge ∈ kruskal graph) :
    edge ∈ validEdges graph

Uses 16 · Used by 1

Statement usesKruskal input graph · Weighted edge · Kruskal's algorithm · Valid edges of an input graph

Proof usesLexicographic order on edge keys · Kruskal scan state · One Kruskal step · Sorting key of a weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Union in a union-find forest

Used byKruskal's output is a spanning forest

TheoremKruskal's output is acyclic#✓fully proved

For every graph \(G\), the edge list returned by Kruskal's algorithm on \(G\) is acyclic: each edge in it joins two vertices that are not connected by the edges before it in the list.

public theorem kruskal_acyclic {n : Nat} (graph : Graph n) :
    Acyclic (kruskal graph)

Uses 16 · Used by 1

Statement usesAcyclic edge list · Kruskal input graph · Kruskal's algorithm

Proof usesAcyclicity of a newest-first edge list · Connectivity by a newest-first edge list · Kruskal scan state · One Kruskal step · Weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Equivalence after a union · Root of a vertex in a parent forest · Union in a union-find forest

Used byKruskal's output is a spanning forest

TheoremKruskal's selected edges span the graph#✓fully proved

For every finite weighted multigraph \(G\) on the vertices \(\{0, \dots, n-1\}\), given by its list of input edges, and every valid input edge of \(G\) (one whose endpoints are both less than \(n\)), the two endpoints of that edge are connected by the edges that Kruskal's algorithm selects on \(G\).

The graph \(G\) need not be connected.

public theorem kruskal_spans {n : Nat} (graph : Graph n) :
    Spans graph (kruskal graph)

Uses 21 · Used by 1

Statement usesKruskal input graph · Edge lists spanning a graph · Kruskal's algorithm

Proof usesConnectivity by an edge list · Connectivity by a newest-first edge list · Lexicographic order on edge keys · Kruskal scan state · One Kruskal step · Weighted edge · Sorting key of a weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Equivalence after a union · Root of a vertex in a parent forest · Union in a union-find forest · Union makes its arguments equivalent

Used byKruskal's output is a spanning forest

TheoremKruskal's output is sorted by key#✓fully proved

For every graph \(G\), if an edge \(e\) comes before an edge \(f\) in the list returned by Kruskal's algorithm on \(G\), then \(e\) has smaller weight than \(f\), or the same weight as \(f\) and input ordinal at most that of \(f\).

public theorem kruskal_pairwise_key_le {n : Nat} (graph : Graph n) :
    (kruskal graph).Pairwise fun left right => KeyLE left.key right.key

Uses 16 · Used by 1

Statement usesKruskal input graph · Lexicographic order on edge keys · Weighted edge · Sorting key of a weighted edge · Kruskal's algorithm

Proof usesKruskal scan state · One Kruskal step · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Root of a vertex in a parent forest · Union in a union-find forest

Used byKruskal's output is a sorted spanning forest

TheoremKruskal's greedy cut property#✓fully proved

Let \(G\) be a graph and let \(e_1, \dots, e_m\) be its valid edges sorted lexicographically by key (weight, then input ordinal). For a position \(k\), let \(P_k\) be the partition of the vertices given by the union-find forest after Kruskal's scan, started from the discrete forest, has processed \(e_1, \dots, e_{k-1}\). If the endpoints of \(e_k\) lie in different classes of \(P_k\), then for every valid edge \(c\) of \(G\) whose endpoints lie in different classes of \(P_k\), the key of \(e_k\) is lexicographically at most the key of \(c\): either \(e_k\) has smaller weight than \(c\), or the same weight and input ordinal at most that of \(c\).

public theorem kruskal_greedy_cut_property {n : Nat} (graph : Graph n) :
    HasGreedyCutProperty graph

Uses 19 · Used by 1

Statement usesKruskal input graph · Greedy cut property of Kruskal's scan

Proof usesConnectivity by a newest-first edge list · Lexicographic order on edge keys · Kruskal scan state · One Kruskal step · Weighted edge · Sorting key of a weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Equivalence after a union · Root of a vertex in a parent forest · Union in a union-find forest · Union makes its arguments equivalent

Used byKruskal accepts light edges

TheoremKruskal accepts light edges#✓fully proved

Let \(G\) be a graph and let \(e_1, \dots, e_m\) be its valid edges sorted lexicographically by key (weight, then input ordinal). For a position \(k\), let \(P_k\) be the partition of the vertices given by the union-find forest after Kruskal's scan, started from the discrete forest, has processed \(e_1, \dots, e_{k-1}\). If the endpoints of \(e_k\) lie in different classes of \(P_k\), then the weight of \(e_k\) is at most the weight of every valid edge of \(G\) whose endpoints lie in different classes of \(P_k\).

public theorem kruskal_light_edge {n : Nat} (graph : Graph n)
    (before : List (WeightedEdge n)) (edge : WeightedEdge n)
    (after : List (WeightedEdge n))
    (decomposition : orderedEdges graph = before ++ edge :: after)
    (separated :
      ¬Equivalent (scan ⟨initialForest n, []⟩ before).forest edge.source edge.target)
    (candidate : WeightedEdge n) (inValid : candidate ∈ validEdges graph)
    (crossing :
      ¬Equivalent (scan ⟨initialForest n, []⟩ before).forest
        candidate.source candidate.target) :
    edge.weight ≤ candidate.weight

Uses 12 · Used by 1

Statement usesKruskal input graph · Kruskal scan state · Weighted edge · Discrete parent forest · Valid edges in Kruskal order · Scanning a list of edges · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate

Proof usesLexicographic order on edge keys · Sorting key of a weighted edge · Kruskal's greedy cut property

Used byKruskal's algorithm gives a minimum spanning forest

TheoremKruskal's output is a spanning forest#✓fully proved

For every graph \(G\), the edge list returned by Kruskal's algorithm on \(G\) is a spanning forest of \(G\): every edge in it is a valid edge of \(G\), it is acyclic, and it connects the two endpoints of every valid edge of \(G\).

public theorem kruskal_isSpanningForest {n : Nat} (graph : Graph n) :
    IsSpanningForest graph (kruskal graph)

Uses 10 · Used by 2

Statement usesKruskal input graph · Spanning forest of an input graph · Kruskal's algorithm

Proof usesAcyclic edge list · Edge lists spanning a graph · Weighted edge · Kruskal's output is acyclic · Kruskal selects only valid input edges · Kruskal's selected edges span the graph · Valid edges of an input graph

Used byKruskal's output is a sorted spanning forest · Kruskal's algorithm gives a minimum spanning forest

TheoremKruskal's output is a sorted spanning forest#✓fully proved

For every graph \(G\), the edge list returned by Kruskal's algorithm on \(G\) is a spanning forest of \(G\) (its edges are valid edges of \(G\), it is acyclic, and it connects the endpoints of every valid edge of \(G\)), and whenever an edge \(e\) comes before an edge \(f\) in it, the key (weight, input ordinal) of \(e\) is lexicographically at most that of \(f\).

public theorem kruskal_isOrderedSpanningForest {n : Nat} (graph : Graph n) :
    IsOrderedSpanningForest graph (kruskal graph)

Uses 9

Statement usesKruskal input graph · Ordered spanning forest · Kruskal's algorithm

Proof usesSpanning forest of an input graph · Lexicographic order on edge keys · Weighted edge · Sorting key of a weighted edge · Kruskal's output is a spanning forest · Kruskal's output is sorted by key

TheoremKruskal's algorithm gives a minimum spanning forest#✓fully proved

Let \(G\) be a graph with natural-number edge weights, and let \(F\) be any spanning forest of \(G\): a list of valid edges of \(G\) that is acyclic and connects the endpoints of every valid edge of \(G\). Then the total weight of the edge list returned by Kruskal's algorithm on \(G\) is at most the total weight of \(F\).

Total weights count parallel edge occurrences separately, and \(G\) need not be connected.

public theorem kruskal_minimal {n : Nat} (graph : Graph n)
    (edges : List (WeightedEdge n)) (forest : IsSpanningForest graph edges) :
    totalWeight (kruskal graph) ≤ totalWeight edges

Sources

• CLRS, fourth edition, §21.2, cut-exchange argument.

Uses 26

Statement usesKruskal input graph · Spanning forest of an input graph · Weighted edge · Kruskal's algorithm · Total weight of a Kruskal edge list

Proof usesAcyclic edge list · Acyclicity of a newest-first edge list · Connectivity by an edge list · Connectivity by a newest-first edge list · Lexicographic order on edge keys · Edge lists spanning a graph · Kruskal scan state · One Kruskal step · Sorting key of a weighted edge · Discrete parent forest · Kruskal's output is a spanning forest · Kruskal accepts light edges · Valid edges in Kruskal order · Scanning a list of edges · Sorting edges by weight and input position · Valid edges of an input graph · Equivalent vertices of a parent forest · Parent forest with a depth certificate · Equivalence after a union · Root of a vertex in a parent forest · Union in a union-find forest

33 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.