Imports
import Mathlib
import CLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.Ford_Fulkerson_Augmentation24.2. The Edmonds-Karp Algorithm
This section formalizes the residual-distance infrastructure used by the Edmonds-Karp analysis and proves the monotonic residual-distance theorem (CLRS Lemma 24.7) for augmentation along a shortest residual path.
Main results:
-
ResidualPathLength: inductive predicate for path existence inG_f -
IsShortestDist: shortest-path distance inG_f -
isShortestDist_self: the residual distance from a vertex to itself is zero -
IsShortestDist.unique: shortest residual distances are unique -
isShortestDist_triangle: one residual edge extends a shortest path by at most one step -
ShortestAugmentingPath: bundled shortest source-to-sink residual path data -
IsShortestDist.exists_predecessor: predecessor and exact-distance witness for a positive shortest path -
ShortestAugmentingPath.shortest_prefix: every prefix of a shortest augmenting path is itself shortest -
ShortestAugmentingPath.exists_shortestDist_le_augment: augmentation cannot create a smaller finite source distance -
shortest_path_nondec: CLRS Lemma 24.7
The shortest-path construction itself lives in the companion submodule
S1_ShortestAugmentingPath, whose headline result
exists_shortest_augmenting_path turns residual reachability into an explicit
shortest augmenting path.
The work analysis lives in S3_WorkAnalysis: critical edges, Lemma 24.8,
the recovery-step timeline lemma, and the full O(VE²) counting argument
(critical_count_bound and augmentation_count_bound). The executable
breadth-first search computing shortest residual paths — and with them the
shortest augmenting paths the loop augments along — lives in
S4_ExecutableBFS (residualBFS, bfs_shortestAugmenting).
Implementation details
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finsetopen Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}inductive ResidualPathLength (φ : Flow V G) : V → V → ℕ → Prop where
| refl (u : V) : ResidualPathLength φ u u 0
| tail (u v w : V) (n : ℕ) : ResidualPathLength φ u v n → Flow.residualEdge φ v w →
ResidualPathLength φ u w (n + 1)Concatenation of length-indexed residual paths.
theorem ResidualPathLength.trans {φ : Flow V G} {u v w : V} {m n : ℕ}
(h₁ : ResidualPathLength φ u v m) (h₂ : ResidualPathLength φ v w n) :
ResidualPathLength φ u w (m + n) := by
induction h₂ generalizing u with
| refl => simpa using h₁
| tail mid w n hprev hedge ih =>
have h := ResidualPathLength.tail u mid w (m + n) (ih h₁) hedge
simpa [Nat.add_assoc] using hdef IsShortestDist (φ : Flow V G) (u v : V) (d : ℕ) : Prop :=
ResidualPathLength φ u v d ∧ ∀ n, ResidualPathLength φ u v n → d ≤ nlemma isShortestDist_self (φ : Flow V G) (u : V) : IsShortestDist φ u u 0 := by
refine ⟨ResidualPathLength.refl u, ?_⟩
intro n hn
cases hn with
| refl => exact Nat.zero_le _
| tail _ _ _ _ _ => apply Nat.zero_lelemma IsShortestDist.unique {φ : Flow V G} {u v : V} {d₁ d₂ : ℕ}
(h₁ : IsShortestDist φ u v d₁) (h₂ : IsShortestDist φ u v d₂) : d₁ = d₂ := by
rcases h₁ with ⟨hpath₁, hmin₁⟩
rcases h₂ with ⟨hpath₂, hmin₂⟩
exact le_antisymm (hmin₁ d₂ hpath₂) (hmin₂ d₁ hpath₁)lemma isShortestDist_triangle (φ : Flow V G) (s u v : V) (d : ℕ)
(hsu : IsShortestDist φ s u d) (h_edge : Flow.residualEdge φ u v) :
∃ d', IsShortestDist φ s v d' ∧ d' ≤ d + 1 := by
rcases hsu with ⟨hsu_path, hsu_min⟩
have hsv_path : ResidualPathLength φ s v (d + 1) :=
ResidualPathLength.tail s u v d hsu_path h_edge
have h_exists_v : ∃ n, ResidualPathLength φ s v n := ⟨d + 1, hsv_path⟩
let d' := Nat.find h_exists_v
have h_d'_path : ResidualPathLength φ s v d' := Nat.find_spec h_exists_v
have h_d'_min : ∀ n, ResidualPathLength φ s v n → d' ≤ n :=
fun n hn => Nat.find_min' h_exists_v hn
have h_d'_le : d' ≤ d + 1 := Nat.find_min' h_exists_v hsv_path
exact ⟨d', ⟨h_d'_path, h_d'_min⟩, h_d'_le⟩A positive-length shortest residual path has a predecessor whose distance is exactly one smaller.
lemma exists_pred_on_path {φ : Flow V G} {s v : V} {d : ℕ}
(hd : IsShortestDist φ s v d) (hd_pos : d ≠ 0) :
∃ u, Flow.residualEdge φ u v ∧ IsShortestDist φ s u (d - 1) := by
rcases hd with ⟨hpath, hmin⟩
cases hpath with
| refl => exact (hd_pos rfl).elim
| tail u v n hpath_to_u hedge =>
have hu_min : ∀ m, ResidualPathLength φ s u m → n ≤ m := by
intro m hm
have hextend : ResidualPathLength φ s v (m + 1) :=
ResidualPathLength.tail s u v m hm hedge
have := hmin (m + 1) hextend
omega
refine ⟨u, hedge, ?_⟩
simpa [IsShortestDist] using And.intro hpath_to_u hu_minSuccessor-form predecessor theorem, convenient for induction on a known positive distance.
theorem IsShortestDist.exists_predecessor {φ : Flow V G} {s v : V} {d : ℕ}
(hd : IsShortestDist φ s v (d + 1)) :
∃ u, Flow.residualEdge φ u v ∧ IsShortestDist φ s u d := by
simpa using exists_pred_on_path hd (by omega)
A shortest augmenting path tied directly to the concrete path consumed by
Flow.augment.
The concrete simple residual path to augment.
Its edge count realizes the source-to-sink residual distance.
structure ShortestAugmentingPath (φ : Flow V G) where path : Flow.AugmentingPath φ h_shortest : IsShortestDist φ G.s G.t path.edges.length
private lemma residualPathLength_segment (φ : Flow V G) (xs : List V)
(hchain : xs.IsChain φ.residualEdge) (i k : ℕ)
(hik : i + k < xs.length) :
ResidualPathLength φ xs[i] xs[i + k] k := by
induction k with
| zero => simpa using ResidualPathLength.refl (φ := φ) xs[i]
| succ k ih =>
have hik' : i + k < xs.length := by omega
have hedge : φ.residualEdge xs[i + k] xs[i + k + 1] :=
hchain.getElem (i + k) (by omega)
have htail := ResidualPathLength.tail (φ := φ)
xs[i] xs[i + k] xs[i + k + 1] k (ih hik') hedge
simpa [Nat.add_assoc] using htailprivate lemma getElem_zero_eq_of_head?_eq_some {α : Type*} {xs : List α} {u : α}
(hzero : 0 < xs.length) (hhead : xs.head? = some u) :
xs[0] = u := by
cases xs with
| nil => simp at hzero
| cons x tail => simpa using hhead
private lemma getElem_last_eq_of_getLast?_eq_some
{α : Type*} {xs : List α} {u : α}
(hne : xs ≠ []) (hlast : xs.getLast? = some u) :
xs[xs.length - 1]'(Nat.sub_lt (List.length_pos_iff.mpr hne) (by omega)) = u := by
rw [← List.getLast_eq_getElem hne]
exact List.getLast_of_getLast?_eq_some hlast
The prefix through index i is a residual path of exactly i edges.
theorem ShortestAugmentingPath.prefix_path {φ : Flow V G}
(p : ShortestAugmentingPath φ) (i : ℕ)
(hi : i < p.path.vertices.length) :
ResidualPathLength φ G.s p.path.vertices[i] i := by
have hsegment := residualPathLength_segment φ p.path.vertices p.path.chain 0 i (by
simpa using hi)
have hfirst : p.path.vertices[0] = G.s :=
getElem_zero_eq_of_head?_eq_some (by omega) p.path.head_eq
simpa [hfirst] using hsegment
The suffix from index i reaches the sink in the remaining edge count.
theorem ShortestAugmentingPath.suffix_path {φ : Flow V G}
(p : ShortestAugmentingPath φ) (i : ℕ)
(hi : i < p.path.vertices.length) :
ResidualPathLength φ p.path.vertices[i] G.t (p.path.edges.length - i) := by
have hne : p.path.vertices ≠ [] := by
intro hnil
simpa [hnil] using p.path.head_eq
have hedges_length := p.path.edges_length
have hi_le_edges : i ≤ p.path.edges.length := by omega
have hsegment := residualPathLength_segment φ p.path.vertices p.path.chain i
(p.path.edges.length - i) (by omega)
have hlast : p.path.vertices[p.path.edges.length] = G.t := by
simpa only [hedges_length] using
getElem_last_eq_of_getLast?_eq_some hne p.path.last_eq
simpa [Nat.add_sub_of_le hi_le_edges, hlast] using hsegmentEvery prefix of a shortest augmenting path is itself shortest.
theorem ShortestAugmentingPath.shortest_prefix {φ : Flow V G}
(p : ShortestAugmentingPath φ) (i : ℕ)
(hi : i < p.path.vertices.length) :
IsShortestDist φ G.s p.path.vertices[i] i := by
refine ⟨p.prefix_path i hi, ?_⟩
intro n hn
have htotal := hn.trans (p.suffix_path i hi)
have hmin := p.h_shortest.2 _ htotal
have hi_le_edges : i ≤ p.path.edges.length := by
rw [p.path.edges_length]
omega
omega
private theorem ShortestAugmentingPath.exists_shortestDist_le_pathLength_augment
{φ : Flow V G} (p : ShortestAugmentingPath φ) {v : V} {n : ℕ}
(hpath : ResidualPathLength (φ.augment p.path) G.s v n) :
∃ d, IsShortestDist φ G.s v d ∧ d ≤ n := by
induction hpath with
| refl =>
exact ⟨0, isShortestDist_self φ G.s, le_rfl⟩
| tail u v n hpath_to_u hedge ih =>
rcases ih with ⟨du, hdu, hdu_le⟩
by_cases hold : φ.residualEdge u v
· rcases isShortestDist_triangle φ G.s u v du hdu hold with
⟨dv, hdv, hdv_le⟩
exact ⟨dv, hdv, by omega⟩
· have hreverse : (v, u) ∈ p.path.edges :=
p.path.reverse_mem_edges_of_new_residualEdge hedge hold
rcases p.path.exists_index_of_mem_edges hreverse with
⟨i, hi, hvi, hui⟩
have hpref_v := p.shortest_prefix i (by omega)
have hpref_u := p.shortest_prefix (i + 1) hi
have hdv : IsShortestDist φ G.s v i := by
simpa [hvi] using hpref_v
have hdu_path : IsShortestDist φ G.s u (i + 1) := by
simpa [hui] using hpref_u
have hdu_eq : du = i + 1 := hdu.unique hdu_path
exact ⟨i, hdv, by omega⟩Every vertex at finite residual distance after augmentation already had a finite residual distance before augmentation, no larger than the new one.
This is the path-lifting core of Lemma 24.7. An edge that already existed uses the one-edge triangle theorem. If an edge is new, the concrete augmentation formula identifies its reverse on the chosen augmenting path; shortest-prefix optimality then supplies the old distance directly.
theorem ShortestAugmentingPath.exists_shortestDist_le_augment
{φ : Flow V G} (p : ShortestAugmentingPath φ) {v : V} {d' : ℕ}
(hd' : IsShortestDist (φ.augment p.path) G.s v d') :
∃ d, IsShortestDist φ G.s v d ∧ d ≤ d' := by
exact p.exists_shortestDist_le_pathLength_augment hd'.1CLRS Lemma 24.7 (monotonic residual distance). Augmenting along a shortest residual source-to-sink path cannot decrease the finite residual distance from the source to any vertex.
theorem shortest_path_nondec (φ : Flow V G) (p : ShortestAugmentingPath φ)
{v : V} {d d' : ℕ}
(hd : IsShortestDist φ G.s v d)
(hd' : IsShortestDist (φ.augment p.path) G.s v d') :
d ≤ d' := by
rcases p.exists_shortestDist_le_augment hd' with ⟨d₀, hd₀, hd₀_le⟩
have hdist : d = d₀ := hd.unique hd₀
omegaend Chapter26end CLRSDefinitions and proofs
CLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.Ford_Fulkerson_Augmentation
24.2. Ford--Fulkerson Augmentation
This file formalizes the constructive augmentation step of the Ford--Fulkerson method. It packages a simple residual path as an explicit list of vertices, defines its bottleneck, constructs the resulting feasible flow, and proves the exact and strict increase in flow value. It also converts residual source-to-sink reachability into a concrete simple augmenting path and derives non-maximality from that witness.
The directed-edge representation is important for networks with anti-parallel capacities: traversing an ordered edge always consumes its directed residual capacity, whether that capacity comes from unused forward capacity, cancellation of existing flow, or both.
Main results:
-
Flow.augmentBy_valueandFlow.augment_value: augmentation increases the flow value by exactly the selected amount or path bottleneck. -
Flow.value_lt_augment: full bottleneck augmentation strictly increases the flow value. -
Flow.hasAugmentingPath_iff_nonempty_augmentingPath: residual reachability is equivalent to an explicit simple augmenting path. -
Flow.not_maximal_of_hasAugmentingPath: a flow with an augmenting path is not maximal.
Current gaps: none for the concrete mathematical augmentation layer. The executable Edmonds--Karp loop remains in the companion analysis; its Lemma 24.7 distance-monotonicity foundation is proved there.
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finset Classicalnamespace FlowA simple directed residual path between two specified vertices.
The endpoint equations ensure that the vertex list is nonempty. The no-duplicates field supplies the local edge-indicator formula, rules out the simultaneous appearance of both orientations of one edge, and supports the capacity proof. Skew symmetry of the update itself does not require path simplicity.
Vertices in path order, including both endpoints.
Every consecutive pair is a residual edge.
The first vertex is the requested path source.
The final vertex is the requested path target.
The path is simple.
structure ResidualPath {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (u v : V) where vertices : List V chain : vertices.IsChain φ.residualEdge head_eq : vertices.head? = some u last_eq : vertices.getLast? = some v nodup : vertices.NodupA simple residual path from the network source to its sink.
abbrev AugmentingPath {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) :=
ResidualPath φ G.s G.tConsecutive directed edges of a residual path.
def ResidualPath.edges {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} {u v : V}
(p : ResidualPath φ u v) : List (V × V) :=
p.vertices.zip p.vertices.tailThe number of directed edges is one less than the number of vertices.
theorem ResidualPath.edges_length {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G} {u v : V}
(p : ResidualPath φ u v) :
p.edges.length = p.vertices.length - 1 := by
simp [ResidualPath.edges]Membership in the directed edge list determines a consecutive pair of vertex indices.
theorem ResidualPath.exists_index_of_mem_edges {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G} {s t u v : V}
(p : ResidualPath φ s t) (huv : (u, v) ∈ p.edges) :
∃ i, ∃ hi : i + 1 < p.vertices.length,
p.vertices[i] = u ∧ p.vertices[i + 1] = v := by
rw [List.mem_iff_getElem] at huv
rcases huv with ⟨i, hi, hget⟩
have hi_vertices : i + 1 < p.vertices.length := by
rw [p.edges_length] at hi
omega
refine ⟨i, hi_vertices, ?_⟩
have hpair : (p.vertices[i], p.vertices[i + 1]) = (u, v) := by
calc
(p.vertices[i], p.vertices[i + 1]) = p.edges[i] := by
simp [ResidualPath.edges, List.getElem_zip, List.getElem_tail]
_ = (u, v) := hget
exact ⟨congrArg Prod.fst hpair, congrArg Prod.snd hpair⟩private theorem residualEdge_of_mem_zip_tail {V : Type*}
{r : V → V → Prop} {vertices : List V} (hchain : vertices.IsChain r)
{u v : V} (hmem : (u, v) ∈ vertices.zip vertices.tail) : r u v := by
induction vertices with
| nil => simp at hmem
| cons a l ih =>
cases l with
| nil => simp at hmem
| cons b l =>
simp only [List.tail_cons, List.zip_cons_cons, List.mem_cons] at hmem
rcases hmem with hfirst | hrest
· have hu : u = a := congrArg Prod.fst hfirst
have hv : v = b := congrArg Prod.snd hfirst
subst u
subst v
exact List.IsChain.rel_head hchain
· exact ih hchain.tail hrestEvery edge listed by a residual path has positive residual capacity.
theorem ResidualPath.residualEdge_of_mem_edges {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G} {s t x y : V}
(p : ResidualPath φ s t) (hxy : (x, y) ∈ p.edges) :
φ.residualEdge x y := by
exact residualEdge_of_mem_zip_tail p.chain hxyAn augmenting path contains at least one directed edge.
theorem AugmentingPath.edges_nonempty {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) : p.edges ≠ [] := by
cases hvertices : p.vertices with
| nil =>
have hhead := p.head_eq
simp [hvertices] at hhead
| cons a l =>
cases l with
| nil =>
have has : a = G.s := by simpa [hvertices] using p.head_eq
have hat : a = G.t := by simpa [hvertices] using p.last_eq
exfalso
exact G.hs_ne_t (has.symm.trans hat)
| cons b l => simp [ResidualPath.edges, hvertices]private theorem reverse_not_mem_zip_tail {V : Type*} [DecidableEq V]
{vertices : List V} (hnodup : vertices.Nodup) {u v : V}
(huv : (u, v) ∈ vertices.zip vertices.tail) :
(v, u) ∉ vertices.zip vertices.tail := by
induction vertices with
| nil => simp at huv
| cons a l ih =>
cases l with
| nil => simp at huv
| cons b l =>
simp only [List.tail_cons, List.zip_cons_cons, List.mem_cons] at huv ⊢
simp only [List.nodup_cons] at hnodup
rcases hnodup with ⟨ha, htail⟩
rcases huv with hfirst | hrest
· have hu : u = a := congrArg Prod.fst hfirst
have hv : v = b := congrArg Prod.snd hfirst
subst u
subst v
intro hreverse
rcases hreverse with hba | hba
· have hba' : b = a := congrArg Prod.fst hba
exact ha (by simp [hba'])
· exact ha (List.mem_of_mem_tail (List.of_mem_zip hba).2)
· intro hreverse
rcases hreverse with hfirst | hrest_reverse
· have hv : v = a := congrArg Prod.fst hfirst
have hu : u = b := congrArg Prod.snd hfirst
subst v
subst u
exact ha (List.mem_of_mem_tail (List.of_mem_zip hrest).2)
· exact ih (List.nodup_cons.mpr htail) hrest hrest_reverseA simple residual path cannot contain both orientations of the same edge.
This combinatorial fact is independent of capacities. In particular, it continues to hold when the network itself has positive capacities in both directions.
theorem ResidualPath.reverse_not_mem_edges {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G} {s t u v : V}
(p : ResidualPath φ s t) (huv : (u, v) ∈ p.edges) :
(v, u) ∉ p.edges := by
exact reverse_not_mem_zip_tail p.nodup huvprivate theorem AugmentingPath.edgeFinset_nonempty {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) : p.edges.toFinset.Nonempty := by
exact (List.toFinset_nonempty_iff p.edges).2 p.edges_nonemptyprivate theorem AugmentingPath.capacityFinset_nonempty {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) :
(p.edges.toFinset.image
(fun e => φ.residualCapacity e.1 e.2)).Nonempty := by
exact Finset.image_nonempty.mpr p.edgeFinset_nonemptyMinimum residual capacity among the directed edges of an augmenting path.
noncomputable def AugmentingPath.bottleneck {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) : ℝ :=
let capacities := p.edges.toFinset.image
(fun e => φ.residualCapacity e.1 e.2)
capacities.min' p.capacityFinset_nonemptyThe bottleneck of an augmenting path is strictly positive.
theorem AugmentingPath.bottleneck_pos {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) : 0 < p.bottleneck := by
unfold AugmentingPath.bottleneck
rw [Finset.lt_min'_iff]
intro capacity hcapacity
rcases Finset.mem_image.mp hcapacity with ⟨edge, hedge, rfl⟩
exact p.residualEdge_of_mem_edges (by simpa using hedge)The path bottleneck is at most the residual capacity of each path edge.
theorem AugmentingPath.bottleneck_le_residualCapacity {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} {φ : Flow V G}
(p : AugmentingPath φ) {u v : V} (huv : (u, v) ∈ p.edges) :
p.bottleneck ≤ φ.residualCapacity u v := by
unfold AugmentingPath.bottleneck
apply Finset.min'_le
exact Finset.mem_image.mpr ⟨(u, v), by simpa using huv, rfl⟩Path updates
Skew-symmetric update contributed by one oriented path edge.
def edgeDelta {V : Type*} [DecidableEq V]
(delta : ℝ) (a b u v : V) : ℝ :=
(if u = a ∧ v = b then delta else 0) -
(if u = b ∧ v = a then delta else 0)Sum of the skew-symmetric updates contributed by consecutive path edges.
def pathDelta {V : Type*} [DecidableEq V]
(delta : ℝ) : List V → V → V → ℝ
| [], _, _ => 0
| [_], _, _ => 0
| a :: b :: xs, u, v =>
edgeDelta delta a b u v + pathDelta delta (b :: xs) u v
termination_by xs => xs.lengthA single oriented-edge update is skew-symmetric.
theorem edgeDelta_skew {V : Type*} [DecidableEq V]
(delta : ℝ) (a b u v : V) :
edgeDelta delta a b u v = -edgeDelta delta a b v u := by
simp only [edgeDelta]
by_cases hua : u = a <;> by_cases hvb : v = b <;>
by_cases hub : u = b <;> by_cases hva : v = a <;>
simp [hua, hvb, hub, hva, and_comm]The complete path update is skew-symmetric.
theorem pathDelta_skew {V : Type*} [DecidableEq V]
(delta : ℝ) (xs : List V) (u v : V) :
pathDelta delta xs u v = -pathDelta delta xs v u := by
induction xs with
| nil => simp [pathDelta]
| cons a xs ih =>
cases xs with
| nil => simp [pathDelta]
| cons b xs =>
simp only [pathDelta]
rw [edgeDelta_skew, ih]
ringNet divergence of the update contributed by one oriented edge.
theorem edgeDelta_sum {V : Type*} [Fintype V] [DecidableEq V]
(delta : ℝ) (a b u : V) :
(Finset.univ : Finset V).sum (fun v => edgeDelta delta a b u v) =
(if u = a then delta else 0) - (if u = b then delta else 0) := by
rw [show (fun v => edgeDelta delta a b u v) =
(fun v => (if u = a ∧ v = b then delta else 0) -
(if u = b ∧ v = a then delta else 0)) by rfl]
rw [Finset.sum_sub_distrib]
have hforward :
(Finset.univ : Finset V).sum
(fun v => if u = a ∧ v = b then delta else 0) =
(if u = a then delta else 0) := by
by_cases h : u = a
· simp [h]
· simp [h]
have hbackward :
(Finset.univ : Finset V).sum
(fun v => if u = b ∧ v = a then delta else 0) =
(if u = b then delta else 0) := by
by_cases h : u = b
· simp [h]
· simp [h]
rw [hforward, hbackward]Net divergence of a path update is concentrated at its two endpoints.
theorem pathDelta_sum {V : Type*} [Fintype V] [DecidableEq V]
(delta : ℝ) (xs : List V) (u : V) :
(Finset.univ : Finset V).sum (fun v => pathDelta delta xs u v) =
(if xs.head? = some u then delta else 0) -
(if xs.getLast? = some u then delta else 0) := by
induction xs with
| nil => simp [pathDelta]
| cons a xs ih =>
cases xs with
| nil => simp [pathDelta]
| cons b xs =>
simp only [pathDelta, Finset.sum_add_distrib]
rw [edgeDelta_sum, ih]
rw [List.getLast?_cons_cons]
simp only [List.head?_cons, Option.some.injEq]
by_cases hua : u = a <;> by_cases hub : u = b <;>
simp [hua, hub, eq_comm]private theorem fst_mem_of_mem_consecutivePairs {V : Type*}
{a b : V} {xs : List V} (h : (a, b) ∈ xs.consecutivePairs) : a ∈ xs := by
exact (List.of_mem_zip h).1private theorem snd_mem_of_mem_consecutivePairs {V : Type*}
{a b : V} {xs : List V} (h : (a, b) ∈ xs.consecutivePairs) : b ∈ xs := by
exact List.mem_of_mem_tail (List.of_mem_zip h).2On a simple vertex list, the path update is exactly the difference of the two directed edge-membership indicators.
theorem pathDelta_eq_edgeIndicators_of_nodup
{V : Type*} [DecidableEq V]
(delta : ℝ) (xs : List V) (u v : V) (hxs : xs.Nodup) :
pathDelta delta xs u v =
(if (u, v) ∈ xs.consecutivePairs then delta else 0) -
(if (v, u) ∈ xs.consecutivePairs then delta else 0) := by
induction xs with
| nil => simp [pathDelta, List.consecutivePairs]
| cons a xs ih =>
cases xs with
| nil => simp [pathDelta, List.consecutivePairs]
| cons b xs =>
have hparts := List.nodup_cons.mp hxs
have ha_not : a ∉ b :: xs := hparts.1
have htail : (b :: xs).Nodup := hparts.2
have hab : a ≠ b := by
intro hab
apply ha_not
simp [hab]
have hab_not_tail : (a, b) ∉ (b :: xs).consecutivePairs := by
intro h
exact ha_not (fst_mem_of_mem_consecutivePairs h)
have hba_not_tail : (b, a) ∉ (b :: xs).consecutivePairs := by
intro h
exact ha_not (snd_mem_of_mem_consecutivePairs h)
have hcp : (a :: b :: xs).consecutivePairs =
(a, b) :: (b :: xs).consecutivePairs := rfl
rw [pathDelta]
rw [ih htail]
by_cases hf : (u, v) = (a, b)
· have hu : u = a := congrArg Prod.fst hf
have hv : v = b := congrArg Prod.snd hf
subst u
subst v
simp [edgeDelta, hcp, hab, hab_not_tail, hba_not_tail]
· by_cases hr : (v, u) = (a, b)
· have hv : v = a := congrArg Prod.fst hr
have hu : u = b := congrArg Prod.snd hr
subst u
subst v
simp [edgeDelta, hcp, hab, hab_not_tail, hba_not_tail]
· have hforward : ¬(u = a ∧ v = b) := by
intro h
exact hf (Prod.ext h.1 h.2)
have hreverse : ¬(u = b ∧ v = a) := by
intro h
exact hr (Prod.ext h.2 h.1)
simp [edgeDelta, hcp, hf, hr, hforward, hreverse]Augment a flow by a nonnegative amount bounded by every residual capacity on the selected path.
def augmentBy {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ)
(delta : ℝ) (hdelta : 0 ≤ delta)
(hcap : ∀ e ∈ p.edges, delta ≤ φ.residualCapacity e.1 e.2) :
Flow V G where
f u v := φ.f u v + pathDelta delta p.vertices u v
hcapacity := by
intro u v
rw [pathDelta_eq_edgeIndicators_of_nodup delta p.vertices u v p.nodup]
by_cases huv : (u, v) ∈ p.vertices.consecutivePairs <;>
by_cases hvu : (v, u) ∈ p.vertices.consecutivePairs
· rw [if_pos huv, if_pos hvu]
ring_nf
exact φ.hcapacity u v
· rw [if_pos huv, if_neg hvu]
have hmem : (u, v) ∈ p.edges := by
simpa [ResidualPath.edges] using huv
have h := hcap (u, v) hmem
unfold residualCapacity at h
linarith
· rw [if_neg huv, if_pos hvu]
have h := φ.hcapacity u v
linarith
· rw [if_neg huv, if_neg hvu]
ring_nf
exact φ.hcapacity u v
hskew_symm := by
intro u v
rw [φ.hskew_symm, pathDelta_skew]
ring
hconservation := by
intro u hu_s hu_t
simp only [Finset.sum_add_distrib]
rw [φ.hconservation u hu_s hu_t]
rw [pathDelta_sum]
rw [p.head_eq, p.last_eq]
simp [Ne.symm hu_s, Ne.symm hu_t]Augmenting by an admissible amount increases flow value by exactly that amount.
theorem augmentBy_value {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ)
(delta : ℝ) (hdelta : 0 ≤ delta)
(hcap : ∀ e ∈ p.edges, delta ≤ φ.residualCapacity e.1 e.2) :
(φ.augmentBy p delta hdelta hcap).value = φ.value + delta := by
unfold value augmentBy
rw [Finset.sum_add_distrib]
rw [pathDelta_sum]
rw [p.head_eq, p.last_eq]
simp [Ne.symm G.hs_ne_t]Augment a flow by the full bottleneck capacity of a selected augmenting path.
noncomputable def augment {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ) : Flow V G :=
φ.augmentBy p p.bottleneck p.bottleneck_pos.le (by
intro e he
rcases e with ⟨u, v⟩
exact p.bottleneck_le_residualCapacity (by simpa using he))Exact residual-capacity update for full augmentation along a simple path.
The formula remains valid when the original network has anti-parallel positive capacities: it records directed path membership rather than classifying an edge as globally forward or backward.
theorem augment_residualCapacity {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ) (u v : V) :
(φ.augment p).residualCapacity u v =
φ.residualCapacity u v -
(if (u, v) ∈ p.edges then p.bottleneck else 0) +
(if (v, u) ∈ p.edges then p.bottleneck else 0) := by
change G.c u v - (φ.f u v + pathDelta p.bottleneck p.vertices u v) = _
rw [pathDelta_eq_edgeIndicators_of_nodup
p.bottleneck p.vertices u v p.nodup]
simp only [ResidualPath.edges]
unfold residualCapacity
ring_nfEvery residual edge created by full augmentation reverses a directed edge of the augmented path.
theorem AugmentingPath.reverse_mem_edges_of_new_residualEdge
{V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} (p : AugmentingPath φ) {u v : V}
(hnew : (φ.augment p).residualEdge u v)
(hold : ¬φ.residualEdge u v) :
(v, u) ∈ p.edges := by
have hold_nonpos : φ.residualCapacity u v ≤ 0 := le_of_not_gt hold
change (φ.augment p).residualCapacity u v > 0 at hnew
rw [φ.augment_residualCapacity p] at hnew
by_contra hreverse
rw [if_neg hreverse] at hnew
by_cases hforward : (u, v) ∈ p.edges
· rw [if_pos hforward] at hnew
nlinarith [p.bottleneck_pos]
· rw [if_neg hforward] at hnew
linarithFull bottleneck augmentation increases value by exactly the bottleneck.
theorem augment_value {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ) :
(φ.augment p).value = φ.value + p.bottleneck := by
simpa [augment] using
φ.augmentBy_value p p.bottleneck p.bottleneck_pos.le (by
intro e he
rcases e with ⟨u, v⟩
exact p.bottleneck_le_residualCapacity (by simpa using he))Augmenting along a residual source-to-sink path strictly increases value.
theorem value_lt_augment {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ) :
φ.value < (φ.augment p).value := by
rw [φ.augment_value p]
linarith [p.bottleneck_pos]Reachability bridge and non-maximality
private theorem exists_dup_decomp {α : Type*} [DecidableEq α] :
∀ {xs : List α}, ¬xs.Nodup →
∃ (x : α) (left middle right : List α),
xs = left ++ x :: middle ++ x :: right := by
intro xs
induction xs with
| nil =>
intro h
simp at h
| cons a tail ih =>
intro h
by_cases ha : a ∈ tail
· obtain ⟨middle, right, htail⟩ := List.mem_iff_append.mp ha
exact ⟨a, [], middle, right, by rw [htail]; simp⟩
· have htail : ¬tail.Nodup :=
fun htail => h (List.nodup_cons.mpr ⟨ha, htail⟩)
obtain ⟨x, left, middle, right, htail_eq⟩ := ih htail
exact ⟨x, a :: left, middle, right, by rw [htail_eq]; simp⟩
private theorem exists_nodup_chain_same_ends
{α : Type*} [DecidableEq α] {r : α → α → Prop} :
∀ (n : ℕ) (xs : List α), xs.length ≤ n → xs ≠ [] →
xs.IsChain r →
∃ ys : List α,
ys ≠ [] ∧ ys.IsChain r ∧ ys.head? = xs.head? ∧
ys.getLast? = xs.getLast? ∧ ys.Nodup := by
intro n
induction n with
| zero =>
intro xs hlen hne _
have hnil : xs = [] := List.length_eq_zero_iff.mp (Nat.le_zero.mp hlen)
exact (hne hnil).elim
| succ n ih =>
intro xs hlen hne hchain
by_cases hnodup : xs.Nodup
· exact ⟨xs, hne, hchain, rfl, rfl, hnodup⟩
· obtain ⟨x, left, middle, right, hxs⟩ := exists_dup_decomp hnodup
let shorter := left ++ x :: right
have hleft_middle : (left ++ x :: middle) <+: xs := by
refine ⟨x :: right, ?_⟩
rw [hxs]
have hright : (x :: right) <:+ xs := by
refine ⟨left ++ x :: middle, ?_⟩
rw [hxs]
have hchain_left_middle : (left ++ x :: middle).IsChain r :=
hchain.prefix hleft_middle
have hchain_left : left.IsChain r := hchain_left_middle.left_of_append
have hchain_right : (x :: right).IsChain r := hchain.suffix hright
have hchain_shorter : shorter.IsChain r := by
dsimp [shorter]
refine hchain_left.append hchain_right ?_
intro a ha b hb
have hbx : b = x := (show x = b by simpa using hb).symm
rw [hbx]
exact (List.isChain_append.1 hchain_left_middle).2.2 a ha x (by simp)
have hhead_shorter : shorter.head? = xs.head? := by
dsimp [shorter]
rw [hxs]
cases left <;> simp
have hlast_shorter : shorter.getLast? = xs.getLast? := by
dsimp [shorter]
have hxright : (x :: right).getLast? = xs.getLast? := by
rw [hxs, List.getLast?_append_of_ne_nil _ (by simp : (x :: right) ≠ [])]
rw [List.getLast?_append_of_ne_nil _ (by simp : (x :: right) ≠ [])]
exact hxright
have hshorter_ne : shorter ≠ [] := by
dsimp [shorter]
simp
have hlen_xs : xs.length = left.length + middle.length + right.length + 2 := by
rw [hxs]
simp only [List.length_append, List.length_cons]
omega
have hlen_shorter : shorter.length = left.length + right.length + 1 := by
dsimp [shorter]
simp only [List.length_append, List.length_cons]
omega
have hshorter_le : shorter.length ≤ n := by omega
obtain ⟨ys, hys_ne, hys_chain, hys_head, hys_last, hys_nodup⟩ :=
ih shorter hshorter_le hshorter_ne hchain_shorter
exact ⟨ys, hys_ne, hys_chain, hys_head.trans hhead_shorter,
hys_last.trans hlast_shorter, hys_nodup⟩Residual reachability from source to sink is equivalent to the existence of an explicit simple augmenting path.
theorem hasAugmentingPath_iff_nonempty_augmentingPath
{V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} :
φ.hasAugmentingPath ↔ Nonempty (AugmentingPath φ) := by
constructor
· intro hreach
rcases List.exists_isChain_ne_nil_of_relationReflTransGen hreach with
⟨xs, hxs_ne, hxs_chain, hxs_head, hxs_last⟩
obtain ⟨ys, hys_ne, hys_chain, hys_head, hys_last, hys_nodup⟩ :=
exists_nodup_chain_same_ends xs.length xs le_rfl hxs_ne hxs_chain
have hxs_head_option : xs.head? = some G.s :=
(List.head?_eq_some_head hxs_ne).trans (congrArg some hxs_head)
have hxs_last_option : xs.getLast? = some G.t :=
(List.getLast?_eq_some_getLast hxs_ne).trans (congrArg some hxs_last)
exact ⟨{
vertices := ys
chain := hys_chain
head_eq := hys_head.trans hxs_head_option
last_eq := hys_last.trans hxs_last_option
nodup := hys_nodup
}⟩
· rintro ⟨path⟩
have hvertices_ne : path.vertices ≠ [] := by
intro hnil
simpa [hnil] using path.head_eq
have hhead : path.vertices.head hvertices_ne = G.s := by
have h := path.head_eq
rw [List.head?_eq_some_head hvertices_ne] at h
exact Option.some.inj h
have hlast : path.vertices.getLast hvertices_ne = G.t := by
have h := path.last_eq
rw [List.getLast?_eq_some_getLast hvertices_ne] at h
exact Option.some.inj h
have hreach := List.relationReflTransGen_of_exists_isChain
path.vertices path.chain hvertices_ne
simpa [hasAugmentingPath, augmentingPathReachable, hhead, hlast]
using hreachA concrete augmenting path witnesses that the current flow is not maximal.
theorem not_maximal_of_augmentingPath
{V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (p : AugmentingPath φ) :
¬φ.isMaximal := by
intro hmaximal
exact (not_le_of_gt (φ.value_lt_augment p)) (hmaximal (φ.augment p))Residual source-to-sink reachability implies that the current flow is not maximal.
theorem not_maximal_of_hasAugmentingPath
{V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (hpath : φ.hasAugmentingPath) :
¬φ.isMaximal := by
rcases hasAugmentingPath_iff_nonempty_augmentingPath.mp hpath with ⟨p⟩
exact φ.not_maximal_of_augmentingPath pend Flowend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S1_ShortestAugmentingPath
24.2 S1. Shortest augmenting paths
This module constructs an explicit shortest residual source-to-sink path
whenever the sink is residual-reachable. The construction walks backwards
from the sink through exact predecessors (IsShortestDist.exists_predecessor),
collecting vertices into a list whose distance from the source strictly
decreases, then reverses it into a simple Flow.ResidualPath whose edge count
realizes the residual distance.
Main results:
-
back: the backwards walk from a vertex at distanced -
back_head,back_last,back_length,back_chain_rev,back_nodup, andback_getElem_shortest: its structural properties -
shortestFlow.ResidualPath: the assembled shortest residual source-to-sink path -
exists_shortest_augmenting_path: residual reachability yields a shortest augmenting path (the mathematical core shared by the Edmonds-Karp loop and theO(VE²)analysis)
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finsetopen Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
The vertices of a shortest residual path from s to v, listed from v
back to s: v, its exact predecessor, and so on down to the source.
noncomputable def back {φ : Flow V G} : (d : ℕ) → (v : V) → IsShortestDist φ G.s v d → List V
| 0, v, _ => [v]
| d + 1, v, hd =>
let u := Classical.choose (IsShortestDist.exists_predecessor hd)
let hdu := (Classical.choose_spec (IsShortestDist.exists_predecessor hd)).2
v :: back d u hduThe backward walk starts at the requested vertex.
lemma back_head {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
(back d v hd).head? = some v := by
induction d generalizing v with
| zero => simp [back]
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
simp [back]The backward walk ends at the source.
lemma back_last {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
(back d v hd).getLast? = some G.s := by
induction d generalizing v with
| zero =>
have hv : v = G.s := by
rcases hd with ⟨hpath, _⟩
cases hpath with
| refl => rfl
simp [back, hv]
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
simp [back, List.getLast?_cons, ih (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2]
The backward walk from distance d has exactly d + 1 vertices.
lemma back_length {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
(back d v hd).length = d + 1 := by
induction d generalizing v with
| zero => simp [back]
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
simp [back, ih (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2]
The vertex at position i of the backward walk has residual distance
d - i from the source.
lemma back_getElem_shortest {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
∀ i (hi : i < (back d v hd).length),
IsShortestDist φ G.s (back d v hd)[i] (d - i) := by
induction d generalizing v with
| zero =>
intro i hi
have hlen : (back 0 v hd).length = 1 := by simp [back]
have hi0 : i = 0 := by omega
subst i
simpa [back] using hd
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
intro i hi
cases i with
| zero => simpa [back] using hd
| succ j =>
have hj : j < (back d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2).length := by
simpa [back] using hi
have hget : (back (d + 1) v hd)[j + 1] =
(back d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2)[j] := by
rfl
rw [hget]
have hshort := ih (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2 j hj
convert hshort using 1
omega
Consecutive pairs of the backward walk are residual edges (in the reverse
direction: a precedes b when the residual edge is b → a).
lemma back_chain_rev {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
(back d v hd).IsChain (fun a b => φ.residualEdge b a) := by
induction d generalizing v with
| zero => simp [back]
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
apply List.IsChain.cons
· exact ih (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2
· intro y hy
have hu := back_head d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2
have hyu : y = Classical.choose (IsShortestDist.exists_predecessor hd) := by
simpa [hu, eq_comm] using hy
simpa [hyu] using hspec.1The backward walk is a simple list: its distances strictly decrease, so no vertex repeats.
lemma back_nodup {φ : Flow V G} (d : ℕ) (v : V) (hd : IsShortestDist φ G.s v d) :
(back d v hd).Nodup := by
induction d generalizing v with
| zero => simp [back]
| succ d ih =>
have hspec := Classical.choose_spec (IsShortestDist.exists_predecessor hd)
constructor
· intro hmem hmem_mem
have hmem' : ∃ i, ∃ (h : i < (back d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2).length),
(back d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2)[i] = hmem :=
List.mem_iff_getElem.mp hmem_mem
rcases hmem' with ⟨j, hj, hget⟩
have hshort := back_getElem_shortest d (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2 j hj
have hd' : IsShortestDist φ G.s hmem (d - j) := by
simpa [hget] using hshort
intro hv
have hd'' : IsShortestDist φ G.s v (d - j) := by
simpa [hv] using hd'
have heq : d + 1 = d - j := hd.unique hd''
omega
· exact ih (Classical.choose (IsShortestDist.exists_predecessor hd)) hspec.2Appending a vertex related to the last element of a chain preserves the chain.
lemma IsChain_append_last {α : Type*} {R : α → α → Prop} {xs : List α} {x : α}
(hchain : xs.IsChain R) (hlast : ∀ y, y ∈ xs.getLast? → R y x) :
(xs ++ [x]).IsChain R := by
induction xs with
| nil => simp
| cons a xs ih =>
apply List.IsChain.cons
· exact ih hchain.tail (by
intro y hy
have h' : y ∈ (a :: xs).getLast? := by
rw [List.getLast?_cons]
simp
have hys : xs.getLast? = some y := by simpa using hy
rw [hys]
rfl
simpa using hlast y h')
· intro y hy
cases xs with
| nil =>
have hyx : y = x := by
have hxy : x = y := by simpa using hy
exact hxy.symm
simpa [hyx] using hlast a (by simp)
| cons b xs =>
have hyb : y = b := by
have hby : b = y := by simpa using hy
exact hby.symm
simpa [hyb] using hchain.rel_headDecomposing a chain that ends in a singleton: the prefix is a chain and its last element relates to the appended one.
lemma IsChain_append_elim {α : Type*} {R : α → α → Prop} {xs : List α} {a : α}
(h : (xs ++ [a]).IsChain R) (hxs : xs ≠ []) :
xs.IsChain R ∧ ∀ y, y ∈ xs.getLast? → R y a := by
induction xs with
| nil => simp at hxs
| cons b xs ih =>
cases xs
case nil =>
constructor
· simp
· intro y hy
have hyb : y = b := by
have hby : b = y := by simpa using hy
exact hby.symm
simpa [hyb] using h.rel_head
case cons c xs =>
rcases ih h.tail (by simp) with ⟨hxs_chain, hlast_xs⟩
constructor
· apply List.IsChain.cons
· exact hxs_chain
· intro y hy
have hyc : y = c := by
have hcy : c = y := by simpa using hy
exact hcy.symm
simpa [hyc] using h.rel_head
· intro y hy
have hget : (b :: c :: xs).getLast? = (c :: xs).getLast? := by
simp [List.getLast?_cons_cons]
have hy' : y ∈ (c :: xs).getLast? := by
simpa [hget] using hy
simpa using hlast_xs y hy'Reversing a chain swaps the relation.
lemma IsChain_reverse_swap {α : Type*} {R : α → α → Prop} {l : List α}
(h : l.IsChain (fun a b => R b a)) : l.reverse.IsChain R := by
induction l using List.reverseRecOn with
| nil => simp
| append_singleton xs a ih =>
by_cases hxs : xs = []
· simp [hxs]
· rcases IsChain_append_elim (R := fun a b => R b a) h hxs with ⟨hxs_chain, hlast_xs⟩
simp [List.reverse_append]
apply List.IsChain.cons
· exact ih hxs_chain
· intro y hy
simpa [List.head?_reverse] using hlast_xs y (by simpa [List.head?_reverse] using hy)
A residual chain from u to v of length k gives a length-indexed
residual path.
lemma chain_segment {φ : Flow V G} (xs : List V)
(hchain : xs.IsChain φ.residualEdge) (i k : ℕ)
(hik : i + k < xs.length) :
ResidualPathLength φ xs[i] xs[i + k] k := by
induction k with
| zero => simpa using ResidualPathLength.refl (φ := φ) xs[i]
| succ k ih =>
have hik' : i + k < xs.length := by omega
have hedge : φ.residualEdge xs[i + k] xs[i + k + 1] :=
hchain.getElem (i + k) (by omega)
have htail := ResidualPathLength.tail (φ := φ)
xs[i] xs[i + k] xs[i + k + 1] k (ih hik') hedge
simpa [Nat.add_assoc] using htail
The shortest residual source-to-sink path realizing residual distance
d.
noncomputable def shortestFlow.ResidualPath {φ : Flow V G} (d : ℕ)
(hd : IsShortestDist φ G.s G.t d) : Flow.ResidualPath φ G.s G.t :=
{ vertices := (back d G.t hd).reverse
, chain := by
exact IsChain_reverse_swap (back_chain_rev d G.t hd)
, head_eq := by
simpa [List.head?_reverse] using back_last d G.t hd
, last_eq := by
simpa [List.getLast?_reverse] using back_head d G.t hd
, nodup := by
exact List.nodup_reverse.mpr (back_nodup d G.t hd)
}The edge count of the shortest path realizes the residual distance.
lemma shortestFlow.ResidualPath_edges_length {φ : Flow V G} (d : ℕ)
(hd : IsShortestDist φ G.s G.t d) :
(shortestFlow.ResidualPath d hd).edges.length = d := by
rw [Flow.ResidualPath.edges_length]
simp [shortestFlow.ResidualPath, back_length d G.t hd]Shortest augmenting path existence. If the sink is residual-reachable from the source, there is an explicit simple augmenting path whose edge count realizes the residual distance (the mathematical core of the Edmonds-Karp loop and its analysis).
theorem exists_shortest_augmenting_path (φ : Flow V G) (h : φ.hasAugmentingPath) :
Nonempty (ShortestAugmentingPath φ) := by
rcases (Flow.hasAugmentingPath_iff_nonempty_augmentingPath.mp h) with ⟨p⟩
have hne : p.vertices ≠ [] := by
intro hnil
simpa [hnil] using p.head_eq
have hlen : 0 < p.vertices.length := List.length_pos_iff.mpr hne
have hseg := chain_segment p.vertices p.chain 0 (p.vertices.length - 1) (by omega)
have hfirst : p.vertices[0] = G.s := by
have hhead : p.vertices.head hne = G.s := by
simpa [List.head?_eq_some_head hne] using p.head_eq
exact (List.head_eq_getElem hne).symm.trans hhead
have hlast : p.vertices[p.vertices.length - 1]'(Nat.sub_lt hlen (by omega)) = G.t := by
rw [← List.getLast_eq_getElem hne]
exact List.getLast_of_getLast?_eq_some p.last_eq
have hpath : ResidualPathLength φ G.s G.t (p.vertices.length - 1) := by
simpa [hfirst, hlast] using hseg
let d := Nat.find ⟨p.vertices.length - 1, hpath⟩
have hd : IsShortestDist φ G.s G.t d :=
⟨Nat.find_spec ⟨p.vertices.length - 1, hpath⟩,
fun n hn => Nat.find_min' ⟨p.vertices.length - 1, hpath⟩ hn⟩
have hshort : IsShortestDist φ G.s G.t (shortestFlow.ResidualPath d hd).edges.length := by
rw [shortestFlow.ResidualPath_edges_length d hd]
exact hd
exact ⟨{ path := shortestFlow.ResidualPath d hd, h_shortest := hshort }⟩end Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S2_EK_Loop
24.2 S2. The Edmonds-Karp loop
This module implements the Edmonds-Karp algorithm: repeatedly augment along a
shortest residual source-to-sink path until none exists. Shortest paths come
from exists_shortest_augmenting_path (S1); integrality and the termination
argument reuse the infrastructure of Section 24.3 (Flow.IsIntegral,
bottleneck_ge_one, IsIntegral_augment), so each augmentation step
increases the integral value by at least one and the iteration terminates at
a flow without augmenting paths, which is maximal.
Main results:
-
shortestAugmentingPath_iff_hasAugmentingPath: a shortest augmenting path exists exactly when the sink is residual-reachable -
ekStep: one Edmonds-Karp augmentation step (along a shortest path) -
ekIter: the full loop from a starting flow -
IsIntegral_ekIterandekStep_value_ge: integrality and value increase are preserved by every step -
exists_noAugmentingPath_ekIter: the loop terminates at a flow without augmenting paths -
edmondsKarp_maximal: the terminal flow is maximal and integral
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finsetopen Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}A shortest augmenting path exists exactly when the sink is residual-reachable.
lemma shortestAugmentingPath_iff_hasAugmentingPath (φ : Flow V G) :
Nonempty (ShortestAugmentingPath φ) ↔ φ.hasAugmentingPath := by
constructor
· intro ⟨p⟩
exact Flow.hasAugmentingPath_iff_nonempty_augmentingPath.mpr ⟨p.path⟩
· intro h
exact exists_shortest_augmenting_path φ hOne Edmonds-Karp step: augment along a shortest residual source-to-sink path if one exists.
noncomputable def ekStep {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : Flow V G :=
if h : Nonempty (ShortestAugmentingPath φ) then
φ.augment (Classical.choice h).path
else φ
ekStep preserves integrality.
lemma IsIntegral_ekStep {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
(ekStep φ).IsIntegral := by
unfold ekStep
by_cases h : Nonempty (ShortestAugmentingPath φ)
· simp [h]
exact IsIntegral_augment φ hint hc (Classical.choice h).path
· simp [h]
exact hintOne Edmonds-Karp step along a shortest path increases the integral value by at least one.
lemma ekStep_value_increase {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(h : Nonempty (ShortestAugmentingPath φ)) :
φ.value + 1 ≤ (ekStep φ).value := by
unfold ekStep
simp [h]
exact augment_value_ge_one φ hint hc (Classical.choice h).pathRepeatedly apply Edmonds-Karp steps from a starting flow.
noncomputable def ekIter {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : ℕ → Flow V G
| 0 => φ
| n + 1 => ekStep (ekIter φ n)
Every iterate of ekIter is integral.
lemma IsIntegral_ekIter {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
∀ n, (ekIter φ n).IsIntegral := by
intro n
induction n with
| zero => simpa [ekIter] using hint
| succ n ih =>
simpa [ekIter] using (IsIntegral_ekStep (ekIter φ n) ih hc)Each Edmonds-Karp step increases the value by at least one, unless the flow is already free of augmenting paths.
lemma ekStep_value_ge {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(n : ℕ) :
¬(ekIter φ n).hasAugmentingPath ∨
(ekIter φ n).value + 1 ≤ (ekIter φ (n + 1)).value := by
by_cases h : (ekIter φ n).hasAugmentingPath
· right
have hshort : Nonempty (ShortestAugmentingPath (ekIter φ n)) :=
(shortestAugmentingPath_iff_hasAugmentingPath (ekIter φ n)).mpr h
have hinc := ekStep_value_increase (ekIter φ n) (IsIntegral_ekIter φ hint hc n) hc hshort
simpa [ekIter] using hinc
· left
exact h
While every step finds an augmenting path, the value after n steps is
at least n.
lemma ekIter_value_ge {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(hφ : 0 ≤ φ.value) (hsteps : ∀ n, (ekIter φ n).hasAugmentingPath) :
∀ n : ℕ, (n : ℝ) ≤ (ekIter φ n).value := by
intro n
induction n with
| zero => simpa [ekIter] using hφ
| succ n ih =>
have hinc := (ekStep_value_ge φ hint hc n).resolve_left (not_not_intro (hsteps n))
push_cast
linarithThe Edmonds-Karp loop terminates at a flow without augmenting paths: the value strictly increases by at least one each step and is bounded by the (integral) source-side cut capacity.
lemma exists_noAugmentingPath_ekIter {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (hint : φ.IsIntegral)
(hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) (hφ : 0 ≤ φ.value) :
∃ n, ¬ (ekIter φ n).hasAugmentingPath := by
by_contra hnot
have hsteps : ∀ n, (ekIter φ n).hasAugmentingPath := by
intro n
by_contra h
exact hnot ⟨n, h⟩
rcases source_cut_integral hc with ⟨K, hK⟩
have hge : ((K + 1 : ℕ) : ℝ) ≤ (ekIter φ (K + 1)).value :=
ekIter_value_ge φ hint hc hφ hsteps (K + 1)
have hle : (ekIter φ (K + 1)).value ≤ (K : ℝ) := by
rw [← hK]
exact value_le_source_cut (ekIter φ (K + 1))
have hle' : ((K + 1 : ℕ) : ℝ) ≤ (K : ℝ) := le_trans hge hle
norm_num at hle'Edmonds-Karp correctness. On an integral-capacity network, the Edmonds-Karp loop reaches an integral maximal flow.
theorem edmondsKarp_maximal {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
∃ φ : Flow V G, φ.isMaximal ∧ φ.IsIntegral := by
let zf : Flow V G := zeroFlow G
have hz : 0 ≤ zf.value := by
unfold Flow.value
simp [zf, zeroFlow]
rcases exists_noAugmentingPath_ekIter zf (IsIntegral_zero (G := G)) hc hz with
⟨n, hn⟩
let φ : Flow V G := ekIter zf n
refine ⟨φ, ?_, ?_⟩
· exact Flow.maximal_of_noAugmentingPath φ hn
· exact IsIntegral_ekIter zf (IsIntegral_zero (G := G)) hc nend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S3_WorkAnalysis
24.2 S3. The O(VE²) work analysis
This module develops the mathematical core of the Edmonds-Karp complexity analysis: critical edges and the distance-growth lemma.
An edge (u,v) of the selected augmenting path is critical when
augmentation saturates it (its residual capacity drops to zero). Every
augmentation saturates at least one edge (the bottleneck is attained by some
path edge). The key lemma (CLRS Lemma 24.8) states that when (u,v) is on a
shortest augmenting path and later (v,u) is on another shortest augmenting
path (the only way the residual capacity of (u,v) can recover), the residual
distance to u has increased by at least two:
δ'(u) = δ'(v) + 1 ≥ δ(v) + 1 = δ(u) + 2
Here the first equality is the BFS-path property on the later path, the
inequality is monotonicity (Lemma 24.7), and the last equality is the
BFS-path property on the earlier path. Since residual distances are bounded
by |V| - 1 (shortest paths are simple), each edge can be critical at most
|V| times, giving O(VE) augmentations and O(VE²) total work.
Main results:
-
Flow.AugmentingPath.isCritical: an edge saturated by the augmentation -
exists_critical_edge: every augmentation saturates at least one edge -
shortest_edge_dist: edges of a shortest path join adjacent distance levels -
critical_dist_increase: CLRS Lemma 24.8, forward direction (distance tougrows by at least two when(v,u)later lies on a shortest path) -
critical_dist_increase_rev: the reverse-direction variant used by the timeline argument -
IsShortestDist.lt_card: residual distances are bounded by|V| - 1 -
ekSeq/ekPath/criticalAt: the Edmonds-Karp timeline (flow afternsteps, selected shortest path, critical-edge predicate) -
ekStep_dist_nondecanddistAt_mono: reverse distance monotonicity across one and several steps -
exists_recovery_step: if(u,v)is critical at stepiand again lies on a selected path at stepj > i + 1, some intermediate step augments along(v,u)(the residual-capacity recovery argument) -
criticalAt_growth: CLRS Lemma 24.8 on the timeline — if(u,v)is critical at stepsiandjwithi + 1 < j, the residual distance tougrows by at least two -
criticalAt_not_succandcriticalAt_growth_strict: consecutive critical steps are impossible, so distances strictly increase between critical occurrences -
critical_count_bound: each edge is critical at most|V|times -
augmentation_count_bound: at most|V|² · |V|augmenting steps, giving theO(VE²)bound once each step is chargedO(E)for BFS
The O(VE²) counting argument is complete; the executable BFS that
computes the shortest augmenting paths lives in S4_ExecutableBFS.
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finsetopen Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}An edge of the selected augmenting path is critical when augmentation saturates it: its residual capacity after augmentation is zero.
def Flow.AugmentingPath.isCritical {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} (p : Flow.AugmentingPath φ) (u v : V) : Prop :=
(u, v) ∈ p.edges ∧ (φ.augment p).residualCapacity u v = 0In a simple list, equal elements occur at the same index.
lemma nodup_getElem_inj {α : Type*} {l : List α} (h : l.Nodup)
{i j : ℕ} (hi : i < l.length) (hj : j < l.length)
(hij : l[i] = l[j]) : i = j := by
revert h i j hi hj
induction l with
| nil => simp
| cons a l ih =>
intro h i j hi hj hij
cases i with
| zero =>
cases j with
| zero => rfl
| succ j =>
exfalso
have hj' : j < l.length := by simpa using hj
have ha_eq : a = l[j] := by simpa using hij
have ha : a ∈ l := by
simp [ha_eq]
exact (List.nodup_cons.mp h).1 ha
| succ i =>
cases j with
| zero =>
exfalso
have hi' : i < l.length := by simpa using hi
have ha_eq : a = l[i] := by
have hla : l[i] = a := by simpa using hij
exact hla.symm
have ha : a ∈ l := by
simp [ha_eq]
exact (List.nodup_cons.mp h).1 ha
| succ j =>
have hi' : i < l.length := by simpa using hi
have hj' : j < l.length := by simpa using hj
have hih : i = j :=
ih (List.nodup_cons.mp h).2 hi' hj' (by simpa using hij)
omegaA simple path contains no pair of opposite directed edges.
lemma edge_reverse_not_mem {φ : Flow V G} (p : Flow.AugmentingPath φ) {u v : V}
(huv : (u, v) ∈ p.edges) : (v, u) ∉ p.edges := by
intro hvu
rcases p.exists_index_of_mem_edges huv with ⟨i, hi, hvi, hui⟩
rcases p.exists_index_of_mem_edges hvu with ⟨j, hj, hvj, huj⟩
have h1 : i + 1 = j := by
exact nodup_getElem_inj p.nodup (by omega) (by omega) (hui.trans hvj.symm)
have h2 : i = j + 1 := by
exact nodup_getElem_inj p.nodup (by omega) (by omega) (hvi.trans huj.symm)
omegaEvery augmentation saturates at least one edge of the selected path.
lemma exists_critical_edge {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} (p : Flow.AugmentingPath φ) :
∃ u v, p.isCritical u v := by
have hmem : p.bottleneck ∈ p.edges.toFinset.image (fun e => φ.residualCapacity e.1 e.2) := by
unfold Flow.AugmentingPath.bottleneck
exact Finset.min'_mem _ _
rcases Finset.mem_image.mp hmem with ⟨e, he, hEq⟩
have he_edges : e ∈ p.edges := List.mem_toFinset.mp he
have hpost : (φ.augment p).residualCapacity e.1 e.2 = 0 := by
rw [Flow.augment_residualCapacity]
have hrev : (e.2, e.1) ∉ p.edges := edge_reverse_not_mem p he_edges
rw [hEq]
simp [he_edges, hrev]
exact ⟨e.1, e.2, he_edges, hpost⟩
Every edge of a shortest augmenting path joins adjacent distance levels:
δ(u) = i and δ(v) = i + 1.
lemma shortest_edge_dist {φ : Flow V G} (p : ShortestAugmentingPath φ) {u v : V}
(huv : (u, v) ∈ p.path.edges) :
∃ d, IsShortestDist φ G.s u d ∧ IsShortestDist φ G.s v (d + 1) := by
rcases p.path.exists_index_of_mem_edges huv with ⟨i, hi, hvi, hui⟩
have hpref_u := p.shortest_prefix i (by omega)
have hpref_v := p.shortest_prefix (i + 1) hi
refine ⟨i, ?_, ?_⟩
· simpa [hvi] using hpref_u
· simpa [hui] using hpref_v
CLRS Lemma 24.8 (critical-edge distance growth). If (u,v) is on a
shortest augmenting path of φ and later (v,u) is on a shortest augmenting
path of ψ, with residual distances not decreasing from φ to ψ, then the
residual distance to u in ψ exceeds that in φ by at least two:
δ_ψ(u) = δ_ψ(v) + 1 ≥ δ_φ(v) + 1 = δ_φ(u) + 2.
lemma critical_dist_increase {φ : Flow V G} (p : ShortestAugmentingPath φ)
{ψ : Flow V G} (q : ShortestAugmentingPath ψ) {u v : V}
(hp : (u, v) ∈ p.path.edges) (hq : (v, u) ∈ q.path.edges)
(hmono : ∀ w d, IsShortestDist φ G.s w d →
∃ d', IsShortestDist ψ G.s w d' ∧ d ≤ d') :
∃ du du', IsShortestDist φ G.s u du ∧ IsShortestDist ψ G.s u du' ∧ du + 2 ≤ du' := by
rcases shortest_edge_dist p hp with ⟨du, hdu, hdv⟩
rcases shortest_edge_dist q hq with ⟨dv', hdv', hdu'⟩
rcases hmono v (du + 1) hdv with ⟨dv'', hdv'', hle⟩
have hdv_eq : dv'' = dv' := hdv''.unique hdv'
refine ⟨du, dv' + 1, hdu, hdu', ?_⟩
have : du + 1 ≤ dv'' := hle
omegaResidual distances are bounded by the number of vertices minus one: shortest paths are simple.
lemma IsShortestDist.lt_card {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {φ : Flow V G} {v : V} {d : ℕ}
(hd : IsShortestDist φ G.s v d) : d < Fintype.card V := by
have hlen : (back d v hd).length = d + 1 := back_length d v hd
have hcard : (back d v hd).length ≤ Fintype.card V :=
List.Nodup.length_le_card (back_nodup d v hd)
omegaAugmentation counting
The flow after n Edmonds-Karp steps from the zero flow.
noncomputable def ekSeq {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(n : ℕ) : Flow V G :=
ekIter (zeroFlow G) n
The shortest augmenting path selected at step n, when one exists.
noncomputable def ekPath {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(n : ℕ) : Option (Flow.AugmentingPath (ekSeq (G := G) n)) :=
if h : Nonempty (ShortestAugmentingPath (ekSeq (G := G) n)) then
some (Classical.choice h).path
else none
Edge (u,v) is critical at step n: it lies on the selected augmenting
path and the augmentation along it saturates the edge.
def criticalAt {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(n : ℕ) (u v : V) : Prop :=
∃ p, ekPath n = some p ∧ (u, v) ∈ p.edges ∧
((ekSeq (G := G) n).augment p).residualCapacity u v = 0
Reverse monotonicity across one step: if the distance to u is finite
after the step, it was finite before the step and no larger.
lemma ekStep_dist_nondec {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(n : ℕ) (u : V) {d' : ℕ}
(hd' : IsShortestDist (ekSeq (G := G) (n + 1)) G.s u d') :
∃ d, IsShortestDist (ekSeq (G := G) n) G.s u d ∧ d ≤ d' := by
by_cases hn : (ekSeq (G := G) n).hasAugmentingPath
· have h : Nonempty (ShortestAugmentingPath (ekSeq (G := G) n)) :=
(shortestAugmentingPath_iff_hasAugmentingPath (ekSeq (G := G) n)).mpr hn
have hekstep : ekStep (ekIter (zeroFlow G) n) = (ekIter (zeroFlow G) n).augment (Classical.choice h).path := by
change ekStep (ekSeq (G := G) n) = (ekSeq (G := G) n).augment (Classical.choice h).path
unfold ekStep
simp [h]
have hd'' : IsShortestDist ((ekIter (zeroFlow G) n).augment (Classical.choice h).path) G.s u d' := by
simpa [ekSeq, ekIter, hekstep] using hd'
exact (Classical.choice h).exists_shortestDist_le_augment hd''
· have hno : ¬ Nonempty (ShortestAugmentingPath (ekSeq (G := G) n)) := by
intro h
exact hn ((shortestAugmentingPath_iff_hasAugmentingPath (ekSeq (G := G) n)).mp h)
have hekstep : ekStep (ekIter (zeroFlow G) n) = ekIter (zeroFlow G) n := by
change ekStep (ekSeq (G := G) n) = ekSeq (G := G) n
unfold ekStep
simp [hno]
have heq : ekSeq (G := G) (n + 1) = ekSeq (G := G) n := by
simp [ekSeq, ekIter, hekstep]
exact ⟨d', by simpa [heq] using hd', le_rfl⟩Reverse monotonicity across several steps.
lemma distAt_mono {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
{i j : ℕ} (hij : i ≤ j) (u : V) {d' : ℕ}
(hd' : IsShortestDist (ekSeq (G := G) j) G.s u d') :
∃ d, IsShortestDist (ekSeq (G := G) i) G.s u d ∧ d ≤ d' := by
revert u d' hd'
refine Nat.le_induction (m := i)
(P := fun k h => ∀ u d', IsShortestDist (ekSeq (G := G) k) G.s u d' →
∃ d, IsShortestDist (ekSeq (G := G) i) G.s u d ∧ d ≤ d') ?_ ?_ j hij
· intro u d' hd'
exact ⟨d', hd', le_rfl⟩
· intro n hn ih u d'' hd''
rcases ekStep_dist_nondec n u hd'' with ⟨dn, hdn, hle0⟩
rcases ih u dn hdn with ⟨d, hd, hle⟩
exact ⟨d, hd, le_trans hle hle0⟩
Reverse-direction version of Lemma 24.8: when (u,v) lies on a shortest
augmenting path of φ and (v,u) lies on one of ψ, with distances of ψ
no smaller than those of φ (for vertices reachable in ψ), the distance to
u in ψ exceeds that in φ by at least two.
lemma critical_dist_increase_rev {φ : Flow V G} (p : ShortestAugmentingPath φ)
{ψ : Flow V G} (q : ShortestAugmentingPath ψ) {u v : V}
(hp : (u, v) ∈ p.path.edges) (hq : (v, u) ∈ q.path.edges)
(hmono : ∀ w d', IsShortestDist ψ G.s w d' →
∃ d, IsShortestDist φ G.s w d ∧ d ≤ d') :
∃ du du', IsShortestDist φ G.s u du ∧ IsShortestDist ψ G.s u du' ∧ du + 2 ≤ du' := by
rcases shortest_edge_dist p hp with ⟨du, hdu, hdv⟩
rcases shortest_edge_dist q hq with ⟨dv', hdv', hdu'⟩
rcases hmono v dv' hdv' with ⟨dv, hdv0, hle⟩
have hdv_eq : dv = du + 1 := hdv0.unique hdv
refine ⟨du, dv' + 1, hdu, hdu', ?_⟩
have : du ≤ dv' := by omega
omega
The selected path at step n equals the path extracted from the
shortest-path witness.
lemma ekPath_eq_of_hasAugmentingPath {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (n : ℕ) (hn : (ekSeq (G := G) n).hasAugmentingPath) :
∃ p : Flow.AugmentingPath (ekSeq (G := G) n), ekPath n = some p ∧
ekStep (ekSeq (G := G) n) = (ekSeq (G := G) n).augment p := by
have h : Nonempty (ShortestAugmentingPath (ekSeq (G := G) n)) :=
(shortestAugmentingPath_iff_hasAugmentingPath (ekSeq (G := G) n)).mpr hn
refine ⟨(Classical.choice h).path, ?_, ?_⟩
· unfold ekPath
simp [h]
· unfold ekStep
simp [h]
If (u,v) is critical at step i and j with i + 1 < j, then between
them some step augments along (v,u) — the only way the residual capacity
of (u,v) can recover from zero.
lemma exists_recovery_step {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {i j : ℕ} (hij : i + 1 < j) {u v : V}
(hci : criticalAt (G := G) i u v) (hcj : criticalAt (G := G) j u v) :
∃ k : ℕ, ∃ h : Nonempty (ShortestAugmentingPath (ekSeq (G := G) k)),
i < k ∧ k < j ∧ (v, u) ∈ (Classical.choice h).path.edges := by
rcases hci with ⟨p_i, hekpath_i, hp_edges, hpost⟩
rcases hcj with ⟨p_j, hekpath_j, hp_edges_j, _⟩
have hpos : 0 < (ekSeq (G := G) j).residualCapacity u v := by
have hres : (ekSeq (G := G) j).residualEdge u v :=
Flow.ResidualPath.residualEdge_of_mem_edges (φ := ekSeq (G := G) j) p_j hp_edges_j
exact hres
-- ekSeq (i+1) = (ekSeq (G := G) i).augment p_i — residual capacity of (u,v) becomes 0
have hcf_i : (ekSeq (G := G) (i + 1)).residualCapacity u v = 0 := by
by_cases h_i : Nonempty (ShortestAugmentingPath (ekSeq (G := G) i))
· have hpath : (Classical.choice h_i).path = p_i := by
have : ekPath i = some (Classical.choice h_i).path := by
unfold ekPath
simp [h_i]
simpa [this] using hekpath_i
have hekstep : ekStep (ekIter (zeroFlow G) i) = (ekIter (zeroFlow G) i).augment p_i := by
change ekStep (ekSeq (G := G) i) = (ekSeq (G := G) i).augment p_i
unfold ekStep
simp [h_i, hpath]
have heq : ekSeq (G := G) (i + 1) = (ekSeq (G := G) i).augment p_i := by
simp [ekSeq, ekIter, hekstep]
simpa [heq] using hpost
· have : ekPath (V := V) (G := G) i = none := by
unfold ekPath
simp [h_i]
simp [this] at hekpath_i
-- first step j' after i with positive residual capacity
let P : ℕ → Prop := fun m => i + 1 < m ∧ m ≤ j ∧ 0 < (ekSeq (G := G) m).residualCapacity u v
have hnonempty : ∃ m, P m := ⟨j, by omega, le_rfl, hpos⟩
let k := Nat.find hnonempty
have hk : P k := Nat.find_spec hnonempty
let k' := k - 1
have hk_gt : i + 1 < k := hk.1
have hk_ge2 : i + 2 ≤ k := by omega
have hk'_ge : i + 1 ≤ k' := by omega
have hk'_lt : k' < k := by omega
have hk'_le : k' < j := by omega
have hnotP : ¬ P k' := by
intro hP
have hmin := Nat.find_min' hnonempty hP
omega
have hcf_le : (ekSeq (G := G) k').residualCapacity u v ≤ 0 := by
by_contra h
apply hnotP
have hk'_gt : i + 1 < k' := by
by_contra hnot
have hk'eq : k' = i + 1 := by omega
have : (ekSeq (G := G) k').residualCapacity u v = (ekSeq (G := G) (i + 1)).residualCapacity u v := by
rw [hk'eq]
linarith [hcf_i, h]
exact ⟨hk'_gt, by omega, by linarith⟩
-- step k' must augment (otherwise the residual capacity would not change)
have hk'_aug : (ekSeq (G := G) k').hasAugmentingPath := by
by_contra h
have hno : ¬ Nonempty (ShortestAugmentingPath (ekSeq (G := G) k')) := by
intro h'
exact h ((shortestAugmentingPath_iff_hasAugmentingPath (ekSeq (G := G) k')).mp h')
have hekstep : ekStep (ekIter (zeroFlow G) k') = ekIter (zeroFlow G) k' := by
change ekStep (ekSeq (G := G) k') = ekSeq (G := G) k'
unfold ekStep
simp [hno]
have heq : ekSeq (G := G) (k' + 1) = ekSeq (G := G) k' := by
simp [ekSeq, ekIter, hekstep]
have hk_eq : k = k' + 1 := by omega
have : (ekSeq (G := G) (k' + 1)).residualCapacity u v = (ekSeq (G := G) k').residualCapacity u v := by
rw [heq]
have hpos' : 0 < (ekSeq (G := G) (k' + 1)).residualCapacity u v := by
simpa [hk_eq] using hk.2.2
linarith [hpos', hcf_le, this]
have h : Nonempty (ShortestAugmentingPath (ekSeq (G := G) k')) :=
(shortestAugmentingPath_iff_hasAugmentingPath (ekSeq (G := G) k')).mpr hk'_aug
let p' : Flow.AugmentingPath (ekSeq (G := G) k') := (Classical.choice h).path
have hekstep' : ekStep (ekSeq (G := G) k') = (ekSeq (G := G) k').augment p' := by
unfold ekStep
rw [dif_pos h]
have heq' : ekSeq (G := G) (k' + 1) = (ekSeq (G := G) k').augment p' := by
change ekStep (ekSeq (G := G) k') = (ekSeq (G := G) k').augment p'
exact hekstep'
have hchange : 0 < (ekSeq (G := G) (k' + 1)).residualCapacity u v - (ekSeq (G := G) k').residualCapacity u v := by
have hk_eq : k = k' + 1 := by omega
have hpos' : 0 < (ekSeq (G := G) (k' + 1)).residualCapacity u v := by
simpa [hk_eq] using hk.2.2
linarith [hpos', hcf_le]
have hrev : (v, u) ∈ p'.edges := by
by_contra hnot
have hformula := Flow.augment_residualCapacity (ekSeq (G := G) k') p' u v
by_cases huv' : (u, v) ∈ p'.edges
· have hcf_eq : (ekSeq (G := G) (k' + 1)).residualCapacity u v =
(ekSeq (G := G) k').residualCapacity u v - p'.bottleneck := by
have := hformula
rw [← heq'] at this
simpa [huv', hnot] using this
have hb : 0 < p'.bottleneck := p'.bottleneck_pos
linarith
· have hcf_eq : (ekSeq (G := G) (k' + 1)).residualCapacity u v =
(ekSeq (G := G) k').residualCapacity u v := by
have := hformula
rw [← heq'] at this
simpa [huv', hnot] using this
linarith
refine ⟨k', h, ?_, ?_, hrev⟩
· omega
· exact hk'_leCounting the augmentations
If ekPath n = some p, the selected path p is the path of the
shortest-augmenting-path witness at step n.
lemma ekPath_some_spec {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {n : ℕ} {p : Flow.AugmentingPath (ekSeq (G := G) n)}
(h : ekPath (G := G) n = some p) :
∃ h' : Nonempty (ShortestAugmentingPath (ekSeq (G := G) n)),
(Classical.choice h').path = p := by
by_cases h' : Nonempty (ShortestAugmentingPath (ekSeq (G := G) n))
· refine ⟨h', ?_⟩
have : ekPath (G := G) n = some (Classical.choice h').path := by
unfold ekPath
simp [h']
simpa [this] using h
· have hnone : ekPath (G := G) n = none := by
unfold ekPath
simp [h']
simp [hnone] at h
Timeline Lemma 24.8. If (u,v) is critical at step i and again at
step j with i + 1 < j, the residual distance to u at step j exceeds
that at step i by at least two.
lemma criticalAt_growth {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {i j : ℕ} (hij : i + 1 < j) {u v : V}
(hci : criticalAt (G := G) i u v) (hcj : criticalAt (G := G) j u v) :
∃ du du', IsShortestDist (ekSeq (G := G) i) G.s u du ∧
IsShortestDist (ekSeq (G := G) j) G.s u du' ∧ du + 2 ≤ du' := by
rcases exists_recovery_step (G := G) hij hci hcj with ⟨k, h_k, hik, hkj, hrev⟩
rcases hci with ⟨p_i, hekpath_i, hp_edges, _⟩
rcases hcj with ⟨p_j, hekpath_j, hp_edges_j, _⟩
rcases ekPath_some_spec (G := G) hekpath_i with ⟨h_i, hpath_i⟩
rcases ekPath_some_spec (G := G) hekpath_j with ⟨h_j, hpath_j⟩
rcases critical_dist_increase_rev (φ := ekSeq (G := G) i) (Classical.choice h_i)
(ψ := ekSeq (G := G) k) (Classical.choice h_k)
(by simpa [hpath_i] using hp_edges) hrev
(fun w d' hd' => distAt_mono (G := G) (i := i) (j := k) (by omega) w hd')
with ⟨du, dk, hdu, hdk, hgrow⟩
rcases shortest_edge_dist (Classical.choice h_j) (by simpa [hpath_j] using hp_edges_j)
with ⟨dj, hdu_j, _⟩
rcases distAt_mono (G := G) (i := k) (j := j) (by omega) u hdu_j with ⟨dk', hdk', hle⟩
have hdk_eq : dk' = dk := hdk'.unique hdk
refine ⟨du, dj, hdu, hdu_j, ?_⟩
omegaA critical edge cannot be critical at the following step: the previous augmentation saturated it, leaving residual capacity zero.
lemma criticalAt_not_succ {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {n : ℕ} {u v : V}
(hci : criticalAt (G := G) n u v) :
¬ criticalAt (G := G) (n + 1) u v := by
rcases hci with ⟨p_n, hekpath_n, hp_edges, hpost⟩
rcases ekPath_some_spec (G := G) hekpath_n with ⟨h_n, hpath_n⟩
have hekstep : ekStep (ekIter (zeroFlow G) n) = (ekIter (zeroFlow G) n).augment p_n := by
change ekStep (ekSeq (G := G) n) = (ekSeq (G := G) n).augment p_n
unfold ekStep
simp [h_n, hpath_n]
have heq : ekSeq (G := G) (n + 1) = (ekSeq (G := G) n).augment p_n := by
simp [ekSeq, ekIter, hekstep]
have hzero : (ekSeq (G := G) (n + 1)).residualCapacity u v = 0 := by
simpa [heq] using hpost
intro hcj
rcases hcj with ⟨p_j, hekpath_j, hp_edges_j, _⟩
have hres : (ekSeq (G := G) (n + 1)).residualEdge u v :=
Flow.ResidualPath.residualEdge_of_mem_edges (φ := ekSeq (G := G) (n + 1)) p_j hp_edges_j
have hpos : 0 < (ekSeq (G := G) (n + 1)).residualCapacity u v := hres
linarith
Strict distance growth between critical occurrences: the residual distance
to u at the later critical step is strictly larger than at the earlier one.
lemma criticalAt_growth_strict {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {i j : ℕ} (hij : i < j) {u v : V}
(hci : criticalAt (G := G) i u v) (hcj : criticalAt (G := G) j u v) :
∃ du du', IsShortestDist (ekSeq (G := G) i) G.s u du ∧
IsShortestDist (ekSeq (G := G) j) G.s u du' ∧ du < du' := by
by_cases hsep : i + 1 < j
· rcases criticalAt_growth (G := G) hsep hci hcj with ⟨du, du', hdu, hdu', hgrow⟩
exact ⟨du, du', hdu, hdu', by omega⟩
· exfalso
have hsucc : j = i + 1 := by omega
exact criticalAt_not_succ hci (by simpa [hsucc] using hcj)
At a critical step, the tail u of the critical edge has a residual
distance, bounded by |V| - 1.
lemma criticalAt_dist {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} {n : ℕ} {u v : V} (h : criticalAt (G := G) n u v) :
∃ d, IsShortestDist (ekSeq (G := G) n) G.s u d ∧ d < Fintype.card V := by
rcases h with ⟨p, hekpath, hp_edges, _⟩
rcases ekPath_some_spec (G := G) hekpath with ⟨h_n, hpath⟩
rcases shortest_edge_dist (Classical.choice h_n) (by simpa [hpath] using hp_edges)
with ⟨d, hdu, _⟩
exact ⟨d, hdu, IsShortestDist.lt_card hdu⟩Every augmenting step has at least one critical edge.
lemma exists_critical_pair_at {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (n : ℕ) (h : (ekSeq (G := G) n).hasAugmentingPath) :
∃ u v, criticalAt (G := G) n u v := by
rcases ekPath_eq_of_hasAugmentingPath (G := G) n h with ⟨p, hekpath, _⟩
rcases exists_critical_edge p with ⟨u, v, he, hpost⟩
exact ⟨u, v, p, hekpath, he, hpost⟩
Edge criticality count. A fixed edge (u,v) is critical at most
|V| times: every critical occurrence determines a residual distance to u,
and that distance strictly increases between occurrences.
lemma critical_count_bound {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (u v : V) (N : ℕ) :
((Finset.range N).filter (fun n => criticalAt (G := G) n u v)).card ≤
Fintype.card V := by
let s : Finset ℕ := (Finset.range N).filter (fun n => criticalAt (G := G) n u v)
let hcrit : ∀ x : {n : ℕ // n ∈ s}, criticalAt (G := G) x.1 u v :=
fun x => (Finset.mem_filter.mp x.2).2
let distOf : {n : ℕ // n ∈ s} → ℕ :=
fun x => Classical.choose (criticalAt_dist (hcrit x))
let f : {n : ℕ // n ∈ s} → Fin (Fintype.card V) :=
fun x => ⟨distOf x, (Classical.choose_spec (criticalAt_dist (hcrit x))).2⟩
have hinj : Set.InjOn f (↑(s.attach) : Set {n : ℕ // n ∈ s}) := by
intro x hx y hy hxy
apply Subtype.ext
by_contra hne
have hxy' : distOf x = distOf y :=
congrArg (fun z : Fin (Fintype.card V) => z.1) hxy
have hlt_or : x.1 < y.1 ∨ y.1 < x.1 := by omega
rcases hlt_or with hxy_lt | hyx_lt
· rcases criticalAt_growth_strict (G := G) hxy_lt (hcrit x) (hcrit y) with
⟨du, du', hdu, hdu', hgrow⟩
have hdx : distOf x = du :=
(Classical.choose_spec (criticalAt_dist (hcrit x))).1.unique hdu
have hdy : distOf y = du' :=
(Classical.choose_spec (criticalAt_dist (hcrit y))).1.unique hdu'
omega
· rcases criticalAt_growth_strict (G := G) hyx_lt (hcrit y) (hcrit x) with
⟨du, du', hdu, hdu', hgrow⟩
have hdy : distOf y = du :=
(Classical.choose_spec (criticalAt_dist (hcrit y))).1.unique hdu
have hdx : distOf x = du' :=
(Classical.choose_spec (criticalAt_dist (hcrit x))).1.unique hdu'
omega
have hsub : s.attach.image f ⊆ (Finset.univ : Finset (Fin (Fintype.card V))) := by
intro x hx
simp
have hcard : (s.attach.image f).card = s.attach.card :=
Finset.card_image_of_injOn hinj
calc
s.card = s.attach.card := Finset.card_attach.symm
_ = (s.attach.image f).card := hcard.symm
_ ≤ (Finset.univ : Finset (Fin (Fintype.card V))).card := Finset.card_le_card hsub
_ = Fintype.card V := by simp
Augmentation count. There are at most |V|² · |V| augmenting steps:
each one has a critical edge, and each of the |V|² edges is critical at most
|V| times.
lemma augmentation_count_bound {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (N : ℕ) :
((Finset.range N).filter (fun n => (ekSeq (G := G) n).hasAugmentingPath)).card ≤
Fintype.card (V × V) * Fintype.card V := by
let s : Finset ℕ :=
(Finset.range N).filter (fun n => (ekSeq (G := G) n).hasAugmentingPath)
let haug : ∀ x : {n : ℕ // n ∈ s}, (ekSeq (G := G) x.1).hasAugmentingPath :=
fun x => (Finset.mem_filter.mp x.2).2
let pair : {n : ℕ // n ∈ s} → V × V := fun x =>
let h := exists_critical_pair_at (G := G) x.1 (haug x)
(Classical.choose h, Classical.choose (Classical.choose_spec h))
let hcrit : ∀ x : {n : ℕ // n ∈ s},
criticalAt (G := G) x.1 (pair x).1 (pair x).2 :=
fun x =>
Classical.choose_spec
(Classical.choose_spec (exists_critical_pair_at (G := G) x.1 (haug x)))
let distOf : {n : ℕ // n ∈ s} → ℕ :=
fun x => Classical.choose (criticalAt_dist (hcrit x))
let f : {n : ℕ // n ∈ s} → (V × V) × Fin (Fintype.card V) :=
fun x => (pair x, ⟨distOf x, (Classical.choose_spec (criticalAt_dist (hcrit x))).2⟩)
have hinj : Set.InjOn f (↑(s.attach) : Set {n : ℕ // n ∈ s}) := by
intro x hx y hy hxy
apply Subtype.ext
by_contra hne
have hpair_eq : pair x = pair y := congrArg Prod.fst hxy
have hdist_eq : distOf x = distOf y :=
congrArg (fun z : (V × V) × Fin (Fintype.card V) => z.2.1) hxy
have hcy : criticalAt (G := G) y.1 (pair x).1 (pair x).2 := by
simpa [hpair_eq] using hcrit y
have hlt_or : x.1 < y.1 ∨ y.1 < x.1 := by omega
rcases hlt_or with hxy_lt | hyx_lt
· rcases criticalAt_growth_strict (G := G) hxy_lt (hcrit x) hcy with
⟨du, du', hdu, hdu', hgrow⟩
have hdx : distOf x = du :=
(Classical.choose_spec (criticalAt_dist (hcrit x))).1.unique hdu
have hdy : distOf y = du' := by
have hd := (Classical.choose_spec (criticalAt_dist (hcrit y))).1
exact hd.unique (by simpa [hpair_eq] using hdu')
omega
· rcases criticalAt_growth_strict (G := G) hyx_lt hcy (hcrit x) with
⟨du, du', hdu, hdu', hgrow⟩
have hdy : distOf y = du := by
have hd := (Classical.choose_spec (criticalAt_dist (hcrit y))).1
exact hd.unique (by simpa [hpair_eq] using hdu)
have hdx : distOf x = du' :=
(Classical.choose_spec (criticalAt_dist (hcrit x))).1.unique hdu'
omega
have hsub : s.attach.image f ⊆ (Finset.univ : Finset ((V × V) × Fin (Fintype.card V))) := by
intro x hx
simp
have hcard : (s.attach.image f).card = s.attach.card :=
Finset.card_image_of_injOn hinj
calc
s.card = s.attach.card := Finset.card_attach.symm
_ = (s.attach.image f).card := hcard.symm
_ ≤ (Finset.univ : Finset ((V × V) × Fin (Fintype.card V))).card :=
Finset.card_le_card hsub
_ = Fintype.card (V × V) * Fintype.card V := by simpend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S4_ExecutableBFS.CostedSupportBFS
Costed residual BFS over finite support buckets
This is the adjacency-list execution companion to residualBFS. A step
reads only the bucket of the dequeued vertex and charges one dequeue plus four
RAM operations per inspected candidate (residual test, visited test, and the
possible discovery bookkeeping). Under residual-support coverage, erasing
the counter gives the existing semantic BFS state exactly.
As in the textbook RAM model, bucket access and queue/discovery primitives carry stipulated unit charges. The attached counter measures that abstract execution, not Lean evaluator time for the underlying persistent containers.
namespace CLRSnamespace Chapter26open Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
A support contains every residual edge of φ.
def SupportsResidual (A : SupportAdjacency V) (φ : Flow V G) : Prop :=
∀ ⦃u v⦄, Flow.residualEdge φ u v → v ∈ A.bucket u
Residual candidates in the bucket of u.
noncomputable def supportResidualAdj (A : SupportAdjacency V)
(φ : Flow V G) (u : V) : Finset V :=
(A.bucket u).filter fun v => Flow.residualEdge φ u v
Undiscovered residual candidates in the bucket of u.
noncomputable def supportBFSNewNeighbors (A : SupportAdjacency V)
(φ : Flow V G) (state : BFSState V) (u : V) : Finset V :=
(supportResidualAdj A φ u).filter fun v => v ∉ state.visitedThe ordinary BFS state update, using only a support bucket.
noncomputable def supportBFSStateAdvance (A : SupportAdjacency V)
(φ : Flow V G) (state : BFSState V) (u : V) (rest : List V) : BFSState V :=
let newNeighbors := supportBFSNewNeighbors A φ state u
let nextDistance := state.level u + 1
{
visited := state.visited ∪ newNeighbors
queue := rest ++ newNeighbors.toList
distance := fun v =>
if v ∈ newNeighbors then some nextDistance else state.distance v
parent := fun v =>
if v ∈ newNeighbors then some u else state.parent v
}theorem supportResidualAdj_eq_residualAdj (A : SupportAdjacency V)
(φ : Flow V G) (cover : SupportsResidual A φ) (u : V) :
supportResidualAdj A φ u = residualAdj φ u := by
ext v
simp only [supportResidualAdj, Finset.mem_filter, mem_residualAdj]
constructor
· exact fun h => h.2
· exact fun h => ⟨cover h, h⟩theorem supportBFSNewNeighbors_eq_bfsNewNeighbors (A : SupportAdjacency V)
(φ : Flow V G) (cover : SupportsResidual A φ) (state : BFSState V) (u : V) :
supportBFSNewNeighbors A φ state u = bfsNewNeighbors φ state u := by
simp [supportBFSNewNeighbors, bfsNewNeighbors,
supportResidualAdj_eq_residualAdj A φ cover u]theorem supportBFSStateAdvance_eq_bfsStateAdvance (A : SupportAdjacency V)
(φ : Flow V G) (cover : SupportsResidual A φ) (state : BFSState V)
(u : V) (rest : List V) :
supportBFSStateAdvance A φ state u rest = bfsStateAdvance φ state u rest := by
simp [supportBFSStateAdvance, bfsStateAdvance,
supportBFSNewNeighbors_eq_bfsNewNeighbors A φ cover state u]Result of the support-bucket execution.
structure CostedBFSRun (V : Type*) [DecidableEq V] where
state : BFSState V
work : Nat
Work already performed before state: every dequeued vertex costs one
unit and four units per candidate in its support bucket.
noncomputable def supportBFSWork (A : SupportAdjacency V)
(visited : Finset V) (queue : List V) : Nat :=
let processed := visited \ queue.toFinset
processed.card + 4 * ∑ u ∈ processed, (A.bucket u).cardtheorem mem_supportBFSNewNeighbors_iff {A : SupportAdjacency V}
{φ : Flow V G} {state : BFSState V} {u v : V} :
v ∈ supportBFSNewNeighbors A φ state u ↔
v ∈ A.bucket u ∧ Flow.residualEdge φ u v ∧ v ∉ state.visited := by
simp [supportBFSNewNeighbors, supportResidualAdj, and_assoc]
Dequeuing u advances the work measure by the exact charge recorded by
the recursive execution.
theorem supportBFSWork_step (A : SupportAdjacency V) (φ : Flow V G)
{u : V} {rest : List V} {state : BFSState V}
(hu : u ∈ state.visited) (hu_rest : u ∉ rest) :
supportBFSWork A (supportBFSStateAdvance A φ state u rest).visited
(supportBFSStateAdvance A φ state u rest).queue =
supportBFSWork A state.visited (u :: rest) + 1 + 4 * (A.bucket u).card := by
let newNeighbors := supportBFSNewNeighbors A φ state u
have hnotVisited {x : V} (hx : x ∈ newNeighbors) : x ∉ state.visited :=
(mem_supportBFSNewNeighbors_iff.mp hx).2.2
have huNew : u ∉ newNeighbors := by
intro h
exact hnotVisited h hu
have hdequeued :
(state.visited ∪ newNeighbors) \ (rest.toFinset ∪ newNeighbors) =
insert u (state.visited \ insert u rest.toFinset) := by
ext x
by_cases hxNew : x ∈ newNeighbors
· simp [hxNew, hnotVisited hxNew]
intro hxu
rw [hxu] at hxNew
exact huNew hxNew
· simp [hxNew]
constructor
· rintro ⟨hxVisited, hxRest⟩
by_cases hxu : x = u
· exact Or.inl hxu
· exact Or.inr ⟨hxVisited, hxu, hxRest⟩
· rintro (hxu | ⟨hxVisited, _hxne, hxRest⟩)
· subst x
exact ⟨hu, hu_rest⟩
· exact ⟨hxVisited, hxRest⟩
simp [supportBFSWork, supportBFSStateAdvance]
rw [hdequeued]
have huProcessed : u ∉ state.visited \ insert u rest.toFinset := by simp
simp [huProcessed]
omegaA support-BFS step preserves duplicate-freedom of the queue.
theorem supportBFSStateAdvance_queue_nodup (A : SupportAdjacency V)
(φ : Flow V G) {state : BFSState V} {u : V} {rest : List V}
(hnodup : (u :: rest).Nodup)
(hqueue : BFSQueueInv φ state.visited (u :: rest)) :
(supportBFSStateAdvance A φ state u rest).queue.Nodup := by
let newNeighbors := supportBFSNewNeighbors A φ state u
have hrest : rest.Nodup := (List.nodup_cons.mp hnodup).2
have hnew : newNeighbors.toList.Nodup := Finset.nodup_toList newNeighbors
have hdisjoint : ∀ a ∈ rest, ∀ b ∈ newNeighbors.toList, a ≠ b := by
intro a ha b hb hab
rw [← hab] at hb
have haVisited : a ∈ state.visited := hqueue a (by simp [ha])
have haNew : a ∈ newNeighbors := Finset.mem_toList.mp hb
exact (mem_supportBFSNewNeighbors_iff.mp haNew).2.2 haVisited
have : (rest ++ newNeighbors.toList).Nodup := by
rw [List.nodup_append]
exact ⟨hrest, hnew, hdisjoint⟩
simpa [supportBFSStateAdvance, newNeighbors] using thisFuelled costed support BFS.
noncomputable def costedBFSAux (A : SupportAdjacency V) (φ : Flow V G) :
Nat → BFSState V → CostedBFSRun V
| 0, state => ⟨state, 0⟩
| fuel + 1, state =>
match state.queue with
| [] => ⟨state, 0⟩
| u :: rest =>
let tail := costedBFSAux A φ fuel
(supportBFSStateAdvance A φ state u rest)
⟨tail.state, 1 + 4 * (A.bucket u).card + tail.work⟩Costed support BFS, fuelled by the finite vertex count.
noncomputable def costedResidualBFS (A : SupportAdjacency V)
(φ : Flow V G) : CostedBFSRun V :=
costedBFSAux A φ (Fintype.card V) (bfsStateInit G.s)
theorem costedBFSAux_state (A : SupportAdjacency V) (φ : Flow V G)
(cover : SupportsResidual A φ) (fuel : Nat) (state : BFSState V) :
(costedBFSAux A φ fuel state).state = bfsStateAux φ fuel state := by
induction fuel generalizing state with
| zero => simp [costedBFSAux, bfsStateAux]
| succ fuel ih =>
cases hqueue : state.queue with
| nil => simp [costedBFSAux, bfsStateAux, hqueue]
| cons u rest =>
simp only [costedBFSAux, bfsStateAux, hqueue]
rw [ih]
exact congrArg (bfsStateAux φ fuel)
(supportBFSStateAdvance_eq_bfsStateAdvance A φ cover state u rest)Erasing the support execution and counters gives the existing residual BFS state exactly.
theorem costedResidualBFS_state (A : SupportAdjacency V) (φ : Flow V G)
(cover : SupportsResidual A φ) :
(costedResidualBFS A φ).state = residualBFS φ := by
exact costedBFSAux_state A φ cover (Fintype.card V) (bfsStateInit G.s)The accumulated recursive counter equals the increase of the execution work measure.
theorem costedBFSAux_work_eq (A : SupportAdjacency V) (φ : Flow V G)
(cover : SupportsResidual A φ) (fuel : Nat) (state : BFSState V)
(hqueue : BFSQueueInv φ state.visited state.queue)
(hnodup : state.queue.Nodup) :
(costedBFSAux A φ fuel state).work +
supportBFSWork A state.visited state.queue =
supportBFSWork A (costedBFSAux A φ fuel state).state.visited
(costedBFSAux A φ fuel state).state.queue := by
induction fuel generalizing state with
| zero => simp [costedBFSAux]
| succ fuel ih =>
cases hq : state.queue with
| nil => simp [costedBFSAux, hq]
| cons u rest =>
have hqueueCons : BFSQueueInv φ state.visited (u :: rest) := by
simpa [hq] using hqueue
have hnodupCons : (u :: rest).Nodup := by simpa [hq] using hnodup
let next := supportBFSStateAdvance A φ state u rest
have hnextEq : next = bfsStateAdvance φ state u rest :=
supportBFSStateAdvance_eq_bfsStateAdvance A φ cover state u rest
have hqueueNext : BFSQueueInv φ next.visited next.queue := by
rw [hnextEq]
exact bfsQueueInv_step hqueueCons
have hnodupNext : next.queue.Nodup := by
exact supportBFSStateAdvance_queue_nodup A φ hnodupCons hqueueCons
have hih := ih next hqueueNext hnodupNext
have hu : u ∈ state.visited := hqueue u (by simp [hq])
have huRest : u ∉ rest := (List.nodup_cons.mp hnodupCons).1
have hstep := supportBFSWork_step A φ hu huRest
simp only [costedBFSAux, hq]
change 1 + 4 * (A.bucket u).card +
(costedBFSAux A φ fuel next).work +
supportBFSWork A state.visited (u :: rest) =
supportBFSWork A (costedBFSAux A φ fuel next).state.visited
(costedBFSAux A φ fuel next).state.queue
rw [← hih, hstep]
omegatheorem supportBFSWork_init (A : SupportAdjacency V) (s : V) :
supportBFSWork A (bfsStateInit s).visited (bfsStateInit s).queue = 0 := by
simp [supportBFSWork, bfsStateInit]The actual support-BFS scan execution is linear in vertices plus stored candidate arcs.
theorem costedResidualBFS_scanWork_le (A : SupportAdjacency V) (φ : Flow V G)
(cover : SupportsResidual A φ) :
(costedResidualBFS A φ).work ≤ Fintype.card V + 4 * A.storage := by
have hinitQueue : BFSQueueInv φ (bfsStateInit G.s).visited
(bfsStateInit G.s).queue := by
intro v hv
simpa [BFSQueueInv, bfsStateInit] using hv
have hinitNodup : (bfsStateInit G.s).queue.Nodup := by
simp [bfsStateInit]
have hcost := costedBFSAux_work_eq A φ cover (Fintype.card V)
(bfsStateInit G.s) hinitQueue hinitNodup
have hzero := supportBFSWork_init A G.s
have hqueueEmpty : (costedResidualBFS A φ).state.queue = [] := by
rw [costedResidualBFS_state A φ cover]
exact residualBFS_queue_empty φ
have hcostEq : (costedResidualBFS A φ).work =
supportBFSWork A (costedResidualBFS A φ).state.visited
(costedResidualBFS A φ).state.queue := by
rw [hzero] at hcost
simpa [costedResidualBFS] using hcost
rw [hcostEq, hqueueEmpty]
simp only [supportBFSWork, List.toFinset_nil, Finset.sdiff_empty]
have hcard : (costedResidualBFS A φ).state.visited.card ≤ Fintype.card V :=
Finset.card_le_univ _
have hsum :
∑ u ∈ (costedResidualBFS A φ).state.visited, (A.bucket u).card ≤ A.storage :=
sum_bucket_card_le_storage A _
omegaPublic work bound for the costed support BFS.
theorem costedResidualBFS_work_le (A : SupportAdjacency V) (φ : Flow V G)
(cover : SupportsResidual A φ) :
(costedResidualBFS A φ).work ≤ Fintype.card V + 4 * A.storage :=
costedResidualBFS_scanWork_le A φ coverAttached parent-path recovery
A recovered path list and the work performed to construct it.
structure CostedPathVertices (V : Type*) where
vertices : List V
work : Natnamespace BFSParentPathBuild the parent path in reverse order using constant-time list cons.
noncomputable def reverseVerticesWithCost {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) : CostedPathVertices V :=
match h with
| root => ⟨[s], 1⟩
| @tail _ _ _ _ v _ hprev _ =>
let prev := reverseVerticesWithCost hprev
⟨v :: prev.vertices, prev.work + 1⟩omit [Fintype V] [DecidableEq V] in
theorem reverseVerticesWithCost_vertices {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) :
(reverseVerticesWithCost h).vertices = (BFSParentPath.vertices h).reverse := by
induction h with
| root => rfl
| @tail u v n hprev hparent ih =>
simp [reverseVerticesWithCost, BFSParentPath.vertices, ih]omit [Fintype V] [DecidableEq V] in
theorem reverseVerticesWithCost_work {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) :
(reverseVerticesWithCost h).work = n + 1 := by
induction h with
| root => rfl
| @tail u v n hprev hparent ih =>
simp [reverseVerticesWithCost, ih]Recover source-to-target order and charge the final linear reversal.
noncomputable def verticesWithCost {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) : CostedPathVertices V :=
let reverseRun := reverseVerticesWithCost h
⟨reverseRun.vertices.reverse, reverseRun.work + reverseRun.vertices.length⟩omit [Fintype V] [DecidableEq V] in
theorem verticesWithCost_vertices {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) :
(verticesWithCost h).vertices = BFSParentPath.vertices h := by
simp [verticesWithCost, reverseVerticesWithCost_vertices]theorem verticesWithCost_work {parent : V → Option V} {s v : V} {n : Nat}
(h : BFSParentPath parent s v n) :
(verticesWithCost h).work = 2 * (n + 1) := by
simp [verticesWithCost, reverseVerticesWithCost_work,
reverseVerticesWithCost_vertices, BFSParentPath.vertices_length]
omegaend BFSParentPathend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S4_ExecutableBFS.SupportAdjacency
Finite support adjacency buckets
This module builds adjacency buckets from a finite directed support. The builder records one RAM-model unit for each executed bucket insertion. Its membership, work, and total-storage specifications are independent of flow semantics and are reused by the costed residual BFS.
This is an explicit unit-cost RAM abstraction for the textbook analysis; the
counter is not a claim about Lean kernel reduction or a particular compiled
Finset representation.
namespace CLRSnamespace Chapter26open Finset Classicalvariable {V : Type*} [DecidableEq V]A finite directed support indexed by its source vertex.
structure SupportAdjacency (V : Type*) [DecidableEq V] where
bucket : V → Finset Vnamespace SupportAdjacencyThe empty support adjacency.
def empty : SupportAdjacency V where
bucket := fun _ => ∅Insert one directed support arc into its source bucket.
def insertArc (A : SupportAdjacency V) (e : V × V) : SupportAdjacency V where
bucket := Function.update A.bucket e.1 (insert e.2 (A.bucket e.1))@[simp]
theorem empty_bucket (u : V) : (empty : SupportAdjacency V).bucket u = ∅ := rfl@[simp]
theorem mem_insertArc_bucket {A : SupportAdjacency V} {e : V × V} {u v : V} :
v ∈ (A.insertArc e).bucket u ↔ (u, v) = e ∨ v ∈ A.bucket u := by
rcases e with ⟨a, b⟩
by_cases h : u = a
· subst u
simp [insertArc]
· simp [insertArc, Function.update, h]Total number of stored bucket entries.
noncomputable def storage [Fintype V] (A : SupportAdjacency V) : Nat :=
∑ u : V, (A.bucket u).card
theorem storage_insertArc_of_not_mem [Fintype V] (A : SupportAdjacency V)
(e : V × V) (hnew : e.2 ∉ A.bucket e.1) :
(A.insertArc e).storage = A.storage + 1 := by
unfold storage
change (∑ u, (Function.update A.bucket e.1
(insert e.2 (A.bucket e.1)) u).card) = ∑ u, (A.bucket u).card + 1
have hfun : (fun u => (Function.update A.bucket e.1
(insert e.2 (A.bucket e.1)) u).card) =
Function.update (fun u => (A.bucket u).card) e.1
(insert e.2 (A.bucket e.1)).card := by
funext u
by_cases h : u = e.1 <;> simp [Function.update, h]
rw [hfun]
rw [Finset.sum_update_of_mem (Finset.mem_univ e.1)]
rw [Finset.card_insert_of_notMem hnew]
rw [Finset.sdiff_singleton_eq_erase]
have hsum := Finset.sum_erase_add (Finset.univ : Finset V)
(fun u => (A.bucket u).card) (Finset.mem_univ e.1)
omegaend SupportAdjacencyResult of building adjacency buckets, including the executed insert count.
structure SupportBuild (V : Type*) [DecidableEq V] where
adjacency : SupportAdjacency V
work : NatBuild buckets from a support list, charging one unit for each insertion.
def buildSupportAux : List (V × V) → SupportBuild V
| [] => ⟨SupportAdjacency.empty, 0⟩
| e :: rest =>
let tail := buildSupportAux rest
⟨tail.adjacency.insertArc e, tail.work + 1⟩@[simp]
theorem buildSupportAux_work (support : List (V × V)) :
(buildSupportAux support).work = support.length := by
induction support with
| nil => rfl
| cons e rest ih => simp [buildSupportAux, ih]theorem mem_buildSupportAux {support : List (V × V)} {u v : V} :
v ∈ (buildSupportAux support).adjacency.bucket u ↔ (u, v) ∈ support := by
induction support with
| nil => simp [buildSupportAux, SupportAdjacency.empty]
| cons e rest ih =>
simp [buildSupportAux, SupportAdjacency.mem_insertArc_bucket, ih]
theorem buildSupportAux_storage [Fintype V] {support : List (V × V)}
(hnodup : support.Nodup) :
(buildSupportAux support).adjacency.storage = support.length := by
induction support with
| nil => simp [buildSupportAux, SupportAdjacency.storage]
| cons e rest ih =>
rw [List.nodup_cons] at hnodup
have hnew : e.2 ∉ (buildSupportAux rest).adjacency.bucket e.1 := by
intro hmem
exact hnodup.1 ((mem_buildSupportAux.mp hmem))
rw [buildSupportAux]
rw [SupportAdjacency.storage_insertArc_of_not_mem _ _ hnew]
rw [ih hnodup.2]
simpBuild adjacency buckets from a duplicate-free finite support.
noncomputable def buildSupportAdjacency (support : Finset (V × V)) : SupportBuild V :=
buildSupportAux support.toListtheorem mem_buildSupportAdjacency {support : Finset (V × V)} {u v : V} :
v ∈ (buildSupportAdjacency support).adjacency.bucket u ↔ (u, v) ∈ support := by
simp [buildSupportAdjacency, mem_buildSupportAux]theorem buildSupportAdjacency_work (support : Finset (V × V)) :
(buildSupportAdjacency support).work = support.card := by
simp [buildSupportAdjacency]
theorem buildSupportAdjacency_storage [Fintype V] (support : Finset (V × V)) :
(buildSupportAdjacency support).adjacency.storage = support.card := by
rw [buildSupportAdjacency, buildSupportAux_storage support.nodup_toList]
simptheorem sum_bucket_card_le_storage [Fintype V] (A : SupportAdjacency V)
(processed : Finset V) :
∑ u ∈ processed, (A.bucket u).card ≤ A.storage := by
exact Finset.sum_le_sum_of_subset (Finset.subset_univ processed)end Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.S4_ExecutableBFS
24.2 S4. Executable breadth-first search
This module implements an executable breadth-first search over the residual
network of a flow φ and proves its correctness: the BFS distance labels are
the exact residual distances (IsShortestDist), the parent pointers walk back
to the source along residual edges, and the parent chain from the sink
assembles a shortest augmenting path whenever one exists. This is the
executable core of the Edmonds-Karp loop: the augmenting path it computes can
be fed to Flow.augment in place of the classical choice used by ekStep
(see ekStep_shortest_path_bfs).
The search mirrors the Chapter 22 BFS state (visited, queue, distance,
parent), fuelled by the number of vertices; the queue invariants
(BFSClosedInv, BFSQueueInv, BFSDistanceInvariant) are the same, with
graph adjacency replaced by the residual relation Flow.residualEdge φ.
Main results:
-
residualBFS: the fuelled breadth-first search over the residual network -
residualBFS_distanceInvariant: the distance/predecessor invariant holds -
residualBFS_queue_empty: the search exhausts its queue after|V|steps -
bfsState_distance_eq_some_iff: the BFS distance of a vertex is its residual shortest distanceIsShortestDist -
bfsParentResidualPath: the parent chain from the sink assembles a simple residual path -
bfs_shortestAugmenting: an executable shortest augmenting path whenever one exists -
ekStep_shortest_path_bfs: the Edmonds-Karp step augments along a shortest path of the same length as the BFS path
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finsetopen Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
The residual out-neighborhood of u: vertices reachable from u by one
residual edge.
noncomputable def residualAdj (φ : Flow V G) (u : V) : Finset V :=
Finset.univ.filter (fun v => Flow.residualEdge φ u v)@[simp]
theorem mem_residualAdj {φ : Flow V G} {u v : V} :
v ∈ residualAdj φ u ↔ Flow.residualEdge φ u v := by
simp [residualAdj]
BFS state: discovered vertices, FIFO queue, distance labels, and parent
pointers. A vertex is discovered exactly when it belongs to visited;
distance and parent record its first discovery.
structure BFSState (V : Type*) [DecidableEq V] where
visited : Finset V
queue : List V
distance : V → Option ℕ
parent : V → Option Vnamespace BFSStateNumeric level used by the queue invariants. It is only inspected for discovered vertices, where the distance is known to be present.
end BFSStateInitial BFS state at the source.
noncomputable def bfsStateInit (s : V) : BFSState V where
visited := {s}
queue := [s]
distance := fun v => if v = s then some 0 else none
parent := fun _ => none
As-yet undiscovered residual out-neighbors of u.
noncomputable def bfsNewNeighbors (φ : Flow V G) (state : BFSState V) (u : V) : Finset V :=
(residualAdj φ u).filter (fun v => v ∉ state.visited)
Process the front vertex u, assigning distance level u + 1 and parent
u to every newly discovered residual neighbor.
noncomputable def bfsStateAdvance (φ : Flow V G) (state : BFSState V)
(u : V) (rest : List V) : BFSState V :=
let newNeighbors := bfsNewNeighbors φ state u
let nextDistance := state.level u + 1
{
visited := state.visited ∪ newNeighbors
queue := rest ++ newNeighbors.toList
distance := fun v =>
if v ∈ newNeighbors then some nextDistance else state.distance v
parent := fun v =>
if v ∈ newNeighbors then some u else state.parent v
}Fuelled residual BFS.
noncomputable def bfsStateAux (φ : Flow V G) : ℕ → BFSState V → BFSState V
| 0, state => state
| fuel + 1, state =>
match state.queue with
| [] => state
| u :: rest => bfsStateAux φ fuel (bfsStateAdvance φ state u rest)
BFS over the residual network of φ, fuelled by the number of vertices.
noncomputable def residualBFS (φ : Flow V G) : BFSState V :=
bfsStateAux φ (Fintype.card V) (bfsStateInit G.s)Closure invariant: every neighbor of a processed (no longer queued) vertex is already visited.
def BFSClosedInv (φ : Flow V G) (visited : Finset V) (queue : List V) : Prop :=
∀ u ∈ visited, u ∉ queue → ∀ v, Flow.residualEdge φ u v → v ∈ visitedQueue invariant: every queued vertex is already marked visited.
def BFSQueueInv (φ : Flow V G) (visited : Finset V) (queue : List V) : Prop :=
∀ v ∈ queue, v ∈ visitedtheorem mem_bfsNewNeighbors_iff {φ : Flow V G} {state : BFSState V} {u v : V} :
v ∈ bfsNewNeighbors φ state u ↔ Flow.residualEdge φ u v ∧ v ∉ state.visited := by
simp [bfsNewNeighbors]The closure invariant is preserved by one BFS step.
theorem bfsClosedInv_step {φ : Flow V G} {u : V} {rest : List V} {visited : Finset V}
(hclosed : BFSClosedInv φ visited (u :: rest)) :
BFSClosedInv φ
(visited ∪ (residualAdj φ u).filter (fun v => v ∉ visited))
(rest ++ ((residualAdj φ u).filter (fun v => v ∉ visited)).toList) := by
intro x hx hxnotin v hvx
simp [BFSClosedInv] at hclosed
simp [Finset.mem_union, Finset.mem_filter] at hx
rcases hx with (hx | ⟨hxadj, hxnvis⟩)
· by_cases hxu : x = u
· rw [hxu] at hvx
by_cases h : v ∈ visited
· simp [h]
· simp [h, hvx]
· by_cases hxrest : x ∈ rest
· exfalso
simp [hxrest] at hxnotin
· have hxnotin' : x ∉ u :: rest := by
simp [hxu, hxrest]
have hxne : x ≠ u := by
intro h
apply hxnotin'
simp [h]
have hxnrest : x ∉ rest := by
intro h
apply hxnotin'
simp [h]
have : v ∈ visited := hclosed x hx hxne hxnrest v hvx
simp [this]
· exfalso
have : x ∈ rest ++ ((residualAdj φ u).filter (fun v => v ∉ visited)).toList := by
simp [hxadj, hxnvis]
contradictionThe queue invariant is preserved by one BFS step.
theorem bfsQueueInv_step {φ : Flow V G} {u : V} {rest : List V} {visited : Finset V}
(hqueue : BFSQueueInv φ visited (u :: rest)) :
BFSQueueInv φ
(visited ∪ (residualAdj φ u).filter (fun v => v ∉ visited))
(rest ++ ((residualAdj φ u).filter (fun v => v ∉ visited)).toList) := by
intro x hx
simp [BFSQueueInv] at hqueue
rcases hqueue with ⟨hu, hrest⟩
simp [List.mem_append, Finset.mem_toList, Finset.mem_filter] at hx
rcases hx with (hx | ⟨hxadj, hxnvis⟩)
· have : x ∈ visited := hrest x hx
simp [this]
· simp [hxadj, hxnvis]Invariant connecting the FIFO search state to CLRS distance and predecessor labels. The queue is ordered by nondecreasing level and spans at most two consecutive levels; processed edges already satisfy the shortest-path upper bound needed at termination.
structure BFSDistanceInvariant (φ : Flow V G) (s : V) (state : BFSState V) : Prop where
closed : BFSClosedInv φ state.visited state.queue
queued : BFSQueueInv φ state.visited state.queue
source_distance : state.distance s = some 0
source_parent : state.parent s = none
distance_iff_visited : ∀ v, v ∈ state.visited ↔ ∃ d, state.distance v = some d
distance_zero : ∀ v, state.distance v = some 0 → v = s
parent_exists : ∀ v, v ∈ state.visited → v ≠ s → ∃ u, state.parent v = some u
parent_unvisited : ∀ v, v ∉ state.visited → state.parent v = none
parent_step : ∀ u v, state.parent v = some u →
Flow.residualEdge φ u v ∧ ∃ d, state.distance u = some d ∧ state.distance v = some (d + 1)
queue_ordered : state.queue.Pairwise (fun u v => state.level u ≤ state.level v)
visited_span : ∀ u rest, state.queue = u :: rest →
∀ v ∈ state.visited, state.level v ≤ state.level u + 1
processed_edge : ∀ u ∈ state.visited, u ∉ state.queue →
∀ v, Flow.residualEdge φ u v → state.level v ≤ state.level u + 1Processing a vertex does not change labels of already discovered vertices.
theorem bfsStateAdvance_distance_of_visited {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ state.visited) :
(bfsStateAdvance φ state u rest).distance v = state.distance v := by
have hvnew : v ∉ bfsNewNeighbors φ state u := by
simp [mem_bfsNewNeighbors_iff, hv]
simp [bfsStateAdvance, hvnew]
theorem bfsStateAdvance_parent_of_visited {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ state.visited) :
(bfsStateAdvance φ state u rest).parent v = state.parent v := by
have hvnew : v ∉ bfsNewNeighbors φ state u := by
simp [mem_bfsNewNeighbors_iff, hv]
simp [bfsStateAdvance, hvnew]theorem bfsStateAdvance_level_of_visited {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ state.visited) :
(bfsStateAdvance φ state u rest).level v = state.level v := by
simp [BFSState.level, bfsStateAdvance_distance_of_visited (φ := φ) hv]Every newly discovered vertex receives the front vertex's level plus one and records the front vertex as its parent.
theorem bfsStateAdvance_distance_of_new {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ bfsNewNeighbors φ state u) :
(bfsStateAdvance φ state u rest).distance v = some (state.level u + 1) := by
simp [bfsStateAdvance, hv]theorem bfsStateAdvance_parent_of_new {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ bfsNewNeighbors φ state u) :
(bfsStateAdvance φ state u rest).parent v = some u := by
simp [bfsStateAdvance, hv]theorem bfsStateAdvance_level_of_new {φ : Flow V G} {state : BFSState V} {u v : V}
{rest : List V} (hv : v ∈ bfsNewNeighbors φ state u) :
(bfsStateAdvance φ state u rest).level v = state.level u + 1 := by
simp [BFSState.level, bfsStateAdvance_distance_of_new (φ := φ) hv]The initial labelled state satisfies all distance and predecessor invariants.
theorem bfsDistanceInvariant_init (φ : Flow V G) (s : V) :
BFSDistanceInvariant φ s (bfsStateInit s) := by
constructor <;> simp [BFSClosedInv, BFSQueueInv, bfsStateInit, BFSState.level]One FIFO step preserves the distance and predecessor invariant.
theorem bfsDistanceInvariant_step {φ : Flow V G} {s u : V} {rest : List V} {state : BFSState V}
(hqueue : state.queue = u :: rest)
(hinv : BFSDistanceInvariant φ s state) :
BFSDistanceInvariant φ s (bfsStateAdvance φ state u rest) := by
have hu_queue : u ∈ state.queue := by simp [hqueue]
have hu_visited : u ∈ state.visited := hinv.queued u hu_queue
have hu_not_new : u ∉ bfsNewNeighbors φ state u := by
simp [mem_bfsNewNeighbors_iff, hu_visited]
have hclosed : BFSClosedInv φ state.visited (u :: rest) := by
simpa [hqueue] using hinv.closed
have hqueued : BFSQueueInv φ state.visited (u :: rest) := by
simpa [hqueue] using hinv.queued
have hs_visited : s ∈ state.visited :=
(hinv.distance_iff_visited s).2 ⟨0, hinv.source_distance⟩
have hs_not_new : s ∉ bfsNewNeighbors φ state u := by
simp [mem_bfsNewNeighbors_iff, hs_visited]
have hordered : (u :: rest).Pairwise
(fun a b => state.level a ≤ state.level b) := by
simpa [hqueue] using hinv.queue_ordered
constructor
· simpa [bfsStateAdvance, bfsNewNeighbors] using
(bfsClosedInv_step (φ := φ) hclosed)
· simpa [bfsStateAdvance, bfsNewNeighbors] using
(bfsQueueInv_step (φ := φ) hqueued)
· simpa [bfsStateAdvance, hs_not_new] using hinv.source_distance
· simpa [bfsStateAdvance, hs_not_new] using hinv.source_parent
· intro v
constructor
· intro hv
change v ∈ state.visited ∪ bfsNewNeighbors φ state u at hv
rcases Finset.mem_union.mp hv with hvold | hvnew
· rcases (hinv.distance_iff_visited v).1 hvold with ⟨d, hd⟩
exact ⟨d, by simpa [bfsStateAdvance_distance_of_visited (φ := φ) hvold] using hd⟩
· exact ⟨state.level u + 1, bfsStateAdvance_distance_of_new (φ := φ) hvnew⟩
· rintro ⟨d, hd⟩
by_cases hvnew : v ∈ bfsNewNeighbors φ state u
· exact Finset.mem_union_right _ hvnew
· have hdold : state.distance v = some d := by
simpa [bfsStateAdvance, hvnew] using hd
exact Finset.mem_union_left _ ((hinv.distance_iff_visited v).2 ⟨d, hdold⟩)
· intro v hvzero
by_cases hvnew : v ∈ bfsNewNeighbors φ state u
· have := bfsStateAdvance_distance_of_new (φ := φ) (rest := rest) hvnew
rw [hvzero] at this
simp at this
· have hvold : state.distance v = some 0 := by
simpa [bfsStateAdvance, hvnew] using hvzero
exact hinv.distance_zero v hvold
· intro v hv hvs
change v ∈ state.visited ∪ bfsNewNeighbors φ state u at hv
rcases Finset.mem_union.mp hv with hvold | hvnew
· rcases hinv.parent_exists v hvold hvs with ⟨p, hp⟩
exact ⟨p, by simpa [bfsStateAdvance_parent_of_visited (φ := φ) hvold] using hp⟩
· exact ⟨u, bfsStateAdvance_parent_of_new (φ := φ) hvnew⟩
· intro v hv
have hvold : v ∉ state.visited := by
intro h
exact hv (Finset.mem_union_left _ h)
have hvnew : v ∉ bfsNewNeighbors φ state u := by
intro h
exact hv (Finset.mem_union_right _ h)
simpa [bfsStateAdvance, hvnew] using hinv.parent_unvisited v hvold
· intro p v hp
by_cases hvnew : v ∈ bfsNewNeighbors φ state u
· have hp_eq : p = u := by
have hnewParent := bfsStateAdvance_parent_of_new (φ := φ) (rest := rest) hvnew
rw [hp] at hnewParent
exact Option.some.inj hnewParent
subst p
have hadj : Flow.residualEdge φ u v := (mem_bfsNewNeighbors_iff (φ := φ)).1 hvnew |>.1
rcases (hinv.distance_iff_visited u).1 hu_visited with ⟨d, hd⟩
have hlevel : state.level u = d := by simp [BFSState.level, hd]
refine ⟨hadj, d, ?_, ?_⟩
simpa [bfsStateAdvance_distance_of_visited (φ := φ) hu_visited] using hd
simpa [hlevel] using bfsStateAdvance_distance_of_new (φ := φ) (rest := rest) hvnew
· have hpold : state.parent v = some p := by
simpa [bfsStateAdvance, hvnew] using hp
rcases hinv.parent_step p v hpold with ⟨hadj, d, hdp, hdv⟩
have hp_visited : p ∈ state.visited :=
(hinv.distance_iff_visited p).2 ⟨d, hdp⟩
have hv_visited : v ∈ state.visited :=
(hinv.distance_iff_visited v).2 ⟨d + 1, hdv⟩
refine ⟨hadj, d, ?_, ?_⟩
· simpa [bfsStateAdvance_distance_of_visited (φ := φ) hp_visited] using hdp
· simpa [bfsStateAdvance_distance_of_visited (φ := φ) hv_visited] using hdv
· change (rest ++ (bfsNewNeighbors φ state u).toList).Pairwise
(fun a b => (bfsStateAdvance φ state u rest).level a ≤
(bfsStateAdvance φ state u rest).level b)
rw [List.pairwise_append]
refine ⟨?_, ?_, ?_⟩
· have hrest := hordered.tail
rw [List.pairwise_iff_get] at hrest ⊢
intro i j hij
have hi_visited : rest.get i ∈ state.visited := hqueued _ (by simp)
have hj_visited : rest.get j ∈ state.visited := hqueued _ (by simp)
rw [bfsStateAdvance_level_of_visited (φ := φ) (rest := rest) hi_visited,
bfsStateAdvance_level_of_visited (φ := φ) (rest := rest) hj_visited]
exact hrest i j hij
· apply List.pairwise_of_reflexive_of_forall_ne
intro a ha b hb _
have ha_new : a ∈ bfsNewNeighbors φ state u := Finset.mem_toList.mp ha
have hb_new : b ∈ bfsNewNeighbors φ state u := Finset.mem_toList.mp hb
rw [bfsStateAdvance_level_of_new (φ := φ) ha_new,
bfsStateAdvance_level_of_new (φ := φ) hb_new]
· intro a ha b hb
have ha_visited : a ∈ state.visited := hqueued a (by simp [ha])
have hb_new : b ∈ bfsNewNeighbors φ state u := Finset.mem_toList.mp hb
rw [bfsStateAdvance_level_of_visited (φ := φ) ha_visited,
bfsStateAdvance_level_of_new (φ := φ) hb_new]
exact hinv.visited_span u rest hqueue a ha_visited
· intro front tail hnext_queue v hv
have hv_union : v ∈ state.visited ∪ bfsNewNeighbors φ state u := by
simpa [bfsStateAdvance] using hv
have hv_bound : (bfsStateAdvance φ state u rest).level v ≤ state.level u + 1 := by
rcases Finset.mem_union.mp hv_union with hvold | hvnew
· rw [bfsStateAdvance_level_of_visited (φ := φ) hvold]
exact hinv.visited_span u rest hqueue v hvold
· rw [bfsStateAdvance_level_of_new (φ := φ) hvnew]
cases rest with
| nil =>
have hlist : (bfsNewNeighbors φ state u).toList = front :: tail := by
simpa [bfsStateAdvance] using hnext_queue
have hfront_new : front ∈ bfsNewNeighbors φ state u := by
apply Finset.mem_toList.mp
rw [hlist]
simp
rw [bfsStateAdvance_level_of_new (φ := φ) hfront_new]
omega
| cons next remaining =>
have hlist : next :: (remaining ++ (bfsNewNeighbors φ state u).toList) =
front :: tail := by
simpa [bfsStateAdvance] using hnext_queue
have hfront : front = next := by
injection hlist with hhead _
exact hhead.symm
subst front
have hnext_visited : next ∈ state.visited := hqueued next (by simp)
have hu_le_next : state.level u ≤ state.level next :=
List.rel_of_pairwise_cons hordered (by simp)
rw [bfsStateAdvance_level_of_visited (φ := φ) hnext_visited]
omega
· intro x hx hnotin y hxy
have hx_union : x ∈ state.visited ∪ bfsNewNeighbors φ state u := by
simpa [bfsStateAdvance] using hx
rcases Finset.mem_union.mp hx_union with hxold | hxnew
· by_cases hxu : x = u
· subst x
by_cases hyold : y ∈ state.visited
· rw [bfsStateAdvance_level_of_visited (φ := φ) hyold,
bfsStateAdvance_level_of_visited (φ := φ) hu_visited]
exact hinv.visited_span u rest hqueue y hyold
· have hynew : y ∈ bfsNewNeighbors φ state u :=
(mem_bfsNewNeighbors_iff (φ := φ)).2 ⟨hxy, hyold⟩
rw [bfsStateAdvance_level_of_new (φ := φ) hynew,
bfsStateAdvance_level_of_visited (φ := φ) hu_visited]
· have hx_not_rest : x ∉ rest := by
intro hxrest
apply hnotin
change x ∈ rest ++ (bfsNewNeighbors φ state u).toList
exact List.mem_append_left _ hxrest
have hx_not_queue : x ∉ state.queue := by
rw [hqueue]
simp [hxu, hx_not_rest]
have hyold : y ∈ state.visited := hclosed x hxold (by
simp [hxu, hx_not_rest]) y hxy
rw [bfsStateAdvance_level_of_visited (φ := φ) hyold,
bfsStateAdvance_level_of_visited (φ := φ) hxold]
exact hinv.processed_edge x hxold hx_not_queue y hxy
· exfalso
apply hnotin
change x ∈ rest ++ (bfsNewNeighbors φ state u).toList
exact List.mem_append_right _ (Finset.mem_toList.mpr hxnew)Every fuelled execution preserves the distance invariant.
theorem bfsDistanceInvariant_aux {φ : Flow V G} {s : V} (fuel : ℕ) (state : BFSState V)
(hinv : BFSDistanceInvariant φ s state) :
BFSDistanceInvariant φ s (bfsStateAux φ fuel state) := by
induction fuel generalizing state with
| zero => simpa [bfsStateAux]
| succ fuel ih =>
cases hqueue : state.queue with
| nil => simpa [bfsStateAux, hqueue]
| cons u rest =>
simp only [bfsStateAux, hqueue]
exact ih (bfsStateAdvance φ state u rest)
(bfsDistanceInvariant_step (φ := φ) hqueue hinv)The final residual BFS state satisfies the distance invariant.
theorem residualBFS_distanceInvariant (φ : Flow V G) :
BFSDistanceInvariant φ G.s (residualBFS φ) := by
simpa [residualBFS] using
(bfsDistanceInvariant_aux (φ := φ) (Fintype.card V) (bfsStateInit G.s)
(bfsDistanceInvariant_init φ G.s))
The BFS measure: unvisited vertices plus queue length. Every step with a
nonempty queue decreases it by exactly one, and it starts at |V|.
Processing the front vertex decreases the measure by exactly one.
theorem bfsStateAdvance_measure {φ : Flow V G} {state : BFSState V} {u : V} {rest : List V} :
bfsMeasure (bfsStateAdvance φ state u rest) + 1 =
bfsMeasure {state with queue := u :: rest} := by
unfold bfsMeasure bfsStateAdvance
have hnew_sub : bfsNewNeighbors φ state u ⊆ Finset.univ \ state.visited := by
intro x hx
simp [Finset.mem_sdiff]
exact (Finset.mem_filter.mp hx).2
have hcard : (Finset.univ \ (state.visited ∪ bfsNewNeighbors φ state u)).card =
(Finset.univ \ state.visited).card - (bfsNewNeighbors φ state u).card := by
have hset : Finset.univ \ (state.visited ∪ bfsNewNeighbors φ state u) =
(Finset.univ \ state.visited) \ bfsNewNeighbors φ state u := by
ext x
simp [Finset.mem_sdiff]
have hEq : bfsNewNeighbors φ state u ∩ (Finset.univ \ state.visited) =
bfsNewNeighbors φ state u := by
exact Finset.inter_eq_left.mpr hnew_sub
rw [hset, Finset.card_sdiff, hEq]
have hle : (bfsNewNeighbors φ state u).card ≤
(Finset.univ \ state.visited).card :=
Finset.card_le_card hnew_sub
simp [hcard]
omegaIf the queue is nonempty throughout, the measure drops by exactly one per step.
theorem bfsStateAux_measure_of_nonempty {φ : Flow V G} (fuel : ℕ) (state : BFSState V)
(h : (bfsStateAux φ fuel state).queue ≠ []) :
bfsMeasure (bfsStateAux φ fuel state) = bfsMeasure state - fuel := by
refine Nat.rec
(motive := fun fuel => ∀ state : BFSState V,
(bfsStateAux φ fuel state).queue ≠ [] →
bfsMeasure (bfsStateAux φ fuel state) = bfsMeasure state - fuel)
?_ ?_ fuel state h
· intro state h
simp [bfsStateAux]
· intro fuel ih state h
cases hqueue : state.queue with
| nil =>
have hnil : (bfsStateAux φ (fuel + 1) state).queue = [] := by
simp [bfsStateAux, hqueue]
exact (h hnil).elim
| cons u rest =>
have h' : (bfsStateAux φ fuel (bfsStateAdvance φ state u rest)).queue ≠ [] := by
simpa [bfsStateAux, hqueue] using h
have hih := ih (bfsStateAdvance φ state u rest) h'
have hdec' : bfsMeasure (bfsStateAdvance φ state u rest) = bfsMeasure state - 1 := by
have hdec := bfsStateAdvance_measure (φ := φ) (state := state) (u := u)
(rest := rest)
have hEq : bfsMeasure {state with queue := u :: rest} = bfsMeasure state := by
unfold bfsMeasure
simp [hqueue]
omega
have hmeas : bfsMeasure (bfsStateAux φ fuel (bfsStateAdvance φ state u rest)) =
bfsMeasure state - (fuel + 1) := by
rw [hih, hdec']
omega
simpa [bfsStateAux, hqueue] using hmeas
The fuelled residual BFS exhausts its queue: after |V| steps every
vertex reachable in the residual network has been discovered.
theorem residualBFS_queue_empty (φ : Flow V G) : (residualBFS φ).queue = [] := by
by_contra h
have hmeas := bfsStateAux_measure_of_nonempty (φ := φ) (fuel := Fintype.card V)
(state := bfsStateInit G.s) h
have hinit : bfsMeasure (bfsStateInit G.s) = Fintype.card V := by
change (Finset.univ \ ({G.s} : Finset V)).card + ([G.s] : List V).length =
Fintype.card V
simp
have hpos : 0 < Fintype.card V := Fintype.card_pos (α := V) (h := ⟨G.s⟩)
have hcard : (Finset.univ \ ({G.s} : Finset V)).card = Fintype.card V - 1 := by
rw [Finset.sdiff_singleton_eq_erase]
exact Finset.card_erase_of_mem (Finset.mem_univ G.s)
rw [hcard]
omega
have hzero : bfsMeasure (residualBFS φ) = 0 := by
unfold residualBFS
rw [hmeas, hinit]
omega
have hge : 1 ≤ bfsMeasure (residualBFS φ) := by
unfold bfsMeasure
have hlen : 1 ≤ (residualBFS φ).queue.length := List.length_pos_iff.mpr h
omega
omega
A path following the recorded parent function from the source. This is a
Type rather than a Prop so that its vertex list can be extracted by
pattern matching (see BFSParentPath.vertices).
inductive BFSParentPath (parent : V → Option V) (s : V) : V → ℕ → Type _ where
| root : BFSParentPath parent s s 0
| tail {u v : V} {n : ℕ} :
BFSParentPath parent s u n → parent v = some u →
BFSParentPath parent s v (n + 1)Every distance label maintained by the invariant is witnessed by a parent path of exactly that length.
noncomputable def BFSDistanceInvariant.parentPath_of_distance
{φ : Flow V G} {s : V} {state : BFSState V} (hinv : BFSDistanceInvariant φ s state)
{v : V} {d : ℕ} (hd : state.distance v = some d) :
BFSParentPath state.parent s v d := by
refine (inferInstance : IsWellFounded ℕ (· < ·)).wf.fix
(C := fun n => ∀ v (hd : state.distance v = some n),
BFSParentPath state.parent s v n) ?_ d v hd
intro n ih v hd
cases n with
| zero =>
have hvs : v = s := hinv.distance_zero v hd
subst v
exact BFSParentPath.root
| succ n =>
have hv_visited : v ∈ state.visited :=
(hinv.distance_iff_visited v).2 ⟨n + 1, hd⟩
have hvs : v ≠ s := by
intro h
subst v
rw [hinv.source_distance] at hd
simp at hd
have hu' : ∃ u, state.parent v = some u := hinv.parent_exists v hv_visited hvs
let u := Classical.choose hu'
have hparent : state.parent v = some u := Classical.choose_spec hu'
have hstep := hinv.parent_step u v hparent
have hdv' : ∃ d, state.distance u = some d ∧ state.distance v = some (d + 1) := hstep.2
let d' := Classical.choose hdv'
have hdu : state.distance u = some d' := (Classical.choose_spec hdv').1
have hdv : state.distance v = some (d' + 1) := (Classical.choose_spec hdv').2
have hdn : d' = n := by
rw [hd] at hdv
simp at hdv
omega
have hdu'' : state.distance u = some n := by
simpa [hdn] using hdu
exact BFSParentPath.tail (ih n (by omega) u hdu'') hparentParent paths in a valid BFS state are residual paths with the same number of edges.
theorem BFSDistanceInvariant.parentPath_ResidualPathLength
{φ : Flow V G} {s : V} {state : BFSState V} (hinv : BFSDistanceInvariant φ s state)
{v : V} {d : ℕ} (hpath : BFSParentPath state.parent s v d) :
ResidualPathLength φ s v d := by
induction hpath with
| root => exact ResidualPathLength.refl s
| @tail u v n hpath hparent ih =>
exact ResidualPathLength.tail s u v n ih (hinv.parent_step u v hparent).1Exact-length reachability in the residual network implies residual reachability.
lemma ResidualPathLength.reachable {φ : Flow V G} {u v : V} {n : ℕ}
(h : ResidualPathLength φ u v n) : Flow.augmentingPathReachable φ u v := by
refine ResidualPathLength.rec
(motive := fun (v : V) (n : ℕ) (_h : ResidualPathLength φ u v n) =>
Flow.augmentingPathReachable φ u v)
(by exact Relation.ReflTransGen.refl)
(fun v w n hprev hedge ih => Relation.ReflTransGen.tail ih hedge)
hEvery recorded distance is attained by a residual path of exactly that length.
theorem bfsState_distance_ResidualPathLength (φ : Flow V G) {v : V} {d : ℕ}
(hd : (residualBFS φ).distance v = some d) :
ResidualPathLength φ G.s v d := by
have hinv := residualBFS_distanceInvariant φ
exact hinv.parentPath_ResidualPathLength (hinv.parentPath_of_distance hd)Along any exact-length residual path from the source, the final BFS distance is no larger than the path length.
theorem bfsState_distance_le_of_ResidualPathLength (φ : Flow V G) {v : V} {n : ℕ}
(hpath : ResidualPathLength φ G.s v n) :
∃ d, (residualBFS φ).distance v = some d ∧ d ≤ n := by
let result := residualBFS φ
have hinv : BFSDistanceInvariant φ G.s result := residualBFS_distanceInvariant φ
have hqueue : result.queue = [] := residualBFS_queue_empty φ
have h := ResidualPathLength.rec
(motive := fun (v : V) (n : ℕ) (_h : ResidualPathLength φ G.s v n) =>
∃ d, result.distance v = some d ∧ d ≤ n)
(by exact ⟨0, hinv.source_distance, le_rfl⟩)
(fun v w n hprev hedge ih => by
rcases ih with ⟨dv, hdv, hle⟩
have hv_visited : v ∈ result.visited :=
(hinv.distance_iff_visited v).2 ⟨dv, hdv⟩
have hw_visited : w ∈ result.visited :=
hinv.closed v hv_visited (by simp [hqueue]) w hedge
rcases (hinv.distance_iff_visited w).1 hw_visited with ⟨dw, hdw⟩
have hdv' : result.distance v = some dv := by simpa [result] using hdv
have hv_level : result.level v = dv := by simp [BFSState.level, hdv']
have hw_level : result.level w = dw := by simp [BFSState.level, hdw]
have hedge' := hinv.processed_edge v hv_visited (by simp [hqueue]) w hedge
rw [hv_level, hw_level] at hedge'
exact ⟨dw, hdw, by omega⟩)
hpath
simpa [result] using hEvery present final BFS label is the residual shortest-path distance.
theorem bfsState_distance_isShortest (φ : Flow V G) {v : V} {d : ℕ}
(hd : (residualBFS φ).distance v = some d) :
IsShortestDist φ G.s v d := by
constructor
· exact bfsState_distance_ResidualPathLength φ hd
· intro n hn
rcases bfsState_distance_le_of_ResidualPathLength φ hn with ⟨d', hd', hle⟩
rw [hd] at hd'
have : d' = d := (Option.some.inj hd').symm
omegaBFS discovers exactly the residual-reachable vertices.
theorem residualBFS_visited_iff_reachable (φ : Flow V G) (v : V) :
v ∈ (residualBFS φ).visited ↔ Flow.augmentingPathReachable φ G.s v := by
let result := residualBFS φ
have hinv : BFSDistanceInvariant φ G.s result := residualBFS_distanceInvariant φ
have hqueue : result.queue = [] := residualBFS_queue_empty φ
constructor
· intro hv
rcases (hinv.distance_iff_visited v).1 hv with ⟨d, hd⟩
exact (bfsState_distance_ResidualPathLength φ hd).reachable
· intro hreach
induction hreach with
| refl =>
exact (hinv.distance_iff_visited G.s).2 ⟨0, hinv.source_distance⟩
| tail hprev hedge ih =>
exact hinv.closed _ ih (by simp [hqueue]) _ hedgeThe final BFS distance map is defined exactly on reachable vertices.
theorem bfsState_distance_defined_iff_reachable (φ : Flow V G) (v : V) :
(∃ d, (residualBFS φ).distance v = some d) ↔ Flow.augmentingPathReachable φ G.s v := by
let result := residualBFS φ
have hinv : BFSDistanceInvariant φ G.s result := residualBFS_distanceInvariant φ
constructor
· rintro ⟨d, hd⟩
exact (bfsState_distance_ResidualPathLength φ hd).reachable
· intro hreach
have hv_visited : v ∈ result.visited :=
(residualBFS_visited_iff_reachable φ v).2 hreach
simpa [result] using (hinv.distance_iff_visited v).1 hv_visitedComplete iff specification for the distance returned by residual BFS.
theorem bfsState_distance_eq_some_iff (φ : Flow V G) (v : V) {d : ℕ} :
(residualBFS φ).distance v = some d ↔ IsShortestDist φ G.s v d := by
constructor
· exact bfsState_distance_isShortest φ
· intro hshortest
rcases (bfsState_distance_defined_iff_reachable φ v).2 hshortest.1.reachable with ⟨d', hd'⟩
have hd'_shortest := bfsState_distance_isShortest φ hd'
have h1 : d ≤ d' := hshortest.2 d' hd'_shortest.1
have h2 : d' ≤ d := hd'_shortest.2 d hshortest.1
have : d' = d := Nat.le_antisymm h2 h1
simpa [this] using hd'Every recorded predecessor is a residual edge and decreases BFS distance by exactly one when followed toward the source.
theorem bfsState_parent_spec (φ : Flow V G) {u v : V}
(hparent : (residualBFS φ).parent v = some u) :
Flow.residualEdge φ u v ∧ ∃ d,
(residualBFS φ).distance u = some d ∧
(residualBFS φ).distance v = some (d + 1) := by
exact (residualBFS_distanceInvariant φ).parent_step u v hparentFollowing a predecessor edge strictly increases level away from the root.
theorem bfsState_parent_level_lt (φ : Flow V G) {u v : V}
(hparent : (residualBFS φ).parent v = some u) :
(residualBFS φ).level u < (residualBFS φ).level v := by
rcases bfsState_parent_spec φ hparent with ⟨_, d, hdu, hdv⟩
simp [BFSState.level, hdu, hdv]The vertices of a parent path, from the source to the endpoint.
noncomputable def BFSParentPath.vertices {parent : V → Option V} {s v : V} {n : ℕ}
(h : BFSParentPath parent s v n) : List V :=
match h with
| root => [s]
| tail hprev _ => BFSParentPath.vertices hprev ++ [v]
The parent path has exactly n + 1 vertices.
lemma BFSParentPath.vertices_length {parent : V → Option V} {s v : V} {n : ℕ}
(h : BFSParentPath parent s v n) : (BFSParentPath.vertices h).length = n + 1 := by
induction h with
| root => simp [BFSParentPath.vertices]
| tail hprev _ ih =>
simp [BFSParentPath.vertices, ih]The parent path starts at the source.
lemma BFSParentPath.vertices_head {parent : V → Option V} {s v : V} {n : ℕ}
(h : BFSParentPath parent s v n) : (BFSParentPath.vertices h).head? = some s := by
induction h with
| root => simp [BFSParentPath.vertices]
| @tail u v n hprev _ ih =>
have hne : BFSParentPath.vertices hprev ≠ [] := by
rw [← List.length_pos_iff, BFSParentPath.vertices_length]
omega
rw [BFSParentPath.vertices]
rw [List.head?_append_of_ne_nil _ hne]
exact ihThe parent path ends at the requested vertex.
lemma BFSParentPath.vertices_getLast {parent : V → Option V} {s v : V} {n : ℕ}
(h : BFSParentPath parent s v n) : (BFSParentPath.vertices h).getLast? = some v := by
induction h with
| root => simp [BFSParentPath.vertices]
| @tail u v n hprev _ ih =>
rw [BFSParentPath.vertices]
rw [List.getLast?_append_of_ne_nil _ (by simp)]
rflConsecutive vertices of a parent path are joined by residual edges.
lemma BFSParentPath.vertices_chain {φ : Flow V G} {s : V} {state : BFSState V}
(hinv : BFSDistanceInvariant φ s state) {v : V} {n : ℕ}
(h : BFSParentPath state.parent s v n) :
(BFSParentPath.vertices h).IsChain (Flow.residualEdge φ) := by
induction h with
| root => simp [BFSParentPath.vertices]
| @tail u v n hprev hpar ih =>
rw [BFSParentPath.vertices]
apply IsChain_append_last
· exact ih
· intro y hy
have hlast := hprev.vertices_getLast
have hyu : y = u := by
have : u = y := by simpa [hlast] using hy
exact this.symm
simpa [hyu] using (hinv.parent_step u v hpar).1
The vertex at position i of a parent path has BFS level exactly i.
lemma BFSParentPath.vertices_level_getElem {φ : Flow V G} {s : V} {state : BFSState V}
(hinv : BFSDistanceInvariant φ s state) {v : V} {n : ℕ}
(h : BFSParentPath state.parent s v n) :
∀ i (hi : i < (BFSParentPath.vertices h).length),
state.level (BFSParentPath.vertices h)[i] = i := by
induction h with
| root =>
intro i hi
have hi0 : i = 0 := by
simp [BFSParentPath.vertices] at hi
exact hi
subst i
simp [BFSParentPath.vertices, BFSState.level, hinv.source_distance]
| @tail u v n hprev hpar ih =>
intro i hi
by_cases hi_lt : i < (BFSParentPath.vertices hprev).length
· have hget : (BFSParentPath.vertices hprev ++ [v])[i] =
(BFSParentPath.vertices hprev)[i] :=
List.getElem_append_left hi_lt
have hle := ih i hi_lt
change state.level ((BFSParentPath.vertices hprev ++ [v])[i]) = i
rw [hget]
exact hle
· have hi_eq : i = (BFSParentPath.vertices hprev).length := by
simp [BFSParentPath.vertices] at hi
omega
subst i
have hget : (BFSParentPath.vertices hprev ++ [v])[
(BFSParentPath.vertices hprev).length] = v := by
simpa using List.getElem_append_right (BFSParentPath.vertices hprev) [v]
(BFSParentPath.vertices hprev).length le_rfl (by simp)
rcases hinv.parent_step u v hpar with ⟨_, d, hdu, hdv⟩
have hlv : state.level v = state.level u + 1 := by
simp [BFSState.level, hdu, hdv]
have hlen := BFSParentPath.vertices_length (h := hprev)
have hne : BFSParentPath.vertices hprev ≠ [] := by
rw [← List.length_pos_iff, hlen]
omega
have hlast := hprev.vertices_getLast
have hgetlast : (BFSParentPath.vertices hprev)[
(BFSParentPath.vertices hprev).length - 1] = u := by
rw [← List.getLast_eq_getElem hne]
exact List.getLast_of_getLast?_eq_some hlast
have hih := ih ((BFSParentPath.vertices hprev).length - 1) (by
rw [hlen]
omega)
have hlu : state.level u = n := by
rw [hgetlast] at hih
have : (BFSParentPath.vertices hprev).length - 1 = n := by omega
simpa [this] using hih
simp [BFSParentPath.vertices]
rw [hlv, hlu]
rw [BFSParentPath.vertices_length (h := hprev)]The parent path is a simple list: BFS levels strictly increase along it.
lemma BFSParentPath.vertices_nodup {φ : Flow V G} {s : V} {state : BFSState V}
(hinv : BFSDistanceInvariant φ s state) {v : V} {n : ℕ}
(h : BFSParentPath state.parent s v n) : (BFSParentPath.vertices h).Nodup := by
rw [List.nodup_iff_injective_getElem]
intro i j hij
apply Fin.ext
have hli := h.vertices_level_getElem hinv i.1 i.2
have hlj := h.vertices_level_getElem hinv j.1 j.2
have hcong := congrArg (state.level) hij
calc
i.1 = state.level (h.vertices[i.1]) := hli.symm
_ = state.level (h.vertices[j.1]) := hcong
_ = j.1 := hljThe parent chain from the sink assembles a simple residual path whose edge count realizes the recorded distance.
noncomputable def bfsParentResidualPath (φ : Flow V G) {d : ℕ}
(hd : (residualBFS φ).distance G.t = some d) : Flow.ResidualPath φ G.s G.t := by
let hpp := (residualBFS_distanceInvariant φ).parentPath_of_distance hd
exact { vertices := BFSParentPath.vertices hpp
, chain := hpp.vertices_chain (residualBFS_distanceInvariant φ)
, head_eq := hpp.vertices_head
, last_eq := hpp.vertices_getLast
, nodup := hpp.vertices_nodup (residualBFS_distanceInvariant φ) }The parent-chain path realizes the recorded distance.
lemma bfsParentResidualPath_edges_length (φ : Flow V G) {d : ℕ}
(hd : (residualBFS φ).distance G.t = some d) :
(bfsParentResidualPath φ hd).edges.length = d := by
rw [Flow.ResidualPath.edges_length]
simp [bfsParentResidualPath, BFSParentPath.vertices_length]Executable shortest augmenting path. When the sink is residual reachable, the BFS parent chain from the sink is a shortest augmenting path.
noncomputable def bfs_shortestAugmenting (φ : Flow V G) (h : φ.hasAugmentingPath) :
ShortestAugmentingPath φ := by
have hd' : ∃ d, (residualBFS φ).distance G.t = some d :=
(bfsState_distance_defined_iff_reachable φ G.t).2 h
let d := Classical.choose hd'
have hd : (residualBFS φ).distance G.t = some d := Classical.choose_spec hd'
have hshort : IsShortestDist φ G.s G.t d :=
(bfsState_distance_eq_some_iff φ G.t).1 hd
let p : Flow.AugmentingPath φ := bfsParentResidualPath φ hd
have hlen : p.edges.length = d := by
simpa [p] using bfsParentResidualPath_edges_length φ hd
exact { path := p, h_shortest := by simpa [hlen] using hshort }
BFS drives the Edmonds-Karp step. ekStep augments along a shortest
path whose length is the one the executable BFS computes: both realize the
same residual distance.
theorem ekStep_shortest_path_bfs (φ : Flow V G) (h : φ.hasAugmentingPath) :
∃ p : ShortestAugmentingPath φ, ekStep φ = φ.augment p.path ∧
p.path.edges.length = (bfs_shortestAugmenting φ h).path.edges.length := by
have hnon : Nonempty (ShortestAugmentingPath φ) :=
(shortestAugmentingPath_iff_hasAugmentingPath φ).mpr h
refine ⟨Classical.choice hnon, ?_, ?_⟩
· unfold ekStep
simp [hnon]
· exact (Classical.choice hnon).h_shortest.unique (bfs_shortestAugmenting φ h).h_shortestend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.SparseExecution.Execution
Edmonds–Karp from the counted BFS-selected paths
Support buckets and the finite vertex count are prepared once. A polynomial number of rounds suffices for arbitrary nonnegative real capacities. A round that finds no path retains its flow; later rounds may repeat the failed BFS, and their work remains included. The same returned flow, path choices, and local updates are used in the correctness and work proofs.
noncomputable sectionnamespace CLRS.Chapter26.SparseEKopen Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}structure ExecutionResult (G : FlowNetwork V) where
flow : Flow V G
work : Nat
augmentations : Natdef step (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (prev : ExecutionResult G) : ExecutionResult G :=
let found := search input A hA prev.flow
match found.path with
| none => ⟨prev.flow,prev.work+found.work,prev.augmentations⟩
| some p =>
let next := augmentWithCost prev.flow p.path
⟨next.flow,prev.work+found.work+next.work,prev.augmentations+1⟩def iterate (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (N : Nat) : ExecutionResult G :=
Nat.rec ⟨zeroFlow G,0,0⟩ (fun _ previous => step input A hA previous) N@[simp] theorem iterate_zero (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) :
iterate input A hA 0 = ⟨zeroFlow G,0,0⟩ := rfl@[simp] theorem iterate_succ (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (N : Nat) :
iterate input A hA (N+1) = step input A hA (iterate input A hA N) := rfldef timeline (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) : Timeline G where
flow i := (iterate input A hA i).flow
path i := (search input A hA (iterate input A hA i).flow).path
next i := by
cases hp : (search input A hA (iterate input A hA i).flow).path with
| none => simp [iterate_succ,step,hp]
| some p => simpa [iterate_succ,step,hp] using
augmentWithCost_refines (iterate input A hA i).flow p.paththeorem iterate_no_path_step (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (i : Nat)
(h : ¬ (iterate input A hA i).flow.hasAugmentingPath) :
(iterate input A hA (i+1)).flow = (iterate input A hA i).flow := by
have hn := (search_none_iff input A hA _).2 h
simp [iterate_succ,step,hn]
theorem iterate_stable (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) {i j : Nat} (hij : i ≤ j)
(h : ¬ (iterate input A hA i).flow.hasAugmentingPath) :
(iterate input A hA j).flow = (iterate input A hA i).flow := by
induction j, hij using Nat.le_induction with
| base => rfl
| succ k hk ih =>
rw [iterate_no_path_step input A hA k (by simpa [ih] using h),ih]The bound comes from the actual selector's timeline, not the old classical chooser.
theorem iterate_terminal (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (N : Nat)
(hN : (support G).card * Fintype.card V < N) :
¬ (iterate input A hA N).flow.hasAugmentingPath := by
intro hlast
have hall : ∀ i < N, (timeline input A hA).Augments i := by
intro i hi
cases hp : (search input A hA (iterate input A hA i).flow).path with
| none =>
have hn := (search_none_iff input A hA _).1 hp
have hs := iterate_stable input A hA (Nat.le_of_lt hi) hn
exact (hn (hs ▸ hlast)).elim
| some p => exact ⟨p,hp⟩
have hc := (timeline input A hA).all_steps_bound N hall
omega
theorem iterate_augmentations (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (N : Nat) :
(iterate input A hA N).augmentations =
((Finset.range N).filter (timeline input A hA).Augments).card := by
induction N with
| zero => simp
| succ N ih =>
rw [Finset.range_add_one]
cases hp : (search input A hA (iterate input A hA N).flow).path with
| none =>
have hn : ¬ (timeline input A hA).Augments N := by
simp [Timeline.Augments,timeline,hp]
simp [iterate_succ,step,hp,Finset.filter_insert,hn,ih]
| some p =>
have hn : (timeline input A hA).Augments N := ⟨p,hp⟩
simp [iterate_succ,step,hp,Finset.filter_insert,hn,ih]theorem iterate_work_le (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (N : Nat) :
(iterate input A hA N).work ≤ N*(5+17*(support G).card) := by
induction N with
| zero => simp
| succ N ih =>
have hs := search_work_le input A hA (iterate input A hA N).flow
simp only [iterate_succ,step]
split
· dsimp only
nlinarith
· rename_i p hp
have hu := augmentWithCost_work_le (iterate input A hA N).flow p
dsimp only
nlinarithCount the input vertex enumeration once; no per-round dense initialization occurs.
def countVertices : List V → Nat
| [] => 0
| _ :: vs => countVertices vs+1omit [Fintype V] [DecidableEq V] in
theorem countVertices_eq (vs : List V) : countVertices vs = vs.length := by
induction vs with
| nil => rfl
| cons v vs ih => simp [countVertices,ih]def execute (input : CapacityInput G) : ExecutionResult G :=
let prepared := prepare input.arcs
let vertices := countVertices (Finset.univ.toList : List V)
let result := iterate input prepared.adjacency rfl (prepared.work*vertices+1)
{ result with work := prepared.work+vertices+result.work }The actual returned flow is maximal, without an integrality premise.
theorem execute_maximal (input : CapacityInput G) : (execute input).flow.isMaximal := by
apply Flow.maximal_of_noAugmentingPath
apply iterate_terminal input _ rfl
have hc := support_card_le G
simp only [prepare_work,countVertices_eq,Finset.length_toList,Finset.card_univ]
rw [input.length_eq]
nlinarith [Nat.mul_le_mul_right (Fintype.card V) hc]Actual augmentations are bounded by positive arcs times vertices.
theorem execute_augmentations_le (input : CapacityInput G) :
(execute input).augmentations ≤ 2*(positiveArcs G).card*Fintype.card V := by
change (iterate input _ rfl _).augmentations ≤ _
rw [iterate_augmentations]
exact (timeline input _ rfl).augmentation_count_sparse _General bound before absorbing lower-order preparation and failed-search costs.
theorem execute_work_polynomial (input : CapacityInput G) :
(execute input).work ≤ 2*(positiveArcs G).card+Fintype.card V+
(2*(positiveArcs G).card*Fintype.card V+1)*(5+34*(positiveArcs G).card) := by
have hi := iterate_work_le input (prepare input.arcs).adjacency rfl
((prepare input.arcs).work*countVertices (Finset.univ.toList : List V)+1)
have hs := support_card_le G
simp only [execute,prepare_work,countVertices_eq,Finset.length_toList,Finset.card_univ,input.length_eq] at *
nlinarith [Nat.mul_le_mul_left (2*(positiveArcs G).card*Fintype.card V+1)
(show 5+17*(support G).card ≤ 5+34*(positiveArcs G).card by omega)]On nonempty sparse inputs the complete counted execution is O(V E²).
theorem execute_work_bound (input : CapacityInput G) (hE : 0 < (positiveArcs G).card) :
(execute input).work ≤ 130*Fintype.card V*((positiveArcs G).card)^2 := by
have hc := execute_work_polynomial input
have hV : 0 < Fintype.card V := Fintype.card_pos_iff.mpr ⟨G.s⟩
have hE1 : 1 ≤ (positiveArcs G).card := hE
have hsq : (positiveArcs G).card ≤ ((positiveArcs G).card)^2 := by nlinarith
have hVE : (positiveArcs G).card ≤ Fintype.card V*(positiveArcs G).card := by nlinarith
have hVE2 : ((positiveArcs G).card)^2 ≤ Fintype.card V*((positiveArcs G).card)^2 := by nlinarith
have hV2 : Fintype.card V ≤ Fintype.card V*((positiveArcs G).card)^2 := by nlinarith
nlinarithEmpty capacity input still pays for vertex enumeration and one failed search.
theorem execute_work_empty (input : CapacityInput G) (hE : (positiveArcs G).card = 0) :
(execute input).work ≤ Fintype.card V+2 := by
have hs : (support G).card = 0 := by have := support_card_le G; omega
have hn : ¬ (zeroFlow G).hasAugmentingPath := by
intro h
obtain ⟨p⟩ := exists_shortest_augmenting_path (zeroFlow G) h
have hp := shortest_length_support (zeroFlow G) p
have hpos := p.path.edges_nonempty
have : 0 < p.path.edges.length := List.length_pos_iff.mpr hpos
omega
have hp := (search_none_iff input (prepare input.arcs).adjacency rfl _).2 hn
have hw := search_work_of_none input (prepare input.arcs).adjacency rfl _ hp
have hb := bfs_work_le input (zeroFlow G)
simp only [hs,Nat.mul_zero,Nat.add_zero] at hb
simp only [execute,prepare_work,countVertices_eq,Finset.length_toList,Finset.card_univ,
input.length_eq,hE,Nat.mul_zero,Nat.zero_mul,Nat.zero_add,iterate_succ,iterate_zero,step,hp]
omegaUniform bound including the empty sparse input and its initialization.
theorem execute_work_uniform (input : CapacityInput G) :
(execute input).work ≤ Fintype.card V+2+
130*Fintype.card V*((positiveArcs G).card)^2 := by
by_cases hE : (positiveArcs G).card = 0
· simpa [hE] using execute_work_empty input hE
· have := execute_work_bound input (Nat.pos_of_ne_zero hE)
omegaend CLRS.Chapter26.SparseEKCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.SparseExecution.Search
Counted BFS parent recovery
The search binds one support-BFS result, tests its stored sink distance, and follows that result's stored parents. The shortest-path proof describes the recovered list; it does not choose a second shortest path or rerun BFS.
noncomputable sectionnamespace CLRS.Chapter26.SparseEKopen Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}def reverseParents (parent : V → Option V) : Nat → V → CostedPathVertices V
| 0, v => ⟨[v],1⟩
| d+1, v =>
match parent v with
| none => ⟨[v],2⟩
| some u =>
let old := reverseParents parent d u
⟨v :: old.vertices, old.work + 2⟩def recoverParents (parent : V → Option V) (d : Nat) (v : V) : CostedPathVertices V :=
let old := reverseParents parent d v
⟨old.vertices.reverse, old.work + old.vertices.length⟩omit [Fintype V] [DecidableEq V] in
theorem reverseParents_spec {parent : V → Option V} {s v : V} {d : Nat}
(hp : BFSParentPath parent s v d) :
(reverseParents parent d v).vertices = hp.vertices.reverse ∧
(reverseParents parent d v).work = 2*d+1 := by
induction hp with
| root => simp [reverseParents, BFSParentPath.vertices]
| @tail u v d hp hpar ih =>
simp [reverseParents, hpar, BFSParentPath.vertices, ih, Nat.mul_add, Nat.add_assoc]theorem recoverParents_spec {parent : V → Option V} {s v : V} {d : Nat}
(hp : BFSParentPath parent s v d) :
(recoverParents parent d v).vertices = hp.vertices ∧
(recoverParents parent d v).work = 3*d+2 := by
have hs := reverseParents_spec hp
simp [recoverParents, hs.1, hs.2, BFSParentPath.vertices_length]
omega
theorem shortest_length_support (φ : Flow V G) (p : ShortestAugmentingPath φ) :
p.path.edges.length ≤ (support G).card := by
have hv : p.path.vertices.toFinset ⊆ (residualBFS φ).visited := by
intro v h
obtain ⟨i,hi,hv⟩ := List.getElem_of_mem (List.mem_toFinset.mp h)
have hr := (p.shortest_prefix i hi).1.reachable
apply (residualBFS_visited_iff_reachable φ v).2
simpa [hv] using hr
have hc := Finset.card_le_card hv
rw [List.toFinset_card_of_nodup p.path.nodup] at hc
have hs := Finset.card_le_card (residualBFS_visited_subset φ)
have hi := Finset.card_insert_le G.s ((support G).image Prod.snd)
have him := Finset.card_image_le (s := support G) (f := Prod.snd)
rw [Flow.ResidualPath.edges_length]
omegaRecover the shortest path from the supplied saved BFS state.
def recoveredShortest (φ : Flow V G) (b : CostedBFSRun V)
(hb : b.state = residualBFS φ) (d : Nat) (hd : b.state.distance G.t = some d) :
ShortestAugmentingPath φ × Nat :=
let recovered := recoverParents b.state.parent d G.t
let inv : BFSDistanceInvariant φ G.s b.state := hb.symm ▸ residualBFS_distanceInvariant φ
let hp := inv.parentPath_of_distance hd
have hv : recovered.vertices = hp.vertices := (recoverParents_spec hp).1
let path : Flow.AugmentingPath φ :=
{ vertices := recovered.vertices
chain := hv ▸ hp.vertices_chain inv
head_eq := hv ▸ hp.vertices_head
last_eq := hv ▸ hp.vertices_getLast
nodup := hv ▸ hp.vertices_nodup inv }
have hlen : path.edges.length = d := by
rw [Flow.ResidualPath.edges_length]
change recovered.vertices.length - 1 = d
rw [hv, BFSParentPath.vertices_length]
omega
(⟨path, by
rw [hlen]
exact (bfsState_distance_eq_some_iff φ G.t).1 (by simpa [hb] using hd)⟩,
recovered.work)theorem recoveredShortest_work (φ : Flow V G) (b : CostedBFSRun V)
(hb : b.state = residualBFS φ) (d : Nat) (hd : b.state.distance G.t = some d) :
(recoveredShortest φ b hb d hd).2 = 3*d+2 := by
exact (recoverParents_spec ((hb.symm ▸ residualBFS_distanceInvariant φ).parentPath_of_distance hd)).2
theorem recoveredShortest_length (φ : Flow V G) (b : CostedBFSRun V)
(hb : b.state = residualBFS φ) (d : Nat) (hd : b.state.distance G.t = some d) :
(recoveredShortest φ b hb d hd).1.path.edges.length = d := by
simp only [recoveredShortest, Flow.ResidualPath.edges_length]
rw [(recoverParents_spec ((hb.symm ▸ residualBFS_distanceInvariant φ).parentPath_of_distance hd)).1,
BFSParentPath.vertices_length]
omegastructure SearchResult (φ : Flow V G) where
path : Option (ShortestAugmentingPath φ)
work : Natdef search (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (φ : Flow V G) : SearchResult φ :=
let b := costedResidualBFS A φ
have hb : b.state = residualBFS φ := costedResidualBFS_state A φ (hA ▸ input.covers φ)
match hd : b.state.distance G.t with
| none => ⟨none,b.work+1⟩
| some d =>
let p := recoveredShortest φ b hb d hd
⟨some p.1,b.work+1+p.2⟩
theorem search_none_iff (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (φ : Flow V G) :
(search input A hA φ).path = none ↔ ¬ φ.hasAugmentingPath := by
have hb := costedResidualBFS_state A φ (hA ▸ input.covers φ)
simp only [search]
split
· rename_i hd
have hd' : (residualBFS φ).distance G.t = none := by simpa [hb] using hd
simp only [true_iff]
intro h
obtain ⟨d,he⟩ := (bfsState_distance_defined_iff_reachable φ G.t).2 h
simp [hd'] at he
· rename_i d hd
have hd' : (residualBFS φ).distance G.t = some d := by simpa [hb] using hd
simp only [Option.some_ne_none, false_iff, not_not]
exact (bfsState_distance_defined_iff_reachable φ G.t).1 ⟨d,hd'⟩theorem search_work_of_none (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (φ : Flow V G)
(hn : (search input A hA φ).path = none) :
(search input A hA φ).work = (costedResidualBFS A φ).work+1 := by
simp only [search] at *
split at hn <;> simp_all
theorem search_work_le (input : CapacityInput G) (A : SupportAdjacency V)
(hA : A = (prepare input.arcs).adjacency) (φ : Flow V G) :
(search input A hA φ).work ≤ 4 + 8 * (support G).card := by
have hb : (costedResidualBFS A φ).work ≤ 1 + 5 * (support G).card := by
simpa [hA] using bfs_work_le input φ
simp only [search]
split
· dsimp only
omega
· rename_i d hd
rw [recoveredShortest_work]
have hp := shortest_length_support φ
(recoveredShortest φ (costedResidualBFS A φ)
(costedResidualBFS_state A φ (hA ▸ input.covers φ)) d hd).1
rw [recoveredShortest_length] at hp
dsimp only
omegaend CLRS.Chapter26.SparseEKCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.SparseExecution.Support
The fixed sparse residual support
Positive-capacity arcs and their reverses contain every residual edge of every feasible flow. The executable input supplies those positive arcs as a list; its representation proof establishes completeness and absence of duplicates. Support preparation executes two bucket insertions per input arc. It does not search an implicit dense capacity matrix to discover the sparse input.
noncomputable sectionnamespace CLRS.Chapter26.SparseEKopen Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}def positiveArcs (G : FlowNetwork V) : Finset (V × V) :=
Finset.univ.filter (fun e => 0 < G.c e.1 e.2)def support (G : FlowNetwork V) : Finset (V × V) :=
positiveArcs G ∪ (positiveArcs G).image Prod.swap@[simp] theorem mem_support (u v : V) :
(u,v) ∈ support G ↔ 0 < G.c u v ∨ 0 < G.c v u := by
simp [support, positiveArcs]theorem support_card_le (G : FlowNetwork V) :
(support G).card ≤ 2 * (positiveArcs G).card := by
have hi := Finset.card_image_le (s := positiveArcs G) (f := Prod.swap)
have hu := Finset.card_union_le (positiveArcs G) ((positiveArcs G).image Prod.swap)
unfold support
omega
theorem residual_mem_support (φ : Flow V G) {u v : V} (h : φ.residualEdge u v) :
(u,v) ∈ support G := by
rw [mem_support]
by_contra hn
push Not at hn
have hc := φ.hcapacity v u
have hs := φ.hskew_symm u v
change 0 < G.c u v - φ.f u v at h
linarithA sparse-capacity input representation, not a premise about execution counts.
structure CapacityInput (G : FlowNetwork V) where
arcs : List (V × V)
nodup : arcs.Nodup
mem_iff : ∀ u v, (u,v) ∈ arcs ↔ 0 < G.c u v
theorem CapacityInput.length_eq (input : CapacityInput G) :
input.arcs.length = (positiveArcs G).card := by
have heq : input.arcs.toFinset = positiveArcs G := by
ext ⟨u,v⟩
simp [positiveArcs, input.mem_iff]
rw [← heq, List.toFinset_card_of_nodup input.nodup]def prepare : List (V × V) → SupportBuild V
| [] => ⟨SupportAdjacency.empty, 0⟩
| e :: es =>
let old := prepare es
⟨(old.adjacency.insertArc e).insertArc e.swap, old.work + 2⟩omit [Fintype V] in
theorem prepare_work (es : List (V × V)) : (prepare es).work = 2 * es.length := by
induction es with
| nil => rfl
| cons e es ih => simp [prepare, ih, Nat.mul_add, Nat.add_comm]omit [Fintype V] in
theorem prepare_mem (es : List (V × V)) (u v : V) :
v ∈ (prepare es).adjacency.bucket u ↔ (u,v) ∈ es ∨ (v,u) ∈ es := by
induction es with
| nil => simp [prepare]
| cons e es ih =>
rcases e with ⟨a,b⟩
simp [prepare, SupportAdjacency.mem_insertArc_bucket, ih]
tautotheorem CapacityInput.prepare_mem (input : CapacityInput G) (u v : V) :
v ∈ (prepare input.arcs).adjacency.bucket u ↔ (u,v) ∈ support G := by
simp [SparseEK.prepare_mem, input.mem_iff]omit [Fintype V] in
private theorem adjacency_ext {A B : SupportAdjacency V} (h : A.bucket = B.bucket) : A = B := by
cases A
cases B
cases h
rfl
theorem CapacityInput.prepare_storage (input : CapacityInput G) :
(prepare input.arcs).adjacency.storage = (support G).card := by
have heq : (prepare input.arcs).adjacency = (buildSupportAdjacency (support G)).adjacency := by
apply adjacency_ext
funext u
ext v
rw [input.prepare_mem, mem_buildSupportAdjacency]
rw [heq, buildSupportAdjacency_storage]theorem CapacityInput.covers (input : CapacityInput G) (φ : Flow V G) :
SupportsResidual (prepare input.arcs).adjacency φ := by
intro u v h
exact (input.prepare_mem u v).2 (residual_mem_support φ h)Isolated vertices are never dequeued: a reached non-source vertex is a support target.
theorem residualBFS_visited_subset (φ : Flow V G) :
(residualBFS φ).visited ⊆ insert G.s ((support G).image Prod.snd) := by
intro v hv
have hr := (residualBFS_visited_iff_reachable φ v).1 hv
induction hr with
| refl => simp
| @tail v w hprev hedge ih =>
exact mem_insert_of_mem (mem_image.mpr ⟨(v,w), residual_mem_support φ hedge, rfl⟩)Actual support BFS work has no ambient-vertex term, even with isolated vertices.
theorem bfs_work_le (input : CapacityInput G) (φ : Flow V G) :
(costedResidualBFS (prepare input.arcs).adjacency φ).work ≤
1 + 5 * (support G).card := by
let A := (prepare input.arcs).adjacency
have cover := input.covers φ
have hinitQueue : BFSQueueInv φ (bfsStateInit G.s).visited (bfsStateInit G.s).queue := by
intro v hv
simpa [BFSQueueInv, bfsStateInit] using hv
have hinitNodup : (bfsStateInit G.s).queue.Nodup := by simp [bfsStateInit]
have hw := costedBFSAux_work_eq A φ cover (Fintype.card V) (bfsStateInit G.s)
hinitQueue hinitNodup
rw [supportBFSWork_init] at hw
have hstate := costedResidualBFS_state A φ cover
have hqueue : (costedResidualBFS A φ).state.queue = [] := by
rw [hstate]; exact residualBFS_queue_empty φ
have hw' : (costedResidualBFS A φ).work =
(residualBFS φ).visited.card + 4 * ∑ u ∈ (residualBFS φ).visited, (A.bucket u).card := by
change (costedResidualBFS A φ).work + 0 =
supportBFSWork A (costedResidualBFS A φ).state.visited
(costedResidualBFS A φ).state.queue at hw
rw [Nat.add_zero, hstate] at hw
simpa [supportBFSWork, residualBFS_queue_empty] using hw
have hc := Finset.card_le_card (residualBFS_visited_subset φ)
have hci := Finset.card_insert_le G.s ((support G).image Prod.snd)
have him := Finset.card_image_le (s := support G) (f := Prod.snd)
have hsum := sum_bucket_card_le_storage A (residualBFS φ).visited
have hstorage : A.storage = (support G).card := input.prepare_storage
rw [hw']
omegaend CLRS.Chapter26.SparseEKCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.SparseExecution.Timeline
Sparse critical-edge counting for any shortest-path execution
The timeline records actual selected shortest paths and their resulting flows. Its step equation is instantiated by the counted BFS execution. No equality with the separate classical shortest-path chooser is required.
noncomputable sectionnamespace CLRS.Chapter26.SparseEKopen Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}structure Timeline (G : FlowNetwork V) where
flow : Nat → Flow V G
path : (i : Nat) → Option (ShortestAugmentingPath (flow i))
next : ∀ i, flow (i+1) = match path i with
| none => flow i
| some p => (flow i).augment p.pathnamespace Timelinevariable (T : Timeline G)def Critical (i : Nat) (u v : V) : Prop :=
∃ p, T.path i = some p ∧ p.path.isCritical u vdef Augments (i : Nat) : Prop := ∃ p, T.path i = some p
theorem next_some {i : Nat} {p : ShortestAugmentingPath (T.flow i)}
(hp : T.path i = some p) : T.flow (i+1) = (T.flow i).augment p.path := by
rw [T.next, hp]
theorem distance_step (i : Nat) (u : V) {d : Nat}
(hd : IsShortestDist (T.flow (i+1)) G.s u d) :
∃ d', IsShortestDist (T.flow i) G.s u d' ∧ d' ≤ d := by
rw [T.next] at hd
cases hp : T.path i with
| none => exact ⟨d, by simpa [hp] using hd, le_rfl⟩
| some p => exact p.exists_shortestDist_le_augment (by simpa [hp] using hd)theorem distance_mono {i j : Nat} (hij : i ≤ j) (u : V) {d : Nat}
(hd : IsShortestDist (T.flow j) G.s u d) :
∃ d', IsShortestDist (T.flow i) G.s u d' ∧ d' ≤ d := by
induction j, hij using Nat.le_induction generalizing d with
| base => exact ⟨d,hd,le_rfl⟩
| succ k hk ih =>
obtain ⟨dk,hdK,hle⟩ := T.distance_step k u hd
obtain ⟨di,hdi,hik⟩ := ih hdK
exact ⟨di,hdi,hik.trans hle⟩
theorem no_reverse_step (i : Nat) (u v : V)
(hno : ∀ p, T.path i = some p → (v,u) ∉ p.path.edges) :
(T.flow (i+1)).residualCapacity u v ≤ (T.flow i).residualCapacity u v := by
rw [T.next]
cases hp : T.path i with
| none => exact le_rfl
| some p =>
rw [Flow.augment_residualCapacity]
simp only [if_neg (hno p hp), add_zero]
split <;> linarith [p.path.bottleneck_pos]theorem no_reverse_interval {i j : Nat} (hij : i ≤ j) (u v : V)
(hno : ∀ k, i ≤ k → k < j → ∀ p, T.path k = some p → (v,u) ∉ p.path.edges) :
(T.flow j).residualCapacity u v ≤ (T.flow i).residualCapacity u v := by
induction j, hij using Nat.le_induction with
| base => exact le_rfl
| succ k hk ih =>
exact (T.no_reverse_step k u v (hno k hk (by omega))).trans
(ih (fun l hl hlk => hno l hl (by omega)))Recovery of a saturated arc requires a real reverse traversal in between.
theorem recovery {i j : Nat} (hij : i < j) {u v : V}
(hci : T.Critical i u v) (hcj : T.Critical j u v) :
∃ k, i < k ∧ k < j ∧ ∃ p, T.path k = some p ∧ (v,u) ∈ p.path.edges := by
obtain ⟨pi,hpi,hei,hzero⟩ := hci
obtain ⟨pj,hpj,hej,_⟩ := hcj
have hz : (T.flow (i+1)).residualCapacity u v = 0 := by
rw [T.next_some hpi]; exact hzero
have hpos : 0 < (T.flow j).residualCapacity u v :=
Flow.ResidualPath.residualEdge_of_mem_edges pj.path hej
by_contra hn
have hno : ∀ k, i+1 ≤ k → k < j → ∀ p, T.path k = some p → (v,u) ∉ p.path.edges := by
intro k hik hkj p hp hr
exact hn ⟨k, by omega, hkj, p, hp, hr⟩
have hle := T.no_reverse_interval (show i+1 ≤ j by omega) u v hno
linarith
theorem critical_growth {i j : Nat} (hij : i < j) {u v : V}
(hci : T.Critical i u v) (hcj : T.Critical j u v) :
∃ d d', IsShortestDist (T.flow i) G.s u d ∧
IsShortestDist (T.flow j) G.s u d' ∧ d < d' := by
obtain ⟨k,hik,hkj,p,hp,hrev⟩ := T.recovery hij hci hcj
obtain ⟨pi,hpi,hei,_⟩ := hci
obtain ⟨pj,hpj,hej,_⟩ := hcj
obtain ⟨di,dk,hdi,hdk,hgrow⟩ := critical_dist_increase_rev pi p hei hrev
(fun x d hd => T.distance_mono (by omega) x hd)
obtain ⟨dj,hdj,_⟩ := shortest_edge_dist pj hej
obtain ⟨dk',hdk',hle⟩ := T.distance_mono (by omega : k ≤ j) u hdj
have heq := hdk.unique hdk'
exact ⟨di,dj,hdi,hdj,by omega⟩theorem critical_dist {i : Nat} {u v : V} (hc : T.Critical i u v) :
∃ d, IsShortestDist (T.flow i) G.s u d ∧ d < Fintype.card V := by
obtain ⟨p,hp,he,_⟩ := hc
obtain ⟨d,hd,_⟩ := shortest_edge_dist p he
exact ⟨d,hd,hd.lt_card⟩theorem critical_support {i : Nat} {u v : V} (hc : T.Critical i u v) :
(u,v) ∈ support G := by
obtain ⟨p,hp,he,_⟩ := hc
exact residual_mem_support _ (Flow.ResidualPath.residualEdge_of_mem_edges p.path he)theorem exists_critical (i : Nat) (ha : T.Augments i) : ∃ u v, T.Critical i u v := by
obtain ⟨p,hp⟩ := ha
obtain ⟨u,v,hc⟩ := exists_critical_edge p.path
exact ⟨u,v,p,hp,hc⟩
theorem augmentation_count_bound (N : ℕ) :
((Finset.range N).filter (fun n => T.Augments n)).card ≤
(support G).card * Fintype.card V := by
let s : Finset ℕ :=
(Finset.range N).filter (fun n => T.Augments n)
let haug : ∀ x : {n : ℕ // n ∈ s}, T.Augments x.1 :=
fun x => (Finset.mem_filter.mp x.2).2
let pair : {n : ℕ // n ∈ s} → V × V := fun x =>
let h := T.exists_critical x.1 (haug x)
(Classical.choose h, Classical.choose (Classical.choose_spec h))
let hcrit : ∀ x : {n : ℕ // n ∈ s},
T.Critical x.1 (pair x).1 (pair x).2 :=
fun x =>
Classical.choose_spec
(Classical.choose_spec (T.exists_critical x.1 (haug x)))
let distOf : {n : ℕ // n ∈ s} → ℕ :=
fun x => Classical.choose (T.critical_dist (hcrit x))
let f : {n : ℕ // n ∈ s} → (V × V) × Fin (Fintype.card V) :=
fun x => (pair x, ⟨distOf x, (Classical.choose_spec (T.critical_dist (hcrit x))).2⟩)
have hinj : Set.InjOn f (↑(s.attach) : Set {n : ℕ // n ∈ s}) := by
intro x hx y hy hxy
apply Subtype.ext
by_contra hne
have hpair_eq : pair x = pair y := congrArg Prod.fst hxy
have hdist_eq : distOf x = distOf y :=
congrArg (fun z : (V × V) × Fin (Fintype.card V) => z.2.1) hxy
have hcy : T.Critical y.1 (pair x).1 (pair x).2 := by
simpa [hpair_eq] using hcrit y
have hlt_or : x.1 < y.1 ∨ y.1 < x.1 := by omega
rcases hlt_or with hxy_lt | hyx_lt
· rcases T.critical_growth hxy_lt (hcrit x) hcy with
⟨du, du', hdu, hdu', hgrow⟩
have hdx : distOf x = du :=
(Classical.choose_spec (T.critical_dist (hcrit x))).1.unique hdu
have hdy : distOf y = du' := by
have hd := (Classical.choose_spec (T.critical_dist (hcrit y))).1
exact hd.unique (by simpa [hpair_eq] using hdu')
omega
· rcases T.critical_growth hyx_lt hcy (hcrit x) with
⟨du, du', hdu, hdu', hgrow⟩
have hdy : distOf y = du := by
have hd := (Classical.choose_spec (T.critical_dist (hcrit y))).1
exact hd.unique (by simpa [hpair_eq] using hdu)
have hdx : distOf x = du' :=
(Classical.choose_spec (T.critical_dist (hcrit x))).1.unique hdu'
omega
have hsub : s.attach.image f ⊆ (support G).product
(Finset.univ : Finset (Fin (Fintype.card V))) := by
intro x hx
obtain ⟨y,hy,rfl⟩ := Finset.mem_image.mp hx
exact Finset.mem_product.mpr ⟨T.critical_support (hcrit y), Finset.mem_univ _⟩
have hcard : (s.attach.image f).card = s.attach.card :=
Finset.card_image_of_injOn hinj
calc
s.card = s.attach.card := Finset.card_attach.symm
_ = (s.attach.image f).card := hcard.symm
_ ≤ ((support G).product (Finset.univ : Finset (Fin (Fintype.card V)))).card :=
Finset.card_le_card hsub
_ = (support G).card * Fintype.card V := by simptheorem augmentation_count_sparse (N : Nat) :
((Finset.range N).filter (fun i => T.Augments i)).card ≤
2 * (positiveArcs G).card * Fintype.card V :=
(T.augmentation_count_bound N).trans (Nat.mul_le_mul_right _ (support_card_le G))
theorem all_steps_bound (N : Nat) (h : ∀ i < N, T.Augments i) :
N ≤ (support G).card * Fintype.card V := by
have hc := T.augmentation_count_bound N
have heq : (Finset.range N).filter T.Augments = Finset.range N := by
ext i
simp only [Finset.mem_filter, Finset.mem_range]
exact ⟨And.left, fun hi => ⟨hi,h i hi⟩⟩
simpa [heq] using hcend Timelineend CLRS.Chapter26.SparseEKCLRSLean.FourthEdition.Chapter_24.Section_24_2_Edmonds_Karp.SparseExecution.Update
Local counted flow updates
The recovered path is converted to consecutive arcs once. A counted scan finds its bottleneck, then two dictionary-cell updates are executed per arc. The resulting dictionary refines the legacy mathematical augmentation. Dictionary reads/writes and exact-real arithmetic are unit-cost abstract primitives, as in the existing support-BFS model; persistent-container evaluator time is excluded.
noncomputable sectionnamespace CLRS.Chapter26.SparseEKopen Finset Classicalvariable {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}def edgesWithCost : List V → List (V × V) × Nat
| [] => ([],0)
| [_] => ([],0)
| a :: b :: vs =>
let old := edgesWithCost (b :: vs)
((a,b) :: old.1, old.2+1)omit [Fintype V] [DecidableEq V] in
theorem edgesWithCost_spec (vs : List V) :
(edgesWithCost vs).1 = vs.consecutivePairs ∧
(edgesWithCost vs).2 = vs.length-1 := by
induction vs with
| nil => exact ⟨rfl,rfl⟩
| cons a vs ih =>
cases vs with
| nil => exact ⟨rfl,rfl⟩
| cons b vs => simp [edgesWithCost, List.consecutivePairs, ih]def scanCaps (φ : Flow V G) : List (V × V) → WithTop ℝ × Nat
| [] => (⊤,0)
| e :: es =>
let old := scanCaps φ es
(min (φ.residualCapacity e.1 e.2 : WithTop ℝ) old.1, old.2+4)@[simp] theorem scanCaps_work (φ : Flow V G) (es : List (V × V)) :
(scanCaps φ es).2 = 4*es.length := by
induction es with
| nil => rfl
| cons e es ih => simp [scanCaps, ih, Nat.mul_add, Nat.add_comm]theorem scanCaps_le (φ : Flow V G) (es : List (V × V)) (e : V × V) (he : e ∈ es) :
(scanCaps φ es).1 ≤ (φ.residualCapacity e.1 e.2 : WithTop ℝ) := by
induction es with
| nil => simp at he
| cons f es ih =>
rcases List.mem_cons.mp he with rfl | he
· exact min_le_left _ _
· exact (min_le_right _ _).trans (ih he)theorem le_scanCaps (φ : Flow V G) (es : List (V × V)) (x : WithTop ℝ)
(h : ∀ e ∈ es, x ≤ (φ.residualCapacity e.1 e.2 : WithTop ℝ)) :
x ≤ (scanCaps φ es).1 := by
induction es with
| nil => exact le_top
| cons e es ih =>
exact le_min (h e (by simp)) (ih (fun f hf => h f (by simp [hf])))
theorem scanCaps_eq_bottleneck (φ : Flow V G) (p : Flow.AugmentingPath φ) :
(scanCaps φ p.edges).1 = (p.bottleneck : WithTop ℝ) := by
apply le_antisymm
· have hm : p.bottleneck ∈ p.edges.toFinset.image
(fun e => φ.residualCapacity e.1 e.2) := by
unfold Flow.AugmentingPath.bottleneck
exact Finset.min'_mem _ _
obtain ⟨e,he,heq⟩ := Finset.mem_image.mp hm
rw [← heq]
exact scanCaps_le φ p.edges e (List.mem_toFinset.mp he)
· apply le_scanCaps
intro e he
exact_mod_cast p.bottleneck_le_residualCapacity hestructure MapRun (V : Type*) where
cells : (V × V) → ℝ
work : Natdef bump (old : MapRun V) (e : V × V) (delta : ℝ) : MapRun V :=
⟨Function.update old.cells e (old.cells e + delta),old.work+2⟩def pushPair (f : (V × V) → ℝ) (delta : ℝ) (e : V × V) : MapRun V :=
bump (bump ⟨f,0⟩ e delta) e.swap (-delta)omit [Fintype V] in
theorem bump_apply (old : MapRun V) (e x : V × V) (delta : ℝ) :
(bump old e delta).cells x = old.cells x + if x=e then delta else 0 := by
by_cases h : x=e <;> simp [bump, Function.update, h]omit [Fintype V] in
theorem pushPair_apply (f : (V × V) → ℝ) (delta : ℝ) (a b u v : V) :
(pushPair f delta (a,b)).cells (u,v) = f (u,v) + Flow.edgeDelta delta a b u v := by
simp only [pushPair, bump_apply, Prod.swap_prod_mk, Prod.mk.injEq, Flow.edgeDelta]
split_ifs <;> ringdef updateAll (f : (V × V) → ℝ) (delta : ℝ) : List (V × V) → MapRun V
| [] => ⟨f,0⟩
| e :: es =>
let first := pushPair f delta e
let rest := updateAll first.cells delta es
⟨rest.cells,first.work+rest.work⟩omit [Fintype V] in
@[simp] theorem updateAll_work (f : (V × V) → ℝ) (delta : ℝ) (es : List (V × V)) :
(updateAll f delta es).work = 4*es.length := by
induction es generalizing f with
| nil => rfl
| cons e es ih => simp [updateAll, pushPair, bump, ih, Nat.mul_add, Nat.add_comm]
omit [Fintype V] in
theorem updateAll_path (f : (V × V) → ℝ) (delta : ℝ) (vs : List V) (u v : V) :
(updateAll f delta vs.consecutivePairs).cells (u,v) = f (u,v) + Flow.pathDelta delta vs u v := by
induction vs generalizing f with
| nil => simp [List.consecutivePairs, updateAll, Flow.pathDelta]
| cons a vs ih =>
cases vs with
| nil => simp [List.consecutivePairs, updateAll, Flow.pathDelta]
| cons b vs =>
have he : (a :: b :: vs).consecutivePairs = (a,b) :: (b :: vs).consecutivePairs := rfl
rw [he]
simp only [updateAll, ih, pushPair_apply, Flow.pathDelta]
ringstructure FlowRun (G : FlowNetwork V) where
flow : Flow V G
work : Natprivate theorem flow_ext {φ ψ : Flow V G} (h : φ.f = ψ.f) : φ = ψ := by
cases φ
cases ψ
cases h
rflAll executable value fields come from the counted scans and local dictionary writes.
def augmentWithCost (φ : Flow V G) (p : Flow.AugmentingPath φ) : FlowRun G :=
let edges := edgesWithCost p.vertices
let bottle := scanCaps φ edges.1
let delta := bottle.1.untopD 0
let updated := updateAll (fun e => φ.f e.1 e.2) delta edges.1
have he : edges.1 = p.edges := (edgesWithCost_spec p.vertices).1
have hd : delta = p.bottleneck := by
dsimp [delta,bottle]
rw [he,scanCaps_eq_bottleneck]
rfl
have hf : ∀ u v, updated.cells (u,v) = (φ.augment p).f u v := by
intro u v
dsimp [updated]
rw [he,hd]
exact updateAll_path _ _ p.vertices u v
let result : Flow V G :=
{ f := fun u v => updated.cells (u,v)
hcapacity := by intro u v; rw [hf]; exact (φ.augment p).hcapacity u v
hskew_symm := by intro u v; rw [hf,hf]; exact (φ.augment p).hskew_symm u v
hconservation := by intro u hu ht; simp only [hf]; exact (φ.augment p).hconservation u hu ht }
⟨result, edges.2+bottle.2+updated.work+1⟩
theorem augmentWithCost_refines (φ : Flow V G) (p : Flow.AugmentingPath φ) :
(augmentWithCost φ p).flow = φ.augment p := by
apply flow_ext
funext u v
simp only [augmentWithCost]
rw [(edgesWithCost_spec p.vertices).1]
change (updateAll (fun e => φ.f e.1 e.2) ((scanCaps φ p.edges).1.untopD 0) p.edges).cells (u,v) = _
rw [scanCaps_eq_bottleneck]
exact updateAll_path _ _ p.vertices u vtheorem augmentWithCost_work (φ : Flow V G) (p : Flow.AugmentingPath φ) :
(augmentWithCost φ p).work = 9*p.edges.length+1 := by
simp only [augmentWithCost, (edgesWithCost_spec p.vertices).1,
(edgesWithCost_spec p.vertices).2, scanCaps_work,updateAll_work,Flow.ResidualPath.edges_length]
have hlen : p.vertices.consecutivePairs.length = p.vertices.length-1 := p.edges_length
omega
theorem augmentWithCost_work_le (φ : Flow V G) (p : ShortestAugmentingPath φ) :
(augmentWithCost φ p.path).work ≤ 9*(support G).card+1 := by
rw [augmentWithCost_work]
have h := shortest_length_support φ p
omegaend CLRS.Chapter26.SparseEKCLRSLean.FourthEdition.Chapter_24.Section_24_6_MaxFlow_MinCut
Theorem 24.6. Max-Flow Min-Cut
This file proves the complete Max-Flow Min-Cut equivalence (CLRS Theorem 24.6). For a feasible flow, the following conditions are equivalent:
-
the flow is maximal;
-
the residual network has no source-to-sink augmenting path;
-
some source-to-sink cut has capacity equal to the flow value.
Main results:
-
Flow.eq_cutCapacity_implies_maximal: equality with one cut capacity certifies maximality. -
Flow.maximal_iff_noAugmentingPath: maximality is equivalent to the absence of an augmenting path. -
Flow.maximal_iff_exists_cut_value_eq: maximality is equivalent to the existence of a cut whose capacity equals the flow value.
Current gaps: none for the mathematical Max-Flow Min-Cut equivalence. Executable Ford--Fulkerson and Edmonds--Karp algorithms are developed separately.
set_option autoImplicit truenamespace CLRSnamespace Chapter26open Finset Classical
Every consecutive pair from a List.IsChain chain satisfies the relation.
lemma forall_zip_edges_of_isChain {V : Type*} {r : V → V → Prop} {a : V} {l : List V}
(h : List.IsChain r (a :: l)) : ∀ (u v : V), (u, v) ∈ List.zip (a :: l) l → r u v := by
have h_eq : l = [] ∨ ∃ (b : V) (l' : List V), l = b :: l' := by
cases l
· left; rfl
· right; refine ⟨_, _, rfl⟩
rcases h_eq with (hl | ⟨b, l', hl⟩)
· subst hl; simp
· subst hl
have h_cons_cons := (List.isChain_cons_cons (a := a) (b := b) (l := l')).mp h
rcases h_cons_cons with ⟨h_rel, h_chain⟩
intro u v h_mem
have h_zip : List.zip (a :: b :: l') (b :: l') = (a, b) :: List.zip (b :: l') l' := by simp
simp [h_zip] at h_mem
rcases h_mem with (⟨rfl, rfl⟩ | h_rest)
· exact h_rel
· exact forall_zip_edges_of_isChain h_chain u v h_restIf the value of a flow equals the capacity of some cut, the flow is maximal. This is the easy direction of Theorem 24.6.
theorem Flow.eq_cutCapacity_implies_maximal {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) (S : Finset V) (hs : G.s ∈ S) (ht : G.t ∉ S)
(h_eq : φ.value = Finset.sum S (fun u => Finset.sum (Sᶜ) (fun v => G.c u v))) :
Flow.isMaximal φ := by
intro ψ
have hψ_le : ψ.value ≤ Finset.sum S (fun u => Finset.sum (Sᶜ) (fun v => G.c u v)) :=
Flow.value_le_cut_capacity φ ψ S hs ht
linarithA feasible flow is maximal exactly when its residual network contains no source-to-sink augmenting path.
theorem Flow.maximal_iff_noAugmentingPath {V : Type*} [Fintype V] [DecidableEq V]
{G : FlowNetwork V} (φ : Flow V G) :
φ.isMaximal ↔ ¬φ.hasAugmentingPath := by
constructor
· intro hmax hpath
exact φ.not_maximal_of_hasAugmentingPath hpath hmax
· exact φ.maximal_of_noAugmentingPathMax-Flow Min-Cut Theorem (CLRS Theorem 24.6). A feasible flow is maximal exactly when some cut separating source and sink has capacity equal to the flow value.
theorem Flow.maximal_iff_exists_cut_value_eq {V : Type*} [Fintype V]
[DecidableEq V] {G : FlowNetwork V} (φ : Flow V G) :
φ.isMaximal ↔
∃ S : Finset V, G.s ∈ S ∧ G.t ∉ S ∧
φ.value = Finset.sum S (fun u => Finset.sum (Sᶜ) (fun v => G.c u v)) := by
constructor
· intro hmax
exact φ.exists_cut_value_eq_of_noAugmentingPath
((φ.maximal_iff_noAugmentingPath).mp hmax)
· rintro ⟨S, hs, ht, hvalue⟩
exact φ.eq_cutCapacity_implies_maximal S hs ht hvalueend Chapter26end CLRS