Chapter 21 — Minimum Spanning Trees
CLRS, fourth edition · Lean 4 formalization
The proofs below use the models and assumptions described in the scope and implementation notes.
Imports
import Mathlibopen Finset21.1. Growing a Minimum Spanning Tree
This section proves the exchange kernel behind the standard minimum-spanning-tree cut property:
-
replacing a heavier tree edge by a no-heavier edge preserves optimality;
-
a light edge crossing a cut is safe, provided the usual tree-exchange certificate is available.
The graph-specific fact that a spanning tree plus a crossing edge contains a replaceable crossing edge is kept as an explicit certificate. This keeps the first MST module focused on the reusable proof pattern rather than on a particular graph representation or union-find implementation.
Main results:
-
Theorem
FiniteGraph.spanning_tree_maximal: a finite spanning tree is maximal among spanning trees under edge-set inclusion. -
Theorems
FiniteGraph.minimumSpanningTree_of_mstExtending_emptyandFiniteGraph.minimumSpanningTree_iff_mstExtending_empty: the abstract empty-prefix optimum specification is equivalent to the concrete finite-graph minimum-spanning-tree specification. -
Theorem
FiniteGraph.exists_crossing_tree_edge_preserving_prefix: a spanning tree path across a respecting cut supplies a replaceable crossing tree edge outside the accepted prefix. -
Theorem
safe_edge_of_lightest_crossing: the CLRS cut property in safe-edge form.
namespace CLRSnamespace MSTvariable {V E : Type} [DecidableEq V] [DecidableEq E]A finite edge-weight sum.
def weight (w : E → Nat) (s : Finset E) : Nat :=
s.sum wThe small amount of graph structure needed to state cuts.
structure Graph (V E : Type) where
src : E → V
dst : E → Vnamespace GraphAn edge crosses a cut when its endpoints are on opposite sides.
def Crosses (G : Graph V E) (S : Finset V) (e : E) : Prop :=
(G.src e ∈ S ∧ G.dst e ∉ S) ∨ (G.dst e ∈ S ∧ G.src e ∉ S)A cut respects a partial solution when no selected edge crosses it.
The undirected adjacency relation induced by a selected edge set.
def AdjIn (G : Graph V E) (A : Finset E) (u v : V) : Prop :=
∃ e ∈ A, (G.src e = u ∧ G.dst e = v) ∨ (G.src e = v ∧ G.dst e = u)Connectivity using only edges from a selected edge set.
def ConnectedIn (G : Graph V E) (A : Finset E) (u v : V) : Prop :=
Relation.ReflTransGen (G.AdjIn A) u vomit [DecidableEq V] [DecidableEq E] in
theorem connected_refl (G : Graph V E) (A : Finset E) (v : V) :
G.ConnectedIn A v v :=
Relation.ReflTransGen.reflomit [DecidableEq V] [DecidableEq E] in
theorem adjIn_mono {G : Graph V E} {A B : Finset E} (hAB : A ⊆ B)
{u v : V} (h : G.AdjIn A u v) : G.AdjIn B u v := by
rcases h with ⟨e, heA, hend⟩
exact ⟨e, hAB heA, hend⟩omit [DecidableEq V] [DecidableEq E] in
theorem connected_mono {G : Graph V E} {A B : Finset E} (hAB : A ⊆ B)
{u v : V} (h : G.ConnectedIn A u v) : G.ConnectedIn B u v := by
induction h with
| refl =>
exact Relation.ReflTransGen.refl
| tail hpath hadj ih =>
exact Relation.ReflTransGen.tail ih (Graph.adjIn_mono hAB hadj)Any selected-edge connection from one side of a cut to the other uses at least one selected edge crossing that cut. This is the lightweight path/cut API used before introducing a heavier finite walk representation.
omit [DecidableEq E] intheorem connected_crosses_cut {G : Graph V E} {A : Finset E}
{S : Finset V} {u v : V}
(hconn : G.ConnectedIn A u v) (hu : u ∈ S) (hv : v ∉ S) :
∃ e, e ∈ A ∧ G.Crosses S e := by
induction hconn with
| refl =>
exact False.elim (hv hu)
| tail hpath hadj ih =>
rcases hadj with ⟨e, heA, hend⟩
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· by_cases hsrcS : G.src e ∈ S
· exact ⟨e, heA, Or.inl ⟨hsrcS, by simpa [hdst] using hv⟩⟩
· exact ih (by simpa [← hsrc] using hsrcS)
· by_cases hdstS : G.dst e ∈ S
· exact ⟨e, heA, Or.inr ⟨hdstS, by simpa [hsrc] using hv⟩⟩
· exact ih (by simpa [← hdst] using hdstS)end GraphConcrete finite graph specification
A concrete finite graph: finite vertex and edge sets plus endpoint maps.
structure FiniteGraph (V E : Type) [DecidableEq V] [DecidableEq E]
extends Graph V E where
vertices : Finset V
edges : Finset E
src_mem : ∀ e ∈ edges, src e ∈ vertices
dst_mem : ∀ e ∈ edges, dst e ∈ verticesnamespace FiniteGraphThe selected edges span the finite vertex set.
def Spans (G : FiniteGraph V E) (A : Finset E) : Prop :=
∀ u ∈ G.vertices, ∀ v ∈ G.vertices, G.toGraph.ConnectedIn A u vA forest is characterized by the standard cycle-test property: removing any selected edge disconnects its endpoints.
def IsForest (G : FiniteGraph V E) (A : Finset E) : Prop :=
∀ e ∈ A, ¬ G.toGraph.ConnectedIn (A.erase e) (G.src e) (G.dst e)A finite-graph spanning tree: selected graph edges, spanning all vertices, and acyclic in the edge-removal sense.
def IsSpanningTree (G : FiniteGraph V E) (A : Finset E) : Prop :=
A ⊆ G.edges ∧ G.Spans A ∧ G.IsForest AA concrete minimum spanning tree for a finite graph and edge-weight map.
def IsMinimumSpanningTree (G : FiniteGraph V E) (w : E → Nat)
(T : Finset E) : Prop :=
G.IsSpanningTree T ∧ ∀ U, G.IsSpanningTree U → weight w T ≤ weight w Uprivate theorem subset_erase_of_subset_of_not_mem {A T : Finset E} {e : E}
(hAT : A ⊆ T) (heA : e ∉ A) : A ⊆ T.erase e := by
intro x hxA
exact Finset.mem_erase.mpr ⟨fun hxe => heA (hxe ▸ hxA), hAT hxA⟩A spanning tree is maximal under edge-set inclusion among spanning trees. This is the concrete graph fact used by the abstract Kruskal theorem.
theorem spanning_tree_maximal (G : FiniteGraph V E) {K T : Finset E}
(hK : G.IsSpanningTree K) (hT : G.IsSpanningTree T) (hKT : K ⊆ T) :
T = K := by
by_contra hne
have h_extra : ∃ e, e ∈ T ∧ e ∉ K := by
by_contra h
have hTK : T ⊆ K := by
intro e heT
by_contra heK
exact h ⟨e, heT, heK⟩
exact hne (Finset.Subset.antisymm hTK hKT)
rcases h_extra with ⟨e, heT, heK⟩
have h_edge : e ∈ G.edges := hT.1 heT
have hsrc : G.src e ∈ G.vertices := G.src_mem e h_edge
have hdst : G.dst e ∈ G.vertices := G.dst_mem e h_edge
have hconnK : G.toGraph.ConnectedIn K (G.src e) (G.dst e) :=
hK.2.1 (G.src e) hsrc (G.dst e) hdst
have hK_erase : K ⊆ T.erase e :=
subset_erase_of_subset_of_not_mem hKT heK
have hconnT : G.toGraph.ConnectedIn (T.erase e) (G.src e) (G.dst e) :=
Graph.connected_mono hK_erase hconnK
exact hT.2.2 e heT hconnTA spanning tree path between the endpoints of an edge crossing a cut contains a tree edge crossing that same cut.
theorem exists_crossing_tree_edge_of_cut (G : FiniteGraph V E)
{T : Finset E} {S : Finset V} {e : E}
(hT : G.IsSpanningTree T) (he : e ∈ G.edges)
(hcross : G.toGraph.Crosses S e) :
∃ f, f ∈ T ∧ G.toGraph.Crosses S f := by
have hsrc : G.src e ∈ G.vertices := G.src_mem e he
have hdst : G.dst e ∈ G.vertices := G.dst_mem e he
rcases hcross with ⟨hsrcS, hdstNot⟩ | ⟨hdstS, hsrcNot⟩
· exact Graph.connected_crosses_cut
(hT.2.1 (G.src e) hsrc (G.dst e) hdst) hsrcS hdstNot
· exact Graph.connected_crosses_cut
(hT.2.1 (G.dst e) hdst (G.src e) hsrc) hdstS hsrcNot
If the cut respects a prefix A, then the crossing tree edge found on the tree
path is outside A. Consequently deleting it while inserting the crossing
edge preserves the prefix edge set.
theorem exists_crossing_tree_edge_preserving_prefix (G : FiniteGraph V E)
{A T : Finset E} {S : Finset V} {e : E}
(hT : G.IsSpanningTree T) (hAT : A ⊆ T)
(hrespects : G.toGraph.Respects S A)
(he : e ∈ G.edges) (hcross : G.toGraph.Crosses S e) :
∃ f, f ∈ T ∧ G.toGraph.Crosses S f ∧
A ⊆ insert e (T.erase f) := by
rcases G.exists_crossing_tree_edge_of_cut hT he hcross with
⟨f, hfT, hfCross⟩
have hf_not_A : f ∉ A := by
intro hfA
exact hrespects f hfA hfCross
refine ⟨f, hfT, hfCross, ?_⟩
intro x hxA
exact Finset.mem_insert_of_mem
(Finset.mem_erase.mpr ⟨fun hxf => hf_not_A (hxf ▸ hxA), hAT hxA⟩)end FiniteGraphA family of feasible spanning trees over the edge type.
structure Problem (E : Type) [DecidableEq E] where
IsSpanningTree : Finset E → Propnamespace FiniteGraphdef toProblem (G : FiniteGraph V E) : Problem E where
IsSpanningTree := G.IsSpanningTreeend FiniteGraph
T is a minimum feasible tree among all trees extending A.
structure IsMSTExtending (P : Problem E) (w : E → Nat)
(A T : Finset E) : Prop where
tree : P.IsSpanningTree T
includes : A ⊆ T
optimal : ∀ U, P.IsSpanningTree U → A ⊆ U → weight w T ≤ weight w Unamespace FiniteGraphThe abstract empty-prefix optimum specification is the concrete finite-graph minimum-spanning-tree specification.
theorem minimumSpanningTree_of_mstExtending_empty (G : FiniteGraph V E)
{w : E → Nat} {T : Finset E}
(h : IsMSTExtending G.toProblem w ∅ T) :
G.IsMinimumSpanningTree w T := by
refine ⟨h.tree, ?_⟩
intro U hUtree
exact h.optimal U hUtree (by simp)Conversely, a concrete finite-graph MST is an abstract optimum extending the empty prefix. This is useful when switching from textbook finite-graph statements back to the reusable Kruskal induction interface.
theorem mstExtending_empty_of_minimumSpanningTree (G : FiniteGraph V E)
{w : E → Nat} {T : Finset E}
(h : G.IsMinimumSpanningTree w T) :
IsMSTExtending G.toProblem w ∅ T := by
refine ⟨h.1, ?_, ?_⟩
· simp
· intro U hUtree _hUextends
exact h.2 U hUtreeThe empty-prefix abstract MST specification is equivalent to the concrete finite-graph minimum-spanning-tree specification.
theorem minimumSpanningTree_iff_mstExtending_empty (G : FiniteGraph V E)
{w : E → Nat} {T : Finset E} :
G.IsMinimumSpanningTree w T ↔ IsMSTExtending G.toProblem w ∅ T := by
constructor
· exact G.mstExtending_empty_of_minimumSpanningTree
· exact G.minimumSpanningTree_of_mstExtending_emptyend FiniteGraph
An edge is safe for A if every optimum extending A can be turned into
an optimum extending A ∪ {e} without losing optimality for the old prefix.
The second conjunct is what lets a Kruskal-style induction keep global optimality for the original prefix, not only optimality for the growing prefix.
def SafeEdge (P : Problem E) (w : E → Nat) (A : Finset E) (e : E) : Prop :=
∀ T, IsMSTExtending P w A T →
∃ T', IsMSTExtending P w (insert e A) T' ∧ IsMSTExtending P w A T'lemma IsMSTExtending.extend_insert_of_mem {P : Problem E} {w : E → Nat}
{A T : Finset E} {e : E} (hT : IsMSTExtending P w A T) (he : e ∈ T) :
IsMSTExtending P w (insert e A) T := by
refine ⟨hT.tree, Finset.insert_subset he hT.includes, ?_⟩
intro U hUtree hUextends
apply hT.optimal U hUtree
intro x hx
exact hUextends (Finset.mem_insert_of_mem hx)
private lemma weight_insert_erase_le (w : E → Nat) {T : Finset E} {e f : E}
(hf : f ∈ T) (he : e ∉ T) (hwe : w e ≤ w f) :
weight w (insert e (T.erase f)) ≤ weight w T := by
have he_not_erase : e ∉ T.erase f := by
intro h
exact he (Finset.mem_of_mem_erase h)
have hf_not_erase : f ∉ T.erase f := Finset.notMem_erase f T
calc
weight w (insert e (T.erase f))
= w e + weight w (T.erase f) := by
simp [weight, he_not_erase]
_ ≤ w f + weight w (T.erase f) := by omega
_ = weight w T := by
unfold weight
exact Finset.add_sum_erase T w hf
The CLRS exchange step: if adding e and dropping f gives another
spanning tree and e is no heavier than f, then the exchanged tree is still
minimum.
theorem mst_exchange_preserves_prefix {P : Problem E} {w : E → Nat} {A T : Finset E}
{e f : E} (hT : IsMSTExtending P w A T)
(hf : f ∈ T) (he : e ∉ T)
(h_tree : P.IsSpanningTree (insert e (T.erase f)))
(h_extends : A ⊆ insert e (T.erase f)) (h_weight : w e ≤ w f) :
IsMSTExtending P w A (insert e (T.erase f)) := by
refine ⟨h_tree, ?_, ?_⟩
· exact h_extends
· intro U hUtree hUextends
exact (weight_insert_erase_le w hf he h_weight).trans
(hT.optimal U hUtree hUextends)The same exchange step, packaged for the enlarged prefix.
theorem mst_exchange_step {P : Problem E} {w : E → Nat} {A T : Finset E}
{e f : E} (hT : IsMSTExtending P w A T)
(hf : f ∈ T) (he : e ∉ T)
(h_tree : P.IsSpanningTree (insert e (T.erase f)))
(h_extends : A ⊆ insert e (T.erase f)) (h_weight : w e ≤ w f) :
IsMSTExtending P w (insert e A) (insert e (T.erase f)) := by
exact (mst_exchange_preserves_prefix hT hf he h_tree h_extends h_weight).extend_insert_of_mem
(Finset.mem_insert_self e (T.erase f))A cut certificate packages the graph-specific part of the CLRS proof.
For every optimum tree extending A that does not already contain e, the
certificate provides a tree edge f crossing the same cut such that replacing
f by e is feasible and preserves A. The light-edge condition then gives
w e ≤ w f.
structure CutCertificate (G : Graph V E) (P : Problem E) (w : E → Nat)
(A : Finset E) (S : Finset V) (e : E) : Prop where
crosses : G.Crosses S e
respects : G.Respects S A
lightest : ∀ f, G.Crosses S f → w e ≤ w f
exchange :
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses S f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f)CLRS cut property in safe-edge form.
omit [DecidableEq V] intheorem safe_edge_of_lightest_crossing {G : Graph V E} {P : Problem E}
{w : E → Nat} {A : Finset E} {S : Finset V} {e : E}
(hcut : CutCertificate G P w A S e) :
SafeEdge P w A e := by
intro T hT
by_cases heT : e ∈ T
· exact ⟨T, hT.extend_insert_of_mem heT, hT⟩
· rcases hcut.exchange T hT heT with
⟨f, hfT, hf_crosses, h_tree, h_extends⟩
exact ⟨insert e (T.erase f),
mst_exchange_step hT hfT heT h_tree h_extends
(hcut.lightest f hf_crosses),
mst_exchange_preserves_prefix hT hfT heT h_tree h_extends
(hcut.lightest f hf_crosses)⟩A direct existence wrapper for using a safe edge in a larger proof.
theorem exists_mst_containing_safe_edge {P : Problem E} {w : E → Nat}
{A T : Finset E} {e : E} (hsafe : SafeEdge P w A e)
(hT : IsMSTExtending P w A T) :
∃ T', IsMSTExtending P w (insert e A) T' :=
let ⟨T', hT', _⟩ := hsafe T hT
⟨T', hT'⟩end MSTend CLRSopen Finset21.2. Kruskal and Prim
This section builds on the safe-edge theorem from Section 21.1. It contains the mathematical Kruskal pass, cut-certificate induction, finite-graph wrappers, and the component-oracle interface. It also isolates the sorted-edge-order lightness argument used by CLRS: once previously processed edges are known not to cross the current component cut, the current edge is light by sorted order. Union-find implementation correctness is deliberately deferred: the current proof works at the mathematical cycle-test interface level.
Closure results:
-
Theorem
FiniteGraph.canonicalSimplePath_unique: a selected forest has a unique simple path between connected endpoints. -
Theorem
FiniteGraph.exists_crossing_exchangePath_of_spanningTree: the canonical tree path automatically yields a crossing exchange edge. -
Theorem
FiniteGraph.cutCertificate_of_lightest_crossing_auto: finite cut certificates no longer require a manual cycle-exchange witness. -
Theorem
FiniteGraph.kruskal_minimum_spanning_tree_of_sorted_complete_exact_component_empty: a sorted complete exact-component Kruskal scan returns an MST, with local lightness and exchange discharged inside the recursion. -
Theorem
FiniteGraph.prim_minimum_spanning_tree: every complete CLRS Prim light-edge trace returns an MST.
The nested implementation modules now provide the incremental stateful union-find scan, executable indexed-queue Prim, and algorithm-level work bounds. Mutable/RAM semantics and concrete array-heap refinement remain.
Implementation details
The executable MST refinements remain available outside the main sidebar:
namespace CLRSnamespace MSTvariable {V E : Type} [DecidableEq V] [DecidableEq E]Component-based cycle-test interface
A mathematical component oracle for the current selected edge set. It is exactly the specification a union-find implementation should refine.
structure ComponentOracle (G : Graph V E) where
component : Finset E → V → Finset V
mem_self : ∀ A v, v ∈ component A v
closed_src :
∀ A root e, e ∈ A → G.src e ∈ component A root → G.dst e ∈ component A root
closed_dst :
∀ A root e, e ∈ A → G.dst e ∈ component A root → G.src e ∈ component A rootnamespace ComponentOracleomit [DecidableEq V] [DecidableEq E] in
theorem respects (C : ComponentOracle G) (A : Finset E) (root : V) :
G.Respects (C.component A root) A := by
intro e he hcross
rcases hcross with ⟨hsrc, hdst⟩ | ⟨hdst, hsrc⟩
· exact hdst (C.closed_src A root e he hsrc)
· exact hsrc (C.closed_dst A root e he hdst)end ComponentOracleExact component oracles
An exact component oracle returns precisely the vertices connected to the root by the currently selected edge set.
def ExactComponentOracle (G : Graph V E) (C : ComponentOracle G) : Prop :=
∀ A root v, v ∈ C.component A root ↔ G.ConnectedIn A root vnamespace GraphThe undirected adjacency relation is symmetric.
omit [DecidableEq V] [DecidableEq E] intheorem adjIn_symm {G : Graph V E} {A : Finset E} {u v : V}
(h : G.AdjIn A u v) :
G.AdjIn A v u := by
rcases h with ⟨e, heA, hend⟩
refine ⟨e, heA, ?_⟩
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· exact Or.inr ⟨hsrc, hdst⟩
· exact Or.inl ⟨hsrc, hdst⟩Connectivity induced by selected undirected edges is symmetric.
omit [DecidableEq V] [DecidableEq E] intheorem connected_symm {G : Graph V E} {A : Finset E} {u v : V}
(h : G.ConnectedIn A u v) :
G.ConnectedIn A v u := by
induction h with
| refl =>
exact Relation.ReflTransGen.refl
| tail hpath hadj ih =>
exact Relation.ReflTransGen.trans
(Relation.ReflTransGen.tail Relation.ReflTransGen.refl
(Graph.adjIn_symm hadj))
ihConnectivity induced by selected edges is transitive.
omit [DecidableEq V] [DecidableEq E] intheorem connected_trans {G : Graph V E} {A : Finset E} {u v x : V}
(huv : G.ConnectedIn A u v) (hvx : G.ConnectedIn A v x) :
G.ConnectedIn A u x :=
Relation.ReflTransGen.trans huv hvxAny selected edge connects its own endpoints.
omit [DecidableEq V] [DecidableEq E] intheorem connected_of_mem_edge {G : Graph V E} {A : Finset E} {e : E}
(he : e ∈ A) :
G.ConnectedIn A (G.src e) (G.dst e) := by
exact Relation.ReflTransGen.tail Relation.ReflTransGen.refl
⟨e, he, Or.inl ⟨rfl, rfl⟩⟩
If every edge of B has endpoints already connected in A, then one
adjacency step in B can be simulated by an A-connection.
omit [DecidableEq V] [DecidableEq E] intheorem connected_of_adjIn_of_edge_connected {G : Graph V E} {A B : Finset E}
(hedge : ∀ e, e ∈ B → G.ConnectedIn A (G.src e) (G.dst e))
{u v : V} (hadj : G.AdjIn B u v) :
G.ConnectedIn A u v := by
rcases hadj with ⟨e, heB, hend⟩
have hconn := hedge e heB
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· simpa [hsrc, hdst] using hconn
· have hconn' := Graph.connected_symm hconn
simpa [hsrc, hdst] using hconn'
If every edge of B has endpoints connected in A, then every
B-path can be transported to an A-path.
omit [DecidableEq V] [DecidableEq E] intheorem connected_of_edgewise_connected {G : Graph V E} {A B : Finset E}
(hedge : ∀ e, e ∈ B → G.ConnectedIn A (G.src e) (G.dst e))
{u v : V} (h : G.ConnectedIn B u v) :
G.ConnectedIn A u v := by
induction h with
| refl =>
exact Relation.ReflTransGen.refl
| tail _ hadj ih =>
exact Graph.connected_trans ih
(Graph.connected_of_adjIn_of_edge_connected hedge hadj)Any path after inserting one edge either already existed before the insertion or crosses the inserted edge once, with old paths on both sides.
omit [DecidableEq V] in
theorem connected_insert_edge_cases {G : Graph V E} {A : Finset E} {e : E}
{u v : V} (h : G.ConnectedIn (insert e A) u v) :
G.ConnectedIn A u v ∨
(G.ConnectedIn A u (G.src e) ∧ G.ConnectedIn A (G.dst e) v) ∨
(G.ConnectedIn A u (G.dst e) ∧ G.ConnectedIn A (G.src e) v) := by
induction h with
| refl =>
exact Or.inl Relation.ReflTransGen.refl
| tail _ hadj ih =>
rcases hadj with ⟨f, hf, hend⟩
rw [Finset.mem_insert] at hf
rcases hf with hfe | hfA
· subst f
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· subst hsrc
subst hdst
rcases ih with hA | ⟨⟨hus, hdy⟩ | ⟨hud, hsy⟩⟩
· exact Or.inr (Or.inl ⟨hA, Relation.ReflTransGen.refl⟩)
· have hsd : G.ConnectedIn A (G.src e) (G.dst e) :=
Graph.connected_trans (Graph.connected_symm hdy)
Relation.ReflTransGen.refl
exact Or.inl (Graph.connected_trans hus hsd)
· exact Or.inl hud
· subst hsrc
subst hdst
rcases ih with hA | ⟨⟨hus, hdy⟩ | ⟨hud, hsy⟩⟩
· exact Or.inr (Or.inr ⟨hA, Relation.ReflTransGen.refl⟩)
· exact Or.inl hus
· have hds : G.ConnectedIn A (G.dst e) (G.src e) :=
Graph.connected_trans (Graph.connected_symm hsy)
Relation.ReflTransGen.refl
exact Or.inl (Graph.connected_trans hud hds)
· have hadjA : G.AdjIn A _ _ := ⟨f, hfA, hend⟩
rcases ih with hA | ⟨⟨hus, hdy⟩ | ⟨hud, hsy⟩⟩
· exact Or.inl (Relation.ReflTransGen.tail hA hadjA)
· exact Or.inr (Or.inl ⟨hus, Relation.ReflTransGen.tail hdy hadjA⟩)
· exact Or.inr (Or.inr ⟨hud, Relation.ReflTransGen.tail hsy hadjA⟩)Canonical simple paths in selected forests
The loop-free simple graph induced by a selected edge set. The explicit inequality removes self-loops without changing connectivity inside a forest.
def selectedSimpleGraph (G : Graph V E) (A : Finset E) : SimpleGraph V where
Adj u v := u ≠ v ∧ G.AdjIn A u v
symm := ⟨by
intro u v h
exact ⟨Ne.symm h.1, Graph.adjIn_symm h.2⟩⟩
loopless := ⟨by
intro v h
exact h.1 rfl⟩A selected-simple-graph walk gives a connection in the original labelled edge model.
omit [DecidableEq V] [DecidableEq E] intheorem connectedIn_of_selectedWalk {G : Graph V E} {A : Finset E}
{u v : V} (p : (G.selectedSimpleGraph A).Walk u v) :
G.ConnectedIn A u v := by
induction p with
| nil => exact Relation.ReflTransGen.refl
| @cons u x v hadj p ih =>
exact Relation.ReflTransGen.head hadj.2 ihIf a simple-graph walk avoids one endpoint of a labelled edge, every step of the walk remains available after that labelled edge is erased.
omit [DecidableEq V] in
theorem connectedIn_erase_of_selectedWalk_avoids_vertex
{G : Graph V E} {T : Finset E} {u v z : V} {f : E}
(p : (G.selectedSimpleGraph T).Walk u v)
(hz : z ∉ p.support)
(hfz : G.src f = z ∨ G.dst f = z) :
G.ConnectedIn (T.erase f) u v := by
induction p with
| nil => exact Relation.ReflTransGen.refl
| @cons u x v hadj p ih =>
rcases hadj.2 with ⟨g, hgT, hend⟩
have hgf : g ≠ f := by
intro hgf
have hzmem : z ∈ (SimpleGraph.Walk.cons hadj p).support := by
have hxmem : x ∈ p.support := p.start_mem_support
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩ <;>
rcases hfz with hsrcz | hdstz <;>
simp_all [SimpleGraph.Walk.support_cons]
exact hz hzmem
have hadjErase : G.AdjIn (T.erase f) u x :=
⟨g, Finset.mem_erase.mpr ⟨hgf, hgT⟩, hend⟩
have hzTail : z ∉ p.support := by
intro hzTail
exact hz (by simp [hzTail])
exact Relation.ReflTransGen.head hadjErase (ih hzTail)Reachability after deleting one unlabelled simple edge maps back to labelled connectivity after erasing the corresponding selected edge.
omit [DecidableEq V] in
theorem connectedIn_erase_of_reachable_delete_selectedEdge
{G : Graph V E} {T : Finset E} {u v x y : V} {f : E}
(hfEnds :
(G.src f = u ∧ G.dst f = v) ∨ (G.src f = v ∧ G.dst f = u))
(hreach :
((G.selectedSimpleGraph T).deleteEdges {s(u, v)}).Reachable x y) :
G.ConnectedIn (T.erase f) x y := by
rw [SimpleGraph.reachable_iff_reflTransGen] at hreach
induction hreach with
| refl => exact Relation.ReflTransGen.refl
| @tail a b hpath hadj ih =>
rw [SimpleGraph.deleteEdges_adj] at hadj
rcases hadj with ⟨hselected, hpair⟩
rcases hselected.2 with ⟨g, hgT, hgEnds⟩
have hgf : g ≠ f := by
intro hgf
apply hpair
simp only [Set.mem_singleton_iff]
subst g
rcases hfEnds with ⟨hfu, hfv⟩ | ⟨hfv, hfu⟩ <;>
rcases hgEnds with ⟨hga, hgb⟩ | ⟨hgb, hga⟩ <;>
simp_all
exact Relation.ReflTransGen.tail ih
⟨g, Finset.mem_erase.mpr ⟨hgf, hgT⟩, hgEnds⟩
A labelled edge on a simple selected path that crosses a cut, together
with the two connections that remain after erasing that edge. This is the
generic endpoint form of ExchangePath.
def PathExchange (G : Graph V E) (T : Finset E) (u v : V) (f : E) : Prop :=
(G.ConnectedIn (T.erase f) (G.src f) u ∧
G.ConnectedIn (T.erase f) v (G.dst f)) ∨
(G.ConnectedIn (T.erase f) (G.src f) v ∧
G.ConnectedIn (T.erase f) u (G.dst f))Reversing the endpoint order preserves a path-exchange witness.
omit [DecidableEq V] intheorem PathExchange.swap {G : Graph V E} {T : Finset E} {u v : V} {f : E}
(h : G.PathExchange T u v f) : G.PathExchange T v u f := by
rcases h with h | h
· exact Or.inr h
· exact Or.inl hA simple selected path whose endpoints lie on opposite sides of a cut has a crossing labelled edge whose deletion leaves the path prefix and suffix connected.
theorem exists_pathExchange_of_simplePath_crosses
{G : Graph V E} {T : Finset E} {S : Finset V} {u v : V}
(p : (G.selectedSimpleGraph T).Walk u v) (hp : p.IsPath)
(hu : u ∈ S) (hv : v ∉ S) :
∃ f, f ∈ T ∧ G.Crosses S f ∧ G.PathExchange T u v f := by
induction p with
| nil => exact False.elim (hv hu)
| @cons u x v hadj p ih =>
rw [SimpleGraph.Walk.cons_isPath_iff] at hp
rcases hp with ⟨hp, huAvoids⟩
rcases hadj.2 with ⟨g, hgT, hend⟩
by_cases hx : x ∈ S
· rcases ih hp hx hv with ⟨f, hfT, hfCross, hfPath⟩
have hgNotCross : ¬ G.Crosses S g := by
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩ <;>
simp [Graph.Crosses, hsrc, hdst, hu, hx]
have hgf : g ≠ f := by
intro hgf
exact hgNotCross (by simpa [hgf] using hfCross)
have hux : G.ConnectedIn (T.erase f) u x :=
Relation.ReflTransGen.single
⟨g, Finset.mem_erase.mpr ⟨hgf, hgT⟩, hend⟩
refine ⟨f, hfT, hfCross, ?_⟩
rcases hfPath with ⟨hfx, hvf⟩ | ⟨hfv, hxf⟩
· exact Or.inl ⟨Graph.connected_trans hfx (Graph.connected_symm hux), hvf⟩
· exact Or.inr ⟨hfv, Graph.connected_trans hux hxf⟩
· have hsuffix : G.ConnectedIn (T.erase g) x v :=
Graph.connectedIn_erase_of_selectedWalk_avoids_vertex p huAvoids
(by
rcases hend with ⟨hsrc, _⟩ | ⟨_, hdst⟩
· exact Or.inl hsrc
· exact Or.inr hdst)
have hgCross : G.Crosses S g := by
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· exact Or.inl ⟨by simpa [hsrc] using hu, by simpa [hdst] using hx⟩
· exact Or.inr ⟨by simpa [hdst] using hu, by simpa [hsrc] using hx⟩
refine ⟨g, hgT, hgCross, ?_⟩
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· exact Or.inl ⟨
by simpa [hsrc] using (Graph.connected_refl G (T.erase g) u),
by simpa [hdst] using (Graph.connected_symm hsuffix)⟩
· exact Or.inr ⟨
by simpa [hsrc] using hsuffix,
by simpa [hdst] using (Graph.connected_refl G (T.erase g) u)⟩
A path-decomposition certificate for the CLRS tree-exchange step. After
removing tree edge f, the endpoints of the new edge e reconnect
the two sides of f, in one of the two undirected orientations.
def ExchangePath (G : Graph V E) (T : Finset E) (e f : E) : Prop :=
(G.ConnectedIn (T.erase f) (G.src f) (G.src e) ∧
G.ConnectedIn (T.erase f) (G.dst e) (G.dst f)) ∨
(G.ConnectedIn (T.erase f) (G.src f) (G.dst e) ∧
G.ConnectedIn (T.erase f) (G.src e) (G.dst f))
Cycle-style exchange witness: after deleting tree edge f, inserting the
new edge e reconnects the endpoints of f. This is the compact
connectivity fact a future finite path/cycle API should produce.
def InsertedEdgeConnection (G : Graph V E) (T : Finset E) (e f : E) : Prop :=
G.ConnectedIn (insert e (T.erase f)) (G.src f) (G.dst f)
An ExchangePath certificate reconnects the endpoints of the deleted tree
edge after the new edge is inserted.
omit [DecidableEq V] intheorem exchangePath_connected_insert {G : Graph V E} {T : Finset E} {e f : E}
(hpath : G.ExchangePath T e f) :
G.ConnectedIn (insert e (T.erase f)) (G.src f) (G.dst f) := by
have hmono : T.erase f ⊆ insert e (T.erase f) :=
Finset.subset_insert e (T.erase f)
have he_conn :
G.ConnectedIn (insert e (T.erase f)) (G.src e) (G.dst e) :=
Graph.connected_of_mem_edge (Finset.mem_insert_self e (T.erase f))
rcases hpath with ⟨hleft, hright⟩ | ⟨hleft, hright⟩
· have h₁ := Graph.connected_mono hmono hleft
have h₂ := Graph.connected_mono hmono hright
exact Graph.connected_trans (Graph.connected_trans h₁ he_conn) h₂
· have h₁ := Graph.connected_mono hmono hleft
have h₂ := Graph.connected_mono hmono hright
exact Graph.connected_trans (Graph.connected_trans h₁
(Graph.connected_symm he_conn)) h₂
An ExchangePath certificate is an inserted-edge connection.
omit [DecidableEq V] intheorem insertedEdgeConnection_of_exchangePath {G : Graph V E} {T : Finset E}
{e f : E} (hpath : G.ExchangePath T e f) :
G.InsertedEdgeConnection T e f :=
Graph.exchangePath_connected_insert hpath
Conversely, if inserting e reconnects the endpoints of f, and
those endpoints were not already connected after erasing f, then the
connection decomposes into an ExchangePath certificate.
omit [DecidableEq V] intheorem exchangePath_of_insert_connected {G : Graph V E} {T : Finset E} {e f : E}
(hconn :
G.ConnectedIn (insert e (T.erase f)) (G.src f) (G.dst f))
(hnot :
¬ G.ConnectedIn (T.erase f) (G.src f) (G.dst f)) :
G.ExchangePath T e f := by
rcases Graph.connected_insert_edge_cases hconn with hbase |
(⟨hleft, hright⟩ | ⟨hleft, hright⟩)
· exact False.elim (hnot hbase)
· exact Or.inl ⟨hleft, hright⟩
· exact Or.inr ⟨hleft, hright⟩
Equivalence between the path-decomposition certificate and the compact
cycle-style inserted-edge connection, assuming deleting f really
separates its endpoints.
omit [DecidableEq V] intheorem exchangePath_iff_insertedEdgeConnection {G : Graph V E} {T : Finset E}
{e f : E}
(hnot : ¬ G.ConnectedIn (T.erase f) (G.src f) (G.dst f)) :
G.ExchangePath T e f ↔ G.InsertedEdgeConnection T e f := by
constructor
· exact Graph.insertedEdgeConnection_of_exchangePath
· intro hconn
exact Graph.exchangePath_of_insert_connected hconn hnotend GraphThe executable-style cycle test induced by a component oracle: accept an edge iff its destination is outside the source component.
def acceptByComponent (G : Graph V E) (C : ComponentOracle G)
(A : Finset E) (e : E) : Bool :=
decide (G.dst e ∉ C.component A (G.src e))omit [DecidableEq E] in
private theorem not_mem_component_of_accept {G : Graph V E} {C : ComponentOracle G}
{A : Finset E} {e : E} (h : acceptByComponent G C A e = true) :
G.dst e ∉ C.component A (G.src e) := by
simpa [acceptByComponent] using h
omit [DecidableEq E] in
private theorem mem_component_of_reject {G : Graph V E} {C : ComponentOracle G}
{A : Finset E} {e : E} (h : acceptByComponent G C A e = false) :
G.dst e ∈ C.component A (G.src e) := by
by_contra hmem
have htrue : acceptByComponent G C A e = true := by
simp [acceptByComponent, hmem]
simp [h] at htrueAccepted component edges induce the cut used in the CLRS proof.
theorem cut_certificate_of_component_oracle {G : Graph V E} {P : Problem E}
{w : E → Nat} (C : ComponentOracle G) {A : Finset E} {e : E}
(haccept : acceptByComponent G C A e = true)
(hlight :
∀ f, G.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f)) :
CutCertificate G P w A (C.component A (G.src e)) e := by
refine ⟨?_, C.respects A (G.src e), hlight, hexchange⟩
exact Or.inl ⟨C.mem_self A (G.src e), not_mem_component_of_accept haccept⟩An edge whose endpoints are already connected by the current selected edge set cannot cross any exact component cut for that selected edge set.
omit [DecidableEq V] [DecidableEq E] intheorem not_crosses_component_of_connected {G : Graph V E}
{C : ComponentOracle G} (hexact : ExactComponentOracle G C)
{A : Finset E} {root : V} {e : E}
(hconn : G.ConnectedIn A (G.src e) (G.dst e)) :
¬ G.Crosses (C.component A root) e := by
intro hcross
rcases hcross with ⟨hsrc, hdst⟩ | ⟨hdst, hsrc⟩
· have hrootSrc : G.ConnectedIn A root (G.src e) :=
(hexact A root (G.src e)).1 hsrc
have hrootDst : G.ConnectedIn A root (G.dst e) :=
Graph.connected_trans hrootSrc hconn
exact hdst ((hexact A root (G.dst e)).2 hrootDst)
· have hrootDst : G.ConnectedIn A root (G.dst e) :=
(hexact A root (G.dst e)).1 hdst
have hdstSrc : G.ConnectedIn A (G.dst e) (G.src e) :=
Graph.connected_symm hconn
have hrootSrc : G.ConnectedIn A root (G.src e) :=
Graph.connected_trans hrootDst hdstSrc
exact hsrc ((hexact A root (G.src e)).2 hrootSrc)If an edge is either selected already or internally connected by the selected edge set, it cannot cross an exact component cut.
omit [DecidableEq V] [DecidableEq E] intheorem not_crosses_component_of_mem_or_connected {G : Graph V E}
{C : ComponentOracle G} (hexact : ExactComponentOracle G C)
{A : Finset E} {root : V} {e : E}
(haccounted : e ∈ A ∨ G.ConnectedIn A (G.src e) (G.dst e)) :
¬ G.Crosses (C.component A root) e := by
rcases haccounted with heA | hconn
· exact C.respects A root e heA
· exact not_crosses_component_of_connected hexact hconnSorted-order lightness certificates
An edge list is sorted in nondecreasing weight order.
This CLRS-facing predicate is deliberately small: the head is no heavier than every later edge, and the tail is sorted recursively.
def WeightSorted (w : E → Nat) : List E → Prop
| [] => True
| e :: es => (∀ f, f ∈ es → w e ≤ w f) ∧ WeightSorted w esA suffix of a sorted edge list is sorted.
omit [DecidableEq E] intheorem weightSorted_suffix_of_append (w : E → Nat)
(processed rest : List E) :
WeightSorted w (processed ++ rest) → WeightSorted w rest := by
induction processed with
| nil =>
intro hsorted
simpa using hsorted
| cons _ processed ih =>
intro hsorted
exact ih hsorted.2In a sorted nonempty edge list, the head is no heavier than any member.
omit [DecidableEq E] in
theorem weightSorted_head_le_of_mem {w : E → Nat} {e f : E}
{suffix : List E} (hsorted : WeightSorted w (e :: suffix))
(hf : f ∈ e :: suffix) :
w e ≤ w f := by
rw [List.mem_cons] at hf
rcases hf with hfe | hfSuffix
· simp [hfe]
· exact hsorted.1 f hfSuffix
If every crossing edge appears in processed ++ e :: suffix, and the
processed edge prefix contains no crossing edge for the current cut, then every
crossing edge appears at or after e.
omit [DecidableEq V] [DecidableEq E] intheorem crossing_mem_current_suffix_of_prefix_excludes
{G : Graph V E} {S : Finset V} {processed suffix : List E} {e f : E}
(hall :
∀ g, G.Crosses S g → g ∈ processed ++ e :: suffix)
(hprefix :
∀ g, g ∈ processed → ¬ G.Crosses S g)
(hcross : G.Crosses S f) :
f ∈ e :: suffix := by
have hfAll := hall f hcross
rcases List.mem_append.mp hfAll with hfPrefix | hfSuffix
· exact False.elim ((hprefix f hfPrefix) hcross)
· exact hfSuffixSorted edge order plus the processed-prefix exclusion invariant proves the lightness side condition for the current Kruskal cut.
This isolates the CLRS sorted-order argument from the graph-specific proof that previously processed edges do not cross the current component cut.
omit [DecidableEq V] [DecidableEq E] intheorem lightest_crossing_of_sorted_prefix {G : Graph V E} {w : E → Nat}
{S : Finset V} {processed suffix : List E} {e : E}
(hsorted : WeightSorted w (processed ++ e :: suffix))
(hall :
∀ f, G.Crosses S f → f ∈ processed ++ e :: suffix)
(hprefix :
∀ f, f ∈ processed → ¬ G.Crosses S f) :
∀ f, G.Crosses S f → w e ≤ w f := by
intro f hcross
have hsuffixSorted :
WeightSorted w (e :: suffix) :=
weightSorted_suffix_of_append w processed (e :: suffix) hsorted
have hfSuffix :
f ∈ e :: suffix :=
crossing_mem_current_suffix_of_prefix_excludes
(G := G) (S := S) (processed := processed) (suffix := suffix)
(e := e) hall hprefix hcross
exact weightSorted_head_le_of_mem hsuffixSorted hfSuffixComponent-oracle cut certificate where the lightness field is discharged from sorted edge order and a processed-prefix exclusion invariant.
theorem cut_certificate_of_component_oracle_sorted_prefix
{G : Graph V E} {P : Problem E} {w : E → Nat} (C : ComponentOracle G)
{A : Finset E} {e : E} {processed suffix : List E}
(haccept : acceptByComponent G C A e = true)
(hsorted : WeightSorted w (processed ++ e :: suffix))
(hall :
∀ f, G.Crosses (C.component A (G.src e)) f →
f ∈ processed ++ e :: suffix)
(hprefix :
∀ f, f ∈ processed →
¬ G.Crosses (C.component A (G.src e)) f)
(hexchange :
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f)) :
CutCertificate G P w A (C.component A (G.src e)) e := by
exact cut_certificate_of_component_oracle C haccept
(lightest_crossing_of_sorted_prefix hsorted hall hprefix)
hexchangeKruskal-style safe-edge induction
A mathematical Kruskal pass over a fixed edge order.
The Boolean accept A e abstracts the cycle test: when it returns true, the
edge is inserted into the current forest; otherwise it is skipped.
def kruskal (accept : Finset E → E → Bool) : List E → Finset E → Finset E
| [], A => A
| e :: es, A => kruskal accept es (if accept A e then insert e A else A)
Prim's mathematical edge-accumulation pass. The dynamic light-edge and
cut obligations are carried by FiniteGraph.PrimTrace below.
def prim : List E → Finset E → Finset E
| [], A => A
| e :: es, A => prim es (insert e A)Splitting an edge order into a processed prefix and a remaining suffix is compatible with the mathematical Kruskal pass.
theorem kruskal_append (accept : Finset E → E → Bool)
(processed suffix : List E) (A : Finset E) :
kruskal accept (processed ++ suffix) A =
kruskal accept suffix (kruskal accept processed A) := by
induction processed generalizing A with
| nil => rfl
| cons e processed ih =>
simp only [List.cons_append, kruskal]
by_cases hacc : accept A e = true
· simp only [if_pos hacc]
exact ih (insert e A)
· have hfalse : accept A e = false := by
cases h : accept A e <;> simp [h] at hacc ⊢
simp only [if_neg (by simpa [hfalse])]
exact ih AThe proof obligation needed by the abstract Kruskal induction: every edge accepted by the cycle test is safe for the current prefix. In a concrete graph development this is discharged by a cut-property certificate.
structure KruskalCertificate (P : Problem E) (w : E → Nat)
(accept : Finset E → E → Bool) : Prop where
safe : ∀ A e, accept A e = true → SafeEdge P w A eA CLRS-style certificate for Kruskal: each accepted edge has a cut certificate showing it is light across some cut respecting the current forest.
structure KruskalCutCertificate (G : Graph V E) (P : Problem E) (w : E → Nat)
(accept : Finset E → E → Bool) : Prop where
cut : ∀ A e, accept A e = true → ∃ S, CutCertificate G P w A S eomit [DecidableEq V] in
theorem kruskal_certificate_of_cut_certificates {G : Graph V E} {P : Problem E}
{w : E → Nat} {accept : Finset E → E → Bool}
(cert : KruskalCutCertificate G P w accept) :
KruskalCertificate P w accept := by
refine ⟨?_⟩
intro A e hacc
rcases cert.cut A e hacc with ⟨S, hcut⟩
exact safe_edge_of_lightest_crossing hcuttheorem kruskal_cut_certificate_of_component_oracle {G : Graph V E}
{P : Problem E} {w : E → Nat} (C : ComponentOracle G)
(hlight :
∀ A e, acceptByComponent G C A e = true →
∀ f, G.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G C A e = true →
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f)) :
KruskalCutCertificate G P w (acceptByComponent G C) := by
refine ⟨?_⟩
intro A e hacc
exact ⟨C.component A (G.src e),
cut_certificate_of_component_oracle C hacc
(hlight A e hacc) (hexchange A e hacc)⟩
theorem kruskal_extends_start (accept : Finset E → E → Bool)
(edges : List E) (A : Finset E) :
A ⊆ kruskal accept edges A := by
induction edges generalizing A with
| nil =>
simp [kruskal]
| cons e es ih =>
by_cases hacc : accept A e = true
· have hA : A ⊆ insert e A := Finset.subset_insert e A
exact hA.trans (by simpa [kruskal, hacc] using ih (insert e A))
· have hfalse : accept A e = false := by
cases h : accept A e <;> simp [h] at hacc ⊢
simpa [kruskal, hfalse] using ih AKruskal never selects an edge outside the initial set or the scanned edge list.
theorem kruskal_subset_of_start_and_edges (accept : Finset E → E → Bool)
(edges : List E) {A B : Finset E}
(hA : A ⊆ B) (hedges : ∀ e, e ∈ edges → e ∈ B) :
kruskal accept edges A ⊆ B := by
induction edges generalizing A with
| nil =>
simpa [kruskal] using hA
| cons e es ih =>
by_cases hacc : accept A e = true
· have heB : e ∈ B := hedges e (by simp)
have hinsert : insert e A ⊆ B := Finset.insert_subset heB hA
have htail : ∀ f, f ∈ es → f ∈ B := by
intro f hf
exact hedges f (by simp [hf])
simpa [kruskal, hacc] using ih hinsert htail
· have hfalse : accept A e = false := by
cases h : accept A e <;> simp [h] at hacc ⊢
have htail : ∀ f, f ∈ es → f ∈ B := by
intro f hf
exact hedges f (by simp [hf])
simpa [kruskal, hfalse] using ih hA htailAfter a Kruskal prefix has been processed by an exact component oracle, every processed edge is accounted for: it is either selected in the current forest or its endpoints are already connected in that forest.
theorem processed_edge_mem_or_connected_of_exact_component_kruskal
{G : Graph V E} (C : ComponentOracle G)
(hexact : ExactComponentOracle G C) (processed : List E)
(A : Finset E) :
∀ f, f ∈ processed →
f ∈ kruskal (acceptByComponent G C) processed A ∨
G.ConnectedIn (kruskal (acceptByComponent G C) processed A)
(G.src f) (G.dst f) := by
induction processed generalizing A with
| nil =>
intro f hf
simp at hf
| cons e es ih =>
intro f hf
rw [List.mem_cons] at hf
by_cases hacc : acceptByComponent G C A e = true
· rcases hf with hfe | hfes
· left
subst f
have heInsert : e ∈ insert e A := Finset.mem_insert_self e A
have hsubset :
insert e A ⊆ kruskal (acceptByComponent G C) es (insert e A) :=
kruskal_extends_start (acceptByComponent G C) es (insert e A)
simpa [kruskal, hacc] using hsubset heInsert
· simpa [kruskal, hacc] using ih (insert e A) f hfes
· have hfalse : acceptByComponent G C A e = false := by
cases h : acceptByComponent G C A e <;> simp [h] at hacc ⊢
rcases hf with hfe | hfes
· right
subst f
have hmem : G.dst e ∈ C.component A (G.src e) :=
mem_component_of_reject hfalse
have hconnA : G.ConnectedIn A (G.src e) (G.dst e) :=
(hexact A (G.src e) (G.dst e)).1 hmem
have hsubset : A ⊆ kruskal (acceptByComponent G C) es A :=
kruskal_extends_start (acceptByComponent G C) es A
have hconnFinal :
G.ConnectedIn (kruskal (acceptByComponent G C) es A)
(G.src e) (G.dst e) :=
Graph.connected_mono hsubset hconnA
simpa [kruskal, hfalse] using hconnFinal
· simpa [kruskal, hfalse] using ih A f hfesAfter an exact-component Kruskal pass, every processed edge has connected endpoints in the final selected set.
theorem processed_edge_connected_of_exact_component_kruskal
{G : Graph V E} (C : ComponentOracle G)
(hexact : ExactComponentOracle G C) (processed : List E)
(A : Finset E) :
∀ f, f ∈ processed →
G.ConnectedIn (kruskal (acceptByComponent G C) processed A)
(G.src f) (G.dst f) := by
intro f hf
rcases processed_edge_mem_or_connected_of_exact_component_kruskal C hexact
processed A f hf with hmem | hconn
· exact Graph.connected_of_mem_edge hmem
· exact hconnExact components derive the processed-prefix exclusion invariant needed by the sorted-order Kruskal lightness proof.
theorem processed_prefix_excludes_of_exact_component_kruskal
{G : Graph V E} (C : ComponentOracle G)
(hexact : ExactComponentOracle G C) (processed : List E)
(A : Finset E) (root : V) :
∀ f, f ∈ processed →
¬ G.Crosses
(C.component (kruskal (acceptByComponent G C) processed A) root) f := by
intro f hf
exact not_crosses_component_of_mem_or_connected hexact
(processed_edge_mem_or_connected_of_exact_component_kruskal C hexact
processed A f hf)Kruskal's sorted edge order proves lightness without a standalone prefix exclusion hypothesis when the component oracle is exact.
theorem lightest_crossing_of_exact_component_kruskal_prefix
{G : Graph V E} {w : E → Nat} (C : ComponentOracle G)
(hexact : ExactComponentOracle G C)
{processed suffix : List E} {A : Finset E} {e : E}
(hsorted : WeightSorted w (processed ++ e :: suffix))
(hall :
∀ f,
G.Crosses
(C.component (kruskal (acceptByComponent G C) processed A)
(G.src e)) f →
f ∈ processed ++ e :: suffix) :
∀ f,
G.Crosses
(C.component (kruskal (acceptByComponent G C) processed A)
(G.src e)) f →
w e ≤ w f := by
exact lightest_crossing_of_sorted_prefix hsorted hall
(processed_prefix_excludes_of_exact_component_kruskal C hexact
processed A (G.src e))Exact-component cut certificate for the current Kruskal edge. This packages the derived processed-prefix exclusion invariant with the sorted edge order.
theorem cut_certificate_of_exact_component_kruskal_prefix
{G : Graph V E} {P : Problem E} {w : E → Nat} (C : ComponentOracle G)
(hexact : ExactComponentOracle G C)
{processed suffix : List E} {A : Finset E} {e : E}
(haccept :
acceptByComponent G C
(kruskal (acceptByComponent G C) processed A) e = true)
(hsorted : WeightSorted w (processed ++ e :: suffix))
(hall :
∀ f,
G.Crosses
(C.component (kruskal (acceptByComponent G C) processed A)
(G.src e)) f →
f ∈ processed ++ e :: suffix)
(hexchange :
∀ T,
IsMSTExtending P w
(kruskal (acceptByComponent G C) processed A) T →
e ∉ T →
∃ f, f ∈ T ∧
G.Crosses
(C.component
(kruskal (acceptByComponent G C) processed A)
(G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
kruskal (acceptByComponent G C) processed A ⊆
insert e (T.erase f)) :
CutCertificate G P w
(kruskal (acceptByComponent G C) processed A)
(C.component (kruskal (acceptByComponent G C) processed A) (G.src e))
e := by
exact cut_certificate_of_component_oracle C haccept
(lightest_crossing_of_exact_component_kruskal_prefix C hexact
hsorted hall)
hexchangeprivate theorem optimal_for_smaller_prefix {P : Problem E} {w : E → Nat}
{A₀ A T T' : Finset E} (hA₀A : A₀ ⊆ A)
(hcur : IsMSTExtending P w A T) (hbase : IsMSTExtending P w A₀ T)
(hnew : IsMSTExtending P w A T') :
IsMSTExtending P w A₀ T' := by
refine ⟨hnew.tree, ?_, ?_⟩
· exact hA₀A.trans hnew.includes
· intro U hUtree hUincludes
exact (hnew.optimal T hcur.tree hcur.includes).trans
(hbase.optimal U hUtree hUincludes)
theorem kruskal_preserves_mst {P : Problem E} {w : E → Nat}
{accept : Finset E → E → Bool} (cert : KruskalCertificate P w accept)
(edges : List E) {A₀ A T : Finset E} (hA₀A : A₀ ⊆ A)
(hcur : IsMSTExtending P w A T) (hbase : IsMSTExtending P w A₀ T) :
∃ T', IsMSTExtending P w (kruskal accept edges A) T' ∧
IsMSTExtending P w A₀ T' := by
induction edges generalizing A T with
| nil =>
exact ⟨T, by simpa [kruskal] using hcur, hbase⟩
| cons e es ih =>
by_cases hacc : accept A e = true
· rcases cert.safe A e hacc T hcur with ⟨T₁, hnext, hprefix⟩
have hbase₁ : IsMSTExtending P w A₀ T₁ :=
optimal_for_smaller_prefix hA₀A hcur hbase hprefix
have hA₀next : A₀ ⊆ insert e A :=
hA₀A.trans (Finset.subset_insert e A)
simpa [kruskal, hacc] using ih hA₀next hnext hbase₁
· have hfalse : accept A e = false := by
cases h : accept A e <;> simp [h] at hacc ⊢
simpa [kruskal, hfalse] using ih hA₀A hcur hbaseMathematical Kruskal optimality.
If the accept rule only accepts safe edges, the initial prefix has an optimum, and the final selected edge set is itself a maximal spanning tree, then the Kruskal result is an optimum extending the initial prefix. The final maximality assumption is the graph-specific fact that a spanning tree cannot be properly extended by another spanning tree; concrete graph modules can prove it from the usual cardinality characterization of spanning trees.
theorem kruskal_optimal {P : Problem E} {w : E → Nat}
{accept : Finset E → E → Bool} (cert : KruskalCertificate P w accept)
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending P w A₀ T₀)
(hfinal_tree : P.IsSpanningTree (kruskal accept edges A₀))
(hfinal_maximal :
∀ T, P.IsSpanningTree T → kruskal accept edges A₀ ⊆ T →
T = kruskal accept edges A₀) :
IsMSTExtending P w A₀ (kruskal accept edges A₀) := by
rcases kruskal_preserves_mst cert edges (Subset.rfl : A₀ ⊆ A₀) hstart hstart with
⟨T, hfinal, hglobal⟩
have hT : T = kruskal accept edges A₀ :=
hfinal_maximal T hfinal.tree hfinal.includes
refine ⟨hfinal_tree, ?_, ?_⟩
· simpa [← hT] using hglobal.includes
· intro U hUtree hUincludes
simpa [hT] using hglobal.optimal U hUtree hUincludesKruskal optimality stated directly from CLRS cut certificates.
omit [DecidableEq V] intheorem kruskal_optimal_of_cut_certificates {G : Graph V E} {P : Problem E}
{w : E → Nat} {accept : Finset E → E → Bool}
(cert : KruskalCutCertificate G P w accept) (edges : List E)
{A₀ T₀ : Finset E} (hstart : IsMSTExtending P w A₀ T₀)
(hfinal_tree : P.IsSpanningTree (kruskal accept edges A₀))
(hfinal_maximal :
∀ T, P.IsSpanningTree T → kruskal accept edges A₀ ⊆ T →
T = kruskal accept edges A₀) :
IsMSTExtending P w A₀ (kruskal accept edges A₀) := by
exact kruskal_optimal (kruskal_certificate_of_cut_certificates cert)
edges hstart hfinal_tree hfinal_maximaltheorem kruskal_optimal_of_component_oracle {G : Graph V E} {P : Problem E}
{w : E → Nat} (C : ComponentOracle G)
(hlight :
∀ A e, acceptByComponent G C A e = true →
∀ f, G.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G C A e = true →
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending P w A₀ T₀)
(hfinal_tree : P.IsSpanningTree (kruskal (acceptByComponent G C) edges A₀))
(hfinal_maximal :
∀ T, P.IsSpanningTree T → kruskal (acceptByComponent G C) edges A₀ ⊆ T →
T = kruskal (acceptByComponent G C) edges A₀) :
IsMSTExtending P w A₀ (kruskal (acceptByComponent G C) edges A₀) := by
exact kruskal_optimal_of_cut_certificates
(kruskal_cut_certificate_of_component_oracle C hlight hexchange)
edges hstart hfinal_tree hfinal_maximal
A verified executable cycle test. A union-find implementation should
provide an accept function and prove that it agrees with the component oracle.
structure CycleTestImplementation (G : Graph V E) (C : ComponentOracle G) where
accept : Finset E → E → Bool
correct : ∀ A e, accept A e = acceptByComponent G C A eThe canonical executable cycle test associated to a component oracle.
def componentCycleTest (G : Graph V E) (C : ComponentOracle G) :
CycleTestImplementation G C where
accept := acceptByComponent G C
correct := by
intro A e
rfl
theorem kruskal_optimal_of_cycle_test {G : Graph V E} {P : Problem E}
{w : E → Nat} {C : ComponentOracle G}
(impl : CycleTestImplementation G C)
(hlight :
∀ A e, impl.accept A e = true →
∀ f, G.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, impl.accept A e = true →
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending P w A₀ T₀)
(hfinal_tree : P.IsSpanningTree (kruskal impl.accept edges A₀))
(hfinal_maximal :
∀ T, P.IsSpanningTree T → kruskal impl.accept edges A₀ ⊆ T →
T = kruskal impl.accept edges A₀) :
IsMSTExtending P w A₀ (kruskal impl.accept edges A₀) := by
have hsame : impl.accept = acceptByComponent G C := by
funext A e
exact impl.correct A e
have hlight' :
∀ A e, acceptByComponent G C A e = true →
∀ f, G.Crosses (C.component A (G.src e)) f → w e ≤ w f := by
intro A e hacc
exact hlight A e (by simpa [hsame] using hacc)
have hexchange' :
∀ A e, acceptByComponent G C A e = true →
∀ T, IsMSTExtending P w A T → e ∉ T →
∃ f, f ∈ T ∧ G.Crosses (C.component A (G.src e)) f ∧
P.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f) := by
intro A e hacc
exact hexchange A e (by simpa [hsame] using hacc)
have hfinal_tree' :
P.IsSpanningTree (kruskal (acceptByComponent G C) edges A₀) := by
simpa [hsame] using hfinal_tree
have hfinal_maximal' :
∀ T, P.IsSpanningTree T → kruskal (acceptByComponent G C) edges A₀ ⊆ T →
T = kruskal (acceptByComponent G C) edges A₀ := by
intro T hT hsub
simpa [hsame] using hfinal_maximal T hT (by simpa [hsame] using hsub)
simpa [hsame] using
(kruskal_optimal_of_component_oracle (G := G) (P := P) (w := w) C
hlight' hexchange' edges hstart hfinal_tree' hfinal_maximal')namespace FiniteGraphThe empty edge set is a forest.
theorem isForest_empty (G : FiniteGraph V E) :
G.IsForest ∅ := by
intro e he
simp at heForest adjacency cannot be a self-loop.
theorem ne_of_adjIn_of_isForest (G : FiniteGraph V E) {A : Finset E}
(hforest : G.IsForest A) {u v : V} (hadj : G.toGraph.AdjIn A u v) :
u ≠ v := by
intro huv
subst v
rcases hadj with ⟨e, heA, hend⟩
apply hforest e heA
rcases hend with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· simpa [hsrc, hdst] using
(Graph.connected_refl G.toGraph (A.erase e) u)
· simpa [hsrc, hdst] using
(Graph.connected_refl G.toGraph (A.erase e) u)Connectivity in a forest lifts to reachability in its loop-free simple graph view.
theorem reachable_selectedSimpleGraph_of_connected (G : FiniteGraph V E)
{A : Finset E} (hforest : G.IsForest A) {u v : V}
(hconn : G.toGraph.ConnectedIn A u v) :
(G.toGraph.selectedSimpleGraph A).Reachable u v := by
rw [SimpleGraph.reachable_iff_reflTransGen]
induction hconn with
| refl => exact Relation.ReflTransGen.refl
| tail hpath hadj ih =>
exact Relation.ReflTransGen.tail ih
⟨G.ne_of_adjIn_of_isForest hforest hadj, hadj⟩The simple-graph view of a selected forest is acyclic: every unlabelled edge is a bridge because erasing its unique labelled representative disconnects its endpoints.
theorem selectedSimpleGraph_isAcyclic (G : FiniteGraph V E)
{A : Finset E} (hforest : G.IsForest A) :
(G.toGraph.selectedSimpleGraph A).IsAcyclic := by
rw [SimpleGraph.isAcyclic_iff_forall_isBridge]
intro edge hedge
obtain ⟨u, v⟩ := edge
have hadj : (G.toGraph.selectedSimpleGraph A).Adj u v :=
(G.toGraph.selectedSimpleGraph A).mem_edgeSet.mp hedge
rcases hadj.2 with ⟨f, hfA, hfEnds⟩
rw [SimpleGraph.isBridge_iff]
intro hreach
have hconn : G.toGraph.ConnectedIn (A.erase f) u v :=
Graph.connectedIn_erase_of_reachable_delete_selectedEdge hfEnds hreach
apply hforest f hfA
rcases hfEnds with ⟨hsrc, hdst⟩ | ⟨hsrc, hdst⟩
· simpa [hsrc, hdst] using hconn
· simpa [hsrc, hdst] using (Graph.connected_symm hconn)The canonical simple path selected from a finite forest connection. The choice is noncomputable, but its result is a genuine Mathlib path and therefore contains no repeated vertices.
noncomputable def canonicalSimplePath (G : FiniteGraph V E) {A : Finset E}
(hforest : G.IsForest A) {u v : V}
(hconn : G.toGraph.ConnectedIn A u v) :
(G.toGraph.selectedSimpleGraph A).Path u v := by
have hreach : (G.toGraph.selectedSimpleGraph A).Reachable u v :=
G.reachable_selectedSimpleGraph_of_connected hforest hconn
let p := Classical.choose hreach.exists_isPath
exact ⟨p, Classical.choose_spec hreach.exists_isPath⟩The canonical forest path is the unique simple path between its endpoints.
theorem canonicalSimplePath_unique (G : FiniteGraph V E) {A : Finset E}
(hforest : G.IsForest A) {u v : V}
(hconn : G.toGraph.ConnectedIn A u v)
(p : (G.toGraph.selectedSimpleGraph A).Path u v) :
p = G.canonicalSimplePath hforest hconn :=
(G.selectedSimpleGraph_isAcyclic hforest).path_unique _ _
The canonical tree path automatically supplies the crossing edge and
ExchangePath certificate required by the CLRS exchange argument.
theorem exists_crossing_exchangePath_of_spanningTree
(G : FiniteGraph V E) {T : Finset E} {S : Finset V} {e : E}
(hT : G.IsSpanningTree T) (heG : e ∈ G.edges)
(hcross : G.toGraph.Crosses S e) :
∃ f, f ∈ T ∧ G.toGraph.Crosses S f ∧
G.toGraph.ExchangePath T e f := by
have hsrc : G.src e ∈ G.vertices := G.src_mem e heG
have hdst : G.dst e ∈ G.vertices := G.dst_mem e heG
have hconn : G.toGraph.ConnectedIn T (G.src e) (G.dst e) :=
hT.2.1 (G.src e) hsrc (G.dst e) hdst
let p := G.canonicalSimplePath hT.2.2 hconn
rcases hcross with hcross | hcross
· rcases Graph.exists_pathExchange_of_simplePath_crosses
p.1 p.2 hcross.1 hcross.2 with ⟨f, hfT, hfCross, hfPath⟩
exact ⟨f, hfT, hfCross, by simpa [Graph.ExchangePath, Graph.PathExchange] using hfPath⟩
· have hpReverse : p.1.reverse.IsPath := p.2.reverse
rcases Graph.exists_pathExchange_of_simplePath_crosses
p.1.reverse hpReverse hcross.1 hcross.2 with
⟨f, hfT, hfCross, hfPath⟩
have hfPath' : G.toGraph.PathExchange T (G.src e) (G.dst e) f :=
Graph.PathExchange.swap hfPath
exact ⟨f, hfT, hfCross,
by simpa [Graph.ExchangePath, Graph.PathExchange] using hfPath'⟩private theorem connected_insert_erase_self_eq
{A : Finset E} {e : E} (heA : e ∉ A) :
(insert e A).erase e = A := by
ext x
by_cases hxe : x = e
· subst x
simp [heA]
· simp [hxe]private theorem erase_insert_comm_of_ne {A : Finset E} {e f : E}
(hef : e ≠ f) :
(insert e A).erase f = insert e (A.erase f) := by
ext x
by_cases hxf : x = f
· subst x
simp [Ne.symm hef]
· simp [hxf]omit [DecidableEq V] in
private theorem connected_insert_bridge_case_left
{G : Graph V E} {A : Finset E} {e f : E} (hfA : f ∈ A)
(hleft : G.ConnectedIn (A.erase f) (G.src f) (G.src e))
(hright : G.ConnectedIn (A.erase f) (G.dst e) (G.dst f)) :
G.ConnectedIn A (G.src e) (G.dst e) := by
have h₁ : G.ConnectedIn A (G.src e) (G.src f) :=
Graph.connected_symm (Graph.connected_mono (Finset.erase_subset f A) hleft)
have hf : G.ConnectedIn A (G.src f) (G.dst f) :=
Graph.connected_of_mem_edge hfA
have h₂ : G.ConnectedIn A (G.dst f) (G.dst e) :=
Graph.connected_symm (Graph.connected_mono (Finset.erase_subset f A) hright)
exact Graph.connected_trans (Graph.connected_trans h₁ hf) h₂omit [DecidableEq V] in
private theorem connected_insert_bridge_case_right
{G : Graph V E} {A : Finset E} {e f : E} (hfA : f ∈ A)
(hleft : G.ConnectedIn (A.erase f) (G.src f) (G.dst e))
(hright : G.ConnectedIn (A.erase f) (G.src e) (G.dst f)) :
G.ConnectedIn A (G.src e) (G.dst e) := by
have h₁ : G.ConnectedIn A (G.src e) (G.dst f) :=
Graph.connected_mono (Finset.erase_subset f A) hright
have hf : G.ConnectedIn A (G.dst f) (G.src f) :=
Graph.connected_symm (Graph.connected_of_mem_edge hfA)
have h₂ : G.ConnectedIn A (G.src f) (G.dst e) :=
Graph.connected_mono (Finset.erase_subset f A) hleft
exact Graph.connected_trans (Graph.connected_trans h₁ hf) h₂Inserting an edge whose endpoints are disconnected preserves the edge-removal forest invariant.
theorem isForest_insert_of_not_connected (G : FiniteGraph V E)
{A : Finset E} {e : E} (hforest : G.IsForest A)
(hnot : ¬ G.toGraph.ConnectedIn A (G.src e) (G.dst e)) :
G.IsForest (insert e A) := by
have heA : e ∉ A := by
intro he
exact hnot (Graph.connected_of_mem_edge he)
intro f hf hconn
rw [Finset.mem_insert] at hf
rcases hf with hfe | hfA
· subst f
have herase : (insert e A).erase e = A :=
connected_insert_erase_self_eq (A := A) (e := e) heA
exact hnot (by simpa [herase] using hconn)
· have hfe : f ≠ e := by
intro h
exact heA (h ▸ hfA)
have hef : e ≠ f := Ne.symm hfe
have herase : (insert e A).erase f = insert e (A.erase f) :=
erase_insert_comm_of_ne hef
have hconn' :
G.toGraph.ConnectedIn (insert e (A.erase f)) (G.src f) (G.dst f) := by
simpa [herase] using hconn
rcases Graph.connected_insert_edge_cases hconn' with hbase |
⟨⟨hleft, hright⟩ | ⟨hleft, hright⟩⟩
· exact hforest f hfA hbase
· exact hnot (connected_insert_bridge_case_left hfA hleft hright)
· exact hnot (connected_insert_bridge_case_right hfA hleft hright)The edge-removal forest invariant is downward closed under edge subsets.
theorem isForest_mono (G : FiniteGraph V E) {A B : Finset E}
(hforest : G.IsForest B) (hAB : A ⊆ B) :
G.IsForest A := by
intro e heA hconn
have hsubset : A.erase e ⊆ B.erase e := by
intro x hx
exact Finset.mem_erase.mpr
⟨(Finset.mem_erase.mp hx).1, hAB (Finset.mem_of_mem_erase hx)⟩
exact hforest e (hAB heA) (Graph.connected_mono hsubset hconn)
Finite-graph bridge from a cycle-style connection to the reusable
ExchangePath certificate. In a spanning tree, deleting f
disconnects its endpoints; if inserting e reconnects them, Lean can
decompose that connection into the two sides of the exchange path.
theorem exchangePath_of_insert_connects_erased_edge (G : FiniteGraph V E)
{T : Finset E} {e f : E}
(hT : G.IsSpanningTree T) (hfT : f ∈ T)
(hconn :
G.toGraph.ConnectedIn (insert e (T.erase f)) (G.src f) (G.dst f)) :
G.toGraph.ExchangePath T e f := by
exact Graph.exchangePath_of_insert_connected hconn (hT.2.2 f hfT)
Named finite-graph wrapper for the compact inserted-edge connection interface.
In a spanning tree, erasing f disconnects its endpoints, so the compact
cycle-style witness is equivalent to an ExchangePath certificate.
theorem exchangePath_iff_insertedEdgeConnection_of_spanningTree
(G : FiniteGraph V E) {T : Finset E} {e f : E}
(hT : G.IsSpanningTree T) (hfT : f ∈ T) :
G.toGraph.ExchangePath T e f ↔ G.toGraph.InsertedEdgeConnection T e f :=
Graph.exchangePath_iff_insertedEdgeConnection (hT.2.2 f hfT)
Finite-graph bridge from the named inserted-edge connection to the reusable
ExchangePath certificate.
theorem exchangePath_of_insertedEdgeConnection (G : FiniteGraph V E)
{T : Finset E} {e f : E}
(hT : G.IsSpanningTree T) (hfT : f ∈ T)
(hconn : G.toGraph.InsertedEdgeConnection T e f) :
G.toGraph.ExchangePath T e f :=
(G.exchangePath_iff_insertedEdgeConnection_of_spanningTree hT hfT).2 hconn
If a path-decomposition certificate says that new edge e reconnects the
two components produced by deleting tree edge f, then replacing
f by e preserves the finite-graph spanning-tree property.
theorem spanningTree_exchange_of_path_certificate (G : FiniteGraph V E)
{T : Finset E} {e f : E}
(hT : G.IsSpanningTree T) (heG : e ∈ G.edges) (hfT : f ∈ T)
(hpath : G.toGraph.ExchangePath T e f) :
G.IsSpanningTree (insert e (T.erase f)) := by
have hnew_subset : insert e (T.erase f) ⊆ G.edges := by
intro x hx
rw [Finset.mem_insert] at hx
rcases hx with hxe | hxT
· exact hxe ▸ heG
· exact hT.1 (Finset.mem_of_mem_erase hxT)
have hnot_connected :
¬ G.toGraph.ConnectedIn (T.erase f) (G.src e) (G.dst e) := by
intro he_conn
have hf_conn : G.toGraph.ConnectedIn (T.erase f) (G.src f) (G.dst f) := by
rcases hpath with ⟨hleft, hright⟩ | ⟨hleft, hright⟩
· exact Graph.connected_trans (Graph.connected_trans hleft he_conn) hright
· exact Graph.connected_trans (Graph.connected_trans hleft
(Graph.connected_symm he_conn)) hright
exact hT.2.2 f hfT hf_conn
have hforest_erase : G.IsForest (T.erase f) :=
G.isForest_mono hT.2.2 (Finset.erase_subset f T)
have hforest_new : G.IsForest (insert e (T.erase f)) :=
G.isForest_insert_of_not_connected hforest_erase hnot_connected
have hedge :
∀ g, g ∈ T →
G.toGraph.ConnectedIn (insert e (T.erase f)) (G.src g) (G.dst g) := by
intro g hgT
by_cases hgf : g = f
· subst g
exact Graph.exchangePath_connected_insert hpath
· have hgErase : g ∈ T.erase f := Finset.mem_erase.mpr ⟨hgf, hgT⟩
have hgNew : g ∈ insert e (T.erase f) := Finset.mem_insert_of_mem hgErase
exact Graph.connected_of_mem_edge hgNew
have hspans_new : G.Spans (insert e (T.erase f)) := by
intro u hu v hv
exact Graph.connected_of_edgewise_connected hedge (hT.2.1 u hu v hv)
exact ⟨hnew_subset, hspans_new, hforest_new⟩Cut-local exchange certificate from an explicit path-decomposition certificate. This packages the reusable finite-graph part needed by the CLRS safe-edge theorem.
theorem cut_exchange_certificate (G : FiniteGraph V E)
{A T : Finset E} {S : Finset V} {e f : E}
(hT : G.IsSpanningTree T) (hAT : A ⊆ T)
(hrespects : G.toGraph.Respects S A)
(heG : e ∈ G.edges) (hfT : f ∈ T)
(hfCross : G.toGraph.Crosses S f)
(hpath : G.toGraph.ExchangePath T e f) :
f ∈ T ∧ G.toGraph.Crosses S f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f) := by
have hf_not_A : f ∉ A := by
intro hfA
exact hrespects f hfA hfCross
refine ⟨hfT, hfCross,
G.spanningTree_exchange_of_path_certificate hT heG hfT hpath, ?_⟩
intro x hxA
exact Finset.mem_insert_of_mem
(Finset.mem_erase.mpr ⟨fun hxf => hf_not_A (hxf ▸ hxA), hAT hxA⟩)
Existential replacement form: once a crossing tree edge is accompanied by an
ExchangePath certificate, Lean constructs the exchanged spanning tree
and proves that the accepted prefix is preserved.
theorem exists_replacement_spanning_tree_of_cut (G : FiniteGraph V E)
{A T : Finset E} {S : Finset V} {e : E}
(hT : G.IsSpanningTree T) (hAT : A ⊆ T)
(hrespects : G.toGraph.Respects S A) (heG : e ∈ G.edges)
(hpath :
∃ f, f ∈ T ∧ G.toGraph.Crosses S f ∧
G.toGraph.ExchangePath T e f) :
∃ f, f ∈ T ∧ G.toGraph.Crosses S f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f) := by
rcases hpath with ⟨f, hfT, hfCross, hcert⟩
exact ⟨f, G.cut_exchange_certificate hT hAT hrespects heG hfT hfCross hcert⟩Finite-graph cut certificate from a light crossing edge and explicit exchange paths for optimum trees. This is the bridge between the mathematical path/cycle exchange argument and the abstract safe-edge theorem.
theorem cutCertificate_of_lightest_crossing (G : FiniteGraph V E)
{w : E → Nat} {A : Finset E} {S : Finset V} {e : E}
(heG : e ∈ G.edges) (hcross : G.toGraph.Crosses S e)
(hrespects : G.toGraph.Respects S A)
(hlight : ∀ f, G.toGraph.Crosses S f → w e ≤ w f)
(hexchangePath :
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses S f ∧
G.toGraph.ExchangePath T e f) :
CutCertificate G.toGraph G.toProblem w A S e := by
refine ⟨hcross, hrespects, hlight, ?_⟩
intro T hT heT
rcases hexchangePath T hT heT with ⟨f, hfT, hfCross, hpath⟩
rcases G.cut_exchange_certificate hT.tree hT.includes hrespects
heG hfT hfCross hpath with
⟨hfT', hfCross', htree, hextends⟩
exact ⟨f, hfT', hfCross', htree, hextends⟩Finite-graph cut certificate with the exchange path generated automatically from the canonical simple path in each optimum tree.
theorem cutCertificate_of_lightest_crossing_auto (G : FiniteGraph V E)
{w : E → Nat} {A : Finset E} {S : Finset V} {e : E}
(heG : e ∈ G.edges) (hcross : G.toGraph.Crosses S e)
(hrespects : G.toGraph.Respects S A)
(hlight : ∀ f, G.toGraph.Crosses S f → w e ≤ w f) :
CutCertificate G.toGraph G.toProblem w A S e := by
exact G.cutCertificate_of_lightest_crossing heG hcross hrespects hlight
(by
intro T hT _heT
exact G.exists_crossing_exchangePath_of_spanningTree hT.tree heG hcross)The finite-graph CLRS cut property with no user-supplied cycle-exchange certificate.
theorem safeEdge_of_lightest_crossing_auto (G : FiniteGraph V E)
{w : E → Nat} {A : Finset E} {S : Finset V} {e : E}
(heG : e ∈ G.edges) (hcross : G.toGraph.Crosses S e)
(hrespects : G.toGraph.Respects S A)
(hlight : ∀ f, G.toGraph.Crosses S f → w e ≤ w f) :
SafeEdge G.toProblem w A e :=
safe_edge_of_lightest_crossing
(G.cutCertificate_of_lightest_crossing_auto heG hcross hrespects hlight)Exact-component Kruskal prefix certificate with both processed-prefix lightness and the tree-exchange witness discharged internally.
theorem cutCertificate_of_exactComponentKruskalPrefix_auto
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
{processed suffix : List E} {A : Finset E} {e : E}
(heG : e ∈ G.edges)
(haccept :
acceptByComponent G.toGraph C
(kruskal (acceptByComponent G.toGraph C) processed A) e = true)
(hsorted : WeightSorted w (processed ++ e :: suffix))
(hall :
∀ f,
G.toGraph.Crosses
(C.component (kruskal (acceptByComponent G.toGraph C) processed A)
(G.src e)) f →
f ∈ processed ++ e :: suffix) :
CutCertificate G.toGraph G.toProblem w
(kruskal (acceptByComponent G.toGraph C) processed A)
(C.component (kruskal (acceptByComponent G.toGraph C) processed A)
(G.src e)) e := by
have hnotMem :
G.dst e ∉ C.component
(kruskal (acceptByComponent G.toGraph C) processed A) (G.src e) :=
not_mem_component_of_accept haccept
have hcross :
G.toGraph.Crosses
(C.component (kruskal (acceptByComponent G.toGraph C) processed A)
(G.src e)) e :=
Or.inl ⟨C.mem_self _ _, hnotMem⟩
exact G.cutCertificate_of_lightest_crossing_auto heG hcross
(C.respects _ _)
(lightest_crossing_of_exact_component_kruskal_prefix C hexact hsorted hall)Recursive safe-edge induction for one fixed sorted Kruskal edge order. The processed-prefix exclusion and cycle-exchange certificate are both constructed at the point where an edge is accepted.
private theorem kruskal_preserves_mst_sorted_exact_aux
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(processed suffix : List E) {A₀ T : Finset E}
(hsorted : WeightSorted w (processed ++ suffix))
(hall : ∀ S f, G.toGraph.Crosses S f → f ∈ processed ++ suffix)
(hedges : ∀ e, e ∈ processed ++ suffix → e ∈ G.edges)
(hcur : IsMSTExtending G.toProblem w
(kruskal (acceptByComponent G.toGraph C) processed A₀) T)
(hbase : IsMSTExtending G.toProblem w A₀ T) :
∃ T', IsMSTExtending G.toProblem w A₀ T' ∧
IsMSTExtending G.toProblem w
(kruskal (acceptByComponent G.toGraph C) (processed ++ suffix) A₀) T' := by
induction suffix generalizing processed T with
| nil =>
exact ⟨T, hbase, by simpa using hcur⟩
| cons e suffix ih =>
let accept := acceptByComponent G.toGraph C
let A := kruskal accept processed A₀
by_cases hacc : accept A e = true
· have heG : e ∈ G.edges := hedges e (by simp)
have hcut : CutCertificate G.toGraph G.toProblem w A
(C.component A (G.src e)) e := by
simpa [accept, A] using
(G.cutCertificate_of_exactComponentKruskalPrefix_auto C hexact
heG hacc hsorted (by
intro f hf
exact hall _ f hf))
rcases (safe_edge_of_lightest_crossing hcut) T hcur with
⟨T₁, hnext, hprefix⟩
have hA₀A : A₀ ⊆ A := by
exact kruskal_extends_start accept processed A₀
have hbase₁ : IsMSTExtending G.toProblem w A₀ T₁ :=
optimal_for_smaller_prefix hA₀A hcur hbase hprefix
have hprocessed :
kruskal accept (processed ++ [e]) A₀ = insert e A := by
rw [kruskal_append]
simp [kruskal, hacc, A]
have hnext' : IsMSTExtending G.toProblem w
(kruskal accept (processed ++ [e]) A₀) T₁ := by
rw [hprocessed]
exact hnext
have hsorted' : WeightSorted w ((processed ++ [e]) ++ suffix) := by
simpa [List.append_assoc] using hsorted
have hall' : ∀ S f, G.toGraph.Crosses S f →
f ∈ (processed ++ [e]) ++ suffix := by
intro S f hf
simpa [List.append_assoc] using hall S f hf
have hedges' : ∀ f, f ∈ (processed ++ [e]) ++ suffix →
f ∈ G.edges := by
intro f hf
exact hedges f (by simpa [List.append_assoc] using hf)
have hrec := ih (processed := processed ++ [e]) (T := T₁)
hsorted' hall' hedges' hnext' hbase₁
simpa [List.append_assoc] using hrec
· have hfalse : accept A e = false := by
cases h : accept A e <;> simp [h] at hacc ⊢
have hprocessed : kruskal accept (processed ++ [e]) A₀ = A := by
rw [kruskal_append]
simp [kruskal, hfalse, A]
have hcur' : IsMSTExtending G.toProblem w
(kruskal accept (processed ++ [e]) A₀) T := by
rw [hprocessed]
exact hcur
have hsorted' : WeightSorted w ((processed ++ [e]) ++ suffix) := by
simpa [List.append_assoc] using hsorted
have hall' : ∀ S f, G.toGraph.Crosses S f →
f ∈ (processed ++ [e]) ++ suffix := by
intro S f hf
simpa [List.append_assoc] using hall S f hf
have hedges' : ∀ f, f ∈ (processed ++ [e]) ++ suffix →
f ∈ G.edges := by
intro f hf
exact hedges f (by simpa [List.append_assoc] using hf)
have hrec := ih (processed := processed ++ [e]) (T := T)
hsorted' hall' hedges' hcur' hbase
simpa [List.append_assoc] using hrecA sorted exact-component Kruskal pass preserves an optimum witness while deriving every local light-edge and exchange obligation internally.
theorem kruskal_preserves_mst_of_sorted_exact_component
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) {A₀ T₀ : Finset E}
(hsorted : WeightSorted w edges)
(hall : ∀ S f, G.toGraph.Crosses S f → f ∈ edges)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hstart : IsMSTExtending G.toProblem w A₀ T₀) :
∃ T, IsMSTExtending G.toProblem w A₀ T ∧
IsMSTExtending G.toProblem w
(kruskal (acceptByComponent G.toGraph C) edges A₀) T := by
simpa using
(kruskal_preserves_mst_sorted_exact_aux G C hexact [] edges
hsorted hall hedges hstart hstart)Prefix-local sorted lightness plus canonical exchange paths prove Kruskal optimality once the accepted set is known to be a spanning tree.
theorem kruskal_optimal_of_sorted_exact_component
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) {A₀ T₀ : Finset E}
(hsorted : WeightSorted w edges)
(hall : ∀ S f, G.toGraph.Crosses S f → f ∈ edges)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hfinal : G.IsSpanningTree
(kruskal (acceptByComponent G.toGraph C) edges A₀)) :
IsMSTExtending G.toProblem w A₀
(kruskal (acceptByComponent G.toGraph C) edges A₀) := by
rcases G.kruskal_preserves_mst_of_sorted_exact_component C hexact edges
hsorted hall hedges hstart with ⟨T, hglobal, hprefix⟩
have hEq : T = kruskal (acceptByComponent G.toGraph C) edges A₀ :=
G.spanning_tree_maximal hfinal hprefix.tree hprefix.includes
simpa [hEq] using hglobalAn exact-component Kruskal pass preserves the forest invariant: every accepted edge joins two previously disconnected components.
theorem kruskal_forest_of_exact_component (G : FiniteGraph V E)
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) {A : Finset E} (hforest : G.IsForest A) :
G.IsForest (kruskal (acceptByComponent G.toGraph C) edges A) := by
induction edges generalizing A with
| nil =>
simpa [kruskal] using hforest
| cons e es ih =>
by_cases hacc : acceptByComponent G.toGraph C A e = true
· have hnot_mem : G.dst e ∉ C.component A (G.src e) :=
not_mem_component_of_accept hacc
have hnot_connected :
¬ G.toGraph.ConnectedIn A (G.src e) (G.dst e) := by
intro hconn
exact hnot_mem ((hexact A (G.src e) (G.dst e)).2 hconn)
have hforest_insert : G.IsForest (insert e A) :=
G.isForest_insert_of_not_connected hforest hnot_connected
simpa [kruskal, hacc] using ih hforest_insert
· have hfalse : acceptByComponent G.toGraph C A e = false := by
cases h : acceptByComponent G.toGraph C A e <;> simp [h] at hacc ⊢
simpa [kruskal, hfalse] using ih hforestA finite-graph Kruskal run selects only graph edges, provided the initial set and scanned list contain only graph edges.
theorem kruskal_subset_edges (G : FiniteGraph V E)
{accept : Finset E → E → Bool} (edges : List E) {A : Finset E}
(hA : A ⊆ G.edges) (hedges : ∀ e, e ∈ edges → e ∈ G.edges) :
kruskal accept edges A ⊆ G.edges :=
CLRS.MST.kruskal_subset_of_start_and_edges accept edges hA hedgesIf the edge list contains every graph edge and the full graph is connected, then an exact-component Kruskal pass spans the finite graph.
theorem kruskal_spans_of_complete_exact_component (G : FiniteGraph V E)
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) (A : Finset E)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
G.Spans (kruskal (acceptByComponent G.toGraph C) edges A) := by
intro u hu v hv
refine Graph.connected_of_edgewise_connected ?_ (hconnected u hu v hv)
intro e heG
exact processed_edge_connected_of_exact_component_kruskal C hexact edges A e
(hcomplete e heG)A complete exact-component Kruskal scan starting from a forest returns a spanning tree of a connected finite graph.
theorem kruskal_spanning_tree_of_complete_exact_component
(G : FiniteGraph V E) (C : ComponentOracle G.toGraph)
(hexact : ExactComponentOracle G.toGraph C) (edges : List E)
{A : Finset E}
(hA : A ⊆ G.edges) (hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges)
(hforest : G.IsForest A) :
G.IsSpanningTree (kruskal (acceptByComponent G.toGraph C) edges A) := by
exact ⟨G.kruskal_subset_edges edges hA hedges,
G.kruskal_spans_of_complete_exact_component C hexact edges A hcomplete
hconnected,
G.kruskal_forest_of_exact_component C hexact edges hforest⟩End-to-end Kruskal optimality from a sorted complete edge order. Unlike the older generic wrapper, this theorem constructs prefix-local lightness and cycle exchange internally and discharges the final spanning-tree condition.
theorem kruskal_optimal_of_sorted_complete_exact_component
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) {A₀ T₀ : Finset E}
(hsorted : WeightSorted w edges)
(hall : ∀ S f, G.toGraph.Crosses S f → f ∈ edges)
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hA₀ : A₀ ⊆ G.edges) (hforest : G.IsForest A₀)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
IsMSTExtending G.toProblem w A₀
(kruskal (acceptByComponent G.toGraph C) edges A₀) := by
exact G.kruskal_optimal_of_sorted_exact_component C hexact edges hsorted
hall hedges hstart
(G.kruskal_spanning_tree_of_complete_exact_component C hexact edges hA₀
hedges hcomplete hconnected hforest)Reader-facing minimum-spanning-tree theorem for sorted complete Kruskal from the empty forest, with no manual lightness or exchange hypotheses.
theorem kruskal_minimum_spanning_tree_of_sorted_complete_exact_component_empty
(G : FiniteGraph V E) {w : E → Nat}
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(edges : List E) {T₀ : Finset E}
(hsorted : WeightSorted w edges)
(hall : ∀ S f, G.toGraph.Crosses S f → f ∈ edges)
(hstart : IsMSTExtending G.toProblem w ∅ T₀)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
G.IsMinimumSpanningTree w
(kruskal (acceptByComponent G.toGraph C) edges ∅) := by
exact G.minimumSpanningTree_of_mstExtending_empty
(G.kruskal_optimal_of_sorted_complete_exact_component C hexact edges
hsorted hall hstart (by simp) G.isForest_empty hedges hcomplete hconnected)Finite-graph Kruskal optimality. The concrete spanning-tree definition discharges the abstract maximality side condition.
theorem kruskal_optimal (G : FiniteGraph V E) {w : E → Nat}
{accept : Finset E → E → Bool}
(cert : KruskalCertificate G.toProblem w accept)
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hfinal_tree : G.IsSpanningTree (kruskal accept edges A₀)) :
IsMSTExtending G.toProblem w A₀ (kruskal accept edges A₀) := by
exact CLRS.MST.kruskal_optimal cert edges hstart hfinal_tree
(by
intro T hT hsub
exact G.spanning_tree_maximal hfinal_tree hT hsub)theorem kruskal_optimal_of_component_oracle (G : FiniteGraph V E)
{w : E → Nat} (C : ComponentOracle G.toGraph)
(hlight :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hfinal_tree : G.IsSpanningTree (kruskal (acceptByComponent G.toGraph C) edges A₀)) :
IsMSTExtending G.toProblem w A₀
(kruskal (acceptByComponent G.toGraph C) edges A₀) := by
exact CLRS.MST.kruskal_optimal_of_component_oracle (G := G.toGraph)
(P := G.toProblem) (w := w) C hlight hexchange edges hstart hfinal_tree
(by
intro T hT hsub
exact G.spanning_tree_maximal hfinal_tree hT hsub)Finite-graph Kruskal optimality with the final spanning-tree side condition discharged from exact components, a complete edge scan, graph connectedness, and an initial forest.
theorem kruskal_optimal_of_complete_exact_component (G : FiniteGraph V E)
{w : E → Nat} (C : ComponentOracle G.toGraph)
(hexact : ExactComponentOracle G.toGraph C)
(hlight :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hA₀ : A₀ ⊆ G.edges) (hforest : G.IsForest A₀)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
IsMSTExtending G.toProblem w A₀
(kruskal (acceptByComponent G.toGraph C) edges A₀) := by
exact G.kruskal_optimal_of_component_oracle C hlight hexchange edges hstart
(G.kruskal_spanning_tree_of_complete_exact_component C hexact edges hA₀
hedges hcomplete hconnected hforest)Standard empty-prefix form of the complete exact-component Kruskal theorem.
theorem kruskal_optimal_of_complete_exact_component_empty (G : FiniteGraph V E)
{w : E → Nat} (C : ComponentOracle G.toGraph)
(hexact : ExactComponentOracle G.toGraph C)
(hlight :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w ∅ T₀)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
IsMSTExtending G.toProblem w ∅
(kruskal (acceptByComponent G.toGraph C) edges ∅) := by
exact G.kruskal_optimal_of_complete_exact_component C hexact hlight hexchange
edges hstart (by simp) G.isForest_empty hedges hcomplete hconnectedReader-facing finite-graph MST theorem for a complete exact-component Kruskal scan from the empty prefix.
theorem kruskal_minimum_spanning_tree_of_complete_exact_component_empty
(G : FiniteGraph V E) {w : E → Nat} (C : ComponentOracle G.toGraph)
(hexact : ExactComponentOracle G.toGraph C)
(hlight :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, acceptByComponent G.toGraph C A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w ∅ T₀)
(hedges : ∀ e, e ∈ edges → e ∈ G.edges)
(hcomplete : ∀ e, e ∈ G.edges → e ∈ edges)
(hconnected : G.Spans G.edges) :
G.IsMinimumSpanningTree w
(kruskal (acceptByComponent G.toGraph C) edges ∅) := by
exact G.minimumSpanningTree_of_mstExtending_empty
(G.kruskal_optimal_of_complete_exact_component_empty C hexact hlight
hexchange edges hstart hedges hcomplete hconnected)theorem kruskal_optimal_of_cycle_test (G : FiniteGraph V E)
{w : E → Nat} {C : ComponentOracle G.toGraph}
(impl : CycleTestImplementation G.toGraph C)
(hlight :
∀ A e, impl.accept A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, impl.accept A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {A₀ T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w A₀ T₀)
(hfinal_tree : G.IsSpanningTree (kruskal impl.accept edges A₀)) :
IsMSTExtending G.toProblem w A₀ (kruskal impl.accept edges A₀) := by
exact CLRS.MST.kruskal_optimal_of_cycle_test (G := G.toGraph)
(P := G.toProblem) (w := w) impl hlight hexchange edges hstart hfinal_tree
(by
intro T hT hsub
exact G.spanning_tree_maximal hfinal_tree hT hsub)Reader-facing finite-graph MST theorem for any Kruskal cycle-test implementation, once the accepted edge set is known to be a spanning tree.
theorem kruskal_minimum_spanning_tree_of_cycle_test (G : FiniteGraph V E)
{w : E → Nat} {C : ComponentOracle G.toGraph}
(impl : CycleTestImplementation G.toGraph C)
(hlight :
∀ A e, impl.accept A e = true →
∀ f, G.toGraph.Crosses (C.component A (G.src e)) f → w e ≤ w f)
(hexchange :
∀ A e, impl.accept A e = true →
∀ T, IsMSTExtending G.toProblem w A T → e ∉ T →
∃ f, f ∈ T ∧ G.toGraph.Crosses (C.component A (G.src e)) f ∧
G.IsSpanningTree (insert e (T.erase f)) ∧
A ⊆ insert e (T.erase f))
(edges : List E) {T₀ : Finset E}
(hstart : IsMSTExtending G.toProblem w ∅ T₀)
(hfinal_tree : G.IsSpanningTree (kruskal impl.accept edges ∅)) :
G.IsMinimumSpanningTree w (kruskal impl.accept edges ∅) := by
exact G.minimumSpanningTree_of_mstExtending_empty
(G.kruskal_optimal_of_cycle_test impl hlight hexchange edges hstart
hfinal_tree)Prim's algorithm
A CLRS-valid Prim edge trace. At every step, the next graph edge crosses the cut induced by the current root component and is light among all edges crossing that cut.
def PrimTrace (G : FiniteGraph V E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : V) : List E → Finset E → Prop
| [], _ => True
| e :: es, A =>
e ∈ G.edges ∧
G.toGraph.Crosses (C.component A root) e ∧
(∀ f, G.toGraph.Crosses (C.component A root) f → w e ≤ w f) ∧
PrimTrace G C w root es (insert e A)A complete Prim run packages the dynamic light-edge trace and final coverage of the finite graph.
structure PrimCertificate (G : FiniteGraph V E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : V)
(start : Finset E) (choices : List E) : Prop where
root_mem : root ∈ G.vertices
trace : G.PrimTrace C w root choices start
spans : G.Spans (prim choices start)A valid Prim trace selects only graph edges when its initial edge set does.
theorem prim_subset_edges_of_trace (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} {w : E → Nat} {root : V}
{choices : List E} {A : Finset E}
(htrace : G.PrimTrace C w root choices A) (hA : A ⊆ G.edges) :
prim choices A ⊆ G.edges := by
induction choices generalizing A with
| nil => simpa [prim] using hA
| cons e choices ih =>
simp only [PrimTrace] at htrace
have hinsert : insert e A ⊆ G.edges :=
Finset.insert_subset htrace.1 hA
simpa [prim] using ih htrace.2.2.2 hinsertExact root components make every Prim edge join two previously disconnected components, so a valid Prim trace preserves the forest invariant.
theorem prim_forest_of_trace (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{w : E → Nat} {root : V} {choices : List E} {A : Finset E}
(htrace : G.PrimTrace C w root choices A) (hforest : G.IsForest A) :
G.IsForest (prim choices A) := by
induction choices generalizing A with
| nil => simpa [prim] using hforest
| cons e choices ih =>
simp only [PrimTrace] at htrace
have hnot : ¬ G.toGraph.ConnectedIn A (G.src e) (G.dst e) := by
intro hconn
exact (not_crosses_component_of_connected hexact hconn) htrace.2.1
have hinsert : G.IsForest (insert e A) :=
G.isForest_insert_of_not_connected hforest hnot
simpa [prim] using ih htrace.2.2.2 hinsertSafe-edge induction for a CLRS-valid Prim trace. Each step reuses the finite-graph automatic cut-property theorem.
theorem prim_preserves_mst (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} {w : E → Nat} {root : V}
{choices : List E} {A₀ A T : Finset E}
(htrace : G.PrimTrace C w root choices A)
(hA₀A : A₀ ⊆ A)
(hcur : IsMSTExtending G.toProblem w A T)
(hbase : IsMSTExtending G.toProblem w A₀ T) :
∃ T', IsMSTExtending G.toProblem w (prim choices A) T' ∧
IsMSTExtending G.toProblem w A₀ T' := by
induction choices generalizing A T with
| nil => exact ⟨T, by simpa [prim] using hcur, hbase⟩
| cons e choices ih =>
simp only [PrimTrace] at htrace
have hsafe : SafeEdge G.toProblem w A e :=
G.safeEdge_of_lightest_crossing_auto htrace.1 htrace.2.1
(C.respects A root) htrace.2.2.1
rcases hsafe T hcur with ⟨T₁, hnext, hprefix⟩
have hbase₁ : IsMSTExtending G.toProblem w A₀ T₁ :=
optimal_for_smaller_prefix hA₀A hcur hbase hprefix
have hA₀next : A₀ ⊆ insert e A :=
hA₀A.trans (Finset.subset_insert e A)
simpa [prim] using
ih htrace.2.2.2 hA₀next hnext hbase₁A complete exact-component Prim certificate produces a spanning tree.
theorem prim_spanning_tree_of_certificate (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{w : E → Nat} {root : V} {choices : List E} {A : Finset E}
(cert : G.PrimCertificate C w root A choices)
(hA : A ⊆ G.edges) (hforest : G.IsForest A) :
G.IsSpanningTree (prim choices A) := by
exact ⟨G.prim_subset_edges_of_trace cert.trace hA, cert.spans,
G.prim_forest_of_trace hexact cert.trace hforest⟩CLRS Prim correctness: every complete dynamic light-edge trace returns an optimum extending its initial forest.
theorem prim_optimal (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{w : E → Nat} {root : V} {choices : List E} {A T₀ : Finset E}
(cert : G.PrimCertificate C w root A choices)
(hstart : IsMSTExtending G.toProblem w A T₀)
(hA : A ⊆ G.edges) (hforest : G.IsForest A) :
IsMSTExtending G.toProblem w A (prim choices A) := by
rcases G.prim_preserves_mst cert.trace (Subset.rfl : A ⊆ A)
hstart hstart with ⟨T, hprefix, hglobal⟩
have hfinal : G.IsSpanningTree (prim choices A) :=
G.prim_spanning_tree_of_certificate hexact cert hA hforest
have hEq : T = prim choices A :=
G.spanning_tree_maximal hfinal hprefix.tree hprefix.includes
simpa [hEq] using hglobalReader-facing minimum-spanning-tree theorem for Prim from the empty forest. Dynamic cut crossing, lightness, acyclicity, and optimality are all discharged by the certificate and the shared cut-property stack.
theorem prim_minimum_spanning_tree (G : FiniteGraph V E)
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{w : E → Nat} {root : V} {choices : List E} {T₀ : Finset E}
(cert : G.PrimCertificate C w root ∅ choices)
(hstart : IsMSTExtending G.toProblem w ∅ T₀) :
G.IsMinimumSpanningTree w (prim choices ∅) := by
exact G.minimumSpanningTree_of_mstExtending_empty
(G.prim_optimal hexact cert hstart (by simp) G.isForest_empty)end FiniteGraphend MSTend CLRSDefinitions and proofs
CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.ArrayPrim.Correctness
Incremental array Prim constructs an MST
The proof follows the stored queue invariant and the real chosen parent edges. The component oracle is used only in propositions, never by this execution. Connectedness and the existing all-edge-label closure condition are graph assumptions. No completed certificate, spanning conclusion, or operation-count premise is supplied by a caller.
namespace CLRS.MST.ExecutablePrim.ArrayPrimopen Finsetvariable {n : Nat} {E : Type} [LinearOrder E]theorem Invariant.crossing_key {G : FiniteGraph (Fin n) E} {adj : Adjacency G}
{w : E → Nat} {S : Finset (Fin n)} {q : Cells n E} (h : Invariant adj w S q)
{e : E} (he : e ∈ G.edges) (hc : G.toGraph.Crosses S e) :
∃ v, (read q v).active = true ∧ (read q v).key ≤ (w e : Key) := by
let v := outsideVertex G.toGraph S e
have hv := (h.active v).2 (outsideVertex_not_mem hc)
refine ⟨v,hv,?_⟩
rcases hc with hc | hc
· apply h.covers (G.src e) hc.1 v e _ hv
apply (adj.mem_iff _ _ _).2
exact ⟨he, Or.inl ⟨rfl, by simp [v, outsideVertex, hc.1]⟩⟩
· apply h.covers (G.dst e) hc.1 v e _ hv
apply (adj.mem_iff _ _ _).2
exact ⟨he, Or.inr ⟨rfl, by simp [v, outsideVertex, hc.2]⟩⟩
theorem Invariant.stop_covers {G : FiniteGraph (Fin n) E} {adj : Adjacency G}
{w : E → Nat} {S : Finset (Fin n)} {q : Cells n E} (h : Invariant adj w S q)
(indices : List (Fin n)) (hfull : ∀ v, v ∈ indices)
(root : Fin n) (hroot : root ∈ G.vertices) (hrS : root ∈ S)
(hconnected : G.Spans G.edges)
(hstop : (scan q indices).choice = none ∨ ∃ u c,
(scan q indices).choice = some (u,c) ∧ c.parent = none) :
G.vertices ⊆ S := by
intro v hv
by_contra hvS
obtain ⟨e,he,hcross⟩ := Graph.connected_crosses_cut
(hconnected root hroot v hv) hrS hvS
obtain ⟨x,hx,hkey⟩ := h.crossing_key he hcross
rcases hstop with hn | ⟨u,c,hs,hp⟩
· have hf := (scan_none q indices).1 hn x (hfull x)
simp [hf] at hx
· obtain ⟨_,rfl,_,hmin⟩ := scan_some q indices u c hs
have ht := h.none_key u hp
have hm := (hmin x (hfull x) hx).trans hkey
rw [ht] at hm
simp at hmomit [LinearOrder E] in
private theorem endpoints_insert {G : Graph (Fin n) E} {S : Finset (Fin n)} {e : E}
(hc : G.Crosses S e) :
G.src e ∈ insert (outsideVertex G S e) S ∧
G.dst e ∈ insert (outsideVertex G S e) S := by
rcases hc with hc | hc <;> simp [outsideVertex, hc.1, hc.2]Sufficient fuel constructs both the light-edge trace and terminal coverage.
theorem run_correct {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(indices : List (Fin n)) (hfull : ∀ v, v ∈ indices)
(hexact : ExactComponentOracle G.toGraph C)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hroot : root ∈ G.vertices) (hconnected : G.Spans G.edges)
(fuel : Nat) (A : Finset E) (q : Cells n E)
(hinv : Invariant adj w (C.component A root) q)
(hA : ∀ f ∈ A, G.src f ∈ C.component A root ∧ G.dst f ∈ C.component A root)
(hfuel : (G.vertices \ C.component A root).card ≤ fuel) :
G.PrimTrace C w root (run adj w indices fuel q).edges A ∧
G.vertices ⊆ C.component (prim (run adj w indices fuel q).edges A) root := by
induction fuel generalizing A q with
| zero =>
refine ⟨trivial, ?_⟩
have hz : G.vertices \ C.component A root = ∅ :=
Finset.card_eq_zero.mp (by omega)
exact Finset.sdiff_eq_empty_iff_subset.mp hz
| succ fuel ih =>
cases hs : (scan q indices).choice with
| none =>
have hc := hinv.stop_covers indices hfull root hroot (C.mem_self A root)
hconnected (Or.inl hs)
simpa [run, hs, prim] using And.intro (show G.PrimTrace C w root [] A from trivial) hc
| some pair =>
rcases pair with ⟨u,c⟩
cases hp : c.parent with
| none =>
have hc := hinv.stop_covers indices hfull root hroot (C.mem_self A root)
hconnected (Or.inr ⟨u,c,hs,hp⟩)
simpa [run, hs, hp, prim] using And.intro (show G.PrimTrace C w root [] A from trivial) hc
| some e =>
obtain ⟨he,hcross,houtside,hlight⟩ := hinv.selected indices hfull hs hp
have hcomp : C.component (insert e A) root = insert u (C.component A root) := by
rw [component_insert_crossing hexact hcross hA, houtside]
have hnext : Invariant adj w (C.component (insert e A) root)
(advance adj w q u).cells := by
rw [hcomp]
exact advance_invariant adj w _ q u hinv
have hnextA : ∀ f ∈ insert e A,
G.src f ∈ C.component (insert e A) root ∧ G.dst f ∈ C.component (insert e A) root := by
intro f hf
rw [hcomp]
rcases mem_insert.mp hf with rfl | hf
· simpa [houtside] using endpoints_insert hcross
· exact ⟨mem_insert_of_mem (hA f hf).1, mem_insert_of_mem (hA f hf).2⟩
have hprogress := crossing_uncovered_lt hexact he hcross
have rest := ih (insert e A) (advance adj w q u).cells hnext hnextA (by omega)
constructor
· simp only [run, hs, hp]
exact ⟨he,hcross,fun f hc => hlight f (hall A f hc) hc,rest.1⟩
· simpa [run, hs, hp, prim] using rest.2The exact component of the empty selected-edge set is the singleton root.
theorem component_empty {G : FiniteGraph (Fin n) E} (C : ComponentOracle G.toGraph)
(hexact : ExactComponentOracle G.toGraph C) (root : Fin n) :
C.component ∅ root = {root} := by
ext v
rw [hexact, Graph.connected_empty_iff]
simp [eq_comm]
theorem execute_correct {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hexact : ExactComponentOracle G.toGraph C)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hroot : root ∈ G.vertices) (hconnected : G.Spans G.edges) :
G.PrimTrace C w root (execute adj w root).edges ∅ ∧
G.vertices ⊆ C.component (prim (execute adj w root).edges ∅) root := by
have hindex := indexPrefix_spec n (Nat.le_refl n)
have hinv : Invariant adj w (C.component ∅ root)
(advance adj w (initialCells n).1 root).cells := by
rw [component_empty C hexact root]
simpa using advance_invariant adj w ∅ (initialCells n).1 root (initialCells_invariant adj w)
apply run_correct adj C w root (indexPrefix n n).1
(fun v => (hindex.2.2 v).2 v.isLt) hexact hall hroot hconnected n ∅ _ hinv
· simp
· exact (Finset.card_le_card (Finset.subset_univ _)).trans (by simp)The same cached-array execution is a minimum spanning tree.
theorem execute_minimum_spanning_tree {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hexact : ExactComponentOracle G.toGraph C)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hroot : root ∈ G.vertices) (hconnected : G.Spans G.edges) :
G.IsMinimumSpanningTree w (prim (execute adj w root).edges ∅) := by
have hc := execute_correct adj C w root hexact hall hroot hconnected
exact minimum_spanning_tree_of_trace_covers hexact hroot hconnected hc.1 hc.2end CLRS.MST.ExecutablePrim.ArrayPrimCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.ArrayPrim.Execution
Incremental array Prim execution
A single prepared index list is reused by all extraction scans. The graph is
supplied as stored adjacency lists satisfying Adjacency.represents.
Initialization writes the queue cells and the index-list cells; there is no
conversion from an unordered edge-set representation inside this algorithm.
Each successful extraction deactivates one cell and reads just that vertex's
adjacency row. The loop returns its chosen edges, final array, and counters.
namespace CLRS.MST.ExecutablePrim.ArrayPrimopen Finsetvariable {n : Nat} {E : Type} [LinearOrder E]def indexPrefix (n : Nat) : Nat → List (Fin n) × Nat
| 0 => ([], 0)
| i + 1 =>
let old := indexPrefix n i
if h : i < n then (⟨i,h⟩ :: old.1, old.2 + 1) else old
theorem indexPrefix_spec (i : Nat) (hi : i ≤ n) :
(indexPrefix n i).1.length = i ∧ (indexPrefix n i).2 = i ∧
∀ v : Fin n, v ∈ (indexPrefix n i).1 ↔ v.val < i := by
induction i with
| zero => simp [indexPrefix]
| succ i ih =>
have old := ih (by omega)
have hin : i < n := by omega
simp only [indexPrefix, hin, ↓reduceDIte, List.length_cons, old.1, old.2.1]
refine ⟨trivial,trivial,?_⟩
intro v
simp only [List.mem_cons, old.2.2 v, Fin.ext_iff]
omegaThe counters refer to queue cells, adjacency rows, comparisons, and visits.
structure Result (n : Nat) (E : Type) where
edges : List E
cells : Cells n E
rounds : Nat
extracts : Nat
queueReads : Nat
queueWrites : Nat
comparisons : Nat
edgeVisits : Nat
adjacencyReads : Nat
preparationWrites : Nat
deriving Reprdef run {G : FiniteGraph (Fin n) E} (adj : Adjacency G) (w : E → Nat)
(indices : List (Fin n)) : Nat → Cells n E → Result n E
| 0, q => ⟨[],q,0,0,0,0,0,0,0,0⟩
| fuel + 1, q =>
let choice := scan q indices
match choice.choice with
| none => ⟨[],q,1,0,choice.reads,0,choice.comparisons,0,0,0⟩
| some (u,c) =>
match c.parent with
| none => ⟨[],q,1,0,choice.reads,0,choice.comparisons,0,0,0⟩
| some e =>
let next := advance adj w q u
let rest := run adj w indices fuel next.cells
⟨e :: rest.edges, rest.cells, rest.rounds + 1, rest.extracts + 1,
choice.reads + 1 + next.edgeVisits + rest.queueReads,
1 + next.writes + rest.queueWrites,
choice.comparisons + next.tests + rest.comparisons,
next.edgeVisits + rest.edgeVisits, rest.adjacencyReads + 1, 0⟩Start at the supplied root, scan its row, then allow n further extraction attempts.
def execute {G : FiniteGraph (Fin n) E} (adj : Adjacency G) (w : E → Nat)
(root : Fin n) : Result n E :=
let initial := initialCells (E := E) n
let indices := indexPrefix n n
let seed := advance adj w initial.1 root
let rest := run adj w indices.1 n seed.cells
{ rest with
extracts := rest.extracts + 1
queueReads := 1 + seed.edgeVisits + rest.queueReads
queueWrites := 1 + seed.writes + rest.queueWrites
comparisons := seed.tests + rest.comparisons
edgeVisits := seed.edgeVisits + rest.edgeVisits
adjacencyReads := rest.adjacencyReads + 1
preparationWrites := initial.2 + indices.2 }Active vertices are the remaining potential, weighted by any nonnegative cost.
def remaining (weight : Fin n → Nat) (q : Cells n E) : Nat :=
∑ v : Fin n, if (read q v).active then weight v else 0
omit [LinearOrder E] in
theorem remaining_deactivate (weight : Fin n → Nat) (q : Cells n E) (u : Fin n)
(hu : (read q u).active = true) :
remaining weight (deactivate q u) + weight u = remaining weight q := by
have hnew := Finset.sum_erase_add (Finset.univ : Finset (Fin n))
(fun v => if (read (deactivate q u) v).active then weight v else 0) (mem_univ u)
have hold := Finset.sum_erase_add (Finset.univ : Finset (Fin n))
(fun v => if (read q v).active then weight v else 0) (mem_univ u)
have hs : (∑ v ∈ Finset.univ.erase u,
if (read (deactivate q u) v).active then weight v else 0) =
∑ v ∈ Finset.univ.erase u, if (read q v).active then weight v else 0 := by
apply Finset.sum_congr rfl
intro v hv
have huv : u ≠ v := (Finset.ne_of_mem_erase hv).symm
simp [huv]
rw [hs] at hnew
simp only [deactivate_active, ↓reduceIte, Bool.false_eq_true, Nat.add_zero] at hnew
simp only [hu, ↓reduceIte] at hold
simp only [remaining, deactivate_active]
omega@[simp] theorem remaining_advance {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (weight : Fin n → Nat) (q : Cells n E) (u : Fin n) :
remaining weight (advance adj w q u).cells = remaining weight (deactivate q u) := by
simp [remaining, advance]A removed adjacency row is subtracted from the remaining scan potential.
theorem advance_remaining {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (q : Cells n E) (u : Fin n) (hu : (read q u).active = true) :
remaining (fun v => (adj.rows[v.val]).length) (advance adj w q u).cells +
(advance adj w q u).edgeVisits = remaining (fun v => (adj.rows[v.val]).length) q := by
rw [remaining_advance]
have hc := (relaxAll_counts w (deactivate q u) adj.rows[u.val]).1
change remaining _ (deactivate q u) +
(relaxAll w (deactivate q u) adj.rows[u.val]).edgeVisits = _
rw [hc]
exact remaining_deactivate _ q u huThe inequalities account for every counter emitted by the loop.
theorem run_counts {G : FiniteGraph (Fin n) E} (adj : Adjacency G) (w : E → Nat)
(indices : List (Fin n)) (fuel : Nat) (q : Cells n E) :
let r := run adj w indices fuel q
r.rounds ≤ fuel ∧
r.extracts + remaining (fun _ => 1) r.cells ≤ remaining (fun _ => 1) q ∧
r.edgeVisits + remaining (fun v => (adj.rows[v.val]).length) r.cells ≤
remaining (fun v => (adj.rows[v.val]).length) q ∧
r.queueReads ≤ fuel * indices.length + r.extracts + r.edgeVisits ∧
r.queueWrites ≤ r.extracts + r.edgeVisits ∧
r.comparisons ≤ fuel * indices.length + r.edgeVisits ∧
r.adjacencyReads = r.extracts ∧ r.preparationWrites = 0 := by
induction fuel generalizing q with
| zero => simp [run]
| succ fuel ih =>
have hc := scan_counts q indices
simp only [run, Nat.add_mul, Nat.one_mul]
split
· simp only
refine ⟨?_, ?_, ?_, ?_, ?_, ?_, trivial, trivial⟩ <;> omega
· rename_i u c hscan
have hu := (scan_some q indices u c hscan).2.2.1
have hcell := (scan_some q indices u c hscan).2.1
rw [hcell] at hu
split
· simp only
refine ⟨?_, ?_, ?_, ?_, ?_, ?_, trivial, trivial⟩ <;> omega
· have hi := ih (advance adj w q u).cells
have hp := advance_remaining adj w q u hu
have hv : remaining (fun _ => 1) (advance adj w q u).cells + 1 =
remaining (fun _ => 1) q := by
rw [remaining_advance]; exact remaining_deactivate _ q u hu
have ha := relaxAll_counts w (deactivate q u) adj.rows[u.val]
change (advance adj w q u).edgeVisits = _ ∧
(advance adj w q u).tests ≤ _ ∧
(advance adj w q u).writes ≤ (advance adj w q u).tests at ha
simp only
refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, trivial⟩ <;> omegaThe generated execution visits at most the input's two incidences per edge.
theorem execute_edgeVisits_le {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (root : Fin n) : (execute adj w root).edgeVisits ≤ 2 * G.edges.card := by
have hc := (run_counts adj w (indexPrefix n n).1 n
(advance adj w (initialCells n).1 root).cells).2.2.1
have hs := advance_remaining adj w (initialCells (E := E) n).1 root (by simp)
have ht : remaining (fun v => (adj.rows[v.val]).length) (initialCells (E := E) n).1 =
2 * G.edges.card := by simp [remaining, adj.total_length]
rw [ht] at hs
simp only [execute]
omegaEach active vertex is extracted at most once, including the initial root.
theorem execute_extracts_le {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (root : Fin n) : (execute adj w root).extracts ≤ n := by
have hc := (run_counts adj w (indexPrefix n n).1 n
(advance adj w (initialCells n).1 root).cells).2.1
have hs : remaining (fun _ => 1) (advance adj w (initialCells (E := E) n).1 root).cells + 1 = n := by
rw [remaining_advance]
simpa [remaining] using remaining_deactivate (fun _ => 1)
(initialCells (E := E) n).1 root (by simp)
simp only [execute]
omegaThe actual work units include preparation, array reads/writes, and key comparisons.
def cellWork (r : Result n E) : Nat :=
r.preparationWrites + r.queueReads + r.queueWrites + r.adjacencyReads + r.comparisons
theorem execute_cost_bound {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (root : Fin n) :
cellWork (execute adj w root) ≤ 2 * n * n + 5 * n + 6 * G.edges.card := by
have hi := indexPrefix_spec n (Nat.le_refl n)
have hc := run_counts adj w (indexPrefix n n).1 n
(advance adj w (initialCells n).1 root).cells
have hs := relaxAll_counts w (deactivate (initialCells (E := E) n).1 root)
adj.rows[root.val]
have hr := advance_remaining adj w (initialCells (E := E) n).1 root (by simp)
have hv : remaining (fun _ => 1) (advance adj w (initialCells (E := E) n).1 root).cells + 1 =
remaining (fun _ => 1) (initialCells (E := E) n).1 := by
rw [remaining_advance]; exact remaining_deactivate _ _ root (by simp)
have hinit : remaining (fun _ => 1) (initialCells (E := E) n).1 = n := by
simp [remaining]
have htotal : remaining (fun v => (adj.rows[v.val]).length) (initialCells (E := E) n).1 =
2 * G.edges.card := by simp [remaining, adj.total_length]
change (advance adj w (initialCells n).1 root).edgeVisits = _ ∧
(advance adj w (initialCells n).1 root).tests ≤ _ ∧
(advance adj w (initialCells n).1 root).writes ≤
(advance adj w (initialCells n).1 root).tests at hs
rw [hinit] at hv
rw [htotal] at hr
simp only [cellWork, execute, initialCells_writes, hi.1, hi.2.1] at *
nlinarith [hc.2.1, hc.2.2.1, hc.2.2.2.1, hc.2.2.2.2.1, hc.2.2.2.2.2.1]When the finite index universe is exactly the graph vertices, the bound uses |V|.
theorem execute_cost_bound_vertices {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (root : Fin n) (hV : G.vertices = Finset.univ) :
cellWork (execute adj w root) ≤
2 * G.vertices.card * G.vertices.card + 5 * G.vertices.card + 6 * G.edges.card := by
simpa [hV] using execute_cost_bound adj w rootend CLRS.MST.ExecutablePrim.ArrayPrimCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.ArrayPrim.Invariant
Adjacency representation and cached-cut invariant
The input is a stored array of adjacency lists. Its representation contract says that each graph edge contributes its two endpoint incidences, in any row order. Thus the total adjacency length is derived as twice the edge count; it is not a supplied bound on the execution's decreases.
namespace CLRS.MST.ExecutablePrim.ArrayPrimopen Finsetvariable {n : Nat} {E : Type} [LinearOrder E]def incidences (G : Graph (Fin n) E) (u : Fin n) (e : E) : List (Fin n × E) :=
(if G.src e = u then [(G.dst e,e)] else []) ++
(if G.dst e = u then [(G.src e,e)] else [])structure Adjacency (G : FiniteGraph (Fin n) E) where
rows : Vector (List (Fin n × E)) n
represents : ∀ u : Fin n, (rows[u.val]).Perm
((G.edges.sort (· ≤ ·)).flatMap (incidences G.toGraph u))
@[simp] theorem Adjacency.mem_iff {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(u v : Fin n) (e : E) :
(v,e) ∈ adj.rows[u.val] ↔ e ∈ G.edges ∧
((G.src e = u ∧ G.dst e = v) ∨ (G.dst e = u ∧ G.src e = v)) := by
rw [(adj.represents u).mem_iff]
simp only [List.mem_flatMap]
constructor
· rintro ⟨f,hf,h⟩
simp only [incidences, List.mem_append] at h
rcases h with h | h
· split at h
· simp only [List.mem_singleton, Prod.mk.injEq] at h
rcases h with ⟨rfl,rfl⟩
exact ⟨(G.edges.mem_sort (· ≤ ·)).1 hf, Or.inl ⟨by assumption,rfl⟩⟩
· simp at h
· split at h
· simp only [List.mem_singleton, Prod.mk.injEq] at h
rcases h with ⟨rfl,rfl⟩
exact ⟨(G.edges.mem_sort (· ≤ ·)).1 hf, Or.inr ⟨by assumption,rfl⟩⟩
· simp at h
· rintro ⟨he,h⟩
refine ⟨e, (G.edges.mem_sort (· ≤ ·)).2 he, ?_⟩
rcases h with ⟨hs,hd⟩ | ⟨hd,hs⟩ <;> simp [incidences, hs, hd]
theorem Adjacency.total_length {G : FiniteGraph (Fin n) E} (adj : Adjacency G) :
∑ u : Fin n, (adj.rows[u.val]).length = 2 * G.edges.card := by
have general (es : List E) :
∑ u : Fin n, (es.flatMap (incidences G.toGraph u)).length = 2 * es.length := by
induction es with
| nil => simp
| cons e es ih =>
simp only [List.flatMap_cons, List.length_append, Finset.sum_add_distrib, ih,
List.length_cons]
have h : ∑ u : Fin n, (incidences G.toGraph u e).length = 2 := by
simp only [incidences, List.length_append]
simp_rw [apply_ite List.length]
simp [Finset.sum_add_distrib, eq_comm]
rw [h]
omega
calc
_ = ∑ u : Fin n,
((G.edges.sort (· ≤ ·)).flatMap (incidences G.toGraph u)).length :=
Finset.sum_congr rfl (fun u _ => (adj.represents u).length_eq)
_ = _ := by simpa using general (G.edges.sort (· ≤ ·))All active cells describe the best known parent into the reached set.
structure Invariant {G : FiniteGraph (Fin n) E} (adj : Adjacency G) (w : E → Nat)
(S : Finset (Fin n)) (q : Cells n E) : Prop where
active : ∀ v, (read q v).active = true ↔ v ∉ S
parent : ∀ v e, (read q v).active = true → (read q v).parent = some e →
∃ u ∈ S, (v,e) ∈ adj.rows[u.val] ∧ (read q v).key = (w e : Key)
covers : ∀ u ∈ S, ∀ v e, (v,e) ∈ adj.rows[u.val] →
(read q v).active = true → (read q v).key ≤ (w e : Key)
none_key : ∀ v, (read q v).parent = none → (read q v).key = ⊤theorem initialCells_invariant {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) : Invariant adj w ∅ (initialCells n).1 := by
refine ⟨?_, ?_, ?_, ?_⟩ <;> simpRemove one vertex and scan only its cached adjacency list.
def advance {G : FiniteGraph (Fin n) E} (adj : Adjacency G) (w : E → Nat)
(q : Cells n E) (u : Fin n) : Relaxed n E :=
relaxAll w (deactivate q u) adj.rows[u.val]@[simp] theorem advance_active {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (q : Cells n E) (u v : Fin n) :
(read (advance adj w q u).cells v).active =
if u = v then false else (read q v).active := by simp [advance]
theorem advance_invariant {G : FiniteGraph (Fin n) E} (adj : Adjacency G)
(w : E → Nat) (S : Finset (Fin n)) (q : Cells n E) (u : Fin n)
(h : Invariant adj w S q) : Invariant adj w (insert u S) (advance adj w q u).cells := by
have ha (v : Fin n) : (read (advance adj w q u).cells v).active = true ↔
u ≠ v ∧ (read q v).active = true := by
by_cases huv : u = v <;> simp [huv]
refine ⟨?_, ?_, ?_, ?_⟩
· intro v
rw [ha, h.active]
simp [eq_comm]
· intro v e hv hp
obtain ⟨huv,hvold⟩ := (ha v).1 hv
rcases relaxAll_origin w (deactivate q u) adj.rows[u.val] v with hold | ⟨f,hf,hcell⟩
· have hpold : (read q v).parent = some e := by
change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).parent = _ at hp
rw [hold, deactivate_parent] at hp
exact hp
obtain ⟨x,hx,he,hkey⟩ := h.parent v e hvold hpold
refine ⟨x, mem_insert_of_mem hx, he, ?_⟩
change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).key = _
rw [hold, deactivate_key, hkey]
· have hfe : f = e := by
change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).parent = _ at hp
rw [hcell] at hp
exact Option.some.inj hp
subst f
exact ⟨u, mem_insert_self _ _, hf, congrArg Cell.key hcell⟩
· intro x hx v e he hv
obtain ⟨huv,hvold⟩ := (ha v).1 hv
rcases mem_insert.mp hx with hx | hx
· subst x
apply relaxAll_target_le w (deactivate q u) _ v e he
simpa [huv] using hvold
· exact (relaxAll_key_le w (deactivate q u) _ v).trans
(by simpa using h.covers x hx v e he hvold)
· intro v hp
rcases relaxAll_origin w (deactivate q u) adj.rows[u.val] v with hold | ⟨e,he,hcell⟩
· have hpold : (read q v).parent = none := by
change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).parent = _ at hp
rw [hold, deactivate_parent] at hp
exact hp
change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).key = _
rw [hold, deactivate_key, h.none_key v hpold]
· change (read (relaxAll w (deactivate q u) adj.rows[u.val]).cells v).parent = _ at hp
rw [hcell] at hp
contradictionSelecting a finite parent yields a real crossing edge and its outside vertex.
theorem Invariant.selected {G : FiniteGraph (Fin n) E} {adj : Adjacency G}
{w : E → Nat} {S : Finset (Fin n)} {q : Cells n E} (h : Invariant adj w S q)
(indices : List (Fin n)) (hfull : ∀ v, v ∈ indices)
{u : Fin n} {c : Cell E} {e : E}
(hs : (scan q indices).choice = some (u,c)) (hp : c.parent = some e) :
e ∈ G.edges ∧ G.toGraph.Crosses S e ∧ outsideVertex G.toGraph S e = u ∧
∀ f ∈ G.edges, G.toGraph.Crosses S f → w e ≤ w f := by
obtain ⟨_,rfl,hu,hmin⟩ := scan_some q _ u c hs
obtain ⟨x,hx,he,hkey⟩ := h.parent u e hu hp
have hout := (h.active u).1 hu
obtain ⟨heG,heEnds⟩ := adj.mem_iff x u e |>.1 he
have hc : G.toGraph.Crosses S e := by
rcases heEnds with ⟨hsrc,hdst⟩ | ⟨hdst,hsrc⟩
· exact Or.inl ⟨hsrc ▸ hx, hdst ▸ hout⟩
· exact Or.inr ⟨hdst ▸ hx, hsrc ▸ hout⟩
refine ⟨heG, hc, ?_, ?_⟩
· rcases heEnds with ⟨hsrc,hdst⟩ | ⟨hdst,hsrc⟩ <;>
simp [outsideVertex, hsrc, hdst, hx, hout]
· intro f hf hfc
let v := outsideVertex G.toGraph S f
have hv : v ∉ S := outsideVertex_not_mem hfc
have hvc := (h.active v).2 hv
have hcover : (read q v).key ≤ (w f : Key) := by
rcases hfc with hfc | hfc
· have hm : (v,f) ∈ adj.rows[(G.src f).val] := by
apply (adj.mem_iff _ _ _).2
exact ⟨hf, Or.inl ⟨rfl, by simp [v, outsideVertex, hfc.1]⟩⟩
exact h.covers _ hfc.1 v f hm hvc
· have hsrc : G.src f ∉ S := hfc.2
have hm : (v,f) ∈ adj.rows[(G.dst f).val] := by
apply (adj.mem_iff _ _ _).2
exact ⟨hf, Or.inr ⟨rfl, by simp [v, outsideVertex, hsrc]⟩⟩
exact h.covers _ hfc.1 v f hm hvc
have hm := hmin v (hfull v) hvc
rw [hkey] at hm
exact_mod_cast hm.trans hcoverend CLRS.MST.ExecutablePrim.ArrayPrimCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.ArrayPrim.Queue
Prim's cached array queue
The queue is an array-backed Vector, with one cell per vertex. Extraction
scans the array and carries the current minimum cell, so it never traverses a
chain of functional updates. Relaxation reads one target cell and writes it
only on a strict improvement. Input adjacency lists are stored separately.
namespace CLRS.MST.ExecutablePrim.ArrayPrimvariable {n : Nat} {E : Type}structure Cell (E : Type) where
active : Bool := true
key : Key := ⊤
parent : Option E := none
deriving Repr, DecidableEqabbrev Cells (n : Nat) (E : Type) := Vector (Cell E) ndef read (q : Cells n E) (v : Fin n) : Cell E := q[v.val]def write (q : Cells n E) (v : Fin n) (c : Cell E) : Cells n E := q.set v.val c@[simp] theorem read_write (q : Cells n E) (u v : Fin n) (c : Cell E) :
read (write q u c) v = if u = v then c else read q v := by
simp only [read, write, Vector.getElem_set]
simp [Fin.ext_iff]Initialization appends each queue cell once, using the shared counted array builder.
def initialCells (n : Nat) : Cells n E × Nat :=
let b := CLRS.Chapter15.DPExecution.buildRow (fun _ => (({} : Cell E), 0)) n
(⟨b.cells, by simp [b]⟩, b.writes)@[simp] theorem initialCells_writes : (initialCells (E := E) n).2 = n := by
simp [initialCells]@[simp] theorem initialCells_read (v : Fin n) : read (initialCells (E := E) n).1 v = {} := by
simp [initialCells, read, CLRS.Chapter15.DPExecution.buildRow_cells]Deactivation is one cached-cell write, retaining the selected parent and key.
def deactivate (q : Cells n E) (v : Fin n) : Cells n E :=
write q v { read q v with active := false }@[simp] theorem deactivate_active (q : Cells n E) (u v : Fin n) :
(read (deactivate q u) v).active = if u = v then false else (read q v).active := by
by_cases h : u = v <;> simp [deactivate, h]@[simp] theorem deactivate_key (q : Cells n E) (u v : Fin n) :
(read (deactivate q u) v).key = (read q v).key := by
by_cases h : u = v <;> simp [deactivate, h]@[simp] theorem deactivate_parent (q : Cells n E) (u v : Fin n) :
(read (deactivate q u) v).parent = (read q v).parent := by
by_cases h : u = v <;> simp [deactivate, h]structure Scan (n : Nat) (E : Type) where
choice : Option (Fin n × Cell E)
reads : Nat
comparisons : Natdef scan (q : Cells n E) : List (Fin n) → Scan n E
| [] => ⟨none, 0, 0⟩
| v :: vs =>
let old := scan q vs
let cell := read q v
if cell.active then
match old.choice with
| none => ⟨some (v, cell), old.reads + 1, old.comparisons⟩
| some (u, prior) =>
⟨if cell.key ≤ prior.key then some (v, cell) else some (u, prior),
old.reads + 1, old.comparisons + 1⟩
else ⟨old.choice, old.reads + 1, old.comparisons⟩theorem scan_counts (q : Cells n E) (vs : List (Fin n)) :
(scan q vs).reads = vs.length ∧ (scan q vs).comparisons ≤ vs.length := by
induction vs with
| nil => simp [scan]
| cons v vs ih =>
simp only [scan]
split
· split <;> simp only [List.length_cons] <;> omega
· simp only [List.length_cons]; omegatheorem scan_none (q : Cells n E) (vs : List (Fin n)) :
(scan q vs).choice = none ↔ ∀ v ∈ vs, (read q v).active = false := by
induction vs with
| nil => simp [scan]
| cons v vs ih =>
simp only [scan]
split
· rename_i ha
split
· simp_all
· split <;> simp_all
· rename_i ha
have hf := Bool.eq_false_iff.mpr ha
simpa [hf] using ihtheorem scan_some (q : Cells n E) (vs : List (Fin n)) (u : Fin n) (c : Cell E)
(h : (scan q vs).choice = some (u,c)) :
u ∈ vs ∧ c = read q u ∧ c.active = true ∧
∀ v ∈ vs, (read q v).active = true → c.key ≤ (read q v).key := by
induction vs generalizing u c with
| nil => simp [scan] at h
| cons v vs ih =>
simp only [scan] at h
split at h
· rename_i ha
split at h
· rename_i hn
cases h
refine ⟨by simp, rfl, ha, ?_⟩
intro x hx hxactive
rcases List.mem_cons.mp hx with rfl | hx
· exact le_rfl
· have hf := (scan_none q vs).1 hn x hx
simp [hf] at hxactive
· rename_i v' c' ho
have old := ih v' c' ho
split at h
· rename_i hle
cases h
refine ⟨by simp, rfl, ha, ?_⟩
intro x hx hxactive
rcases List.mem_cons.mp hx with rfl | hx
· exact le_rfl
· exact hle.trans (old.2.2.2 x hx hxactive)
· rename_i hle
cases h
refine ⟨by simp [old.1], old.2.1, old.2.2.1, ?_⟩
intro x hx hxactive
rcases List.mem_cons.mp hx with rfl | hx
· exact le_of_not_ge hle
· exact old.2.2.2 x hx hxactive
· rename_i ha
have old := ih u c h
refine ⟨by simp [old.1], old.2.1, old.2.2.1, ?_⟩
intro x hx hxactive
rcases List.mem_cons.mp hx with rfl | hx
· exact (ha hxactive).elim
· exact old.2.2.2 x hx hxactivestructure Relaxed (n : Nat) (E : Type) where
cells : Cells n E
edgeVisits : Nat
tests : Nat
writes : Natdef relax (w : E → Nat) (q : Cells n E) (v : Fin n) (e : E) : Relaxed n E :=
let cell := read q v
if cell.active then
if (w e : Key) < cell.key then
⟨write q v ⟨true, w e, some e⟩, 1, 1, 1⟩
else ⟨q, 1, 1, 0⟩
else ⟨q, 1, 0, 0⟩@[simp] theorem relax_active (w : E → Nat) (q : Cells n E) (v x : Fin n) (e : E) :
(read (relax w q v e).cells x).active = (read q x).active := by
simp only [relax]
split
· rename_i ha
split
· by_cases hx : v = x
· subst v; simp [ha]
· simp [hx]
· rfl
· rfltheorem relax_key_le (w : E → Nat) (q : Cells n E) (v x : Fin n) (e : E) :
(read (relax w q v e).cells x).key ≤ (read q x).key := by
simp only [relax]
split
· split
· rename_i hk
by_cases hx : v = x
· subst v; simpa using hk.le
· simp [hx]
· exact le_rfl
· exact le_rfltheorem relax_target_le (w : E → Nat) (q : Cells n E) (v : Fin n) (e : E)
(ha : (read q v).active = true) :
(read (relax w q v e).cells v).key ≤ (w e : Key) := by
simp only [relax, ha, ↓reduceIte]
split
· simp
· rename_i h; exact le_of_not_gt htheorem relax_changed (w : E → Nat) (q : Cells n E) (v x : Fin n) (e : E) :
read (relax w q v e).cells x = read q x ∨
(x = v ∧ read (relax w q v e).cells x = ⟨true, w e, some e⟩) := by
simp only [relax]
split
· split
· by_cases hx : v = x
· subst v; right; simp
· left; simp [hx]
· exact Or.inl rfl
· exact Or.inl rfldef relaxAll (w : E → Nat) (q : Cells n E) : List (Fin n × E) → Relaxed n E
| [] => ⟨q, 0, 0, 0⟩
| (v,e) :: es =>
let first := relax w q v e
let rest := relaxAll w first.cells es
⟨rest.cells, first.edgeVisits + rest.edgeVisits,
first.tests + rest.tests, first.writes + rest.writes⟩theorem relax_counts (w : E → Nat) (q : Cells n E) (v : Fin n) (e : E) :
(relax w q v e).edgeVisits = 1 ∧ (relax w q v e).tests ≤ 1 ∧
(relax w q v e).writes ≤ (relax w q v e).tests := by
simp only [relax]
split
· split <;> simp
· simptheorem relaxAll_counts (w : E → Nat) (q : Cells n E) (es : List (Fin n × E)) :
(relaxAll w q es).edgeVisits = es.length ∧
(relaxAll w q es).tests ≤ es.length ∧
(relaxAll w q es).writes ≤ (relaxAll w q es).tests := by
induction es generalizing q with
| nil => simp [relaxAll]
| cons ve es ih =>
rcases ve with ⟨v,e⟩
have old := ih (relax w q v e).cells
have first := relax_counts w q v e
simp only [relaxAll, List.length_cons]
omega@[simp] theorem relaxAll_active (w : E → Nat) (q : Cells n E)
(es : List (Fin n × E)) (x : Fin n) :
(read (relaxAll w q es).cells x).active = (read q x).active := by
induction es generalizing q with
| nil => rfl
| cons ve es ih => simp [relaxAll, ih]theorem relaxAll_key_le (w : E → Nat) (q : Cells n E)
(es : List (Fin n × E)) (x : Fin n) :
(read (relaxAll w q es).cells x).key ≤ (read q x).key := by
induction es generalizing q with
| nil => exact le_rfl
| cons ve es ih => exact (ih _).trans (relax_key_le w q ve.1 x ve.2)theorem relaxAll_target_le (w : E → Nat) (q : Cells n E) (es : List (Fin n × E))
(v : Fin n) (e : E) (he : (v,e) ∈ es) (ha : (read q v).active = true) :
(read (relaxAll w q es).cells v).key ≤ (w e : Key) := by
induction es generalizing q with
| nil => simp at he
| cons ve es ih =>
rcases ve with ⟨u,f⟩
rcases List.mem_cons.mp he with h | he
· cases h
exact (relaxAll_key_le w _ es v).trans (relax_target_le w q v e ha)
· exact ih (relax w q u f).cells he (by simpa using ha)theorem relaxAll_origin (w : E → Nat) (q : Cells n E) (es : List (Fin n × E))
(x : Fin n) :
read (relaxAll w q es).cells x = read q x ∨
∃ e, (x,e) ∈ es ∧ read (relaxAll w q es).cells x = ⟨true, w e, some e⟩ := by
induction es generalizing q with
| nil => exact Or.inl rfl
| cons ve es ih =>
rcases ve with ⟨v,e⟩
rcases ih (relax w q v e).cells with hold | ⟨f,hf,hcell⟩
· rcases relax_changed w q v x e with hs | ⟨rfl,hs⟩
· exact Or.inl (hold.trans hs)
· exact Or.inr ⟨e, by simp, hold.trans hs⟩
· exact Or.inr ⟨f, by simp [hf], hcell⟩end CLRS.MST.ExecutablePrim.ArrayPrimCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S1_UnionFindBridge
Chapter 21 - Union-find bridge for Kruskal
This module connects the executable Chapter 19 equivalence query to the component-oracle interface used by the mathematical Kruskal proof. The bridge is extensional in the current selected edge set: a provider supplies a forest and vertex encoding for every edge set and proves that forest equivalence is exactly graph connectivity. A later stateful scan refinement may reuse the same invariant while constructing the states incrementally.
Main results:
-
Theorem
UnionFindConnectivityRefinement.checkEquiv_iff_connected: the executable Boolean query decides graph connectivity. -
Definition
UnionFindConnectivityRefinement.cycleTest: a verifiedCycleTestImplementationaccepted by the existing Kruskal theorems. -
Theorem
UnionFindConnectivityRefinement.cycleTest_correct: the packaged implementation agrees with the component oracle.
namespace CLRSnamespace MSTopen Finsetvariable {V E : Type} [DecidableEq V] [DecidableEq E]
A family of union-find states that represents connectivity in each selected
edge set. The varying Fin type records that every supplied encoding is
in bounds for its corresponding executable forest.
structure UnionFindConnectivityRefinement (G : Graph V E) where
state : Finset E → Chapter21.Forest.State
encode : ∀ A, V → Fin (state A).size
sameSet_iff_connected :
∀ A u v,
(Chapter21.Forest.partition (state A)).sameSet
(encode A u) (encode A v) ↔
G.ConnectedIn A u vnamespace UnionFindConnectivityRefinementvariable {G : Graph V E}The raw union-find cycle-test decision for a selected edge set.
def accept (R : UnionFindConnectivityRefinement G) (A : Finset E) (e : E) : Bool :=
!((R.state A).checkEquiv
(R.encode A (G.src e)) (R.encode A (G.dst e))).2The executable equivalence query agrees exactly with graph connectivity.
theorem checkEquiv_iff_connected (R : UnionFindConnectivityRefinement G)
(A : Finset E) (u v : V) :
((R.state A).checkEquiv (R.encode A u) (R.encode A v)).2 = true ↔
G.ConnectedIn A u v := by
rw [Chapter21.Forest.checkEquiv_correct]
exact R.sameSet_iff_connected A u vUnion-find accepts exactly edges whose endpoints are not already connected.
theorem accept_eq_true_iff_not_connected
(R : UnionFindConnectivityRefinement G) (A : Finset E) (e : E) :
R.accept A e = true ↔
¬G.ConnectedIn A (G.src e) (G.dst e) := by
unfold accept
rw [Bool.not_eq_true_eq_eq_false]
rw [Chapter21.Forest.checkEquiv_eq_false_iff]
exact not_congr (R.sameSet_iff_connected A (G.src e) (G.dst e))Convert connectivity faithfulness into faithfulness for any exact oracle.
theorem sameSet_iff_mem_component
(R : UnionFindConnectivityRefinement G) (C : ComponentOracle G)
(hExact : ExactComponentOracle G C) (A : Finset E) (u v : V) :
(Chapter21.Forest.partition (R.state A)).sameSet
(R.encode A u) (R.encode A v) ↔
v ∈ C.component A u := by
rw [R.sameSet_iff_connected, hExact]The Chapter 19 union-find query packaged as the Chapter 21 cycle-test implementation. The exact component oracle is used only as the mathematical specification of the Boolean result.
def cycleTest (R : UnionFindConnectivityRefinement G) (C : ComponentOracle G)
(hExact : ExactComponentOracle G C) :
CycleTestImplementation G C where
accept := R.accept
correct := by
intro A e
apply Bool.eq_iff_iff.2
rw [R.accept_eq_true_iff_not_connected]
simp only [acceptByComponent, decide_eq_true_iff]
exact not_congr (hExact A (G.src e) (G.dst e)).symmPublic correctness theorem for the packaged union-find cycle test.
theorem cycleTest_correct
(R : UnionFindConnectivityRefinement G) (C : ComponentOracle G)
(hExact : ExactComponentOracle G C) (A : Finset E) (e : E) :
(R.cycleTest C hExact).accept A e = acceptByComponent G C A e :=
(R.cycleTest C hExact).correct A eend UnionFindConnectivityRefinementend MSTend CLRSCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S2_StatefulKruskal
Chapter 21 - Incremental costed Kruskal
This module refines the mathematical Kruskal pass to the real costed
Batteries.UnionFind machine proved correct in Chapter 19. Vertices are
represented by Fin n, so every graph endpoint is directly usable as a
fixed-universe union-find node.
Each scanned edge performs one fused union operation. Batteries union runs the two required finds and links their roots only when they differ. The Boolean acceptance decision is taken from the pre-state partition; rejected edges therefore retain path compression while leaving both the represented partition and selected edge set unchanged.
namespace CLRSnamespace MSTopen Finsetvariable {n : Nat} {E : Type} [DecidableEq E]namespace GraphConnectivity after inserting one undirected edge has exactly the same three-way relational form as a disjoint-set merge.
theorem connected_insert_edge_iff {G : Graph (Fin n) E} {A : Finset E}
{e : E} {u v : Fin n} :
G.ConnectedIn (insert e A) u v ↔
G.ConnectedIn A u v ∨
(G.ConnectedIn A u (G.src e) ∧
G.ConnectedIn A (G.dst e) v) ∨
(G.ConnectedIn A u (G.dst e) ∧
G.ConnectedIn A (G.src e) v) := by
constructor
· exact connected_insert_edge_cases
· intro h
have hmono : A ⊆ insert e A := Finset.subset_insert e A
rcases h with hbase | hbridge
· exact connected_mono hmono hbase
· have hedge : G.ConnectedIn (insert e A) (G.src e) (G.dst e) :=
connected_of_mem_edge (Finset.mem_insert_self e A)
rcases hbridge with ⟨hus, hdv⟩ | ⟨hud, hsv⟩
· exact connected_trans (connected_mono hmono hus)
(connected_trans hedge (connected_mono hmono hdv))
· exact connected_trans (connected_mono hmono hud)
(connected_trans (connected_symm hedge) (connected_mono hmono hsv))With no selected edges, graph connectivity is equality.
theorem connected_empty_iff {G : Graph (Fin n) E} {u v : Fin n} :
G.ConnectedIn ∅ u v ↔ u = v := by
constructor
· intro h
induction h with
| refl => rfl
| tail _ hadj _ =>
rcases hadj with ⟨e, he, _⟩
simp at he
· rintro rfl
exact connected_refl G ∅ uend Graphnamespace StatefulKruskalabbrev UFMachine (n : Nat) := Chapter21.Analysis.Costed.Machine nabbrev UFOperation (n : Nat) := Chapter21.Analysis.Costed.Operation nExecutable Kruskal state: the Chapter 19 machine, selected edges, and accumulated concrete union-find work.
structure State (n : Nat) (E : Type) where
machine : UFMachine n
selected : Finset E
cost : NatThe initial singleton forest and empty edge set.
def initial (n : Nat) (E : Type) [DecidableEq E] : State n E where
machine := Chapter21.Analysis.Costed.Machine.initial n
selected := ∅
cost := 0The executable cycle decision in the pre-state partition.
def accepts (s : State n E) (G : Graph (Fin n) E) (e : E) : Bool :=
!((s.machine.forest.checkEquiv
(s.machine.node (G.src e)) (s.machine.node (G.dst e))).2)
Concrete two-find cost of the executable checkEquiv cycle query.
def cycleQueryCost (s : State n E) (G : Graph (Fin n) E) (e : E) : Nat :=
let x := s.machine.node (G.src e)
let y := s.machine.node (G.dst e)
Chapter21.Analysis.Costed.findEdges s.machine.forest x +
Chapter21.Analysis.Costed.findEdges (s.machine.forest.find x).1
(Chapter21.Analysis.Costed.secondNodeAfterFind s.machine.forest x y) + 2The Chapter 19 union charge covers the preceding equivalence query: both perform the same two finds, while union reserves one additional link unit.
theorem cycleQueryCost_le_unionStepCost
(s : State n E) (G : Graph (Fin n) E) (e : E) :
cycleQueryCost s G e ≤
(Chapter21.Analysis.Costed.step s.machine
(.union (G.src e) (G.dst e))).cost := by
simp [cycleQueryCost, Chapter21.Analysis.Costed.step,
Chapter21.Analysis.Costed.unionCost]One executable cycle query followed by the Chapter 19 union operation. The union state performs the actual merge; charging twice its cost covers both two-find traversals, since the query omits only the union's constant link.
def step (G : Graph (Fin n) E) (s : State n E) (e : E) : State n E :=
let one := Chapter21.Analysis.Costed.step s.machine
(.union (G.src e) (G.dst e))
{ machine := one.state
selected := if accepts s G e then insert e s.selected else s.selected
cost := s.cost + 2 * one.cost }The charged step bounds the actual query-plus-union work.
theorem query_add_union_le_charged_step
(s : State n E) (G : Graph (Fin n) E) (e : E) :
cycleQueryCost s G e +
(Chapter21.Analysis.Costed.step s.machine
(.union (G.src e) (G.dst e))).cost ≤
2 * (Chapter21.Analysis.Costed.step s.machine
(.union (G.src e) (G.dst e))).cost := by
have h := cycleQueryCost_le_unionStepCost s G e
omegaIncrementally scan a fixed edge order.
def scan (G : Graph (Fin n) E) : List E → State n E → State n E
| [], s => s
| e :: es, s => scan G es (step G s e)The central state invariant: union-find equivalence is exactly graph connectivity in the currently selected forest.
def Valid (G : Graph (Fin n) E) (s : State n E) : Prop :=
∀ (u v : Fin n),
(Chapter21.Forest.partition s.machine.forest).sameSet (u : Nat) v ↔
G.ConnectedIn s.selected u v
@[simp]
theorem accepts_eq_true_iff (G : Graph (Fin n) E) (s : State n E) (e : E) :
accepts s G e = true ↔
¬(Chapter21.Forest.partition s.machine.forest).sameSet
(G.src e) (G.dst e) := by
rw [accepts, Bool.not_eq_true_eq_eq_false,
Chapter21.Forest.checkEquiv_eq_false_iff]
simp [Chapter21.Analysis.Costed.Machine.node]
theorem accepts_eq_false_iff (G : Graph (Fin n) E) (s : State n E) (e : E) :
accepts s G e = false ↔
(Chapter21.Forest.partition s.machine.forest).sameSet
(G.src e) (G.dst e) := by
rw [accepts, Bool.not_eq_false_eq_eq_true,
Chapter21.Forest.checkEquiv_correct]
simp [Chapter21.Analysis.Costed.Machine.node]A valid machine makes the executable cycle decision exactly the usual graph cycle test.
theorem accepts_eq_true_iff_not_connected {G : Graph (Fin n) E}
{s : State n E} (hs : Valid G s) (e : E) :
accepts s G e = true ↔
¬G.ConnectedIn s.selected (G.src e) (G.dst e) := by
rw [accepts_eq_true_iff]
exact not_congr (hs (G.src e) (G.dst e))One real Chapter 19 union preserves the graph-connectivity invariant.
theorem step_valid {G : Graph (Fin n) E} {s : State n E}
(hs : Valid G s) (e : E) : Valid G (step G s e) := by
intro u v
by_cases hacc : accepts s G e = true
· have hnot :
¬(Chapter21.Forest.partition s.machine.forest).sameSet
(G.src e) (G.dst e) :=
(accepts_eq_true_iff G s e).1 hacc
simp only [step, hacc, if_pos]
change
(Chapter21.Forest.partition
(s.machine.forest.union (s.machine.node (G.src e))
(s.machine.node (G.dst e)))).sameSet u v ↔
G.ConnectedIn (insert e s.selected) u v
rw [Chapter21.Forest.union_sameSet_iff]
simp only [Chapter21.Analysis.Costed.Machine.node]
rw [Graph.connected_insert_edge_iff]
simpa using
or_congr (hs u v)
(or_congr
(and_congr (hs u (G.src e)) (hs (G.dst e) v))
(and_congr (hs u (G.dst e)) (hs (G.src e) v)))
· have hfalse : accepts s G e = false := by
cases h : accepts s G e <;> simp [h] at hacc ⊢
have hsame :
(Chapter21.Forest.partition s.machine.forest).sameSet
(G.src e) (G.dst e) :=
(accepts_eq_false_iff G s e).1 hfalse
simp only [step, hfalse]
change
(Chapter21.Forest.partition
(s.machine.forest.union (s.machine.node (G.src e))
(s.machine.node (G.dst e)))).sameSet u v ↔
G.ConnectedIn s.selected u v
rw [Chapter21.Forest.union_refines_merge]
have hnode :
(Chapter21.Forest.partition s.machine.forest).sameSet
(s.machine.node (G.src e)) (s.machine.node (G.dst e)) := by
simpa [Chapter21.Analysis.Costed.Machine.node] using hsame
rw [(Chapter21.Forest.partition s.machine.forest).merge_related_sameSet_iff
hnode]
exact hs u vThe invariant is inductive over the full edge scan.
theorem scan_valid {G : Graph (Fin n) E} {s : State n E}
(hs : Valid G s) (edges : List E) : Valid G (scan G edges s) := by
induction edges generalizing s with
| nil => exact hs
| cons e edges ih => exact ih (step_valid hs e)Singleton initialization represents empty-graph connectivity exactly.
theorem initial_valid (G : Graph (Fin n) E) : Valid G (initial n E) := by
intro u v
change
(Chapter21.Forest.partition (Chapter21.Forest.singletonForest n)).sameSet
(u : Nat) v ↔ G.ConnectedIn ∅ u v
rw [Graph.connected_empty_iff]
change (Chapter21.Forest.singletonForest n).Equiv (u : Nat) v ↔ u = v
rw [Chapter21.Forest.singletonForest_equiv_iff]
exact Fin.ext_iff.symmEvery reachable incremental Kruskal state remains connectivity-faithful.
theorem scan_initial_valid (G : Graph (Fin n) E) (edges : List E) :
Valid G (scan G edges (initial n E)) :=
scan_valid (initial_valid G) edgesThe graph-level cycle test used by the mathematical Kruskal pass.
noncomputable def connectivityAccept (G : Graph (Fin n) E)
(A : Finset E) (e : E) : Bool := by
classical
exact if G.ConnectedIn A (G.src e) (G.dst e) then false else trueA valid state makes the machine decision extensionally equal to the mathematical connectivity decision.
theorem accepts_eq_connectivityAccept {G : Graph (Fin n) E}
{s : State n E} (hs : Valid G s) (e : E) :
accepts s G e = connectivityAccept G s.selected e := by
classical
apply Bool.eq_iff_iff.2
rw [accepts_eq_true_iff_not_connected hs]
simp [connectivityAccept]Stateful execution selects exactly the same edges as the mathematical Kruskal recursion driven by graph connectivity.
theorem scan_selected_eq_kruskal {G : Graph (Fin n) E}
{s : State n E} (hs : Valid G s) (edges : List E) :
(scan G edges s).selected =
kruskal (connectivityAccept G) edges s.selected := by
induction edges generalizing s with
| nil => rfl
| cons e edges ih =>
simp only [scan, kruskal]
rw [← accepts_eq_connectivityAccept hs e]
by_cases hacc : accepts s G e = true
· simpa [step, hacc] using ih (step_valid hs e)
· have hfalse : accepts s G e = false := by
cases h : accepts s G e <;> simp [h] at hacc ⊢
simpa [step, hfalse] using ih (step_valid hs e)Reader-facing empty-prefix refinement theorem.
theorem scan_initial_selected_eq_kruskal (G : Graph (Fin n) E)
(edges : List E) :
(scan G edges (initial n E)).selected =
kruskal (connectivityAccept G) edges ∅ :=
scan_selected_eq_kruskal (initial_valid G) edgesConcrete work bounds
The exact Chapter 19 operation trace generated by a fused Kruskal scan.
def unionOperations (G : Graph (Fin n) E) (edges : List E) :
List (UFOperation n) :=
edges.map fun e => .union (G.src e) (G.dst e)
@[simp]
theorem unionOperations_length (G : Graph (Fin n) E) (edges : List E) :
(unionOperations G edges).length = edges.length := by
simp [unionOperations]The machine threaded by Kruskal is exactly the Chapter 19 costed run.
theorem scan_machine_eq_run (G : Graph (Fin n) E) (edges : List E)
(s : State n E) :
(scan G edges s).machine =
(Chapter21.Analysis.Costed.run s.machine
(unionOperations G edges)).state := by
induction edges generalizing s with
| nil => rfl
| cons e edges ih =>
simpa [scan, step, unionOperations, Chapter21.Analysis.Costed.run] using
ih (step G s e)The charged Kruskal work is twice the Chapter 19 union trace: one charge for the executable cycle query and one for the following union.
theorem scan_cost_eq_run (G : Graph (Fin n) E) (edges : List E)
(s : State n E) :
(scan G edges s).cost = s.cost + 2 *
(Chapter21.Analysis.Costed.run s.machine
(unionOperations G edges)).cost := by
induction edges generalizing s with
| nil => simp [scan, unionOperations, Chapter21.Analysis.Costed.run]
| cons e edges ih =>
rw [scan, ih]
simp only [step, unionOperations, List.map_cons,
Chapter21.Analysis.Costed.run]
omega
The union-find part of incremental Kruskal has the Chapter 19
O((E + V) alpha(V)) concrete bound.
theorem scan_initial_cost_le_inverseAckermann
(G : Graph (Fin n) E) (edges : List E) :
(scan G edges (initial n E)).cost ≤
18 * (edges.length + n) *
Chapter21.Analysis.inverseAckermann n := by
rw [scan_cost_eq_run]
have h := Chapter21.Analysis.Ackermann.run_cost_le_inverseAckermann n
(unionOperations G edges)
rw [unionOperations_length] at h
simp only [initial, zero_add]
nlinarithAbstract comparison-sort budget; this module does not execute a counted sort.
def comparisonSortWork (m : Nat) : Nat :=
m * (Nat.log2 m + 1)Combined Kruskal budget: abstract sorting, one scan charge per edge, and the actual Chapter 19 union-find execution. Only the union-find component is derived from the returned scan trace.
def totalWork (G : Graph (Fin n) E) (edges : List E) : Nat :=
comparisonSortWork edges.length + edges.length +
(scan G edges (initial n E)).costExact decomposition of the combined sorting budget and union-find counter.
theorem totalWork_eq (G : Graph (Fin n) E) (edges : List E) :
totalWork G edges =
edges.length * (Nat.log2 edges.length + 1) + edges.length +
(scan G edges (initial n E)).cost :=
rflSorting, linear scan, and inverse-Ackermann union-find work composed in one explicit bound.
theorem totalWork_le_sort_add_scan_add_inverseAckermann
(G : Graph (Fin n) E) (edges : List E) :
totalWork G edges ≤
edges.length * (Nat.log2 edges.length + 1) + edges.length +
18 * (edges.length + n) *
Chapter21.Analysis.inverseAckermann n := by
exact Nat.add_le_add_left
(scan_initial_cost_le_inverseAckermann G edges)
(comparisonSortWork edges.length + edges.length)
Textbook O(E log E) endpoint with an explicit constant. The final
side condition records the standard domination alpha(V) = O(log E); keeping
it visible avoids hiding an asymptotic fact inside the concrete cost model.
theorem totalWork_le_forty_mul_edge_log
(G : Graph (Fin n) E) (edges : List E)
(hvertices : n ≤ edges.length)
(halpha : Chapter21.Analysis.inverseAckermann n ≤
Nat.log2 edges.length + 1) :
totalWork G edges ≤
40 * edges.length * (Nat.log2 edges.length + 1) := by
have hwork := totalWork_le_sort_add_scan_add_inverseAckermann G edges
have hlog : 1 ≤ Nat.log2 edges.length + 1 := by omega
nlinarithend StatefulKruskalend MSTend CLRSCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S3_ExecutablePrim
Chapter 21 - Executable indexed-queue Prim
This module supplies the implementation-facing state omitted by the abstract
PrimTrace: a finite priority queue, vertex keys, parent edges,
decreaseKey, and extractMin. The queue implementation is a small
executable reference model. Its operation trace is also the semantic target
for an array-backed binary heap refinement.
namespace CLRSnamespace MSTnamespace ExecutablePrimopen Finsetvariable {n : Nat} {E : Type} [LinearOrder E]
top is the CLRS infinity key; finite values are edge weights.
abbrev Key := WithTop NatIndexed minimum-priority-queue state used by Prim.
structure Queue (n : Nat) (E : Type) where
members : Finset (Fin n)
key : Fin n → Key
parent : Fin n → Option EEmpty-key initialization over a prescribed queue universe.
def Queue.initial (members : Finset (Fin n)) : Queue n E where
members := members
key := fun _ => ⊤
parent := fun _ => none
CLRS DECREASE-KEY, together with the parent edge attaining the new key.
An update whose key is not strictly smaller is ignored.
def Queue.decreaseKey (q : Queue n E) (v : Fin n) (k : Nat) (e : E) :
Queue n E :=
if (k : Key) < q.key v then
{ q with
key := Function.update q.key v k
parent := Function.update q.parent v (some e) }
else q@[simp]
theorem Queue.initial_members (members : Finset (Fin n)) :
(Queue.initial (E := E) members).members = members :=
rfl@[simp]
theorem Queue.initial_key (members : Finset (Fin n)) (v : Fin n) :
(Queue.initial (E := E) members).key v = ⊤ :=
rfl@[simp]
theorem Queue.initial_parent (members : Finset (Fin n)) (v : Fin n) :
(Queue.initial (E := E) members).parent v = none :=
rfl
@[simp]
theorem Queue.decreaseKey_members (q : Queue n E) (v : Fin n)
(k : Nat) (e : E) :
(q.decreaseKey v k e).members = q.members := by
unfold Queue.decreaseKey
split <;> rflDecreasing one key never raises any queue key.
theorem Queue.decreaseKey_key_le (q : Queue n E) (v x : Fin n)
(k : Nat) (e : E) :
(q.decreaseKey v k e).key x ≤ q.key x := by
unfold Queue.decreaseKey
split <;> rename_i h
· by_cases hx : x = v
· subst x
simp [Function.update, h.le]
· simp [Function.update, hx]
· exact le_rfl
After decreaseKey v k, the target key is at most k.
theorem Queue.decreaseKey_target_le (q : Queue n E) (v : Fin n)
(k : Nat) (e : E) :
(q.decreaseKey v k e).key v ≤ (k : Key) := by
unfold Queue.decreaseKey
split <;> rename_i h
· simp
· exact le_of_not_gt hA changed parent entry records exactly the supplied edge and finite key.
theorem Queue.decreaseKey_parent_some {q : Queue n E} {v x : Fin n}
{k : Nat} {e f : E}
(hparent : (q.decreaseKey v k e).parent x = some f) :
(x = v ∧ f = e ∧ (q.decreaseKey v k e).key x = k) ∨
(q.parent x = some f ∧ (q.decreaseKey v k e).key x = q.key x) := by
by_cases hk : (k : Key) < q.key v
· by_cases hx : x = v
· subst x
have hfe : f = e := by
have : e = f := by
simpa [Queue.decreaseKey, hk, Function.update] using hparent
exact this.symm
subst f
left
simp [Queue.decreaseKey, hk, Function.update]
· right
have hold : q.parent x = some f := by
simpa [Queue.decreaseKey, hk, Function.update, hx] using hparent
exact ⟨hold, by simp [Queue.decreaseKey, hk, Function.update, hx]⟩
· right
have hold : q.parent x = some f := by
simpa [Queue.decreaseKey, hk] using hparent
exact ⟨hold, by simp [Queue.decreaseKey, hk]⟩Executable extract-min
Linear reference implementation of minimum selection. A binary heap will refine the same operation contract below.
def extractMinList (key : Fin n → Key) : List (Fin n) → Option (Fin n)
| [] => none
| v :: vs =>
match extractMinList key vs with
| none => some v
| some u => if key v ≤ key u then some v else some utheorem extractMinList_mem {key : Fin n → Key} {vs : List (Fin n)} {u : Fin n}
(h : extractMinList key vs = some u) : u ∈ vs := by
induction vs with
| nil => simp [extractMinList] at h
| cons v vs ih =>
simp only [extractMinList] at h
split at h
· simp_all
· split at h <;> simp_alltheorem extractMinList_eq_none_iff (key : Fin n → Key) (vs : List (Fin n)) :
extractMinList key vs = none ↔ vs = [] := by
cases vs with
| nil => simp [extractMinList]
| cons v vs =>
cases hrest : extractMinList key vs with
| none => simp [extractMinList, hrest]
| some u =>
by_cases hle : key v ≤ key u <;>
simp [extractMinList, hrest, hle]theorem extractMinList_key_le {key : Fin n → Key} {vs : List (Fin n)}
{u : Fin n} (h : extractMinList key vs = some u) :
∀ v ∈ vs, key u ≤ key v := by
induction vs generalizing u with
| nil => simp [extractMinList] at h
| cons x xs ih =>
intro v hv
simp only [extractMinList] at h
split at h
· rename_i hnone
simp only [Option.some.injEq] at h
subst u
have hempty : xs = [] :=
(extractMinList_eq_none_iff key xs).1 hnone
simp_all
· rename_i y hy
split at h <;> rename_i hxy
· simp only [Option.some.injEq] at h
subst u
rcases List.mem_cons.mp hv with rfl | hv
· exact le_rfl
· exact hxy.trans (ih hy v hv)
· simp only [Option.some.injEq] at h
subst u
rcases List.mem_cons.mp hv with rfl | hv
· exact le_of_not_ge hxy
· exact ih hy v hvRemove and return a minimum-key queue member.
def Queue.extractMin (q : Queue n E) : Option (Fin n × Queue n E) :=
match h : extractMinList q.key (q.members.sort (· ≤ ·)) with
| none => none
| some u => some (u, { q with members := q.members.erase u })
theorem Queue.extractMin_mem {q : Queue n E} {u : Fin n} {q' : Queue n E}
(h : q.extractMin = some (u, q')) : u ∈ q.members := by
unfold Queue.extractMin at h
split at h <;> rename_i hmin
· contradiction
· cases h
exact (q.members.mem_sort (· ≤ ·)).mp (extractMinList_mem hmin)
theorem Queue.extractMin_key_le {q : Queue n E} {u : Fin n} {q' : Queue n E}
(h : q.extractMin = some (u, q')) {v : Fin n} (hv : v ∈ q.members) :
q.key u ≤ q.key v := by
unfold Queue.extractMin at h
split at h <;> rename_i hmin
· contradiction
· cases h
exact extractMinList_key_le hmin v ((q.members.mem_sort (· ≤ ·)).mpr hv)
theorem Queue.extractMin_members {q : Queue n E} {u : Fin n} {q' : Queue n E}
(h : q.extractMin = some (u, q')) :
q'.members = q.members.erase u := by
unfold Queue.extractMin at h
split at h
· contradiction
· cases h
rflBuilding the indexed queue by edge relaxation
The endpoint outside a cut. It is used only when the edge is known to cross the cut, in which case exactly one endpoint is outside.
def outsideVertex (G : Graph (Fin n) E) (S : Finset (Fin n)) (e : E) : Fin n :=
if G.src e ∈ S then G.dst e else G.src e
theorem outsideVertex_not_mem {G : Graph (Fin n) E} {S : Finset (Fin n)}
{e : E} (hcross : G.Crosses S e) : outsideVertex G S e ∉ S := by
unfold outsideVertex
split <;> rename_i hsrc
· rcases hcross with h | h
· exact h.2
· exact (h.2 hsrc).elim
· exact hsrc
theorem outsideVertex_eq_endpoint {G : Graph (Fin n) E}
{S : Finset (Fin n)} {e : E} :
outsideVertex G S e = G.src e ∨ outsideVertex G S e = G.dst e := by
unfold outsideVertex
split <;> simp
theorem outsideVertex_mem_vertices {G : FiniteGraph (Fin n) E}
{S : Finset (Fin n)} {e : E} (he : e ∈ G.edges) :
outsideVertex G.toGraph S e ∈ G.vertices := by
rcases outsideVertex_eq_endpoint (G := G.toGraph) (S := S) (e := e) with h | h
· rw [h]
exact G.src_mem e he
· rw [h]
exact G.dst_mem e heRelax one crossing edge into the indexed queue.
def crossesBool (G : Graph (Fin n) E) (S : Finset (Fin n)) (e : E) : Bool :=
if G.src e ∈ S then decide (G.dst e ∉ S) else decide (G.dst e ∈ S)
theorem crossesBool_eq_true_iff (G : Graph (Fin n) E)
(S : Finset (Fin n)) (e : E) :
crossesBool G S e = true ↔ G.Crosses S e := by
by_cases hs : G.src e ∈ S <;> by_cases hd : G.dst e ∈ S <;>
simp [crossesBool, Graph.Crosses, hs, hd]def relaxEdge (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (q : Queue n E) (e : E) : Queue n E :=
if crossesBool G.toGraph S e then
q.decreaseKey (outsideVertex G.toGraph S e) (w e) e
else q
Build the frontier queue by repeated CLRS decreaseKey.
def buildQueue (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) : List E → Queue n E
| [] => Queue.initial (G.vertices \ S)
| e :: es => relaxEdge G w S (buildQueue G w S es) eInductive specification of a queue built from a finite edge prefix.
structure BuildInvariant (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (edges : List E) (q : Queue n E) : Prop where
members_eq : q.members = G.vertices \ S
parent_sound : ∀ v e, q.parent v = some e →
e ∈ edges ∧ e ∈ G.edges ∧ G.toGraph.Crosses S e ∧
outsideVertex G.toGraph S e = v ∧ q.key v = w e
covers : ∀ e, e ∈ edges → G.toGraph.Crosses S e →
q.key (outsideVertex G.toGraph S e) ≤ (w e : Key)
theorem buildQueue_invariant (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (edges : List E)
(hall : ∀ e, e ∈ edges → e ∈ G.edges) :
BuildInvariant G w S edges (buildQueue G w S edges) := by
induction edges with
| nil =>
refine ⟨rfl, ?_, ?_⟩
· intro v e h
simp [buildQueue, Queue.initial] at h
· intro e he
simp at he
| cons e edges ih =>
have ihall : ∀ f, f ∈ edges → f ∈ G.edges := by
intro f hf
exact hall f (by simp [hf])
have old := ih ihall
by_cases hcross : G.toGraph.Crosses S e
· let v := outsideVertex G.toGraph S e
have hcrossBool : crossesBool G.toGraph S e = true :=
(crossesBool_eq_true_iff G.toGraph S e).2 hcross
have hstep :
buildQueue G w S (e :: edges) =
(buildQueue G w S edges).decreaseKey v (w e) e := by
simp [buildQueue, relaxEdge, hcrossBool, v]
rw [hstep]
refine ⟨?_, ?_, ?_⟩
· rw [Queue.decreaseKey_members, old.members_eq]
· intro x f hparent
rcases Queue.decreaseKey_parent_some hparent with hnew | hold
· rcases hnew with ⟨hx, hfe, hkey⟩
subst x
subst f
exact ⟨List.mem_cons_self, hall e List.mem_cons_self,
hcross, rfl, hkey⟩
· rcases hold with ⟨hparentOld, hkeyEq⟩
rcases old.parent_sound x f hparentOld with
⟨hf, hfG, hfcross, hout, hkey⟩
exact ⟨by simp [hf], hfG, hfcross, hout, hkeyEq.trans hkey⟩
· intro f hf hfcross
rw [List.mem_cons] at hf
rcases hf with rfl | hf
· exact Queue.decreaseKey_target_le _ _ _ _
· exact (Queue.decreaseKey_key_le _ _ _ _ _).trans
(old.covers f hf hfcross)
· have hcrossBool : crossesBool G.toGraph S e = false := by
cases h : crossesBool G.toGraph S e
· rfl
· exact (hcross ((crossesBool_eq_true_iff G.toGraph S e).1 h)).elim
have hstep : buildQueue G w S (e :: edges) =
buildQueue G w S edges := by
simp [buildQueue, relaxEdge, hcrossBool]
rw [hstep]
refine ⟨old.members_eq, ?_, ?_⟩
· intro v f hparent
rcases old.parent_sound v f hparent with
⟨hf, hfG, hfcross, hout, hkey⟩
exact ⟨by simp [hf], hfG, hfcross, hout, hkey⟩
· intro f hf hfcross
rw [List.mem_cons] at hf
rcases hf with rfl | hf
· exact (hcross hfcross).elim
· exact old.covers f hf hfcrossThe concrete queue for the current Prim cut.
def frontierQueue (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) : Queue n E :=
buildQueue G w S (G.edges.sort (· ≤ ·))theorem frontierQueue_invariant (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) :
BuildInvariant G w S (G.edges.sort (· ≤ ·)) (frontierQueue G w S) := by
apply buildQueue_invariant
intro e he
exact (G.edges.mem_sort (· ≤ ·)).mp heQueue evidence implies a CLRS light edge
The queue facts needed at one Prim extraction. covers is the familiar
key invariant: every crossing edge has an outside queue endpoint whose current
key is no greater than that edge's weight.
structure ChoiceCertificate (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(A : Finset E) (q : Queue n E) (u : Fin n) (e : E) : Prop where
extracted : ∃ q', q.extractMin = some (u, q')
parent_eq : q.parent u = some e
edge_mem : e ∈ G.edges
crosses : G.toGraph.Crosses (C.component A root) e
key_eq : q.key u = w e
covers : ∀ f, G.toGraph.Crosses (C.component A root) f →
∃ v, v ∈ q.members ∧ q.key v ≤ (w f : Key)Extract-min plus the key invariant proves that the parent edge is globally light across the current Prim cut.
theorem ChoiceCertificate.light {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} {w : E → Nat} {root : Fin n}
{A : Finset E} {q : Queue n E} {u : Fin n} {e : E}
(cert : ChoiceCertificate G C w root A q u e) :
∀ f, G.toGraph.Crosses (C.component A root) f → w e ≤ w f := by
intro f hcross
rcases cert.extracted with ⟨q', hextract⟩
rcases cert.covers f hcross with ⟨v, hv, hkey⟩
have hmin : q.key u ≤ q.key v := q.extractMin_key_le hextract hv
rw [cert.key_eq] at hmin
exact_mod_cast hmin.trans hkeyExecutable queue-driven Prim loop
Extract a minimum-key vertex and return its recorded parent edge.
def Queue.choose (q : Queue n E) : Option (Fin n × E) := do
let (u, _) ← q.extractMin
let e ← q.parent u
pure (u, e)
theorem Queue.choose_eq_some {q : Queue n E} {u : Fin n} {e : E}
(h : q.choose = some (u, e)) :
∃ q', q.extractMin = some (u, q') ∧ q.parent u = some e := by
cases hExtract : q.extractMin with
| none => simp [Queue.choose, hExtract] at h
| some pair =>
rcases pair with ⟨v, q'⟩
cases hParent : q.parent v with
| none => simp [Queue.choose, hExtract, hParent] at h
| some f =>
simp [Queue.choose, hExtract, hParent] at h
rcases h with ⟨rfl, rfl⟩
exact ⟨q', rfl, hParent⟩A queue provider recomputes or incrementally maintains the indexed heap for each selected edge set. The proof field is erased at runtime.
structure QueueProvider (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n) where
queue : Finset E → Queue n E
choose : Finset E → Option (Fin n × E) := fun A => (queue A).choose
correct : ∀ A u e, choose A = some (u, e) →
ChoiceCertificate G C w root A (queue A) u e
Concrete provider obtained by scanning graph edges and applying
decreaseKey to their outside endpoints. The closure hypothesis rules out
edge values outside the finite graph, matching the existing Chapter 21
PrimTrace quantification over all edge labels.
def frontierProvider (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges) :
QueueProvider G C w root where
queue A := frontierQueue G w (C.component A root)
choose A := (frontierQueue G w (C.component A root)).choose
correct := by
intro A u e hchoose
let S := C.component A root
let q := frontierQueue G w S
have hchoose' : q.choose = some (u, e) := by
simpa [q, S] using hchoose
rcases Queue.choose_eq_some hchoose' with ⟨q', hextract, hparent⟩
have inv := frontierQueue_invariant G w S
rcases inv.parent_sound u e hparent with
⟨heList, heG, heCross, hout, hkey⟩
refine
{ extracted := ⟨q', hextract⟩
parent_eq := hparent
edge_mem := heG
crosses := heCross
key_eq := hkey
covers := ?_ }
intro f hfCross
have hfG : f ∈ G.edges := hall A f (by simpa [S] using hfCross)
let v := outsideVertex G.toGraph S f
refine ⟨v, ?_, ?_⟩
· rw [inv.members_eq]
exact Finset.mem_sdiff.mpr
⟨outsideVertex_mem_vertices hfG, outsideVertex_not_mem hfCross⟩
· exact inv.covers f ((G.edges.mem_sort (· ≤ ·)).mpr hfG)
(by simpa [S] using hfCross)Fuelled executable Prim edge choices. Fuel bounds the number of successful vertex extractions.
def run {G : FiniteGraph (Fin n) E} {C : ComponentOracle G.toGraph}
{w : E → Nat} {root : Fin n}
(provider : QueueProvider G C w root) : Nat → Finset E → List E
| 0, _ => []
| fuel + 1, A =>
match provider.choose A with
| none => []
| some (_, e) => e :: run provider fuel (insert e A)
The executable key/parent/extract-min loop refines the abstract CLRS
PrimTrace consumed by the Chapter 21 MST theorem.
theorem run_refines_PrimTrace {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} {w : E → Nat} {root : Fin n}
(provider : QueueProvider G C w root) (fuel : Nat) (A : Finset E) :
G.PrimTrace C w root (run provider fuel A) A := by
induction fuel generalizing A with
| zero => trivial
| succ fuel ih =>
simp only [run]
split
· trivial
· rename_i u e hchoose
have cert := provider.correct A u e hchoose
exact ⟨cert.edge_mem, cert.crosses, cert.light, ih (insert e A)⟩Fully instantiated executable Prim choices from the concrete frontier queue.
def frontierRun (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(fuel : Nat) (A : Finset E) : List E :=
run (frontierProvider G C w root hall) fuel Atheorem frontierRun_refines_PrimTrace (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(fuel : Nat) (A : Finset E) :
G.PrimTrace C w root (frontierRun G C w root hall fuel A) A :=
run_refines_PrimTrace (frontierProvider G C w root hall) fuel ABinary-heap operation-count model
One extraction and a finite batch of decreases in a binary heap.
structure HeapRound where
decreases : NatBinary-heap work charged to a sequence of Prim rounds.
def binaryHeapWork (vertices : Nat) (rounds : List HeapRound) : Nat :=
(rounds.map fun r =>
(r.decreases + 1) * (Nat.log2 vertices + 1)).sum
theorem binaryHeapWork_eq (vertices : Nat) (rounds : List HeapRound) :
binaryHeapWork vertices rounds =
((rounds.map HeapRound.decreases).sum + rounds.length) *
(Nat.log2 vertices + 1) := by
induction rounds with
| nil => simp [binaryHeapWork]
| cons r rounds ih =>
rw [show binaryHeapWork vertices (r :: rounds) =
(r.decreases + 1) * (Nat.log2 vertices + 1) +
binaryHeapWork vertices rounds by rfl]
rw [ih]
simp only [List.map_cons, List.sum_cons, List.length_cons]
ringDirect binary-heap bound before using graph connectedness to absorb the vertex term into the edge term.
theorem binaryHeapWork_le_edges_vertices_log {vertices edges : Nat}
{rounds : List HeapRound}
(hdecreases : (rounds.map HeapRound.decreases).sum ≤ 2 * edges)
(hextracts : rounds.length ≤ vertices) :
binaryHeapWork vertices rounds ≤
(2 * edges + vertices) * (Nat.log2 vertices + 1) := by
rw [binaryHeapWork_eq]
exact Nat.mul_le_mul_right _ (Nat.add_le_add hdecreases hextracts)
With at most one decrease per scanned adjacency and at most one extraction
per vertex, a binary-heap Prim trace has the textbook O(E log V) bound.
theorem binaryHeapWork_le_edge_log {vertices edges : Nat}
{rounds : List HeapRound}
(hdecreases : (rounds.map HeapRound.decreases).sum ≤ 2 * edges)
(hextracts : rounds.length ≤ vertices)
(hconnected : vertices ≤ 2 * edges) :
binaryHeapWork vertices rounds ≤
4 * edges * (Nat.log2 vertices + 1) := by
exact (binaryHeapWork_le_edges_vertices_log hdecreases hextracts).trans <| by
nlinarith [Nat.zero_le (Nat.log2 vertices + 1)]
Alternative queue costs: an unsorted array gives quadratic extraction,
whereas Fibonacci-heap decrease-key yields the usual E + V log V profile.
def unsortedArrayWork (vertices edges : Nat) : Nat :=
vertices * vertices + edgesdef fibonacciHeapWork (vertices edges : Nat) : Nat :=
edges + vertices * (Nat.log2 vertices + 1)end ExecutablePrimend MSTend CLRSCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S4_Completion
Terminal coverage and MST correctness for executable Prim
Each certified crossing edge strictly decreases the number of vertices outside the exact root component. The concrete frontier queue cannot stop while a crossing graph edge remains: its finite key would contradict a minimum parentless vertex having an infinite key. Sufficient fuel therefore constructs a full Prim certificate, including spanning.
The final MST theorem constructs its initial optimum witness from a complete Kruskal forest scan and natural-weight minimization. It retains the existing all-edge-label closure hypothesis of the source Prim trace. Queue and component oracle running costs are separate from these completion theorems.
namespace CLRS.MST.ExecutablePrimopen Finsetvariable {n : Nat} {E : Type} [LinearOrder E]theorem component_mono {G : FiniteGraph (Fin n) E} {C : ComponentOracle G.toGraph}
(hexact : ExactComponentOracle G.toGraph C) {A B : Finset E} (h : A ⊆ B)
(root : Fin n) : C.component A root ⊆ C.component B root := by
intro v hv
exact (hexact B root v).2 (Graph.connected_mono h ((hexact A root v).1 hv))theorem crossing_outside_mem_insert {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{A : Finset E} {root : Fin n} {e : E}
(hc : G.toGraph.Crosses (C.component A root) e) :
outsideVertex G.toGraph (C.component A root) e ∈ C.component (insert e A) root := by
have hm := component_mono hexact (Finset.subset_insert e A) root
unfold outsideVertex
split
· rename_i hs
exact C.closed_src (insert e A) root e (mem_insert_self _ _) (hm hs)
· rename_i hs
rcases hc with hc | hc
· exact (hs hc.1).elim
· exact C.closed_dst (insert e A) root e (mem_insert_self _ _) (hm hc.1)A selected crossing edge strictly reduces the actual number of uncovered vertices.
theorem crossing_uncovered_lt {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{A : Finset E} {root : Fin n} {e : E} (he : e ∈ G.edges)
(hc : G.toGraph.Crosses (C.component A root) e) :
(G.vertices \ C.component (insert e A) root).card <
(G.vertices \ C.component A root).card := by
have hm := component_mono hexact (Finset.subset_insert e A) root
apply Finset.card_lt_card
apply Finset.ssubset_iff_subset_ne.mpr
refine ⟨(by intro v hv; exact mem_sdiff.mpr ⟨(mem_sdiff.mp hv).1, fun h => (mem_sdiff.mp hv).2 (hm h)⟩), ?_⟩
intro heq
have hv : outsideVertex G.toGraph (C.component A root) e ∈
G.vertices \ C.component A root :=
mem_sdiff.mpr ⟨outsideVertex_mem_vertices he, outsideVertex_not_mem hc⟩
rw [← heq] at hv
exact (mem_sdiff.mp hv).2 (crossing_outside_mem_insert hexact hc)Generic completion for any light-edge provider that stops only after coverage.
theorem run_covers {G : FiniteGraph (Fin n) E} {C : ComponentOracle G.toGraph}
{w : E → Nat} {root : Fin n} (provider : QueueProvider G C w root)
(hexact : ExactComponentOracle G.toGraph C)
(hstop : ∀ A, provider.choose A = none → G.vertices ⊆ C.component A root)
(fuel : Nat) (A : Finset E)
(hfuel : (G.vertices \ C.component A root).card ≤ fuel) :
G.vertices ⊆ C.component (prim (run provider fuel A) A) root := by
induction fuel generalizing A with
| zero =>
have hz : G.vertices \ C.component A root = ∅ := by
apply Finset.card_eq_zero.mp
omega
simpa [run, prim] using Finset.sdiff_eq_empty_iff_subset.mp hz
| succ fuel ih =>
cases hc : provider.choose A with
| none => simpa [run, hc, prim] using hstop A hc
| some pair =>
rcases pair with ⟨u, e⟩
have cert := provider.correct A u e hc
have hg := crossing_uncovered_lt hexact cert.edge_mem cert.crosses
simpa [run, hc, prim] using ih (insert e A) (by omega)theorem run_spans {G : FiniteGraph (Fin n) E} {C : ComponentOracle G.toGraph}
{w : E → Nat} {root : Fin n} (provider : QueueProvider G C w root)
(hexact : ExactComponentOracle G.toGraph C)
(hstop : ∀ A, provider.choose A = none → G.vertices ⊆ C.component A root)
(fuel : Nat) (A : Finset E)
(hfuel : (G.vertices \ C.component A root).card ≤ fuel) :
G.Spans (prim (run provider fuel A) A) := by
have hcover := run_covers provider hexact hstop fuel A hfuel
intro u hu v hv
exact Graph.connected_trans (Graph.connected_symm ((hexact _ root u).1 (hcover hu)))
((hexact _ root v).1 (hcover hv))omit [LinearOrder E] in
theorem Queue.decreaseKey_none_key {q : Queue n E}
(hq : ∀ x, q.parent x = none → q.key x = ⊤) (v : Fin n) (k : Nat) (e : E) :
∀ x, (q.decreaseKey v k e).parent x = none → (q.decreaseKey v k e).key x = ⊤ := by
intro x hp
by_cases hk : (k : Key) < q.key v
· simp only [Queue.decreaseKey, if_pos hk] at hp ⊢
by_cases hx : x = v
· subst x; simp at hp
· simpa [Function.update, hx] using hq x (by simpa [Function.update, hx] using hp)
· simpa only [Queue.decreaseKey, if_neg hk] using hq x (by simpa [Queue.decreaseKey, hk] using hp)theorem buildQueue_none_key (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (edges : List E) :
∀ x, (buildQueue G w S edges).parent x = none → (buildQueue G w S edges).key x = ⊤ := by
induction edges with
| nil => simp [buildQueue, Queue.initial]
| cons e es ih =>
simp only [buildQueue, relaxEdge]
split
· exact Queue.decreaseKey_none_key ih _ _ _
· exact ihomit [LinearOrder E] in
theorem Queue.exists_extractMin_of_mem {q : Queue n E} {v : Fin n} (hv : v ∈ q.members) :
∃ u q', q.extractMin = some (u, q') := by
cases he : q.extractMin with
| some p => exact ⟨p.1, p.2, rfl⟩
| none =>
unfold Queue.extractMin at he
split at he
· rename_i hm
have hz := (extractMinList_eq_none_iff q.key (q.members.sort (· ≤ ·))).1 hm
have hvl := (q.members.mem_sort (· ≤ ·)).2 hv
simp [hz] at hvl
· contradiction
theorem frontierQueue_choose_exists {G : FiniteGraph (Fin n) E} {w : E → Nat}
{S : Finset (Fin n)} {e : E} (he : e ∈ G.edges) (hc : G.toGraph.Crosses S e) :
∃ u f, (frontierQueue G w S).choose = some (u, f) := by
let q := frontierQueue G w S
have inv := frontierQueue_invariant G w S
let v := outsideVertex G.toGraph S e
have hv : v ∈ q.members := by
rw [inv.members_eq]
exact mem_sdiff.mpr ⟨outsideVertex_mem_vertices he, outsideVertex_not_mem hc⟩
obtain ⟨u, q', hu⟩ := Queue.exists_extractMin_of_mem hv
have hkey := (Queue.extractMin_key_le hu hv).trans
(inv.covers e ((G.edges.mem_sort (· ≤ ·)).2 he) hc)
cases hp : q.parent u with
| none =>
have ht : q.key u = ⊤ := buildQueue_none_key G w S _ u hp
rw [ht] at hkey
simp at hkey
| some f => exact ⟨u, f, by change q.choose = _; simp [Queue.choose, hu, hp]⟩
theorem frontierQueue_none_covers {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} {w : E → Nat} {root : Fin n}
(hroot : root ∈ G.vertices) (hconnected : G.Spans G.edges) (A : Finset E)
(hnone : (frontierQueue G w (C.component A root)).choose = none) :
G.vertices ⊆ C.component A root := by
intro v hv
by_contra hvout
obtain ⟨e, he, hc⟩ := Graph.connected_crosses_cut
(hconnected root hroot v hv) (C.mem_self A root) hvout
obtain ⟨u, f, hchoose⟩ := frontierQueue_choose_exists (w := w) he hc
rw [hnone] at hchoose
contradictionA sufficient-fuel run constructs the full certificate, including spanning.
theorem run_certificate {G : FiniteGraph (Fin n) E} {C : ComponentOracle G.toGraph}
{w : E → Nat} {root : Fin n} (provider : QueueProvider G C w root)
(hexact : ExactComponentOracle G.toGraph C) (hroot : root ∈ G.vertices)
(hstop : ∀ A, provider.choose A = none → G.vertices ⊆ C.component A root)
(fuel : Nat) (A : Finset E)
(hfuel : (G.vertices \ C.component A root).card ≤ fuel) :
G.PrimCertificate C w root A (run provider fuel A) :=
⟨hroot, run_refines_PrimTrace provider fuel A, run_spans provider hexact hstop fuel A hfuel⟩theorem frontierRun_certificate (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hexact : ExactComponentOracle G.toGraph C) (hroot : root ∈ G.vertices)
(hconnected : G.Spans G.edges) (fuel : Nat) (A : Finset E)
(hfuel : (G.vertices \ C.component A root).card ≤ fuel) :
G.PrimCertificate C w root A (frontierRun G C w root hall fuel A) := by
apply run_certificate (frontierProvider G C w root hall) hexact hroot
· intro B hb
exact frontierQueue_none_covers hroot hconnected B hb
· exact hfuelA finite connected graph has a minimum spanning tree. The witness is constructed from the existing complete Kruskal forest scan and natural-weight minimization; callers need not supply an already-minimum tree.
theorem exists_mstExtending_empty (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (hexact : ExactComponentOracle G.toGraph C)
(w : E → Nat) (hconnected : G.Spans G.edges) :
∃ T, IsMSTExtending G.toProblem w ∅ T := by
classical
have htree : ∃ T, G.IsSpanningTree T := by
refine ⟨kruskal (acceptByComponent G.toGraph C) (G.edges.sort (· ≤ ·)) ∅, ?_⟩
exact G.kruskal_spanning_tree_of_complete_exact_component C hexact _
(by simp) (by intro e he; exact (G.edges.mem_sort (· ≤ ·)).1 he)
(by intro e he; exact (G.edges.mem_sort (· ≤ ·)).2 he)
hconnected G.isForest_empty
have hex : ∃ k : Nat, ∃ T, G.IsSpanningTree T ∧ weight w T = k := by
obtain ⟨T, ht⟩ := htree
exact ⟨weight w T, T, ht, rfl⟩
obtain ⟨T, ht, hw⟩ := Nat.find_spec hex
refine ⟨T, ht, by simp, ?_⟩
intro U hu _
rw [hw]
exact Nat.find_min' hex ⟨U, hu, rfl⟩End-to-end executable Prim MST theorem: sufficient fuel and graph/oracle assumptions construct both terminal spanning and the initial optimum witness.
theorem frontierRun_minimum_spanning_tree (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hexact : ExactComponentOracle G.toGraph C) (hroot : root ∈ G.vertices)
(hconnected : G.Spans G.edges) (fuel : Nat)
(hfuel : (G.vertices \ C.component ∅ root).card ≤ fuel) :
G.IsMinimumSpanningTree w (prim (frontierRun G C w root hall fuel ∅) ∅) := by
obtain ⟨T, ht⟩ := exists_mstExtending_empty G C hexact w hconnected
exact G.prim_minimum_spanning_tree hexact
(frontierRun_certificate G C w root hall hexact hroot hconnected fuel ∅ hfuel) htThe graph vertex count is always sufficient fuel.
theorem frontierRun_minimum_spanning_tree_of_card (G : FiniteGraph (Fin n) E)
(C : ComponentOracle G.toGraph) (w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(hexact : ExactComponentOracle G.toGraph C) (hroot : root ∈ G.vertices)
(hconnected : G.Spans G.edges) :
G.IsMinimumSpanningTree w
(prim (frontierRun G C w root hall G.vertices.card ∅) ∅) := by
exact frontierRun_minimum_spanning_tree G C w root hall hexact hroot hconnected _
(Finset.card_le_card (Finset.sdiff_subset))Component coverage is a terminal spanning criterion for any Prim implementation.
theorem spans_of_component_covers {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{A : Finset E} {root : Fin n} (hcover : G.vertices ⊆ C.component A root) :
G.Spans A := by
intro u hu v hv
exact Graph.connected_trans (Graph.connected_symm ((hexact A root u).1 (hcover hu)))
((hexact A root v).1 (hcover hv))An implementation's light-edge trace and terminal root-component coverage suffice for MST correctness; an initial optimum is constructed internally.
theorem minimum_spanning_tree_of_trace_covers {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{w : E → Nat} {root : Fin n} (hroot : root ∈ G.vertices)
(hconnected : G.Spans G.edges) {choices : List E}
(htrace : G.PrimTrace C w root choices ∅)
(hcover : G.vertices ⊆ C.component (prim choices ∅) root) :
G.IsMinimumSpanningTree w (prim choices ∅) := by
obtain ⟨T, ht⟩ := exists_mstExtending_empty G C hexact w hconnected
exact G.prim_minimum_spanning_tree hexact
⟨hroot, htrace, spans_of_component_covers hexact hcover⟩ htWhen all selected edges lie inside the root component, a crossing insertion adds exactly its outside endpoint. This supports cached adjacency-once Prim.
theorem component_insert_crossing {G : FiniteGraph (Fin n) E}
{C : ComponentOracle G.toGraph} (hexact : ExactComponentOracle G.toGraph C)
{A : Finset E} {root : Fin n} {e : E}
(hc : G.toGraph.Crosses (C.component A root) e)
(hA : ∀ f ∈ A, G.src f ∈ C.component A root ∧ G.dst f ∈ C.component A root) :
C.component (insert e A) root =
insert (outsideVertex G.toGraph (C.component A root) e) (C.component A root) := by
let S := C.component A root
let T := insert (outsideVertex G.toGraph S e) S
have hend : G.src e ∈ T ∧ G.dst e ∈ T := by
by_cases hs : G.src e ∈ S
· simp [T, outsideVertex, hs]
· rcases hc with hc | hc
· exact (hs hc.1).elim
· simp [T, outsideVertex, hs, show G.dst e ∈ S from hc.1]
apply Finset.Subset.antisymm
· intro v hv
change v ∈ T
by_contra hvout
obtain ⟨f, hf, hcross⟩ := Graph.connected_crosses_cut
((hexact (insert e A) root v).1 hv)
(show root ∈ T from mem_insert_of_mem (C.mem_self A root)) hvout
have hfend : G.src f ∈ T ∧ G.dst f ∈ T := by
rcases mem_insert.mp hf with rfl | hf
· exact hend
· exact ⟨mem_insert_of_mem (hA f hf).1, mem_insert_of_mem (hA f hf).2⟩
rcases hcross with hc | hc
· exact hc.2 hfend.2
· exact hc.2 hfend.1
· apply Finset.insert_subset
· exact crossing_outside_mem_insert hexact hc
· exact component_mono hexact (Finset.subset_insert e A) rootend CLRS.MST.ExecutablePrimCLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S5_CountedFrontier
Counters on the reference frontier execution
These counters measure edge visits, attempted and successful decreases, and minimum-key comparisons in the actual reference loop. This implementation rebuilds its frontier each round. Its finite-set sorting, functional-map access, and component-oracle evaluation are not constant-time operations certified by these counters. In particular, these results do not imply binary-heap runtime.
namespace CLRS.MST.ExecutablePrim.CountedFrontiervariable {n : Nat} {E : Type} [LinearOrder E]structure Built (n : Nat) (E : Type) where
queue : Queue n E
edgeVisits : Nat
decreaseTests : Nat
decreases : Natdef build (G : FiniteGraph (Fin n) E) (w : E → Nat) (S : Finset (Fin n)) :
List E → Built n E
| [] => ⟨Queue.initial (G.vertices \ S), 0, 0, 0⟩
| e :: es =>
let old := build G w S es
if crossesBool G.toGraph S e then
let v := outsideVertex G.toGraph S e
if (w e : Key) < old.queue.key v then
⟨{ old.queue with key := Function.update old.queue.key v (w e)
parent := Function.update old.queue.parent v (some e) },
old.edgeVisits + 1, old.decreaseTests + 1, old.decreases + 1⟩
else ⟨old.queue, old.edgeVisits + 1, old.decreaseTests + 1, old.decreases⟩
else ⟨old.queue, old.edgeVisits + 1, old.decreaseTests, old.decreases⟩theorem build_refines (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (es : List E) :
(build G w S es).queue = buildQueue G w S es := by
induction es with
| nil => rfl
| cons e es ih =>
simp only [build, buildQueue, relaxEdge]
split
· simp only [Queue.decreaseKey, ih]
split <;> rfl
· exact ihtheorem build_counts (G : FiniteGraph (Fin n) E) (w : E → Nat)
(S : Finset (Fin n)) (es : List E) :
(build G w S es).edgeVisits = es.length ∧
(build G w S es).decreases ≤ (build G w S es).decreaseTests ∧
(build G w S es).decreaseTests ≤ es.length := by
induction es with
| nil => simp [build]
| cons e es ih =>
simp only [build, List.length_cons]
split
· split <;> dsimp <;> omega
· dsimp; omegaTail-first linear extraction with one count at each actual key comparison.
def minimum (key : Fin n → Key) : List (Fin n) → Option (Fin n) × Nat
| [] => (none, 0)
| v :: vs =>
let old := minimum key vs
match old.1 with
| none => (some v, old.2)
| some u => (if key v ≤ key u then some v else some u, old.2 + 1)theorem minimum_refines (key : Fin n → Key) (vs : List (Fin n)) :
(minimum key vs).1 = extractMinList key vs := by
induction vs with
| nil => rfl
| cons v vs ih =>
simp only [minimum, extractMinList, ih]
cases extractMinList key vs <;> rfl
theorem minimum_comparisons (key : Fin n → Key) (vs : List (Fin n)) :
(minimum key vs).2 = vs.length - 1 := by
induction vs with
| nil => rfl
| cons v vs ih =>
simp only [minimum]
split
· rename_i h
have hv : vs = [] := (extractMinList_eq_none_iff key vs).1
((minimum_refines key vs).symm.trans h)
subst vs
rfl
· rename_i u h
have hv : vs ≠ [] := by
intro he; subst vs; simp [minimum] at h
have hp := List.length_pos_iff.mpr hv
simp only [List.length_cons]
omegastructure Round where
edgeVisits : Nat
decreaseTests : Nat
decreases : Nat
minComparisons : Nat
extracted : Bool
deriving Repr, DecidableEqdef choose (G : FiniteGraph (Fin n) E) (w : E → Nat) (S : Finset (Fin n)) :
Option (Fin n × E) × Round :=
let b := build G w S (G.edges.sort (· ≤ ·))
let m := minimum b.queue.key (b.queue.members.sort (· ≤ ·))
let result := m.1.bind (fun u => (b.queue.parent u).map (fun e => (u, e)))
(result, ⟨b.edgeVisits, b.decreaseTests, b.decreases, m.2, result.isSome⟩)theorem choose_refines (G : FiniteGraph (Fin n) E) (w : E → Nat) (S : Finset (Fin n)) :
(choose G w S).1 = (frontierQueue G w S).choose := by
simp only [choose, build_refines, minimum_refines, frontierQueue, Queue.choose, Queue.extractMin]
cases extractMinList (buildQueue G w S (G.edges.sort (· ≤ ·))).key
((buildQueue G w S (G.edges.sort (· ≤ ·))).members.sort (· ≤ ·)) with
| none => rfl
| some u =>
simp only [Option.bind_some]
cases hp : (buildQueue G w S (G.edges.sort (· ≤ ·))).parent u <;> simp [hp]
theorem choose_counts (G : FiniteGraph (Fin n) E) (w : E → Nat) (S : Finset (Fin n)) :
(choose G w S).2.edgeVisits = G.edges.card ∧
(choose G w S).2.decreases ≤ (choose G w S).2.decreaseTests ∧
(choose G w S).2.decreaseTests ≤ G.edges.card ∧
(choose G w S).2.minComparisons = (G.vertices \ S).card - 1 := by
have hb := build_counts G w S (G.edges.sort (· ≤ ·))
simp only [Finset.length_sort] at hb
refine ⟨hb.1, hb.2.1, hb.2.2, ?_⟩
simp only [choose, minimum_comparisons, build_refines, Finset.length_sort]
rw [(buildQueue_invariant G w S (G.edges.sort (· ≤ ·))
(fun e he => (G.edges.mem_sort (· ≤ ·)).1 he)).members_eq]structure Execution (E : Type) where
edges : List E
rounds : List Round
deriving Reprdef execute (G : FiniteGraph (Fin n) E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : Fin n) : Nat → Finset E → Execution E
| 0, _ => ⟨[], []⟩
| fuel + 1, A =>
let step := choose G w (C.component A root)
match step.1 with
| none => ⟨[], [step.2]⟩
| some (_, e) =>
let rest := execute G C w root fuel (insert e A)
⟨e :: rest.edges, step.2 :: rest.rounds⟩theorem execute_refines (G : FiniteGraph (Fin n) E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : Fin n)
(hall : ∀ A f, G.toGraph.Crosses (C.component A root) f → f ∈ G.edges)
(fuel : Nat) (A : Finset E) :
(execute G C w root fuel A).edges = frontierRun G C w root hall fuel A := by
induction fuel generalizing A with
| zero => rfl
| succ fuel ih =>
simp only [execute, frontierRun, run, frontierProvider, choose_refines]
split <;> rename_i h <;> simp_all [frontierRun, frontierProvider]The recorded rounds are generated by the execution, including its last failed extraction.
theorem execute_rounds_le (G : FiniteGraph (Fin n) E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : Fin n) (fuel : Nat) (A : Finset E) :
(execute G C w root fuel A).rounds.length ≤ fuel := by
induction fuel generalizing A with
| zero => simp [execute]
| succ fuel ih =>
simp only [execute]
split
· simp
· simp only [List.length_cons]
exact Nat.succ_le_succ (ih _)Every recorded round scans the entire edge list; it is not an adjacency-once heap trace.
theorem execute_edgeVisits (G : FiniteGraph (Fin n) E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : Fin n) (fuel : Nat) (A : Finset E) :
((execute G C w root fuel A).rounds.map Round.edgeVisits).sum =
(execute G C w root fuel A).rounds.length * G.edges.card := by
induction fuel generalizing A with
| zero => simp [execute]
| succ fuel ih =>
simp only [execute]
split <;> simp [choose_counts, ih, Nat.add_mul, Nat.add_comm]
theorem execute_edgeVisits_le (G : FiniteGraph (Fin n) E) (C : ComponentOracle G.toGraph)
(w : E → Nat) (root : Fin n) (fuel : Nat) (A : Finset E) :
((execute G C w root fuel A).rounds.map Round.edgeVisits).sum ≤ fuel * G.edges.card := by
rw [execute_edgeVisits]
exact Nat.mul_le_mul_right _ (execute_rounds_le G C w root fuel A)end CLRS.MST.ExecutablePrim.CountedFrontierScope and implementation notes
Imports
import CLRSLean.Chapter_23
import CLRSLean.FourthEdition.Chapter_21.Section_21_1_Growing_Minimum_Spanning_Trees
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S1_UnionFindBridge
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S2_StatefulKruskal
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S3_ExecutablePrim
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S4_Completion
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S5_CountedFrontier
import CLRSLean.FourthEdition.Chapter_21.Section_21_2_Kruskal_And_Prim.S6_ArrayPrimCurrent source
Sections 21.1--21.2 are native fourth-edition sections (growing a minimum
spanning tree, and Kruskal and Prim with the nested union-find bridge,
incremental costed Kruskal, and executable indexed-queue Prim
developments), imported directly from
Section 21.1
and
Section 21.2.
The Kruskal bridge imports the fourth-edition disjoint-set sources
(Chapter 19). Declarations retain the legacy CLRS.MST namespace during
the compatibility period; the third-edition-numbered imports
CLRSLean.Chapter_23 and CLRSLean.Chapter_23.Section_23_* forward
to these sources.
Implementation details
The supporting implementation pages remain available outside the main sidebar:
Coverage boundary
The native sections supply the represented fourth-edition minimum-spanning-tree sections (Theorem 21.1 safe-edge characterization and the Kruskal/Prim correctness chains). Prim now derives coverage from sufficient fuel and constructs the MST of the actual run; no final spanning certificate or initial optimal tree is supplied by the caller. The graph premises still include connectedness, an exact component interpretation, and the existing restriction that crossing edge identifiers belong to the graph.
ArrayPrim.execute uses stored adjacency rows, cached array keys/parents,
and minimum scans. Its own counters prove 2n² + 5n + 6|E| cell work,
including index/queue initialization, at most n extractions and
2|E| adjacency visits. Here n is the ambient array size; it equals
|V| for the full index universe. Adjacency representation is input,
not constructed from an unordered edge set by this algorithm. Array allocation,
bit operations and arbitrary weight-function internals are outside this model.
The reference frontier execution also exposes actual full-edge rescans. The old binary-heap expression remains a conditional backend budget. Kruskal's combined formula includes a sorting budget plus the actual union-find scan cost; it does not count an executed comparison sort.
See docs/clrs-fourth-edition-map.csv for the section-level mapping and
docs/migrations/clrs4.md for compatibility and deprecation policy.
CLRS, fourth edition · Chapter 21 of 35