97 Graph Theory — Basic
97.1 Overview
This module formalises the core data structures and the greedy selection loop underlying Kruskal’s minimum-spanning-tree algorithm. It defines weighted edges over \(n\) vertices, a union-find structure represented as a flat array of representatives, the edge-processing sweep that builds the spanning tree, and the top-level kruskal function. The two main correctness results show that every edge returned by the algorithm was present in the original input list.
97.2 Declarations
A weighted edge over \(n\) vertices is a structure with two endpoints \(u, v : \mathrm{Fin}\, n\) and a natural-number weight \(w : \mathbb {N}\).
The union-find state for \(n\) nodes is defined as a function \(\mathrm{Fin}\, n \to \mathbb {N}\) mapping each node to its current representative (component label).
\(\mathtt{init}\, n\) constructs the identity union-find on \(n\) nodes: every node \(i\) is its own representative, i.e. \(\mathtt{init}\, n\, (i) = i\).
\(\mathtt{find}\, \mathit{uf}\, i\) returns the representative of node \(i\) in the union-find state \(\mathit{uf}\), defined simply as \(\mathit{uf}(i)\).
\(\mathtt{merge}\, \mathit{uf}\, i\, j\) unifies the components of nodes \(i\) and \(j\) by reassigning every node whose representative equals \(\mathit{uf}(j)\) to instead carry the representative \(\mathit{uf}(i)\).
For every \(i : \mathrm{Fin}\, n\), the find operation on the initial union-find returns \(i\)’s numeric value: \((\mathtt{init}\, n).\mathtt{find}\, i = i.\mathtt{val}\).
For any union-find state \(\mathit{uf}\) and index \(i\), \(\mathit{uf}.\mathtt{find}\, i = \mathit{uf}(i)\); this is the unfolding simp-lemma for find.
\(\mathtt{mergeAll}\, \mathit{uf}\, \mathit{es}\) folds a list of weighted edges \(\mathit{es}\) into the union-find \(\mathit{uf}\) by calling merge on each edge’s endpoints in sequence.
\(\mathtt{SamePartition}\, \mathit{uf}_1\, \mathit{uf}_2\) holds when two union-find states induce the same equivalence relation on nodes: for all \(i, j : \mathrm{Fin}\, n\), \(\mathit{uf}_1(i) = \mathit{uf}_1(j)\) if and only if \(\mathit{uf}_2(i) = \mathit{uf}_2(j)\).
\(\mathtt{processEdges}\, \mathit{es}\, \mathit{uf}\, \mathit{acc}\) scans the edge list \(\mathit{es}\) left-to-right: an edge \(e\) is added to the accumulator and its endpoints are merged whenever \(\mathit{uf}.\mathtt{find}\, e.u \ne \mathit{uf}.\mathtt{find}\, e.v\); otherwise \(e\) is skipped. The reversed accumulator is returned when the list is exhausted.
\(\mathtt{kruskal}\, n\, \mathit{edges}\) sorts the edge list by weight and then runs processEdges on the sorted list starting from the identity union-find, returning the selected spanning-tree edges.
Let \(\mathit{es}\) be a list of weighted edges, \(\mathit{uf}\) a union-find state, \(\mathit{acc}\) an accumulator list, and \(e\) an edge. If \(e \in \mathtt{processEdges}\, \mathit{es}\, \mathit{uf}\, \mathit{acc}\), then \(e \in \mathit{acc}\) or \(e \in \mathit{es}\).
Every edge \(e\) returned by \(\mathtt{kruskal}\, n\, \mathit{edges}\) was already present in \(\mathit{edges}\): if \(e \in \mathtt{kruskal}\, n\, \mathit{edges}\) then \(e \in \mathit{edges}\).