Imports
import Mathlib
import CLRSLean.Chapter_26.Section_26_3_Bipartite_Matching
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S1_Matching_API
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S2_Alternating_Paths
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S3_Simple_Paths
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S4_Matching_Flow
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S5_Residual_Translation
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S6_Berge_Flow_Method
import CLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution25.1. Maximum bipartite matching revisited
This section develops the native fourth-edition matching interface of CLRS
§25.1 on top of the flow reduction of §26.3
(CLRS.Chapter26.maxMatching_eq_maxFlow_value). The flow development
proves that a maximum matching can be computed; this section supplies the
combinatorial characterisation of when a matching is maximum: Berge's
augmenting-path lemma.
Main results:
-
Matching.matchedLeft/Matching.matchedRight: matched endpoint sets -
Matching.IsMaximum: a matching no other matching exceeds in size -
IsAugmentingPath: alternating paths with unmatched endpoints -
Matching.exists_augment: an augmenting path yields a matching that is larger by one -
augmentingPath_of_hasAugmentingPath: a residual augmenting path in the §26.3 flow network induces an augmenting path in the graph -
berge_maximum_iff_no_augmentingPath(Berge's lemma): a matching is maximum iff it admits no augmenting path -
flowMethod_finds_maximum_matching: a maximum matching exists and is certified by the flow method -
flowMethod_finds_maximum_matching_with_bfs: the BFS-selected unit-capacity run returns a maximum matching with at most|V|augmentations -
flowMethod_finds_maximum_matching_with_attached_cost: the support-indexed run returns a maximum matching with same-executionO(V_f E_f)work
The legacy Chapter 24 residual BFS remains the semantic reference whose neighbor operation enumerates the finite vertex universe. The attached-cost execution separately builds finite support buckets, proves exact BFS-state erasure, recovers the same parent chain, executes and charges the graph-path projection and matching updates, and proves the textbook product bound.
Notation conventions used in this section:
-
G: bipartite graph (reused from §26.3) -
M: matching (reused from §26.3) -
p: vertex list representing an alternating path
Implementation details
The section is split into the following sub-modules:
Definitions and proofs
CLRSLean.FourthEdition.Chapter_24.Section_24_3_Bipartite_Matching
24.3. Maximum Bipartite Matching
This file formalizes the bipartite-to-flow-network reduction of CLRS §24.3 and proves Theorem 24.12: the maximum matching size equals the maximum flow value in the unit-capacity network. It constructs the feasible flow induced by every matching, recovers a matching from every integral flow, iterates augmentation from the zero flow to obtain an integral maximum flow, and combines the two directions.
Main results:
-
BipartiteGraph,Matching, andMatching.size -
capFuncandtoFlowNetwork -
matchingFlowFunandmatchingFlowFunSummand -
matchingToFlowandmatchingToFlow_value: the feasible flow induced by a matching has value|M| -
Flow.IsIntegral,matchingOfIntegralFlow, andmatchingOfIntegralFlow_size: an integral flow of valuevyields a matching of sizev -
maxMatching_eq_maxFlow_value(Theorem 24.12): the maximum matching size equals the value of a maximal flow
namespace CLRSnamespace Chapter26open Finset Classical
A bipartite graph with left partition L, right partition R, and
edges E that only go from L to R. (CLRS §24.3.)
structure BipartiteGraph (V : Type*) [Fintype V] [DecidableEq V] where
L : Finset V
R : Finset V
h_disjoint : L ∩ R = ∅
h_cover : L ∪ R = Finset.univ
E : Finset (V × V)
hE_subset : ∀ e ∈ E, e.1 ∈ L ∧ e.2 ∈ RA matching in a bipartite graph: a set of edges with no shared endpoints.
structure Matching (V : Type*) [Fintype V] [DecidableEq V] (G : BipartiteGraph V) where
edges : Finset (V × V)
h_subset : edges ⊆ G.E
h_unique_left : ∀ (l r₁ r₂ : V), (l, r₁) ∈ edges → (l, r₂) ∈ edges → r₁ = r₂
h_unique_right : ∀ (l₁ l₂ r : V), (l₁, r) ∈ edges → (l₂, r) ∈ edges → l₁ = l₂The size (cardinality) of a matching.
def Matching.size {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : ℕ := M.edges.cardlemma Matching.left_mem_L {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) {l r : V} (h : (l, r) ∈ M.edges) : l ∈ G.L := by
have hE : (l, r) ∈ G.E := M.h_subset h; exact (G.hE_subset (l, r) hE).1lemma Matching.right_mem_R {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) {l r : V} (h : (l, r) ∈ M.edges) : r ∈ G.R := by
have hE : (l, r) ∈ G.E := M.h_subset h; exact (G.hE_subset (l, r) hE).2
Capacity function defined as a standalone def so simp can use it.
def capFunc (V : Type*) [Fintype V] [DecidableEq V] (G : BipartiteGraph V) (u v : V ⊕ Bool) : ℝ :=
match u, v with
| Sum.inr true, Sum.inl l' => if l' ∈ G.L then (1 : ℝ) else 0
| Sum.inl l', Sum.inl r' => if (l', r') ∈ G.E then (1 : ℝ) else 0
| Sum.inl r', Sum.inr false => if r' ∈ G.R then (1 : ℝ) else 0
| _, _ => 0The flow network constructed from a bipartite graph (CLRS eq. (24.11)).
def toFlowNetwork (V : Type*) [Fintype V] [DecidableEq V] (G : BipartiteGraph V) :
FlowNetwork (V ⊕ Bool) :=
{ s := Sum.inr true
, t := Sum.inr false
, c := capFunc V G
, hc_nonneg := λ u v =>
have h_nonneg : 0 ≤ capFunc V G u v := by
unfold capFunc
cases u with
| inl a =>
cases v with
| inl b => simp; split_ifs <;> norm_num
| inr b => cases b <;> simp <;> try (split_ifs <;> norm_num)
| inr a =>
cases a with
| true =>
cases v with
| inl b => simp; split_ifs <;> norm_num
| inr b => cases b <;> simp <;> try (split_ifs <;> norm_num)
| false =>
cases v with
| inl b => norm_num
| inr b => cases b <;> simp <;> try (split_ifs <;> norm_num)
h_nonneg
, hc_self := λ u =>
by
unfold capFunc
match u with
| Sum.inl v =>
by_cases h : (v, v) ∈ G.E
· have hvL : v ∈ G.L := (G.hE_subset (v, v) h).1
have hvR : v ∈ G.R := (G.hE_subset (v, v) h).2
have : v ∈ G.L ∩ G.R := Finset.mem_inter.mpr ⟨hvL, hvR⟩
rw [G.h_disjoint] at this; simp at this
· simp [h]
| Sum.inr _ => simp
, hs_ne_t := by simp
}The flow induced by a matching
The contribution of a single matched edge e to the matching-induced flow
on pair (u,v) (CLRS eq. (24.11)): +1 along s → e.1, e.1 → e.2,
e.2 → t, −1 on the reverse edges, and 0 elsewhere.
The (e.1, e.2) direction is written as the sum of two indicators so that the
forward and reverse contributions cancel on degenerate pairs, making the
summand skew-symmetric for every e.
def matchingFlowFunSummand {V : Type*} [DecidableEq V] (e : V × V) (u v : V ⊕ Bool) : ℝ :=
match u, v with
| Sum.inr true, Sum.inl l => if e.1 = l then (1 : ℝ) else 0
| Sum.inl a, Sum.inl b =>
(if e = (a, b) then (1 : ℝ) else 0) + (if e = (b, a) then (-1 : ℝ) else 0)
| Sum.inl r, Sum.inr false => if e.2 = r then (1 : ℝ) else 0
| Sum.inl l, Sum.inr true => if e.1 = l then (-1 : ℝ) else 0
| Sum.inr false, Sum.inl r => if e.2 = r then (-1 : ℝ) else 0
| _, _ => 0
The flow induced by a matching M in the constructed flow network.
def matchingFlowFun {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (u v : V ⊕ Bool) : ℝ :=
Finset.sum M.edges (fun (e : V × V) => matchingFlowFunSummand e u v)A matching has at most one edge leaving a given left vertex.
lemma count_left_le_one {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (l : V) :
Finset.sum M.edges (fun (e : V × V) => if e.1 = l then (1 : ℝ) else 0) ≤ 1 := by
have hcard : (M.edges.filter (fun e : V × V => e.1 = l)).card ≤ 1 := by
refine Finset.card_le_one.mpr ?_
intro e1 he1 e2 he2
have he1' : e1 ∈ M.edges := (Finset.mem_filter.mp he1).1
have he2' : e2 ∈ M.edges := (Finset.mem_filter.mp he2).1
have h1 : e1.1 = e2.1 := (Finset.mem_filter.mp he1).2.trans (Finset.mem_filter.mp he2).2.symm
have h2 : e1.2 = e2.2 := M.h_unique_left e1.1 e1.2 e2.2 he1' (by simpa [h1] using he2')
exact Prod.ext h1 h2
have hsum : Finset.sum M.edges (fun (e : V × V) => if e.1 = l then (1 : ℝ) else 0)
= ((M.edges.filter (fun e : V × V => e.1 = l)).card : ℝ) := by
rw [← Finset.sum_filter]
simp
rw [hsum]
exact_mod_cast hcardA matching has at most one edge entering a given right vertex.
lemma count_right_le_one {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (r : V) :
Finset.sum M.edges (fun (e : V × V) => if e.2 = r then (1 : ℝ) else 0) ≤ 1 := by
have hcard : (M.edges.filter (fun e : V × V => e.2 = r)).card ≤ 1 := by
refine Finset.card_le_one.mpr ?_
intro e1 he1 e2 he2
have he1' : e1 ∈ M.edges := (Finset.mem_filter.mp he1).1
have he2' : e2 ∈ M.edges := (Finset.mem_filter.mp he2).1
have h1 : e1.2 = e2.2 := (Finset.mem_filter.mp he1).2.trans (Finset.mem_filter.mp he2).2.symm
have h2 : e1.1 = e2.1 := M.h_unique_right e1.1 e2.1 e1.2 he1' (by simpa [h1] using he2')
exact Prod.ext h2 h1
have hsum : Finset.sum M.edges (fun (e : V × V) => if e.2 = r then (1 : ℝ) else 0)
= ((M.edges.filter (fun e : V × V => e.2 = r)).card : ℝ) := by
rw [← Finset.sum_filter]
simp
rw [hsum]
exact_mod_cast hcard
The single-edge summand is skew-symmetric: its value on (u,v) is the
negation of its value on (v,u).
lemma matchingFlowFunSummand_skew {V : Type*} [DecidableEq V] (e : V × V) (u v : V ⊕ Bool) :
matchingFlowFunSummand e u v = - matchingFlowFunSummand e v u := by
unfold matchingFlowFunSummand
cases u with
| inl a =>
cases v with
| inl b =>
by_cases h1 : e = (a, b)
· by_cases h2 : e = (b, a)
· have hab : a = b := by
exact (congrArg Prod.fst h1).symm.trans (congrArg Prod.fst h2)
simp [h1, hab]
· have hab_ne : a ≠ b := by
intro hab
apply h2
simp [h1, hab]
simp [h1, hab_ne]
· by_cases h2 : e = (b, a)
· have hab_ne : a ≠ b := by
intro hab
apply h1
simp [h2, hab]
simp [h2, hab_ne]
· simp [h1, h2]
| inr b =>
cases b with
| true => by_cases h : e.1 = a <;> simp [h]
| false => by_cases h : e.2 = a <;> simp [h]
| inr b =>
cases b with
| true =>
cases v with
| inl l => by_cases h : e.1 = l <;> simp [h]
| inr b' => cases b' <;> simp
| false =>
cases v with
| inl r => by_cases h : e.2 = r <;> simp [h]
| inr b' => cases b' <;> simpThe flow induced by a matching is skew-symmetric.
lemma matchingFlowFun_skew_symm {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (u v : V ⊕ Bool) : matchingFlowFun M u v = - matchingFlowFun M v u := by
unfold matchingFlowFun
rw [← Finset.sum_neg_distrib]
refine Finset.sum_congr rfl (fun e _ => ?_)
exact matchingFlowFunSummand_skew e u v
For a fixed edge e, summing the (inl a, inl b) summand over all b
counts how many endpoints of e equal a.
lemma matchingFlowFunSummand_inl_inl_sum {V : Type*} [Fintype V] [DecidableEq V]
(e : V × V) (a : V) :
(∑ b : V, matchingFlowFunSummand e (Sum.inl a) (Sum.inl b)) =
(if e.1 = a then (1 : ℝ) else 0) - (if e.2 = a then (1 : ℝ) else 0) := by
have hS1 : (∑ b : V, if e = (a, b) then (1 : ℝ) else 0) = if e.1 = a then (1 : ℝ) else 0 := by
by_cases h : e.1 = a
· calc
(∑ b : V, if e = (a, b) then (1 : ℝ) else 0) = if e = (a, e.2) then (1 : ℝ) else 0 := by
refine Finset.sum_eq_single e.2 ?_ ?_
· intro b _ hb
have hNe : e ≠ (a, b) := by
intro hEq
exact hb (congrArg Prod.snd hEq).symm
simp [hNe]
· simp
_ = if e.1 = a then 1 else 0 := by
have hEq : e = (a, e.2) := Prod.ext h rfl
rw [hEq]
simp
· have hsum : (∑ b : V, if e = (a, b) then (1 : ℝ) else 0) = 0 := by
refine Finset.sum_eq_zero (fun b _ => ?_)
have hNe : e ≠ (a, b) := by
intro hEq
exact h (congrArg Prod.fst hEq)
simp [hNe]
simpa [h] using hsum
have hS2 : (∑ b : V, if e = (b, a) then (-1 : ℝ) else 0) = if e.2 = a then (-1 : ℝ) else 0 := by
by_cases h : e.2 = a
· calc
(∑ b : V, if e = (b, a) then (-1 : ℝ) else 0) = if e = (e.1, a) then (-1 : ℝ) else 0 := by
refine Finset.sum_eq_single e.1 ?_ ?_
· intro b _ hb
have hNe : e ≠ (b, a) := by
intro hEq
exact hb (congrArg Prod.fst hEq).symm
simp [hNe]
· simp
_ = if e.2 = a then -1 else 0 := by
have hEq : e = (e.1, a) := Prod.ext rfl h
rw [hEq]
simp
· have hsum : (∑ b : V, if e = (b, a) then (-1 : ℝ) else 0) = 0 := by
refine Finset.sum_eq_zero (fun b _ => ?_)
have hNe : e ≠ (b, a) := by
intro hEq
exact h (congrArg Prod.snd hEq)
simp [hNe]
simpa [h] using hsum
calc
(∑ b : V, matchingFlowFunSummand e (Sum.inl a) (Sum.inl b))
= (∑ b : V, ((if e = (a, b) then (1 : ℝ) else 0) + (if e = (b, a) then (-1 : ℝ) else 0))) := by
rfl
_ = (∑ b : V, if e = (a, b) then (1 : ℝ) else 0)
+ (∑ b : V, if e = (b, a) then (-1 : ℝ) else 0) := by
rw [Finset.sum_add_distrib]
_ = (if e.1 = a then (1 : ℝ) else 0) + (if e.2 = a then (-1 : ℝ) else 0) := by
rw [hS1, hS2]
_ = (if e.1 = a then (1 : ℝ) else 0) - (if e.2 = a then (1 : ℝ) else 0) := by
by_cases h1 : e.1 = a <;> by_cases h2 : e.2 = a <;> simp [h1, h2]The flow induced by a matching satisfies flow conservation at every non-source non-sink vertex.
lemma matchingFlowFun_conservation {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (M : Matching V G) (a : V) :
(∑ v : V ⊕ Bool, matchingFlowFun M (Sum.inl a) v) = 0 := by
have h1 : (∑ b : V, matchingFlowFun M (Sum.inl a) (Sum.inl b)) =
Finset.sum M.edges (fun (e : V × V) =>
(if e.1 = a then (1 : ℝ) else 0) - (if e.2 = a then (1 : ℝ) else 0)) := by
unfold matchingFlowFun
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun e _ => ?_)
exact matchingFlowFunSummand_inl_inl_sum e a
have h2 : matchingFlowFun M (Sum.inl a) (Sum.inr false) =
Finset.sum M.edges (fun (e : V × V) => if e.2 = a then (1 : ℝ) else 0) := by
unfold matchingFlowFun
refine Finset.sum_congr rfl (fun e _ => ?_)
rfl
have h3 : matchingFlowFun M (Sum.inl a) (Sum.inr true) =
-(Finset.sum M.edges (fun (e : V × V) => if e.1 = a then (1 : ℝ) else 0)) := by
unfold matchingFlowFun
rw [← Finset.sum_neg_distrib]
refine Finset.sum_congr rfl (fun e _ => ?_)
dsimp [matchingFlowFunSummand]
by_cases h : e.1 = a <;> simp [h]
calc
(∑ v : V ⊕ Bool, matchingFlowFun M (Sum.inl a) v)
= (∑ b : V, matchingFlowFun M (Sum.inl a) (Sum.inl b))
+ (matchingFlowFun M (Sum.inl a) (Sum.inr false) + matchingFlowFun M (Sum.inl a) (Sum.inr true)) := by
rw [← Finset.univ_disjSum_univ (α := V) (β := Bool)]
rw [Finset.sum_disjSum (Finset.univ : Finset V) (Finset.univ : Finset Bool)
(fun v : V ⊕ Bool => matchingFlowFun M (Sum.inl a) v)]
rw [Fintype.univ_bool]
rw [Finset.sum_pair (by decide : true ≠ false)]
ring
_ = 0 := by
rw [h1, h2, h3]
rw [Finset.sum_sub_distrib]
ring
The flow induced by a matching satisfies the capacity constraint
f(u,v) ≤ c(u,v).
lemma matchingFlowFun_capacity {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (u v : V ⊕ Bool) : matchingFlowFun M u v ≤ capFunc V G u v := by
cases u with
| inl a =>
cases v with
| inr b =>
cases b with
| true =>
have hflow : matchingFlowFun M (Sum.inl a) (Sum.inr true) ≤ 0 := by
unfold matchingFlowFun
exact Finset.sum_nonpos (fun e he => by
dsimp [matchingFlowFunSummand]
by_cases h : e.1 = a <;> simp [h])
simpa [capFunc] using hflow
| false =>
by_cases hR : a ∈ G.R
· have hflow : matchingFlowFun M (Sum.inl a) (Sum.inr false) ≤ 1 := by
have hsum : matchingFlowFun M (Sum.inl a) (Sum.inr false) =
Finset.sum M.edges (fun (e : V × V) => if e.2 = a then (1 : ℝ) else 0) := by
unfold matchingFlowFun
refine Finset.sum_congr rfl (fun e _ => ?_)
rfl
rw [hsum]
exact count_right_le_one M a
simpa [capFunc, hR] using hflow
· have hflow : matchingFlowFun M (Sum.inl a) (Sum.inr false) ≤ 0 := by
unfold matchingFlowFun
exact Finset.sum_nonpos (fun e he => by
have hNe : e.2 ≠ a := by
intro hEq
exact hR (by simpa [hEq] using M.right_mem_R he)
dsimp [matchingFlowFunSummand]
simp [hNe])
simpa [capFunc, hR] using hflow
| inl b =>
by_cases hE : (a, b) ∈ G.E
· have hflow : matchingFlowFun M (Sum.inl a) (Sum.inl b) ≤ 1 := by
have hsum_le : Finset.sum M.edges (fun (e : V × V) => if e = (a, b) then (1 : ℝ) else 0) ≤ 1 := by
rw [Finset.sum_ite_eq' M.edges (a, b) (fun _ => (1 : ℝ))]
by_cases h : (a, b) ∈ M.edges <;> simp [h]
have hflow_le : matchingFlowFun M (Sum.inl a) (Sum.inl b) ≤
Finset.sum M.edges (fun (e : V × V) => if e = (a, b) then (1 : ℝ) else 0) := by
unfold matchingFlowFun
exact Finset.sum_le_sum (fun e he => by
dsimp [matchingFlowFunSummand]
by_cases h1 : e = (a, b)
· by_cases h2 : e = (b, a)
· have hab : a = b := by
exact (congrArg Prod.fst h1).symm.trans (congrArg Prod.fst h2)
simp [h1, hab]
· have hab_ne : a ≠ b := by
intro hab
apply h2
simp [h1, hab]
simp [h1, hab_ne]
· by_cases h2 : e = (b, a)
· have hab_ne : a ≠ b := by
intro hab
apply h1
simp [h2, hab]
simp [h2, hab_ne]
· simp [h1, h2])
linarith
simpa [capFunc, hE] using hflow
· have hflow : matchingFlowFun M (Sum.inl a) (Sum.inl b) ≤ 0 := by
unfold matchingFlowFun
exact Finset.sum_nonpos (fun e he => by
have hNe : e ≠ (a, b) := by
intro hEq
exact hE (by simpa [hEq] using M.h_subset he)
dsimp [matchingFlowFunSummand]
by_cases h2 : e = (b, a)
· have hab_ne : a ≠ b := by
intro hab
exact hNe (by simp [h2, hab])
simp [h2, hab_ne]
· simp [hNe, h2])
simpa [capFunc, hE] using hflow
| inr b =>
cases b with
| true =>
cases v with
| inr b' => cases b' <;> dsimp [matchingFlowFun, matchingFlowFunSummand] <;> simp [capFunc]
| inl l =>
by_cases hL : l ∈ G.L
· have hflow : matchingFlowFun M (Sum.inr true) (Sum.inl l) ≤ 1 := by
have hsum : matchingFlowFun M (Sum.inr true) (Sum.inl l) =
Finset.sum M.edges (fun (e : V × V) => if e.1 = l then (1 : ℝ) else 0) := by
unfold matchingFlowFun
refine Finset.sum_congr rfl (fun e _ => ?_)
rfl
rw [hsum]
exact count_left_le_one M l
simpa [capFunc, hL] using hflow
· have hflow : matchingFlowFun M (Sum.inr true) (Sum.inl l) ≤ 0 := by
unfold matchingFlowFun
exact Finset.sum_nonpos (fun e he => by
have hNe : e.1 ≠ l := by
intro hEq
exact hL (by simpa [hEq] using M.left_mem_L he)
dsimp [matchingFlowFunSummand]
simp [hNe])
simpa [capFunc, hL] using hflow
| false =>
cases v with
| inl r =>
have hflow : matchingFlowFun M (Sum.inr false) (Sum.inl r) ≤ 0 := by
unfold matchingFlowFun
exact Finset.sum_nonpos (fun e he => by
dsimp [matchingFlowFunSummand]
by_cases h : e.2 = r <;> simp [h])
simpa [capFunc] using hflow
| inr b' => cases b' <;> dsimp [matchingFlowFun, matchingFlowFunSummand] <;> simp [capFunc]
The feasible flow induced by a matching (CLRS §24.3). The flow sends one
unit along s → l, l → r, r → t for every matched edge (l, r), with
skew-symmetric reverse contributions.
noncomputable def matchingToFlow {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : Flow (V ⊕ Bool) (toFlowNetwork V G) :=
{ f := matchingFlowFun M
, hcapacity := matchingFlowFun_capacity M
, hskew_symm := matchingFlowFun_skew_symm M
, hconservation := by
intro u hu hs
cases u with
| inl a => exact matchingFlowFun_conservation M a
| inr b =>
cases b with
| true => simp [toFlowNetwork] at hu
| false => simp [toFlowNetwork] at hs
}The total flow out of the source equals the number of matched edges.
lemma matchingFlowFun_value_sum {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) :
Finset.sum (Finset.univ : Finset (V ⊕ Bool)) (fun v => matchingFlowFun M (Sum.inr true) v)
= (M.size : ℝ) := by
calc
Finset.sum (Finset.univ : Finset (V ⊕ Bool)) (fun v => matchingFlowFun M (Sum.inr true) v)
= Finset.sum (Finset.univ : Finset (V ⊕ Bool)) (fun v =>
Finset.sum M.edges (fun (e : V × V) =>
match v with
| Sum.inl l => if e.1 = l then (1 : ℝ) else 0
| Sum.inr _ => 0)) := by
refine Finset.sum_congr rfl (fun v hv => ?_)
unfold matchingFlowFun
cases v with
| inl l => rfl
| inr b => cases b <;> rfl
_ = Finset.sum M.edges (fun (e : V × V) =>
Finset.sum (Finset.univ : Finset (V ⊕ Bool)) (fun v =>
match v with
| Sum.inl l => if e.1 = l then (1 : ℝ) else 0
| Sum.inr _ => 0)) := by
rw [Finset.sum_comm]
_ = Finset.sum M.edges (fun (e : V × V) => (1 : ℝ)) := by
refine Finset.sum_congr rfl (fun e _ => ?_)
simp
_ = (M.size : ℝ) := by
simp [Matching.size]
Theorem (matching-flow value). The flow induced by a matching M has
value equal to |M| (CLRS Theorem 24.12, value direction).
theorem matchingToFlow_value {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : (matchingToFlow M).value = (M.size : ℝ) := by
simp [Flow.value, matchingToFlow, toFlowNetwork, matchingFlowFun_value_sum M]Integral flows and the converse construction
An integral flow takes only integer values on every edge. Values may be
negative (reverse flow); the {0,1} recovery uses the capacity bounds to
force nonnegativity on the relevant pairs.
def Flow.IsIntegral {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : Prop :=
∀ u v, ∃ n : ℤ, φ.f u v = (n : ℝ)
A real in [0,1] that is an integer is 0 or 1.
lemma integral_of_unit_range {x : ℝ} (h01 : 0 ≤ x ∧ x ≤ 1) (hint : ∃ n : ℤ, x = (n : ℝ)) :
x = 0 ∨ x = 1 := by
rcases hint with ⟨n, hn⟩
have hn_ge : 0 ≤ n := by
have hx_ge : 0 ≤ x := h01.1
rw [hn] at hx_ge
exact_mod_cast hx_ge
have hn_le : n ≤ 1 := by
have hx_le : x ≤ 1 := h01.2
rw [hn] at hx_le
exact_mod_cast hx_le
have hn_eq : n = 0 ∨ n = 1 := by omega
rcases hn_eq with h | h <;> simp [hn, h]
A vertex in R is not in L (the partitions are disjoint).
lemma BipartiteGraph.not_mem_L_of_mem_R {V : Type*} [Fintype V] [DecidableEq V]
(G : BipartiteGraph V) {v : V} (h : v ∈ G.R) : v ∉ G.L := by
intro hL
have : v ∈ G.L ∩ G.R := Finset.mem_inter.mpr ⟨hL, h⟩
rw [G.h_disjoint] at this
simp at this
A vertex in L is not in R (the partitions are disjoint).
lemma BipartiteGraph.not_mem_R_of_mem_L {V : Type*} [Fintype V] [DecidableEq V]
(G : BipartiteGraph V) {v : V} (h : v ∈ G.L) : v ∉ G.R := by
intro hR
have : v ∈ G.L ∩ G.R := Finset.mem_inter.mpr ⟨h, hR⟩
rw [G.h_disjoint] at this
simp at this
In the unit-capacity matching network, the flow on every L→R pair lies
in [0, 1], and is zero when the edge is absent. The reverse capacity is
zero because the graph has no anti-parallel edges: (r, l) ∈ E would put
l in both partitions.
lemma matchingFlow_lr_bounds {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (l : V) (hl : l ∈ G.L) (r : V) :
0 ≤ φ.f (Sum.inl l) (Sum.inl r) ∧
φ.f (Sum.inl l) (Sum.inl r) ≤ (if (l, r) ∈ G.E then (1 : ℝ) else 0) := by
have hrev : (toFlowNetwork V G).c (Sum.inl r) (Sum.inl l) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : (r, l) ∈ G.E
· exact False.elim (G.not_mem_R_of_mem_L hl (G.hE_subset (r, l) h).2)
· simp [h]
simpa [toFlowNetwork, capFunc] using (Flow.range_of_zero_reverse_cap φ (Sum.inl l) (Sum.inl r) hrev)
In the matching network, the flow out of a left vertex equals its inflow
from the source (conservation at l ∈ L).
lemma matchingFlow_conservation_left {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (φ : Flow (V ⊕ Bool) (toFlowNetwork V G))
(l : V) (hl : l ∈ G.L) :
φ.f (Sum.inr true) (Sum.inl l) = ∑ r : V, φ.f (Sum.inl l) (Sum.inl r) := by
have hcons : (∑ v : V ⊕ Bool, φ.f (Sum.inl l) v) = 0 :=
φ.hconservation (Sum.inl l) (by simp [toFlowNetwork]) (by simp [toFlowNetwork])
have hdecomp : (∑ v : V ⊕ Bool, φ.f (Sum.inl l) v) =
(∑ r : V, φ.f (Sum.inl l) (Sum.inl r)) +
(φ.f (Sum.inl l) (Sum.inr true) + φ.f (Sum.inl l) (Sum.inr false)) := by
rw [← Finset.univ_disjSum_univ (α := V) (β := Bool)]
rw [Finset.sum_disjSum (Finset.univ : Finset V) (Finset.univ : Finset Bool)
(fun v : V ⊕ Bool => φ.f (Sum.inl l) v)]
rw [Fintype.univ_bool]
rw [Finset.sum_pair (by decide : true ≠ false)]
have hlt : φ.f (Sum.inl l) (Sum.inr false) = 0 := by
have hrev : (toFlowNetwork V G).c (Sum.inr false) (Sum.inl l) = 0 := by
simp [toFlowNetwork, capFunc]
have hr0 := Flow.range_of_zero_reverse_cap φ (Sum.inl l) (Sum.inr false) hrev
have hcap : (toFlowNetwork V G).c (Sum.inl l) (Sum.inr false) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : l ∈ G.R
· exact False.elim (G.not_mem_R_of_mem_L hl h)
· simp [h]
linarith
have hls : φ.f (Sum.inl l) (Sum.inr true) = -φ.f (Sum.inr true) (Sum.inl l) :=
φ.hskew_symm (Sum.inl l) (Sum.inr true)
rw [hdecomp, hlt, hls] at hcons
linarith
In the matching network, the flow into a right vertex equals its outflow
to the sink (conservation at r ∈ R).
lemma matchingFlow_conservation_right {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (φ : Flow (V ⊕ Bool) (toFlowNetwork V G))
(r : V) (hr : r ∈ G.R) :
φ.f (Sum.inl r) (Sum.inr false) = ∑ l : V, φ.f (Sum.inl l) (Sum.inl r) := by
have hcons : (∑ v : V ⊕ Bool, φ.f (Sum.inl r) v) = 0 :=
φ.hconservation (Sum.inl r) (by simp [toFlowNetwork]) (by simp [toFlowNetwork])
have hdecomp : (∑ v : V ⊕ Bool, φ.f (Sum.inl r) v) =
(∑ l : V, φ.f (Sum.inl r) (Sum.inl l)) +
(φ.f (Sum.inl r) (Sum.inr true) + φ.f (Sum.inl r) (Sum.inr false)) := by
rw [← Finset.univ_disjSum_univ (α := V) (β := Bool)]
rw [Finset.sum_disjSum (Finset.univ : Finset V) (Finset.univ : Finset Bool)
(fun v : V ⊕ Bool => φ.f (Sum.inl r) v)]
rw [Fintype.univ_bool]
rw [Finset.sum_pair (by decide : true ≠ false)]
have hrs : φ.f (Sum.inl r) (Sum.inr true) = 0 := by
have hrev : (toFlowNetwork V G).c (Sum.inr true) (Sum.inl r) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : r ∈ G.L
· exact False.elim (G.not_mem_L_of_mem_R hr h)
· simp [h]
have hr0 := Flow.range_of_zero_reverse_cap φ (Sum.inl r) (Sum.inr true) hrev
have hcap : (toFlowNetwork V G).c (Sum.inl r) (Sum.inr true) = 0 := by
simp [toFlowNetwork, capFunc]
linarith
have hlr_sum : (∑ l : V, φ.f (Sum.inl r) (Sum.inl l)) =
-(∑ l : V, φ.f (Sum.inl l) (Sum.inl r)) := by
calc
(∑ l : V, φ.f (Sum.inl r) (Sum.inl l)) = ∑ l : V, -φ.f (Sum.inl l) (Sum.inl r) := by
refine Finset.sum_congr rfl (fun l _ => ?_)
exact φ.hskew_symm (Sum.inl r) (Sum.inl l)
_ = -(∑ l : V, φ.f (Sum.inl l) (Sum.inl r)) := by
rw [Finset.sum_neg_distrib]
rw [hdecomp, hrs, hlr_sum] at hcons
linarithFlow between two right vertices is zero (both directions have zero capacity).
lemma matchingFlow_rr_zero {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) {r₁ r₂ : V}
(hr₁ : r₁ ∈ G.R) (hr₂ : r₂ ∈ G.R) : φ.f (Sum.inl r₁) (Sum.inl r₂) = 0 := by
have hcap : (toFlowNetwork V G).c (Sum.inl r₁) (Sum.inl r₂) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : (r₁, r₂) ∈ G.E
· exact False.elim (G.not_mem_L_of_mem_R hr₁ (G.hE_subset (r₁, r₂) h).1)
· simp [h]
have hrev : (toFlowNetwork V G).c (Sum.inl r₂) (Sum.inl r₁) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : (r₂, r₁) ∈ G.E
· exact False.elim (G.not_mem_L_of_mem_R hr₂ (G.hE_subset (r₂, r₁) h).1)
· simp [h]
have hle := Flow.nonpos_of_zero_cap φ (Sum.inl r₁) (Sum.inl r₂) hcap
have hge := Flow.nonneg_of_zero_reverse_cap φ (Sum.inl r₁) (Sum.inl r₂) hrev
linarith
On the unit-capacity network an integral flow takes values in {0, 1}
on every L→R pair.
lemma integral_lr_unit {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral)
(l : V) (hl : l ∈ G.L) (r : V) :
φ.f (Sum.inl l) (Sum.inl r) = 0 ∨ φ.f (Sum.inl l) (Sum.inl r) = 1 := by
have hb := matchingFlow_lr_bounds φ l hl r
have hle : φ.f (Sum.inl l) (Sum.inl r) ≤ 1 := by
by_cases hE : (l, r) ∈ G.E
· simpa [hE] using hb.2
· simp [hE] at hb
linarith
exact integral_of_unit_range ⟨hb.1, hle⟩ (hint (Sum.inl l) (Sum.inl r))
On the unit-capacity network an integral flow sends 0 or 1 units out
of the source to every left vertex.
lemma integral_source_unit {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral)
(l : V) (hl : l ∈ G.L) :
φ.f (Sum.inr true) (Sum.inl l) = 0 ∨ φ.f (Sum.inr true) (Sum.inl l) = 1 := by
have hrev : (toFlowNetwork V G).c (Sum.inl l) (Sum.inr true) = 0 := by
simp [toFlowNetwork, capFunc]
exact integral_of_unit_range
(by simpa [toFlowNetwork, capFunc, hl] using
(Flow.range_of_zero_reverse_cap φ (Sum.inr true) (Sum.inl l) hrev))
(hint (Sum.inr true) (Sum.inl l))
An edge carrying one unit of flow in the matching network belongs to
G.E.
lemma mem_edges_of_flow_one {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) {l r : V}
(h : φ.f (Sum.inl l) (Sum.inl r) = 1) : (l, r) ∈ G.E := by
have hle1 : 1 ≤ (toFlowNetwork V G).c (Sum.inl l) (Sum.inl r) := by
linarith [φ.hcapacity (Sum.inl l) (Sum.inl r), h]
by_cases hE : (l, r) ∈ G.E
· exact hE
· simp [toFlowNetwork, capFunc, hE] at hle1
norm_num at hle1
The indicator of a one-unit flow into a right vertex equals the flow
value: integral flows take 0 or 1 on L→R pairs and zero on R→R
pairs.
lemma flow_one_indicator_eq_of_right {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral)
{r : V} (hr : r ∈ G.R) (l : V) :
(if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0) = φ.f (Sum.inl l) (Sum.inl r) := by
by_cases hl : l ∈ G.L
· rcases integral_lr_unit φ hint l hl r with h | h <;> simp [h]
· have hlR : l ∈ G.R := by
have : l ∈ G.L ∪ G.R := by simp [G.h_cover]
exact (Finset.mem_union.mp this).resolve_left hl
have hz : φ.f (Sum.inl l) (Sum.inl r) = 0 := matchingFlow_rr_zero φ hlR hr
simp [hz]
The matching recovered from an integral flow: every L→R pair carrying
one unit of flow.
noncomputable def matchingOfIntegralFlow {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral) :
Matching V G :=
{ edges := (Finset.univ : Finset (V × V)).filter (fun e : V × V => φ.f (Sum.inl e.1) (Sum.inl e.2) = 1)
, h_subset := by
intro e he
exact mem_edges_of_flow_one φ (Finset.mem_filter.mp he).2
, h_unique_left := by
intro l r₁ r₂ h1 h2
have hf1 : φ.f (Sum.inl l) (Sum.inl r₁) = 1 := (Finset.mem_filter.mp h1).2
have hl : l ∈ G.L := (G.hE_subset (l, r₁) (mem_edges_of_flow_one φ hf1)).1
have hcount : φ.f (Sum.inr true) (Sum.inl l) =
((Finset.univ.filter (fun r : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) := by
calc
φ.f (Sum.inr true) (Sum.inl l) = ∑ r : V, φ.f (Sum.inl l) (Sum.inl r) :=
matchingFlow_conservation_left φ l hl
_ = ∑ r : V, (if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0) := by
refine Finset.sum_congr rfl (fun r _ => ?_)
rcases integral_lr_unit φ hint l hl r with h | h <;> simp [h]
_ = ((Finset.univ.filter (fun r : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) := by
rw [← Finset.sum_filter]
simp
have hle : φ.f (Sum.inr true) (Sum.inl l) ≤ 1 := by
rcases integral_source_unit φ hint l hl with h | h <;> simp [h]
have hcard : (Finset.univ.filter (fun r : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card ≤ 1 := by
have hℝ : (↑(Finset.univ.filter (fun r : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) ≤ 1 := by
rw [← hcount]
exact hle
exact_mod_cast hℝ
exact Finset.card_le_one.mp hcard r₁ (by simp [hf1]) r₂ (by simp [(Finset.mem_filter.mp h2).2])
, h_unique_right := by
intro l₁ l₂ r h1 h2
have hf1 : φ.f (Sum.inl l₁) (Sum.inl r) = 1 := (Finset.mem_filter.mp h1).2
have hr : r ∈ G.R := (G.hE_subset (l₁, r) (mem_edges_of_flow_one φ hf1)).2
have hcount : φ.f (Sum.inl r) (Sum.inr false) =
((Finset.univ.filter (fun l : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) := by
calc
φ.f (Sum.inl r) (Sum.inr false) = ∑ l : V, φ.f (Sum.inl l) (Sum.inl r) :=
matchingFlow_conservation_right φ r hr
_ = ∑ l : V, (if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0) := by
refine Finset.sum_congr rfl (fun l _ => ?_)
exact (flow_one_indicator_eq_of_right φ hint hr l).symm
_ = ((Finset.univ.filter (fun l : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) := by
rw [← Finset.sum_filter]
simp
have hr01 : 0 ≤ φ.f (Sum.inl r) (Sum.inr false) ∧ φ.f (Sum.inl r) (Sum.inr false) ≤ 1 := by
have hrev : (toFlowNetwork V G).c (Sum.inr false) (Sum.inl r) = 0 := by
simp [toFlowNetwork, capFunc]
have hr0 := Flow.range_of_zero_reverse_cap φ (Sum.inl r) (Sum.inr false) hrev
have hc : (toFlowNetwork V G).c (Sum.inl r) (Sum.inr false) = 1 := by
simp [toFlowNetwork, capFunc, hr]
exact ⟨hr0.1, by simpa [hc] using hr0.2⟩
have hcard : (Finset.univ.filter (fun l : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card ≤ 1 := by
have hℝ : (↑(Finset.univ.filter (fun l : V => φ.f (Sum.inl l) (Sum.inl r) = 1)).card : ℝ) ≤ 1 := by
rw [← hcount]
exact hr01.2
exact_mod_cast hℝ
exact Finset.card_le_one.mp hcard l₁ (by simp [hf1]) l₂ (by simp [(Finset.mem_filter.mp h2).2])
}
Theorem (integral-flow converse). An integral flow of value v in
the matching network yields a matching of size v (CLRS Theorem 24.12,
converse direction).
theorem matchingOfIntegralFlow_size {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} (φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral) :
((matchingOfIntegralFlow φ hint).size : ℝ) = φ.value := by
have hcard : ((matchingOfIntegralFlow φ hint).edges.card : ℝ) =
∑ e : V × V, (if φ.f (Sum.inl e.1) (Sum.inl e.2) = 1 then (1 : ℝ) else 0) := by
unfold matchingOfIntegralFlow
rw [← Finset.sum_filter]
simp
have hval : φ.value = ∑ l : V, φ.f (Sum.inr true) (Sum.inl l) := by
calc
φ.value = (∑ l : V, φ.f (Sum.inr true) (Sum.inl l)) +
(φ.f (Sum.inr true) (Sum.inr true) + φ.f (Sum.inr true) (Sum.inr false)) := by
simp [Flow.value, toFlowNetwork]
_ = ∑ l : V, φ.f (Sum.inr true) (Sum.inl l) := by
have hss : φ.f (Sum.inr true) (Sum.inr true) = 0 := Flow.self_zero φ (Sum.inr true)
have hst : φ.f (Sum.inr true) (Sum.inr false) = 0 := by
have hrev : (toFlowNetwork V G).c (Sum.inr false) (Sum.inr true) = 0 := by
simp [toFlowNetwork, capFunc]
have hr0 := Flow.range_of_zero_reverse_cap φ (Sum.inr true) (Sum.inr false) hrev
have hcap : (toFlowNetwork V G).c (Sum.inr true) (Sum.inr false) = 0 := by
simp [toFlowNetwork, capFunc]
linarith
simp [hss, hst]
calc
((matchingOfIntegralFlow φ hint).size : ℝ)
= ∑ e : V × V, (if φ.f (Sum.inl e.1) (Sum.inl e.2) = 1 then (1 : ℝ) else 0) := by
simp only [Matching.size]
rw [hcard]
_ = ∑ l : V, ∑ r : V, (if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0) := by
have huniv : (Finset.univ : Finset (V × V)) = Finset.univ.product Finset.univ := by
ext e; simp
rw [huniv]
exact (Finset.sum_product Finset.univ Finset.univ
(fun e : V × V => if φ.f (Sum.inl e.1) (Sum.inl e.2) = 1 then (1 : ℝ) else 0))
_ = ∑ l : V, φ.f (Sum.inr true) (Sum.inl l) := by
refine Finset.sum_congr rfl (fun l _ => ?_)
by_cases hl : l ∈ G.L
· calc
∑ r : V, (if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0)
= ∑ r : V, φ.f (Sum.inl l) (Sum.inl r) := by
refine Finset.sum_congr rfl (fun r _ => ?_)
rcases integral_lr_unit φ hint l hl r with h | h <;> simp [h]
_ = φ.f (Sum.inr true) (Sum.inl l) := (matchingFlow_conservation_left φ l hl).symm
· have hlR : l ∈ G.R := by
have : l ∈ G.L ∪ G.R := by simp [G.h_cover]
exact (Finset.mem_union.mp this).resolve_left hl
have hsum : ∑ r : V, (if φ.f (Sum.inl l) (Sum.inl r) = 1 then (1 : ℝ) else 0) = 0 := by
refine Finset.sum_eq_zero (fun r _ => ?_)
have hcap : (toFlowNetwork V G).c (Sum.inl l) (Sum.inl r) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : (l, r) ∈ G.E
· exact False.elim (hl (G.hE_subset (l, r) h).1)
· simp [h]
have hf : φ.f (Sum.inl l) (Sum.inl r) ≤ 0 :=
Flow.nonpos_of_zero_cap φ (Sum.inl l) (Sum.inl r) hcap
by_cases h : φ.f (Sum.inl l) (Sum.inl r) = 1
· exfalso; linarith
· simp [h]
have hsrc : φ.f (Sum.inr true) (Sum.inl l) = 0 := by
have hcap : (toFlowNetwork V G).c (Sum.inr true) (Sum.inl l) = 0 := by
simp [toFlowNetwork, capFunc]
by_cases h : l ∈ G.L
· exact False.elim (hl h)
· simp [h]
have hrev : (toFlowNetwork V G).c (Sum.inl l) (Sum.inr true) = 0 := by
simp [toFlowNetwork, capFunc]
have hr0 := Flow.range_of_zero_reverse_cap φ (Sum.inr true) (Sum.inl l) hrev
linarith
rw [hsum, hsrc]
_ = φ.value := hval.symmIntegral maximum flow and Theorem 24.12
The zero flow on a network.
noncomputable def zeroFlow {V : Type*} [Fintype V] [DecidableEq V] (G : FlowNetwork V) : Flow V G :=
{ f := fun _ _ => 0
, hcapacity := by intro u v; exact G.hc_nonneg u v
, hskew_symm := by intro u v; simp
, hconservation := by intro u hu ht; simp
}The zero flow is integral.
lemma IsIntegral_zero {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V} :
(zeroFlow G).IsIntegral := by
intro u v
exact ⟨0, by simp [zeroFlow]⟩The residual capacity of an integral flow on an integral-capacity network is an integer.
lemma residualCapacity_integral {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(u v : V) : ∃ n : ℤ, φ.residualCapacity u v = (n : ℝ) := by
rcases hc u v with ⟨m, hm⟩
rcases hint u v with ⟨n, hn⟩
unfold Flow.residualCapacity
refine ⟨m - n, ?_⟩
rw [hm, hn]
push_cast
ringThe bottleneck of an augmenting path in an integral network is an integer.
lemma bottleneck_integral {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(p : Flow.AugmentingPath φ) : ∃ n : ℤ, p.bottleneck = (n : ℝ) := 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⟩
rw [← hEq]
exact residualCapacity_integral φ hint hc e.1 e.2
The bottleneck of an augmenting path in an integral network is at least
1.
lemma bottleneck_ge_one {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(p : Flow.AugmentingPath φ) : 1 ≤ p.bottleneck := by
unfold Flow.AugmentingPath.bottleneck
rw [Finset.le_min'_iff]
intro x hx
rcases Finset.mem_image.mp hx with ⟨e, he, rfl⟩
have hpos : 0 < φ.residualCapacity e.1 e.2 :=
p.residualEdge_of_mem_edges (by simpa using he)
rcases residualCapacity_integral φ hint hc e.1 e.2 with ⟨n, hn⟩
rw [hn]
have hn_pos : 0 < n := by
have h0 : 0 < (n : ℝ) := by simpa [hn] using hpos
exact_mod_cast h0
exact_mod_cast (by omega : 1 ≤ n)The single-edge update of an integral delta is integral.
lemma edgeDelta_integral {V : Type*} [DecidableEq V] {delta : ℝ}
(hdelta : ∃ n : ℤ, delta = (n : ℝ)) (a b u v : V) :
∃ n : ℤ, Flow.edgeDelta delta a b u v = (n : ℝ) := by
rcases hdelta with ⟨n, hn⟩
by_cases h1 : u = a ∧ v = b
· by_cases h2 : u = b ∧ v = a
· have hab : a = b := h1.1.symm.trans h2.1
exact ⟨0, by simp [Flow.edgeDelta, h1, hab, hn]⟩
· have hab_ne : a ≠ b := by
intro hab
apply h2
exact ⟨by simpa [hab] using h1.1, by simpa [hab] using h1.2⟩
exact ⟨n, by simp [Flow.edgeDelta, h1, hab_ne, hn]⟩
· by_cases h2 : u = b ∧ v = a
· have hab_ne : a ≠ b := by
intro hab
apply h1
exact ⟨by simpa [hab] using h2.1, by simpa [hab] using h2.2⟩
exact ⟨-n, by simp [Flow.edgeDelta, h2, hab_ne, hn]⟩
· exact ⟨0, by simp [Flow.edgeDelta, h1, h2]⟩The path update of an integral delta is integral.
lemma pathDelta_integral {V : Type*} [DecidableEq V] {delta : ℝ}
(hdelta : ∃ n : ℤ, delta = (n : ℝ)) (xs : List V) (u v : V) :
∃ n : ℤ, Flow.pathDelta delta xs u v = (n : ℝ) := by
induction xs with
| nil => exact ⟨0, by simp [Flow.pathDelta]⟩
| cons a xs ih =>
cases xs with
| nil => exact ⟨0, by simp [Flow.pathDelta]⟩
| cons b xs =>
rcases edgeDelta_integral hdelta a b u v with ⟨m, hm⟩
rcases ih with ⟨k, hk⟩
exact ⟨m + k, by
simp only [Flow.pathDelta]
rw [hm, hk]
push_cast
ring⟩Augmentation preserves integrality on an integral-capacity network.
lemma IsIntegral_augment {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(p : Flow.AugmentingPath φ) : (φ.augment p).IsIntegral := by
intro u v
have hb : ∃ n : ℤ, p.bottleneck = (n : ℝ) := bottleneck_integral φ hint hc p
have hf : ∃ n : ℤ, φ.f u v = (n : ℝ) := hint u v
have hp : ∃ n : ℤ, Flow.pathDelta p.bottleneck p.vertices u v = (n : ℝ) :=
pathDelta_integral hb p.vertices u v
rcases hf with ⟨n, hn⟩
rcases hp with ⟨k, hk⟩
exact ⟨n + k, by
change φ.f u v + Flow.pathDelta p.bottleneck p.vertices u v = ((n + k : ℤ) : ℝ)
rw [hn, hk]
push_cast
ring⟩Augmenting along a residual path increases the value by at least one on an integral network.
lemma augment_value_ge_one {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(p : Flow.AugmentingPath φ) : φ.value + 1 ≤ (φ.augment p).value := by
rw [φ.augment_value p]
linarith [bottleneck_ge_one φ hint hc p]One augmentation step: augment along an arbitrary residual source-to-sink path if one exists.
noncomputable def augmentOnce {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : Flow V G :=
if h : φ.hasAugmentingPath then
φ.augment (Classical.choice (Flow.hasAugmentingPath_iff_nonempty_augmentingPath.mp h))
else φ
augmentOnce preserves integrality.
lemma IsIntegral_augmentOnce {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
(augmentOnce φ).IsIntegral := by
unfold augmentOnce
by_cases h : φ.hasAugmentingPath
· simp [h]
exact IsIntegral_augment φ hint hc
(Classical.choice (Flow.hasAugmentingPath_iff_nonempty_augmentingPath.mp h))
· simp [h]
exact hintRepeatedly augment from a starting flow.
noncomputable def iterAugment {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : ℕ → Flow V G
| 0 => φ
| n + 1 => augmentOnce (iterAugment φ n)
Every iterate of iterAugment is integral.
lemma IsIntegral_iterAugment {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
∀ n, (iterAugment φ n).IsIntegral := by
intro n
induction n with
| zero => simpa [iterAugment] using hint
| succ n ih =>
simpa [iterAugment] using (IsIntegral_augmentOnce (iterAugment φ n) ih hc)Each augmentation step increases the value by at least one, unless the flow is already free of augmenting paths.
lemma iterAugment_step_value {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) (hint : φ.IsIntegral) (hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ))
(n : ℕ) :
¬(iterAugment φ n).hasAugmentingPath ∨
(iterAugment φ n).value + 1 ≤ (iterAugment φ (n + 1)).value := by
by_cases h : (iterAugment φ n).hasAugmentingPath
· right
simp [iterAugment, augmentOnce, h]
exact augment_value_ge_one (iterAugment φ n) (IsIntegral_iterAugment φ hint hc n) hc
(Classical.choice (Flow.hasAugmentingPath_iff_nonempty_augmentingPath.mp h))
· left
exact hFlow value is bounded by the total capacity out of the source.
lemma value_le_source_cut {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(φ : Flow V G) : φ.value ≤ Finset.sum (Finset.univ : Finset V) (fun v => G.c G.s v) := by
unfold Flow.value
exact Finset.sum_le_sum (fun v _ => φ.hcapacity G.s v)The total capacity out of the source is an integer on an integral network.
lemma source_cut_integral {V : Type*} [Fintype V] [DecidableEq V] {G : FlowNetwork V}
(hc : ∀ u v, ∃ n : ℕ, G.c u v = (n : ℝ)) :
∃ n : ℕ, Finset.sum (Finset.univ : Finset V) (fun v => G.c G.s v) = (n : ℝ) := by
classical
choose nv hnv using (fun v => hc G.s v)
refine ⟨Finset.sum (Finset.univ : Finset V) nv, ?_⟩
rw [show (fun v : V => G.c G.s v) = fun v : V => (nv v : ℝ) by
funext v
exact hnv v]
norm_cast
While every step finds an augmenting path, the value after n steps is
at least n.
lemma iterAugment_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, (iterAugment φ n).hasAugmentingPath) :
∀ n : ℕ, (n : ℝ) ≤ (iterAugment φ n).value := by
intro n
induction n with
| zero => simpa [iterAugment] using hφ
| succ n ih =>
have hinc := (iterAugment_step_value φ hint hc n).resolve_left (not_not_intro (hsteps n))
push_cast
linarithRepeated augmentation from an integral flow 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_iter {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, ¬ (iterAugment φ n).hasAugmentingPath := by
by_contra hnot
have hsteps : ∀ n, (iterAugment φ n).hasAugmentingPath := by
intro n
by_contra h
exact hnot ⟨n, h⟩
rcases source_cut_integral hc with ⟨K, hK⟩
have hge : ((K + 1 : ℕ) : ℝ) ≤ (iterAugment φ (K + 1)).value :=
iterAugment_value_ge φ hint hc hφ hsteps (K + 1)
have hle : (iterAugment φ (K + 1)).value ≤ (K : ℝ) := by
rw [← hK]
exact value_le_source_cut (iterAugment φ (K + 1))
have hle' : ((K + 1 : ℕ) : ℝ) ≤ (K : ℝ) := le_trans hge hle
norm_num at hle'
The matching network has integral capacities (in fact 0 or 1).
lemma toFlowNetwork_integral_capacity {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} : ∀ u v, ∃ n : ℕ, (toFlowNetwork V G).c u v = (n : ℝ) := by
intro u v
cases u with
| inl a =>
cases v with
| inl b =>
change ∃ n : ℕ, (if (a, b) ∈ G.E then (1 : ℝ) else 0) = (n : ℝ)
by_cases h : (a, b) ∈ G.E
· exact ⟨1, by simp [h]⟩
· exact ⟨0, by simp [h]⟩
| inr b =>
cases b with
| true =>
change ∃ n : ℕ, (0 : ℝ) = (n : ℝ)
exact ⟨0, by norm_num⟩
| false =>
change ∃ n : ℕ, (if a ∈ G.R then (1 : ℝ) else 0) = (n : ℝ)
by_cases h : a ∈ G.R
· exact ⟨1, by simp [h]⟩
· exact ⟨0, by simp [h]⟩
| inr a =>
cases a with
| true =>
cases v with
| inl b =>
change ∃ n : ℕ, (if b ∈ G.L then (1 : ℝ) else 0) = (n : ℝ)
by_cases h : b ∈ G.L
· exact ⟨1, by simp [h]⟩
· exact ⟨0, by simp [h]⟩
| inr b =>
cases b <;> (change ∃ n : ℕ, (0 : ℝ) = (n : ℝ); exact ⟨0, by norm_num⟩)
| false =>
cases v with
| inl b =>
change ∃ n : ℕ, (0 : ℝ) = (n : ℝ)
exact ⟨0, by norm_num⟩
| inr b =>
cases b <;> (change ∃ n : ℕ, (0 : ℝ) = (n : ℝ); exact ⟨0, by norm_num⟩)Theorem 24.12 (CLRS). In the unit-capacity network of a bipartite graph, the maximum matching size equals the maximum flow value: there is a matching at least as large as every matching, and a maximal flow whose value is exactly its size.
theorem maxMatching_eq_maxFlow_value {V : Type*} [Fintype V] [DecidableEq V]
{G : BipartiteGraph V} :
∃ M : Matching V G, (∀ M' : Matching V G, M'.size ≤ M.size) ∧
∃ φ : Flow (V ⊕ Bool) (toFlowNetwork V G), φ.isMaximal ∧ φ.value = (M.size : ℝ) := by
let N : FlowNetwork (V ⊕ Bool) := toFlowNetwork V G
let zf : Flow (V ⊕ Bool) N := zeroFlow N
have hc : ∀ u v, ∃ n : ℕ, N.c u v = (n : ℝ) := by
intro u v
exact toFlowNetwork_integral_capacity u v
have hz : 0 ≤ zf.value := by
unfold Flow.value
simp [zf, zeroFlow]
rcases exists_noAugmentingPath_iter zf (IsIntegral_zero (G := N)) hc hz with
⟨n, hn⟩
let φ : Flow (V ⊕ Bool) N := iterAugment zf n
have hintφ : φ.IsIntegral := IsIntegral_iterAugment zf (IsIntegral_zero (G := N)) hc n
have hmax : φ.isMaximal := Flow.maximal_of_noAugmentingPath φ hn
let M : Matching V G := matchingOfIntegralFlow φ hintφ
refine ⟨M, ?_, φ, hmax, ?_⟩
· intro M'
have hvalφ : φ.value = (M.size : ℝ) := (matchingOfIntegralFlow_size φ hintφ).symm
have hvalM : (matchingToFlow M').value = (M'.size : ℝ) := matchingToFlow_value M'
have hle : (matchingToFlow M').value ≤ φ.value := hmax (matchingToFlow M')
have hsize : (M'.size : ℝ) ≤ (M.size : ℝ) := by linarith
exact_mod_cast hsize
· exact (matchingOfIntegralFlow_size φ hintφ).symmend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S1_Matching_API
S1. Matching API extensions
Extensions to the §26.3 Matching structure that the §25.1 development
needs: matched-endpoint sets, matched/unmatched predicates, maximality, the
empty matching, and their cardinality and participation lemmas.
These declarations live in the original CLRS.Chapter26.Matching namespace
so that dot notation keeps working.
Main results:
-
matchedLeft_card/matchedRight_card: the matched endpoint sets have the same cardinality as the matching -
IsMaximum: a matching that no other matching exceeds in size -
mem_L_of_isMatchedLeft/mem_R_of_isMatchedRight: matched vertices lie in the corresponding partition
namespace CLRSopen Finset Classical/- API extensions to the §26.3 matching structures live in their original
namespace so that dot notation keeps working. -/
namespace Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}namespace MatchingThe left endpoints of the edges of a matching.
def matchedLeft {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : Finset V :=
M.edges.image Prod.fstThe right endpoints of the edges of a matching.
def matchedRight {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : Finset V :=
M.edges.image Prod.sndA left vertex is matched when it is the left endpoint of a matching edge.
def IsMatchedLeft {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (l : V) : Prop :=
∃ r, (l, r) ∈ M.edgesA right vertex is matched when it is the right endpoint of a matching edge.
def IsMatchedRight {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (r : V) : Prop :=
∃ l, (l, r) ∈ M.edgesA left vertex is unmatched when no matching edge leaves it.
def IsUnmatchedLeft {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (l : V) : Prop :=
∀ r, (l, r) ∉ M.edgesA right vertex is unmatched when no matching edge enters it.
def IsUnmatchedRight {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) (r : V) : Prop :=
∀ l, (l, r) ∉ M.edgesA matching is maximum when no matching has more edges.
def IsMaximum {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
(M : Matching V G) : Prop :=
∀ M' : Matching V G, M'.size ≤ M.sizeThe empty matching.
def empty (G : BipartiteGraph V) : Matching V G where
edges := ∅
h_subset := Finset.empty_subset _
h_unique_left := by simp
h_unique_right := by simpThe empty matching has size zero.
@[simp]
lemma empty_size (G : BipartiteGraph V) : (empty G).size = 0 := rflLeft endpoints of distinct matching edges are distinct, so the matched left set has the same cardinality as the matching.
lemma matchedLeft_card (M : Matching V G) : M.matchedLeft.card = M.size := by
unfold matchedLeft Matching.size
rw [Finset.card_image_of_injOn]
intro e₁ he₁ e₂ he₂ h
exact Prod.ext h (M.h_unique_left e₁.1 e₁.2 e₂.2 he₁ (by simpa [h] using he₂))Right endpoints of distinct matching edges are distinct, so the matched right set has the same cardinality as the matching.
lemma matchedRight_card (M : Matching V G) : M.matchedRight.card = M.size := by
unfold matchedRight Matching.size
rw [Finset.card_image_of_injOn]
intro e₁ he₁ e₂ he₂ h
exact Prod.ext (M.h_unique_right e₁.1 e₂.1 e₁.2 he₁ (by simpa [h] using he₂)) h
Membership in matchedLeft is exactly being matched on the left.
lemma mem_matchedLeft_iff (M : Matching V G) (l : V) :
l ∈ M.matchedLeft ↔ M.IsMatchedLeft l := by
simp [matchedLeft, IsMatchedLeft]
Membership in matchedRight is exactly being matched on the right.
lemma mem_matchedRight_iff (M : Matching V G) (r : V) :
r ∈ M.matchedRight ↔ M.IsMatchedRight r := by
simp [matchedRight, IsMatchedRight]Unmatched on the left is the negation of matched on the left.
lemma isUnmatchedLeft_iff_not_matched (M : Matching V G) (l : V) :
M.IsUnmatchedLeft l ↔ ¬ M.IsMatchedLeft l := by
simp [IsUnmatchedLeft, IsMatchedLeft]Unmatched on the right is the negation of matched on the right.
lemma isUnmatchedRight_iff_not_matched (M : Matching V G) (r : V) :
M.IsUnmatchedRight r ↔ ¬ M.IsMatchedRight r := by
simp [IsUnmatchedRight, IsMatchedRight]
Matched left vertices lie in G.L.
lemma mem_L_of_isMatchedLeft (M : Matching V G) {l : V} (h : M.IsMatchedLeft l) :
l ∈ G.L := by
rcases h with ⟨r, hr⟩
exact M.left_mem_L hr
Matched right vertices lie in G.R.
lemma mem_R_of_isMatchedRight (M : Matching V G) {r : V} (h : M.IsMatchedRight r) :
r ∈ G.R := by
rcases h with ⟨l, hl⟩
exact M.right_mem_R hlLeft vertices are never right vertices.
lemma not_mem_R_of_mem_L {G : BipartiteGraph V} {v : V} (hv : v ∈ G.L) : v ∉ G.R :=
G.not_mem_R_of_mem_L hvRight vertices are never left vertices.
lemma not_mem_L_of_mem_R {G : BipartiteGraph V} {v : V} (hv : v ∈ G.R) : v ∉ G.L :=
G.not_mem_L_of_mem_R hvend Matchingend Chapter26end CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S2_Alternating_Paths
S2. Alternating paths and augmentation
Alternating-path infrastructure: the altEdges decomposition of a vertex
list into forward and backward edges, the IsAugmentingPath structure, and
the forward direction of Berge's lemma — an augmenting path yields a matching
that is larger by one.
Main results:
-
IsAugmentingPath: alternating vertex-simple paths with unmatched endpoints -
exists_augment_singleand the swap step: single-edge building blocks -
exists_augment: augmentation theorem (CLRS §25.1, Berge, forward direction) -
not_isMaximum_of_isAugmentingPath: an augmenting path certifies non-maximality
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}
The alternating edges of a vertex list, in canonical (L, R) orientation.
(altEdges p).1 is the list of forward edges (p₀,p₁), (p₂,p₃), … and
(altEdges p).2 is the list of backward edges (p₂,p₁), (p₄,p₃), ….
def altEdges : List V → List (V × V) × List (V × V)
| [] => ([], [])
| [_] => ([], [])
| l :: r :: rest =>
let recRes := altEdges rest
((l, r) :: recRes.1,
match rest with
| [] => recRes.2
| l' :: _ => (l', r) :: recRes.2)The first component of a forward edge occurs in the path.
lemma fst_mem_of_mem_altEdges_left {p : List V} {e : V × V}
(h : e ∈ (altEdges p).1) : e.1 ∈ p := by
induction p using altEdges.induct with
| case1 => simp [altEdges] at h
| case2 => simp [altEdges] at h
| case3 l r rest ih =>
simp only [altEdges, List.mem_cons] at h
rcases h with h | h
· exact h ▸ List.mem_cons_self
· exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (ih h))The second component of a forward edge occurs in the path.
lemma snd_mem_of_mem_altEdges_left {p : List V} {e : V × V}
(h : e ∈ (altEdges p).1) : e.2 ∈ p := by
induction p using altEdges.induct with
| case1 => simp [altEdges] at h
| case2 => simp [altEdges] at h
| case3 l r rest ih =>
simp only [altEdges, List.mem_cons] at h
rcases h with h | h
· exact h ▸ List.mem_cons_of_mem _ (List.mem_cons_self)
· exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (ih h))The first component of a backward edge occurs in the path.
lemma fst_mem_of_mem_altEdges_right {p : List V} {e : V × V}
(h : e ∈ (altEdges p).2) : e.1 ∈ p := by
induction p using altEdges.induct with
| case1 => simp [altEdges] at h
| case2 => simp [altEdges] at h
| case3 l r rest ih =>
cases rest with
| nil => simp [altEdges] at h
| cons l' u =>
simp only [altEdges, List.mem_cons] at h
rcases h with h | h
· exact h ▸ List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (List.mem_cons_self))
· exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (ih h))The second component of a backward edge occurs in the path.
lemma snd_mem_of_mem_altEdges_right {p : List V} {e : V × V}
(h : e ∈ (altEdges p).2) : e.2 ∈ p := by
induction p using altEdges.induct with
| case1 => simp [altEdges] at h
| case2 => simp [altEdges] at h
| case3 l r rest ih =>
cases rest with
| nil => simp [altEdges] at h
| cons l' u =>
simp only [altEdges, List.mem_cons] at h
rcases h with h | h
· exact h ▸ List.mem_cons_of_mem _ (List.mem_cons_self)
· exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (ih h))
An augmenting path for a matching M in a bipartite graph G
(CLRS §25.1): an even-length, vertex-simple list p = [l₀, r₀, l₁, r₁, …]
whose forward edges (lᵢ, rᵢ) are non-matching graph edges, whose backward
edges (lᵢ₊₁, rᵢ) are matching edges, and whose two endpoints are unmatched
in M.
No vertex repeats along the path.
The path has even length.
The path has at least two vertices.
The path starts on the left.
The path's start vertex is unmatched.
The path ends on the right.
The path's end vertex is unmatched.
Forward edges are non-matching graph edges.
Backward edges are matching edges.
structure IsAugmentingPath (G : BipartiteGraph V) (M : Matching V G)
(p : List V) : Prop where nodup : p.Nodup length_even : Even p.length length_ge : 2 ≤ p.length head_mem_L : ∀ h : p ≠ [], p.head h ∈ G.L head_unmatched : ∀ h : p ≠ [], ∀ r, (p.head h, r) ∉ M.edges getLast_mem_R : ∀ h : p ≠ [], p.getLast h ∈ G.R getLast_unmatched : ∀ h : p ≠ [], ∀ l, (l, p.getLast h) ∉ M.edges forward : ∀ e ∈ (altEdges p).1, e ∈ G.E ∧ e ∉ M.edges backward : ∀ e ∈ (altEdges p).2, e ∈ M.edges
Single-edge augmenting step: if (l, r) is a non-matching graph edge
whose endpoints are both unmatched, inserting it into M gives a matching
that is larger by one.
lemma exists_augment_single {M : Matching V G} {l r : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges)
(hl : M.IsUnmatchedLeft l) (hr : M.IsUnmatchedRight r) :
∃ M' : Matching V G, M'.size = M.size + 1 := by
refine ⟨{ edges := insert (l, r) M.edges
h_subset := Finset.insert_subset hE M.h_subset
h_unique_left := ?_
h_unique_right := ?_ }, ?_⟩
· intro l₂ r₁ r₂ h₁ h₂
simp only [Finset.mem_insert, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | h₁ <;> rcases h₂ with ⟨e2a, e2b⟩ | h₂
· exact e1b.trans e2b.symm
· exact (hl r₂ (e1a ▸ h₂)).elim
· exact (hl r₁ (e2a ▸ h₁)).elim
· exact M.h_unique_left l₂ r₁ r₂ h₁ h₂
· intro l₁ l₂ r₃ h₁ h₂
simp only [Finset.mem_insert, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | h₁ <;> rcases h₂ with ⟨e2a, e2b⟩ | h₂
· exact e1a.trans e2a.symm
· exact (hr l₂ (e1b ▸ h₂)).elim
· exact (hr l₁ (e2b ▸ h₁)).elim
· exact M.h_unique_right l₁ l₂ r₃ h₁ h₂
· show (insert (l, r) M.edges).card = M.size + 1
rw [Finset.card_insert_of_notMem hM]
rfl
Swap step: if (l, r) is a non-matching graph edge, (l', r) is a
matching edge, and l is unmatched on the left, then replacing (l', r) by
(l, r) gives a matching of the same size in which l' is unmatched.
lemma exists_swap {M : Matching V G} {l r l' : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges) (hM' : (l', r) ∈ M.edges)
(hl : M.IsUnmatchedLeft l) (hne : l ≠ l') :
∃ M₁ : Matching V G, M₁.size = M.size ∧ M₁.IsUnmatchedLeft l' ∧
∀ e, e ∈ M₁.edges ↔ e = (l, r) ∨ (e ∈ M.edges ∧ e ≠ (l', r)) := by
refine ⟨{ edges := insert (l, r) (M.edges.erase (l', r))
h_subset := Finset.insert_subset hE
((Finset.erase_subset _ _).trans M.h_subset)
h_unique_left := ?_
h_unique_right := ?_ }, ?_, ?_, ?_⟩
· intro l₂ r₁ r₂ h₁ h₂
simp only [Finset.mem_insert, Finset.mem_erase, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | ⟨-, h₁⟩ <;> rcases h₂ with ⟨e2a, e2b⟩ | ⟨-, h₂⟩
· exact e1b.trans e2b.symm
· exact (hl r₂ (e1a ▸ h₂)).elim
· exact (hl r₁ (e2a ▸ h₁)).elim
· exact M.h_unique_left l₂ r₁ r₂ h₁ h₂
· intro l₁ l₂ r₃ h₁ h₂
simp only [Finset.mem_insert, Finset.mem_erase, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | ⟨hne₁, h₁⟩ <;> rcases h₂ with ⟨e2a, e2b⟩ | ⟨hne₂, h₂⟩
· exact e1a.trans e2a.symm
· exact (hne₂ (Prod.ext (M.h_unique_right l₂ l' r (e1b ▸ h₂) hM') e1b)).elim
· exact (hne₁ (Prod.ext (M.h_unique_right l₁ l' r (e2b ▸ h₁) hM') e2b)).elim
· exact M.h_unique_right l₁ l₂ r₃ h₁ h₂
· show (insert (l, r) (M.edges.erase (l', r))).card = M.size
have hnotin : (l, r) ∉ M.edges.erase (l', r) := fun h =>
hM (Finset.mem_of_mem_erase h)
rw [Finset.card_insert_of_notMem hnotin, Finset.card_erase_of_mem hM',
Nat.sub_add_cancel (Finset.card_pos.mpr ⟨(l', r), hM'⟩)]
rfl
· intro r₂ h
simp only [Finset.mem_insert, Finset.mem_erase, Prod.mk.injEq] at h
rcases h with ⟨e1, -⟩ | ⟨hne2, hmem⟩
· exact hne e1.symm
· exact hne2 (Prod.ext rfl (M.h_unique_left l' r r₂ hM' hmem).symm)
· intro e
simp only [Finset.mem_insert, Finset.mem_erase]
constructor
· rintro (h | ⟨h1, h2⟩)
· exact Or.inl h
· exact Or.inr ⟨h2, h1⟩
· rintro (h | ⟨h1, h2⟩)
· exact Or.inl h
· exact Or.inr ⟨h2, h1⟩Augmentation theorem (CLRS §25.1, Berge's lemma, forward direction): a matching that admits an augmenting path can be enlarged by one edge.
theorem exists_augment {M : Matching V G} {p : List V}
(hp : IsAugmentingPath G M p) : ∃ M' : Matching V G, M'.size = M.size + 1 := by
suffices aux : ∀ (n : ℕ) (M : Matching V G) (p : List V), p.length ≤ n →
IsAugmentingPath G M p → ∃ M' : Matching V G, M'.size = M.size + 1 from
aux p.length M p le_rfl hp
intro n
induction n with
| zero =>
intro M p hlen hp
have h2 := hp.length_ge
omega
| succ n ih =>
intro M p hlen hp
cases p with
| nil =>
have h2 := hp.length_ge
simp at h2
| cons l t =>
cases t with
| nil =>
have h2 := hp.length_ge
simp at h2
| cons r rest =>
cases rest with
| nil =>
have hfw := hp.forward (l, r) List.mem_cons_self
exact exists_augment_single hfw.1 hfw.2
(hp.head_unmatched (by simp)) (hp.getLast_unmatched (by simp))
| cons l' rest' =>
have hne_p : l :: r :: l' :: rest' ≠ [] := by simp
have hnd := hp.nodup
rw [List.nodup_cons] at hnd
obtain ⟨hl_notin, hnd⟩ := hnd
rw [List.nodup_cons] at hnd
obtain ⟨hr_notin, hnd⟩ := hnd
have hfw := hp.forward (l, r) List.mem_cons_self
have hbw := hp.backward (l', r) List.mem_cons_self
have hhu : ∀ r₂, (l, r₂) ∉ M.edges := hp.head_unmatched hne_p
have hll : l ≠ l' := fun h =>
hl_notin (h ▸ List.mem_cons_of_mem _ List.mem_cons_self)
obtain ⟨M₁, hM₁size, hM₁un, hM₁mem⟩ := exists_swap hfw.1 hfw.2 hbw hhu hll
-- The tail `l' :: rest'` is augmenting for `M₁`.
have hgl : (l :: r :: l' :: rest').getLast hne_p =
(l' :: rest').getLast (by simp) := by
simp [List.getLast_cons]
have htail : IsAugmentingPath G M₁ (l' :: rest') := by
refine ⟨hnd, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· have h2 := hp.length_even
have h4 := hp.length_ge
simp only [List.length_cons] at h2 h4 ⊢
obtain ⟨k, hk⟩ := h2
exact ⟨k - 1, by omega⟩
· have h2 := hp.length_even
have h4 := hp.length_ge
simp only [List.length_cons] at h2 h4 ⊢
obtain ⟨k, hk⟩ := h2
omega
· intro _
exact (G.hE_subset _ (M.h_subset hbw)).1
· intro _ r₂ h
exact hM₁un r₂ h
· intro _
have := hp.getLast_mem_R hne_p
rwa [hgl] at this
· intro _ l₂ h
rw [hM₁mem] at h
rcases h with h | ⟨hmem, -⟩
· obtain ⟨-, e2⟩ := Prod.mk.inj h
have hrmem : r ∈ l' :: rest' := by
have hglmem := List.getLast_mem (l := l' :: rest') (by simp)
rwa [e2] at hglmem
exact absurd hrmem hr_notin
· exact hp.getLast_unmatched hne_p l₂ (hgl ▸ hmem)
· intro e he
have hf := hp.forward e (List.mem_cons_of_mem _ he)
refine ⟨hf.1, fun hmem => ?_⟩
rw [hM₁mem] at hmem
rcases hmem with h | ⟨hmem, -⟩
· obtain ⟨e1, -⟩ := Prod.mk.inj h
have hm2 := fst_mem_of_mem_altEdges_left he
rw [e1] at hm2
exact hl_notin (List.mem_cons_of_mem _ hm2)
· exact hf.2 hmem
· intro e he
have hb := hp.backward e (List.mem_cons_of_mem _ he)
have hne : e ≠ (l', r) := by
intro hcontra
have hm2 := snd_mem_of_mem_altEdges_right he
rw [hcontra] at hm2
exact hr_notin hm2
exact (hM₁mem e).mpr (Or.inr ⟨hb, hne⟩)
obtain ⟨M₂, hM₂⟩ := ih M₁ (l' :: rest') (by
have := hp.length_ge
simp only [List.length_cons] at hlen this ⊢
omega) htail
exact ⟨M₂, by omega⟩An augmenting path certifies that a matching is not maximum.
lemma not_isMaximum_of_isAugmentingPath {M : Matching V G} {p : List V}
(hp : IsAugmentingPath G M p) : ¬ M.IsMaximum := by
intro hmax
obtain ⟨M', hM'⟩ := exists_augment hp
have := hmax M'
omegaend Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S3_Simple_Paths
S3. Simple-path extraction
Generic list theory bridging reachability proofs to vertex-simple paths: a reflexive-transitive reachability proof unfolds to an explicit walk, every walk contains a vertex-simple walk with the same endpoints, and distinct endpoints force a simple path of length at least two.
Main results:
-
exists_isChain_of_reflTransGen: reachability unfolds to an explicit walk -
exists_nodup_isChain: every walk contains a vertex-simple walk with the same endpoints -
exists_nodup_path_of_reflTransGen: a simple path with the same endpoints and length at least two
namespace CLRSnamespace MatchingsSimple-path extraction
A reflexive-transitive reachability proof contains a vertex-simple path with
the same endpoints. This is the bridge between the reachability-based
Flow.hasAugmentingPath of §26.1 and the explicit alternating paths of this
section.
A reflexive-transitive reachability proof unfolds to an explicit walk.
theorem exists_isChain_of_reflTransGen {α : Type*} {r : α → α → Prop} {a b : α}
(h : Relation.ReflTransGen r a b) :
∃ p : List α, p.IsChain r ∧ p[0]? = some a ∧ p[p.length - 1]? = some b := by
induction h
case refl =>
exact ⟨[a], List.isChain_singleton a, rfl, rfl⟩
case tail b' c' hab hbc ih =>
obtain ⟨p, hp, h0, hlast⟩ := ih
have hpne : p ≠ [] := fun h => by simp [h] at h0
refine ⟨p ++ [c'], ?_, ?_, ?_⟩
· rw [List.isChain_iff_getElem] at hp ⊢
intro i hi
have hlen : (p ++ [c']).length = p.length + 1 := by simp
by_cases hi1 : i + 1 < p.length
· rw [List.getElem_append_left (by omega), List.getElem_append_left hi1]
exact hp i hi1
· have hi2 : i + 1 = p.length := by rw [hlen] at hi; omega
have hi0 : i < p.length := by omega
rw [List.getElem_append_left hi0, List.getElem_append_right (by omega)]
have hpi : p[i]? = some b' := by simpa [← hi2] using hlast
have hpi' : p[i] = b' := by simpa [hi0] using hpi
simpa [hpi', hi2] using hbc
· simpa [hpne, List.length_pos_of_ne_nil] using h0
· have hlen : (p ++ [c']).length = p.length + 1 := by simp
rw [hlen]
simp [List.getElem_append_right, hpne]Every walk contains a vertex-simple walk with the same endpoints.
theorem exists_nodup_isChain {α : Type*} [DecidableEq α] {r : α → α → Prop}
(p : List α) (hp : p.IsChain r) :
∃ q : List α, q.IsChain r ∧ q.Nodup ∧
q[0]? = p[0]? ∧ q[q.length - 1]? = p[p.length - 1]? := by
suffices aux : ∀ (n : ℕ) (p : List α), p.length ≤ n → p.IsChain r →
∃ q : List α, q.IsChain r ∧ q.Nodup ∧
q[0]? = p[0]? ∧ q[q.length - 1]? = p[p.length - 1]? from
aux p.length p le_rfl hp
intro n
induction n with
| zero =>
intro p hl hp
simp at hl
subst hl
exact ⟨[], by simp, by simp, rfl, rfl⟩
| succ n ih =>
intro p hl hp
by_cases hnd : p.Nodup
· exact ⟨p, hp, hnd, rfl, rfl⟩
· rw [List.nodup_iff_getElem?_ne_getElem?] at hnd
push Not at hnd
obtain ⟨i, j, hij, hj, heq⟩ := hnd
have hi : i < p.length := by omega
have hpi : p[i]? = some p[i] := List.getElem?_eq_getElem hi
have hpj : p[j]? = some p[j] := List.getElem?_eq_getElem hj
rw [hpi, hpj] at heq
simp only [Option.some.injEq] at heq
set q := p.take (i + 1) ++ p.drop (j + 1) with hq_def
have hqlen : q.length = p.length - (j - i) := by
simp [hq_def, List.length_append, List.length_take, List.length_drop, hi, hj]
omega
have hqchain : q.IsChain r := by
rw [List.isChain_iff_getElem] at hp ⊢
intro k hk
rw [hqlen] at hk
have htake : (p.take (i + 1)).length = i + 1 := by
simp [List.length_take, hi]
by_cases hk2 : k + 1 < i + 1
· rw [List.getElem_append_left (by omega), List.getElem_append_left (by omega),
List.getElem_take, List.getElem_take]
exact hp k (by omega)
· by_cases hk3 : k < i
· omega
· by_cases hk4 : k = i
· subst hk4
rw [List.getElem_append_left (by omega), List.getElem_take]
rw [List.getElem_append_right (by omega), List.getElem_drop]
simpa only [htake, heq, Nat.sub_self, Nat.add_zero] using hp j (by omega)
· have hki : i + 1 ≤ k := by omega
rw [List.getElem_append_right (by omega), List.getElem_append_right (by omega),
List.getElem_drop, List.getElem_drop]
have he1 : j + 1 + (k - (i + 1)) = k + (j - i) := by omega
have he2 : j + 1 + (k + 1 - (i + 1)) = k + (j - i) + 1 := by omega
simpa only [htake, he1, he2] using hp (k + (j - i)) (by omega)
obtain ⟨q', hq'c, hq'n, hq'0, hq'l⟩ := ih q (by rw [hqlen]; omega) hqchain
refine ⟨q', hq'c, hq'n, ?_, ?_⟩
· rw [hq'0]
have h0 : q[0]? = p[0]? := by
simp only [hq_def, List.getElem?_append, List.getElem?_take]
simp [Nat.lt_add_one_iff, hi]
exact h0
· rw [hq'l]
by_cases hjl : j + 1 < p.length
· have hlast : q[q.length - 1]? = p[p.length - 1]? := by
rw [hqlen]
simp only [hq_def, List.getElem?_append, List.getElem?_take,
List.getElem?_drop]
have h1 : ¬ p.length - (j - i) - 1 < i + 1 := by omega
simp [h1]
congr 2
omega
exact hlast
· have hjeq : j + 1 = p.length := by omega
have hlast : q[q.length - 1]? = p[p.length - 1]? := by
rw [hqlen]
simp only [hq_def, List.getElem?_append, List.getElem?_take,
List.getElem?_drop]
have h1 : p.length - (j - i) - 1 < i + 1 := by omega
simp [h1]
have h2 : p.length - (j - i) - 1 = i := by omega
rw [h2]
have h3 : p.length - 1 = j := by omega
rw [h3]
simp [hi]
rw [hpj]
exact congrArg some heq
exact hlastA reflexive-transitive reachability proof between distinct endpoints contains a vertex-simple path of length at least two.
theorem exists_nodup_path_of_reflTransGen {α : Type*} [DecidableEq α] {r : α → α → Prop}
{a b : α} (h : Relation.ReflTransGen r a b) (hab : a ≠ b) :
∃ q : List α, q.IsChain r ∧ q.Nodup ∧ 2 ≤ q.length ∧
q[0]? = some a ∧ q[q.length - 1]? = some b := by
obtain ⟨p, hpc, hp0, hpl⟩ := exists_isChain_of_reflTransGen h
obtain ⟨q, hqc, hqn, hq0, hql⟩ := exists_nodup_isChain p hpc
refine ⟨q, hqc, hqn, ?_, by rw [hq0, hp0], by rw [hql, hpl]⟩
by_contra hlen
push Not at hlen
have hq0len : q.length = 0 ∨ q.length = 1 := by omega
rcases hq0len with hq0len | hq1len
· cases q with
| nil => simp [hp0] at hq0
| cons a l => simp at hq0len
· have h1 : q[0]? = q[q.length - 1]? := by simp [hq1len]
rw [hq0, hql] at h1
rw [hp0, hpl] at h1
exact hab (Option.some.inj h1)end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S4_Matching_Flow
S4. Residual edges of the matching flow
Computation of the residual-capacity structure of the §26.3 matching flow: the flow values on source, left, right, and sink arcs, and the exact residual-edge characterisations used by the reachability translation.
Main results:
-
matchingToFlow_f_source/matchingToFlow_f_right: unit flow exactly on matched vertices -
matchingToFlow_residualEdge_source/matchingToFlow_residualEdge_right: residual edges out of the source and into the sink -
matchingToFlow_residualEdge_inl_inl: residual edges inside the vertex set are non-matching graph edges forward and matching edges backward
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}Residual edges of the matching flow
The flow out of the source into a left vertex is 1 exactly when the
vertex is matched.
lemma matchingToFlow_f_source (M : Matching V G) (l : V) :
(matchingToFlow M).f (Sum.inr true) (Sum.inl l) =
if M.IsMatchedLeft l then (1 : ℝ) else 0 := by
have h1 : (matchingToFlow M).f (Sum.inr true) (Sum.inl l) =
((M.edges.filter fun e => e.1 = l).card : ℝ) := by
simp only [matchingToFlow, matchingFlowFun, matchingFlowFunSummand]
rw [← Finset.sum_filter]
simp
rw [h1]
by_cases h : M.IsMatchedLeft l
· simp only [h, ↓reduceIte]
obtain ⟨r, hr⟩ := h
have hcard : (M.edges.filter fun e => e.1 = l).card = 1 := by
rw [Finset.card_eq_one]
refine ⟨(l, r), Finset.eq_singleton_iff_unique_mem.mpr ⟨?_, ?_⟩⟩
· simp [hr]
· intro e he
simp only [Finset.mem_filter] at he
exact Prod.ext he.2 (M.h_unique_left l e.2 r (by rw [← he.2, Prod.mk.eta]; exact he.1) hr)
rw [hcard]
simp
· simp only [h, ↓reduceIte]
have hempty : (M.edges.filter fun e => e.1 = l) = ∅ := by
rw [Finset.filter_eq_empty_iff]
intro e he
intro he1
exact h ⟨e.2, by rwa [← he1]⟩
rw [hempty]
simp
The flow out of a right vertex into the sink is 1 exactly when the
vertex is matched.
lemma matchingToFlow_f_right (M : Matching V G) (r : V) :
(matchingToFlow M).f (Sum.inl r) (Sum.inr false) =
if M.IsMatchedRight r then (1 : ℝ) else 0 := by
have h1 : (matchingToFlow M).f (Sum.inl r) (Sum.inr false) =
((M.edges.filter fun e => e.2 = r).card : ℝ) := by
simp only [matchingToFlow, matchingFlowFun, matchingFlowFunSummand]
rw [← Finset.sum_filter]
simp
rw [h1]
by_cases h : M.IsMatchedRight r
· simp only [h, ↓reduceIte]
obtain ⟨l, hl⟩ := h
have hcard : (M.edges.filter fun e => e.2 = r).card = 1 := by
rw [Finset.card_eq_one]
refine ⟨(l, r), Finset.eq_singleton_iff_unique_mem.mpr ⟨?_, ?_⟩⟩
· simp [hl]
· intro e he
simp only [Finset.mem_filter] at he
exact Prod.ext (M.h_unique_right e.1 l r (by rw [← he.2, Prod.mk.eta]; exact he.1) hl) he.2
rw [hcard]
simp
· simp only [h, ↓reduceIte]
have hempty : (M.edges.filter fun e => e.2 = r) = ∅ := by
rw [Finset.filter_eq_empty_iff]
intro e he
intro he2
exact h ⟨e.1, by rwa [← he2]⟩
rw [hempty]
simp
The flow across an L→R pair is 1 on matching edges, -1 on reversed
matching edges, and 0 elsewhere.
lemma matchingToFlow_f_lr (M : Matching V G) (l r : V) :
(matchingToFlow M).f (Sum.inl l) (Sum.inl r) =
(if (l, r) ∈ M.edges then (1 : ℝ) else 0) +
(if (r, l) ∈ M.edges then (-1 : ℝ) else 0) := by
simp only [matchingToFlow, matchingFlowFun, matchingFlowFunSummand]
rw [Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.sum_ite_eq']A residual edge out of the source reaches exactly the unmatched left vertices.
lemma matchingToFlow_residualEdge_source (M : Matching V G) (l : V) :
Flow.residualEdge (matchingToFlow M) (Sum.inr true) (Sum.inl l) ↔
l ∈ G.L ∧ M.IsUnmatchedLeft l := by
unfold Flow.residualEdge Flow.residualCapacity
have hc : (toFlowNetwork V G).c (Sum.inr true) (Sum.inl l) =
if l ∈ G.L then (1 : ℝ) else 0 := by simp [toFlowNetwork, capFunc]
rw [hc, matchingToFlow_f_source]
by_cases hl : l ∈ G.L
· by_cases hm : M.IsMatchedLeft l
· obtain ⟨r, hr⟩ := hm
have hm' : M.IsMatchedLeft l := ⟨r, hr⟩
have hnot : ¬ M.IsUnmatchedLeft l := fun hu => hu r hr
simp [hl, hm', hnot]
· simp [hm, Matching.IsMatchedLeft] at hm ⊢
constructor
· intro _
exact ⟨hl, hm⟩
· intro _
by_cases hc : ∃ r, (l, r) ∈ M.edges
· rcases hc with ⟨r', hr'⟩
exact False.elim (hm r' hr')
· simp [hc, hl]
· have hnm : ¬ M.IsMatchedLeft l := fun h => hl (M.mem_L_of_isMatchedLeft h)
simp [hl, hnm]The source has no residual edges into the extra vertices.
lemma matchingToFlow_not_residualEdge_source_inr (M : Matching V G) (b : Bool) :
¬ Flow.residualEdge (matchingToFlow M) (Sum.inr true) (Sum.inr b) := by
unfold Flow.residualEdge Flow.residualCapacity
have hc : (toFlowNetwork V G).c (Sum.inr true) (Sum.inr b) = 0 := by
simp [toFlowNetwork, capFunc]
have hf : (matchingToFlow M).f (Sum.inr true) (Sum.inr b) = 0 := by
simp [matchingToFlow, matchingFlowFun, matchingFlowFunSummand]
rw [hc, hf]
norm_numResidual edges inside the vertex set are exactly the non-matching graph edges in the forward direction and the matching edges in the backward direction.
lemma matchingToFlow_residualEdge_inl_inl (M : Matching V G) (u v : V) :
Flow.residualEdge (matchingToFlow M) (Sum.inl u) (Sum.inl v) ↔
((u, v) ∈ G.E ∧ (u, v) ∉ M.edges) ∨ (v, u) ∈ M.edges := by
unfold Flow.residualEdge Flow.residualCapacity
have hc : (toFlowNetwork V G).c (Sum.inl u) (Sum.inl v) =
if (u, v) ∈ G.E then (1 : ℝ) else 0 := by simp [toFlowNetwork, capFunc]
rw [hc, matchingToFlow_f_lr]
by_cases huv : (u, v) ∈ M.edges
· have hnv : (v, u) ∉ M.edges := fun hcon =>
G.not_mem_L_of_mem_R (G.hE_subset _ (M.h_subset huv)).2 (G.hE_subset _ (M.h_subset hcon)).1
have hE : (u, v) ∈ G.E := M.h_subset huv
simp [huv, hnv, hE]
· by_cases hvu : (v, u) ∈ M.edges
· have hE : (u, v) ∉ G.E := fun hcon =>
G.not_mem_L_of_mem_R (G.hE_subset _ hcon).2 (G.hE_subset _ (M.h_subset hvu)).1
simp [huv, hvu, hE]
· by_cases hE : (u, v) ∈ G.E
· simp [huv, hvu, hE]
· simp [huv, hvu, hE]A residual edge into the sink leaves exactly the unmatched right vertices.
lemma matchingToFlow_residualEdge_right (M : Matching V G) (r : V) :
Flow.residualEdge (matchingToFlow M) (Sum.inl r) (Sum.inr false) ↔
r ∈ G.R ∧ M.IsUnmatchedRight r := by
unfold Flow.residualEdge Flow.residualCapacity
have hc : (toFlowNetwork V G).c (Sum.inl r) (Sum.inr false) =
if r ∈ G.R then (1 : ℝ) else 0 := by simp [toFlowNetwork, capFunc]
rw [hc, matchingToFlow_f_right]
by_cases hr : r ∈ G.R
· by_cases hm : M.IsMatchedRight r
· obtain ⟨l, hl⟩ := hm
have hm' : M.IsMatchedRight r := ⟨l, hl⟩
have hnot : ¬ M.IsUnmatchedRight r := fun hu => hu l hl
simp [hr, hm', hnot]
· simp [hm, Matching.IsMatchedRight] at hm ⊢
constructor
· intro _
exact ⟨hr, hm⟩
· intro _
by_cases hc : ∃ l, (l, r) ∈ M.edges
· rcases hc with ⟨l', hl'⟩
exact False.elim (hm l' hl')
· simp [hc, hr]
· have hnm : ¬ M.IsMatchedRight r := fun h => hr (M.mem_R_of_isMatchedRight h)
simp [hr, hnm]Left vertices have no residual edge into the sink.
lemma matchingToFlow_not_residualEdge_left_sink (M : Matching V G) {l : V}
(hl : l ∈ G.L) :
¬ Flow.residualEdge (matchingToFlow M) (Sum.inl l) (Sum.inr false) := by
unfold Flow.residualEdge Flow.residualCapacity
have hnr : l ∉ G.R := G.not_mem_R_of_mem_L hl
have hc : (toFlowNetwork V G).c (Sum.inl l) (Sum.inr false) = 0 := by
simp [toFlowNetwork, capFunc, hnr]
have hf : (matchingToFlow M).f (Sum.inl l) (Sum.inr false) = 0 := by
have h1 : (matchingToFlow M).f (Sum.inl l) (Sum.inr false) =
((M.edges.filter fun e => e.2 = l).card : ℝ) := by
simp only [matchingToFlow, matchingFlowFun, matchingFlowFunSummand]
rw [← Finset.sum_filter]
simp
have hempty : (M.edges.filter fun e => e.2 = l) = ∅ := by
rw [Finset.filter_eq_empty_iff]
intro e he he2
have := M.right_mem_R he
rw [he2] at this
exact hnr this
rw [h1, hempty]
simp
rw [hc, hf]
norm_numRight vertices have no residual edge into the source.
lemma matchingToFlow_not_residualEdge_right_source (M : Matching V G) {r : V}
(hr : r ∈ G.R) :
¬ Flow.residualEdge (matchingToFlow M) (Sum.inl r) (Sum.inr true) := by
unfold Flow.residualEdge Flow.residualCapacity
have hnl : r ∉ G.L := G.not_mem_L_of_mem_R hr
have hc : (toFlowNetwork V G).c (Sum.inl r) (Sum.inr true) = 0 := by
simp [toFlowNetwork, capFunc]
have hf : (matchingToFlow M).f (Sum.inl r) (Sum.inr true) = 0 := by
have hskew := (matchingToFlow M).hskew_symm (Sum.inl r) (Sum.inr true)
rw [matchingToFlow_f_source] at hskew
have hnm : ¬ M.IsMatchedLeft r := fun h => hnl (M.mem_L_of_isMatchedLeft h)
simp [hnm] at hskew
linarith
rw [hc, hf]
norm_numend Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S5_Residual_Translation
S5. From residual reachability to graph augmenting paths
The translation from §26.3 residual reachability to explicit §25.1
augmenting paths: the well-founded translation_inner walk-to-path
construction and the headline augmentingPath_of_hasAugmentingPath.
Main results:
-
translation_inner: a vertex-simple residual walk from an embedded left vertex to the sink induces an alternating path -
augmentingPath_of_hasAugmentingPath: a residual augmenting path of the matching flow induces a graph augmenting path
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}From residual reachability to graph augmenting paths
Project the embedded graph vertices from a residual-network walk.
def projectGraphVertices : List (V ⊕ Bool) → List V
| [] => []
| Sum.inl v :: rest => v :: projectGraphVertices rest
| Sum.inr _ :: rest => projectGraphVertices rest
Translation lemma (auxiliary, well-founded on the walk length): a
vertex-simple residual walk from an inl-embedded left vertex to the sink
induces an alternating path in the bipartite graph. The conclusion lists
exactly the IsAugmentingPath fields except the (unneeded here) start
unmatched condition, plus a membership tracker used for the no-repeat
arguments.
theorem translation_inner (M : Matching V G) (l : V) (hl : l ∈ G.L) :
∀ (w : List (V ⊕ Bool)), w.IsChain (Flow.residualEdge (matchingToFlow M)) →
w.Nodup → w[0]? = some (Sum.inl l) → w[w.length - 1]? = some (Sum.inr false) →
Sum.inr true ∉ w →
∃ p : List V, p.Nodup ∧ Even p.length ∧ 2 ≤ p.length ∧ p.head? = some l ∧
(∀ r₂ : V, p.getLast? = some r₂ → r₂ ∈ G.R ∧ M.IsUnmatchedRight r₂) ∧
(∀ e ∈ (altEdges p).1, e ∈ G.E ∧ e ∉ M.edges) ∧
(∀ e ∈ (altEdges p).2, e ∈ M.edges) ∧
(∀ v ∈ p, Sum.inl v ∈ w) ∧ p = projectGraphVertices w := by
suffices aux : ∀ (n : ℕ) (l : V) (hl : l ∈ G.L) (w : List (V ⊕ Bool)),
w.length ≤ n → w.IsChain (Flow.residualEdge (matchingToFlow M)) →
w.Nodup → w[0]? = some (Sum.inl l) → w[w.length - 1]? = some (Sum.inr false) →
Sum.inr true ∉ w →
∃ p : List V, p.Nodup ∧ Even p.length ∧ 2 ≤ p.length ∧ p.head? = some l ∧
(∀ r₂ : V, p.getLast? = some r₂ → r₂ ∈ G.R ∧ M.IsUnmatchedRight r₂) ∧
(∀ e ∈ (altEdges p).1, e ∈ G.E ∧ e ∉ M.edges) ∧
(∀ e ∈ (altEdges p).2, e ∈ M.edges) ∧
(∀ v ∈ p, Sum.inl v ∈ w) ∧ p = projectGraphVertices w from
fun w hw hnd h0 hlst hns => aux w.length l hl w le_rfl hw hnd h0 hlst hns
intro n
induction n with
| zero =>
intro l hl w hlen hw hnd h0 hlst hns
simp at hlen
subst hlen
simp at h0
| succ n ih =>
intro l hl w hlen hw hnd h0 hlst hns
cases w with
| nil => simp at h0
| cons x rest =>
simp only [List.length_cons, List.getElem?_cons_zero, Option.some.injEq] at h0
subst h0
cases rest with
| nil =>
simp only [List.length_cons, List.length_nil, Nat.add_zero, Nat.sub_self,
List.getElem?_cons_zero] at hlst
simp at hlst
| cons y rest' =>
have hstep0 : Flow.residualEdge (matchingToFlow M) (Sum.inl l) y := by
have hc := (List.isChain_iff_getElem.mp hw) 0 (by simp)
simpa using hc
cases y with
| inl r =>
have hiff := (matchingToFlow_residualEdge_inl_inl M l r).mp hstep0
rcases hiff with ⟨hE, hnotM⟩ | hcon
· have hr : r ∈ G.R := (G.hE_subset _ hE).2
cases rest' with
| nil =>
simp only [List.length_cons, List.length_nil] at hlst
norm_num at hlst
simp at hlst
| cons z rest'' =>
have hstep1 : Flow.residualEdge (matchingToFlow M) (Sum.inl r) z := by
have hc := (List.isChain_iff_getElem.mp hw) 1 (by simp)
simpa using hc
cases z with
| inl l₂ =>
have hiff1 := (matchingToFlow_residualEdge_inl_inl M r l₂).mp hstep1
rcases hiff1 with ⟨hE1, -⟩ | hback
· exact (G.not_mem_L_of_mem_R hr (G.hE_subset _ hE1).1).elim
· have hl₂ : l₂ ∈ G.L := (G.hE_subset _ (M.h_subset hback)).1
-- recurse on the tail `inl l₂ :: rest''`
have hw₂len : (Sum.inl l₂ :: rest'').length ≤ n := by
have hlen' : (Sum.inl l :: Sum.inl r :: Sum.inl l₂ :: rest'').length =
(Sum.inl l₂ :: rest'').length + 2 := by simp
rw [hlen'] at hlen
omega
have hw₂chain : (Sum.inl l₂ :: rest'').IsChain
(Flow.residualEdge (matchingToFlow M)) := by
rw [List.isChain_iff_getElem] at hw ⊢
intro i hi
have := hw (i + 2) (by simp at hi ⊢; omega)
simpa using this
have hw₂nodup : (Sum.inl l₂ :: rest'').Nodup := by
have h1 := hnd
rw [List.nodup_cons] at h1
exact h1.2.of_cons
have hw₂0 : (Sum.inl l₂ :: rest'')[0]? = some (Sum.inl l₂) := rfl
have hw₂last : (Sum.inl l₂ :: rest'')[(Sum.inl l₂ :: rest'').length - 1]? =
some (Sum.inr false) := by
have h1 : (Sum.inl l :: Sum.inl r :: Sum.inl l₂ :: rest'').length =
(Sum.inl l₂ :: rest'').length + 2 := by simp
have h2 : (Sum.inl l :: Sum.inl r :: Sum.inl l₂ :: rest'')[
(Sum.inl l :: Sum.inl r :: Sum.inl l₂ :: rest'').length - 1]? =
(Sum.inl l₂ :: rest'')[(Sum.inl l₂ :: rest'').length - 1]? := by
rw [h1]
simp [List.getElem?_cons_succ, Nat.add_sub_cancel]
rw [h2] at hlst
exact hlst
have hw₂ns : Sum.inr true ∉ Sum.inl l₂ :: rest'' := by
intro hcon
exact hns (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hcon))
obtain ⟨p', hp'n, hp'e, hp'ge, hp'head, hp'last, hp'fw,
hp'bw, hp'mem, hp'project⟩ :=
ih l₂ hl₂ (Sum.inl l₂ :: rest'') hw₂len hw₂chain hw₂nodup hw₂0 hw₂last hw₂ns
-- assemble `l :: r :: p'`
have hp'ne : p' ≠ [] := fun h => by simp [h] at hp'ge
obtain ⟨l₃, p'', hp'⟩ := List.exists_cons_of_ne_nil hp'ne
have hl₃ : l₃ = l₂ := by
rw [hp'] at hp'head
simp at hp'head
exact hp'head
rw [hp'] at hp'project
subst l₃
subst p'
refine ⟨l :: r :: l₂ :: p'', ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· have hlr : l ≠ r := fun h => G.not_mem_R_of_mem_L hl (h ▸ hr)
have hlnotin : l ∉ r :: l₂ :: p'' := by
intro hcon
simp only [List.mem_cons] at hcon
rcases hcon with hcon | hcon'
· exact hlr hcon
· rcases hcon' with hcon' | hcon'
· have h2 := hnd
rw [List.nodup_cons] at h2
exact h2.1 (by simpa [hcon'])
· have h1 := hp'mem l (List.mem_cons_of_mem l₂ hcon')
have h2 := hnd
rw [List.nodup_cons] at h2
exact h2.1 (List.mem_cons_of_mem _ h1)
have hrnotin : r ∉ l₂ :: p'' := by
intro hcon
simp only [List.mem_cons] at hcon
rcases hcon with hcon | hcon'
· exact G.not_mem_L_of_mem_R hr (hcon ▸ hl₂)
· have h1 := hp'mem r (List.mem_cons_of_mem l₂ hcon')
have h2 := hnd
rw [List.nodup_cons] at h2
obtain ⟨-, h2⟩ := h2
rw [List.nodup_cons] at h2
exact h2.1 h1
exact List.nodup_cons.mpr ⟨hlnotin,
List.nodup_cons.mpr ⟨hrnotin, hp'n⟩⟩
· simp at hp'e ⊢
exact hp'e.add (by norm_num : Even 2)
· simp [hp'ge]
· rfl
· intro r₂ hr₂
rw [List.getLast?_cons_cons, List.getLast?_cons_cons] at hr₂
exact hp'last r₂ hr₂
· intro e he
rw [altEdges.eq_def] at he
simp only [List.mem_cons] at he
rcases he with he | he
· rw [he]
exact ⟨hE, hnotM⟩
· exact hp'fw e he
· intro e he
rw [altEdges.eq_def] at he
simp only [List.mem_cons] at he
rcases he with he | he
· rw [he]
exact hback
· exact hp'bw e he
· intro v hv
simp only [List.mem_cons] at hv
rcases hv with rfl | rfl | hv
· exact List.mem_cons_self
· exact List.mem_cons_of_mem _ List.mem_cons_self
· rcases hv with rfl | hv
· exact List.mem_cons_of_mem _
(List.mem_cons_of_mem _ List.mem_cons_self)
· exact List.mem_cons_of_mem _
(List.mem_cons_of_mem _ (hp'mem v (List.mem_cons_of_mem _ hv)))
· simpa [projectGraphVertices] using congrArg (l :: r :: ·) hp'project
| inr b =>
cases b with
| true => exact absurd (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ List.mem_cons_self)) hns
| false =>
have hr_un := (matchingToFlow_residualEdge_right M r).mp hstep1
-- the sink must be the last vertex: `rest'' = []`
have hrest'' : rest'' = [] := by
cases rest'' with
| nil => rfl
| cons u rest''' =>
have hlast' : (Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''')[
(Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''').length - 1]? =
some (Sum.inr false) := hlst
have hget : (Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''')[
(Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''').length - 1] =
Sum.inr false := by
rw [List.getElem?_eq_getElem (by simp)] at hlast'
exact Option.some.inj hlast'
have hdup' : (Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''')[2] =
Sum.inr false := by simp
have hinj := List.Nodup.getElem_inj_iff hnd (i := 2) (hi := by simp)
(j := (Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''').length - 1)
(hj := by simp)
rw [hdup', hget] at hinj
rw [show (2 = (Sum.inl l :: Sum.inl r :: Sum.inr false :: u :: rest''').length - 1) =
False by simp] at hinj
exact False.elim (hinj.mp rfl)
subst hrest''
refine ⟨[l, r], ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· exact List.nodup_cons.mpr ⟨by
simp; exact fun h => G.not_mem_R_of_mem_L hl (h ▸ hr),
List.nodup_singleton _⟩
· norm_num
· norm_num
· rfl
· intro r₂ hr₂
rw [List.getLast?_cons_cons] at hr₂
simp at hr₂
subst hr₂
exact hr_un
· intro e he
simp [altEdges] at he
simpa [he] using ⟨hE, hnotM⟩
· intro e he
simp [altEdges] at he
· intro v hv
simp at hv
rcases hv with rfl | rfl
· exact List.mem_cons_self
· exact List.mem_cons_of_mem _ List.mem_cons_self
· rfl
· exact (G.not_mem_R_of_mem_L hl (G.hE_subset _ (M.h_subset hcon)).2).elim
| inr b =>
cases b with
| true => exact absurd (List.mem_cons_of_mem _ List.mem_cons_self) hns
| false => exact absurd hstep0 (matchingToFlow_not_residualEdge_left_sink M hl)Translation lemma: a residual augmenting path in the §26.3 flow network of a bipartite graph induces an augmenting path for the matching in the graph itself.
theorem augmentingPath_of_hasAugmentingPath (M : Matching V G)
(hpath : (matchingToFlow M).hasAugmentingPath) :
∃ p : List V, IsAugmentingPath G M p := by
have hne : Sum.inr true ≠ (Sum.inr false : V ⊕ Bool) := by simp
obtain ⟨q, hqchain, hqnodup, hqlen, hq0, hqend⟩ :=
exists_nodup_path_of_reflTransGen hpath hne
cases q with
| nil => simp at hq0
| cons x rest =>
simp only [List.getElem?_cons_zero, Option.some.injEq] at hq0
subst hq0
cases rest with
| nil => simp at hqlen
| cons y rest' =>
have hstep0 : Flow.residualEdge (matchingToFlow M) (Sum.inr true) y := by
have hc := (List.isChain_iff_getElem.mp hqchain) 0 (by simp)
simpa [toFlowNetwork] using hc
cases y with
| inl l =>
have ⟨hl, hlu⟩ := (matchingToFlow_residualEdge_source M l).mp hstep0
have hw : (Sum.inl l :: rest').IsChain (Flow.residualEdge (matchingToFlow M)) := by
rw [List.isChain_iff_getElem] at hqchain ⊢
intro i hi
have := hqchain (i + 1) (by simp at hi ⊢; omega)
simpa [toFlowNetwork] using this
have hwnd : (Sum.inl l :: rest').Nodup := hqnodup.of_cons
have hw0 : (Sum.inl l :: rest')[0]? = some (Sum.inl l) := rfl
have hwlast : (Sum.inl l :: rest')[(Sum.inl l :: rest').length - 1]? =
some (Sum.inr false) := by
have h1 : (Sum.inr true :: Sum.inl l :: rest')[(Sum.inr true :: Sum.inl l ::
rest').length - 1]? = (Sum.inl l :: rest')[(Sum.inl l :: rest').length - 1]? := by
simp [List.getElem?_cons_succ, List.length_cons]
rw [show (toFlowNetwork V G).s = Sum.inr true by rfl,
show (toFlowNetwork V G).t = Sum.inr false by rfl] at hqend
rw [h1] at hqend
exact hqend
have hwns : Sum.inr true ∉ Sum.inl l :: rest' := by
have h1 := hqnodup
rw [List.nodup_cons] at h1
exact h1.1
obtain ⟨p, hpn, hpe, hpge, hphead, hplast, hpfw, hpbw, -, -⟩ :=
translation_inner M l hl (Sum.inl l :: rest') hw hwnd hw0 hwlast hwns
have hpne : p ≠ [] := fun h => by simp [h] at hpge
refine ⟨p, hpn, hpe, hpge, ?_, ?_, ?_, ?_, hpfw, hpbw⟩
· intro h
have h1 : p.head h = l := by
have h2 : p.head? = some (p.head h) := List.head?_eq_some_head _
rw [hphead] at h2
exact (Option.some.inj h2).symm
rw [h1]
exact hl
· intro h r₂
have h1 : p.head h = l := by
have h2 : p.head? = some (p.head h) := List.head?_eq_some_head _
rw [hphead] at h2
exact (Option.some.inj h2).symm
rw [h1]
exact hlu r₂
· intro h
have h1 : p.getLast? = some (p.getLast h) := List.getLast?_eq_some_getLast hpne
obtain ⟨hr, -⟩ := hplast _ h1
exact hr
· intro h l₂
have h1 : p.getLast? = some (p.getLast h) := List.getLast?_eq_some_getLast hpne
obtain ⟨-, hu⟩ := hplast _ h1
exact hu l₂
| inr b => exact absurd hstep0 (matchingToFlow_not_residualEdge_source_inr M b)end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.S6_Berge_Flow_Method
S6. Berge's lemma and the flow-method headline
The section's closing theorems: Berge's maximum-matching characterisation and the flow-method existence and certification theorem.
Main results:
-
berge_maximum_iff_no_augmentingPath(Berge's lemma): a matching is maximum iff it admits no augmenting path -
flowMethod_finds_maximum_matching: a maximum matching exists, and the flow method certifies it
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}Berge's lemma and the flow-method headline
Berge's lemma (CLRS §25.1): a matching is maximum if and only if it admits no augmenting path.
theorem berge_maximum_iff_no_augmentingPath (M : Matching V G) :
M.IsMaximum ↔ ¬ ∃ p : List V, IsAugmentingPath G M p := by
constructor
· rintro hmax ⟨p, hp⟩
exact not_isMaximum_of_isAugmentingPath hp hmax
· intro hno
have hφ : ¬ (matchingToFlow M).hasAugmentingPath := fun h =>
hno (augmentingPath_of_hasAugmentingPath M h)
have hmaxφ := Flow.maximal_of_noAugmentingPath _ hφ
intro M'
have hle := hmaxφ (matchingToFlow M')
rw [matchingToFlow_value, matchingToFlow_value] at hle
exact_mod_cast hleFlow-method correctness (CLRS §25.1, revisited): a maximum matching exists, and the flow method certifies it — there is a maximal flow in the unit-capacity network whose value is exactly the size of a maximum matching.
theorem flowMethod_finds_maximum_matching (G : BipartiteGraph V) :
∃ M : Matching V G, M.IsMaximum ∧
∃ φ : Flow (V ⊕ Bool) (toFlowNetwork V G), φ.isMaximal ∧
φ.value = (M.size : ℝ) := by
obtain ⟨M, hM, φ, hφ, hval⟩ := maxMatching_eq_maxFlow_value (G := G)
exact ⟨M, hM, φ, hφ, hval⟩end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.Model
Cost vocabulary for the adjacency-list §25.1 execution
These definitions state the textbook adjacency-list budget vocabulary for the
support of the unit-capacity flow network. The legacy residualBFS still
enumerates the finite vertex universe; CostedSupportBFS and CostedRun
provide the separate support-indexed execution and its attached O(VE)
theorem.
namespace CLRSnamespace Matchingsopen Finset Classicalopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]Number of forward support arcs in the bipartite flow network.
def flowArcCount (G : BipartiteGraph V) : ℕ :=
G.L.card + G.E.card + G.R.cardNumber of vertices in the flow network, including source and sink.
def flowVertexCount (V : Type*) [Fintype V] : ℕ :=
Fintype.card (V ⊕ Bool)Coarse adjacency-list specification budget for one residual BFS.
def adjacencyBFSBudget (G : BipartiteGraph V) : ℕ :=
flowVertexCount V + 2 * flowArcCount GCoarse specification budget for updating a simple augmenting path.
def pathUpdateBudget (_G : BipartiteGraph V) : ℕ :=
flowVertexCount VCoarse specification budget for one adjacency-list augmentation attempt.
def augmentationAttemptBudget (G : BipartiteGraph V) : ℕ :=
adjacencyBFSBudget G + pathUpdateBudget GThe two bipartition sizes add up to the number of graph vertices.
theorem partition_card (G : BipartiteGraph V) :
G.L.card + G.R.card = Fintype.card V := by
have hd : Disjoint G.L G.R :=
Finset.disjoint_iff_inter_eq_empty.mpr G.h_disjoint
rw [← Finset.card_union_of_disjoint hd, G.h_cover]
simpThe constructed network has one support arc per graph vertex plus one arc per graph edge.
theorem flowArcCount_eq (G : BipartiteGraph V) :
flowArcCount G = Fintype.card V + G.E.card := by
unfold flowArcCount
have h := partition_card G
omegaomit [DecidableEq V] in
@[simp]
theorem flowVertexCount_eq :
flowVertexCount V = Fintype.card V + 2 := by
simp [flowVertexCount]
The number of possible matching augmentations is at most |V|.
theorem left_card_le_vertex_card (G : BipartiteGraph V) :
G.L.card ≤ Fintype.card V := by
exact Finset.card_le_card (Finset.subset_univ G.L)The target per-attempt budget is linear in the number of support arcs.
This arithmetic lemma is a coarse specification bound; it is not a cost
theorem about the legacy all-vertices residualBFS. The attached execution
theorem is costedMatchingRun_work_le_product.
theorem augmentationAttemptBudget_le (G : BipartiteGraph V) :
augmentationAttemptBudget G ≤ 4 * (flowArcCount G + 1) := by
simp only [augmentationAttemptBudget, adjacencyBFSBudget, pathUpdateBudget,
flowVertexCount_eq]
rw [flowArcCount_eq]
omegaend Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.Step
BFS-selected unit-capacity augmentation
This module defines the flow iteration used by the executable §25.1 algorithm. Unlike the abstract existence-level loop, an active step augments along the shortest path reconstructed by the executable residual BFS.
namespace CLRSnamespace Matchingsopen Finset Classicalopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]One BFS-selected augmentation step in the bipartite flow network.
noncomputable def bfsFlowStep (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) :
Flow (V ⊕ Bool) (toFlowNetwork V G) :=
if h : φ.hasAugmentingPath then
φ.augment (bfs_shortestAugmenting φ h).path
else φtheorem bfsFlowStep_of_hasAugmentingPath (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (h : φ.hasAugmentingPath) :
bfsFlowStep G φ = φ.augment (bfs_shortestAugmenting φ h).path := by
simp [bfsFlowStep, h]theorem bfsFlowStep_of_noAugmentingPath (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (h : ¬ φ.hasAugmentingPath) :
bfsFlowStep G φ = φ := by
simp [bfsFlowStep, h]The BFS step preserves integrality on the unit-capacity network.
theorem bfsFlowStep_integral (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral) :
(bfsFlowStep G φ).IsIntegral := by
by_cases h : φ.hasAugmentingPath
· rw [bfsFlowStep_of_hasAugmentingPath G φ h]
exact IsIntegral_augment φ hint toFlowNetwork_integral_capacity _
· rw [bfsFlowStep_of_noAugmentingPath G φ h]
exact hintAn active BFS step increases the integral flow value by at least one.
theorem bfsFlowStep_value_ge_one (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (hint : φ.IsIntegral)
(h : φ.hasAugmentingPath) :
φ.value + 1 ≤ (bfsFlowStep G φ).value := by
rw [bfsFlowStep_of_hasAugmentingPath G φ h]
exact augment_value_ge_one φ hint toFlowNetwork_integral_capacity _Iterate the BFS step from an arbitrary starting flow.
noncomputable def bfsFlowIterFrom (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) : ℕ →
Flow (V ⊕ Bool) (toFlowNetwork V G)
| 0 => φ
| n + 1 => bfsFlowStep G (bfsFlowIterFrom G φ n)The §25.1 flow iteration starts from the zero flow.
noncomputable def bfsFlowIter (G : BipartiteGraph V) (n : ℕ) :
Flow (V ⊕ Bool) (toFlowNetwork V G) :=
bfsFlowIterFrom G (zeroFlow (toFlowNetwork V G)) n@[simp]
theorem bfsFlowIterFrom_zero (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) :
bfsFlowIterFrom G φ 0 = φ := rfl@[simp]
theorem bfsFlowIterFrom_succ (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (n : ℕ) :
bfsFlowIterFrom G φ (n + 1) = bfsFlowStep G (bfsFlowIterFrom G φ n) := rflIteration composes over addition of step counts.
theorem bfsFlowIterFrom_add (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G)) (m n : ℕ) :
bfsFlowIterFrom G φ (m + n) =
bfsFlowIterFrom G (bfsFlowIterFrom G φ m) n := by
induction n with
| zero => simp
| succ n ih =>
rw [Nat.add_succ, bfsFlowIterFrom_succ, bfsFlowIterFrom_succ, ih]Once no augmenting path exists, every later iterate is the same flow.
theorem bfsFlowIterFrom_eq_of_noAugmentingPath (G : BipartiteGraph V)
(φ : Flow (V ⊕ Bool) (toFlowNetwork V G))
(h : ¬ φ.hasAugmentingPath) :
∀ n, bfsFlowIterFrom G φ n = φ := by
intro n
induction n with
| zero => rfl
| succ n ih =>
rw [bfsFlowIterFrom_succ, ih, bfsFlowStep_of_noAugmentingPath G φ h]A later augmenting path implies that all earlier iterates also had one.
theorem bfsFlowIter_hasAugmentingPath_of_le (G : BipartiteGraph V)
{i j : ℕ} (hij : i ≤ j)
(hj : (bfsFlowIter G j).hasAugmentingPath) :
(bfsFlowIter G i).hasAugmentingPath := by
by_contra hi
have hji : j = i + (j - i) := by omega
have hstable := bfsFlowIterFrom_eq_of_noAugmentingPath G (bfsFlowIter G i) hi (j - i)
have heq : bfsFlowIter G j = bfsFlowIter G i := by
unfold bfsFlowIter
rw [hji, bfsFlowIterFrom_add]
change bfsFlowIterFrom G (bfsFlowIter G i) (j - i) = bfsFlowIter G i
exact hstable
rw [heq] at hj
exact hi hjEvery iterate from the zero flow is integral.
theorem bfsFlowIter_integral (G : BipartiteGraph V) :
∀ n, (bfsFlowIter G n).IsIntegral := by
intro n
induction n with
| zero =>
exact IsIntegral_zero
| succ n ih =>
simpa [bfsFlowIter, bfsFlowIterFrom] using bfsFlowStep_integral G _ ih
The source cut of the constructed network has capacity exactly |L|.
theorem matchingNetwork_sourceCut (G : BipartiteGraph V) :
∑ v : V ⊕ Bool,
(toFlowNetwork V G).c (toFlowNetwork V G).s v = (G.L.card : ℝ) := by
simp [toFlowNetwork, capFunc]Every iterate is bounded by the source cut.
theorem bfsFlowIter_value_le_left_card (G : BipartiteGraph V) (n : ℕ) :
(bfsFlowIter G n).value ≤ (G.L.card : ℝ) := by
rw [← matchingNetwork_sourceCut G]
exact value_le_source_cut (bfsFlowIter G n)
If the first n iterates all admit augmentation, the nth flow has
value at least n.
theorem bfsFlowIter_value_ge_of_prefix (G : BipartiteGraph V) (n : ℕ)
(hsteps : ∀ i < n, (bfsFlowIter G i).hasAugmentingPath) :
(n : ℝ) ≤ (bfsFlowIter G n).value := by
induction n with
| zero => simp [bfsFlowIter, bfsFlowIterFrom, zeroFlow, Flow.value]
| succ n ih =>
have hn : (bfsFlowIter G n).hasAugmentingPath := hsteps n (by omega)
have hprefix : ∀ i < n, (bfsFlowIter G i).hasAugmentingPath :=
fun i hi => hsteps i (by omega)
have hge := ih hprefix
have hinc := bfsFlowStep_value_ge_one G (bfsFlowIter G n)
(bfsFlowIter_integral G n) hn
have hnext : bfsFlowIter G (n + 1) = bfsFlowStep G (bfsFlowIter G n) := rfl
rw [hnext]
push_cast
linarithend Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.Run
The §25.1 BFS-selected flow run
The flow and number of successful augmentations are advanced together. The
current Chapter 24 residual BFS enumerates all finite vertices; consequently
this module makes no adjacency-list O(VE) claim.
namespace CLRSnamespace Matchingsopen Finset Classicalopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]State returned by a fixed number of BFS augmentation attempts.
Current feasible flow.
Number of attempts whose input flow admitted an augmenting path.
structure FlowRun (G : BipartiteGraph V) where flow : Flow (V ⊕ Bool) (toFlowNetwork V G) augmentations : ℕ
Run n BFS augmentation attempts from the zero flow, accumulating the
successful-augmentation counter in the same recursion.
noncomputable def flowRun (G : BipartiteGraph V) : ℕ → FlowRun G
| 0 =>
{ flow := zeroFlow (toFlowNetwork V G)
augmentations := 0 }
| n + 1 =>
let previous := flowRun G n
{ flow := bfsFlowStep G previous.flow
augmentations := previous.augmentations +
if previous.flow.hasAugmentingPath then 1 else 0 }Erasing the augmentation counter gives the BFS flow iteration.
theorem flowRun_flow (G : BipartiteGraph V) :
∀ n, (flowRun G n).flow = bfsFlowIter G n := by
intro n
induction n with
| zero => rfl
| succ n ih =>
simp only [flowRun]
rw [ih]
rflThere is at most one successful augmentation per attempted step.
theorem flowRun_augmentations_le (G : BipartiteGraph V) :
∀ n, (flowRun G n).augmentations ≤ n := by
intro n
induction n with
| zero => simp [flowRun]
| succ n ih =>
simp only [flowRun]
split_ifs <;> omegaEvery flow stored by the run is integral.
theorem flowRun_integral (G : BipartiteGraph V) (n : ℕ) :
(flowRun G n).flow.IsIntegral := by
rw [flowRun_flow]
exact bfsFlowIter_integral G n
After |L| BFS attempts the unit-capacity flow has no augmenting path.
If the final flow still had a path, stability would imply that all earlier
flows had paths. Their integral values would therefore reach at least
|L|, and one more active step would exceed the source cut of capacity
|L|.
theorem bfsFlowIter_noAugmentingPath_left_card (G : BipartiteGraph V) :
¬ (bfsFlowIter G G.L.card).hasAugmentingPath := by
intro hfinal
have hprefix : ∀ i < G.L.card, (bfsFlowIter G i).hasAugmentingPath := by
intro i hi
exact bfsFlowIter_hasAugmentingPath_of_le G (by omega) hfinal
have hge := bfsFlowIter_value_ge_of_prefix G G.L.card hprefix
have hinc := bfsFlowStep_value_ge_one G (bfsFlowIter G G.L.card)
(bfsFlowIter_integral G G.L.card) hfinal
have hle := bfsFlowIter_value_le_left_card G (G.L.card + 1)
have hnext : bfsFlowIter G (G.L.card + 1) =
bfsFlowStep G (bfsFlowIter G G.L.card) := rfl
rw [hnext] at hle
linarith
The flow returned after |L| attempts is maximal.
theorem flowRun_maximal (G : BipartiteGraph V) :
(flowRun G G.L.card).flow.isMaximal := by
apply Flow.maximal_of_noAugmentingPath
rw [flowRun_flow]
exact bfsFlowIter_noAugmentingPath_left_card G
The successful-augmentation count of the textbook run is at most |V|.
theorem flowRun_augmentations_le_vertex_card (G : BipartiteGraph V) :
(flowRun G G.L.card).augmentations ≤ Fintype.card V := by
exact (flowRun_augmentations_le G G.L.card).trans
(left_card_le_vertex_card G)end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.Refinement
Matching refinement and the executable §25.1 headline
Every integral state of the costed flow run is refined to a matching of the
same value. The final state is a maximal flow, so its recovered matching is
maximum. The executable run also bounds the number of augmentations; an
attached adjacency-list work theorem is supplied by the sibling CostedRun
module, while this file remains the semantic flow reference.
namespace CLRSnamespace Matchingsopen Finset Classicalopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]
Matching recovered from the integral flow stored after n
augmentation attempts.
noncomputable def flowMatchingAt (G : BipartiteGraph V) (n : ℕ) : Matching V G :=
matchingOfIntegralFlow (flowRun G n).flow (flowRun_integral G n)At every index, the recovered matching size is exactly the flow value.
theorem flowMatchingAt_size (G : BipartiteGraph V) (n : ℕ) :
((flowMatchingAt G n).size : ℝ) = (flowRun G n).flow.value := by
exact matchingOfIntegralFlow_size _ _Every successful BFS augmentation strictly grows the recovered matching size (in fact by at least one).
theorem flowMatchingAt_size_increase (G : BipartiteGraph V) (n : ℕ)
(h : (flowRun G n).flow.hasAugmentingPath) :
(flowMatchingAt G n).size + 1 ≤ (flowMatchingAt G (n + 1)).size := by
have hinc := bfsFlowStep_value_ge_one G (flowRun G n).flow
(flowRun_integral G n) h
have hstep : (flowRun G (n + 1)).flow =
bfsFlowStep G (flowRun G n).flow := by
simp [flowRun]
rw [← hstep, ← flowMatchingAt_size G n, ← flowMatchingAt_size G (n + 1)] at hinc
exact_mod_cast hinc
The matching recovered after |L| attempts is maximum.
theorem flowMatchingAt_maximum (G : BipartiteGraph V) :
(flowMatchingAt G G.L.card).IsMaximum := by
intro M'
have hle := flowRun_maximal G (matchingToFlow M')
rw [matchingToFlow_value, ← flowMatchingAt_size G G.L.card] at hle
exact_mod_cast hle
Executable bipartite-flow method (CLRS §25.1). One concrete BFS
augmentation run returns a maximum matching and a maximal integral flow of
the same value and records at most |V| augmentations.
theorem flowMethod_finds_maximum_matching_with_bfs (G : BipartiteGraph V) :
let run := flowRun G G.L.card
let M := flowMatchingAt G G.L.card
M.IsMaximum ∧
run.flow.isMaximal ∧
run.flow.IsIntegral ∧
run.flow.value = (M.size : ℝ) ∧
run.augmentations ≤ Fintype.card V := by
dsimp only
exact ⟨flowMatchingAt_maximum G,
flowRun_maximal G,
flowRun_integral G G.L.card,
(flowMatchingAt_size G G.L.card).symm,
flowRun_augmentations_le_vertex_card G⟩end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.ResidualSupport
Residual support of a bipartite matching flow
The constructed network has one forward support arc for every left vertex, graph edge, and right vertex. Residual search needs at most the two orientations of those arcs. This file defines that finite support, proves its exact cardinality and residual coverage, and builds the indexed adjacency used by the costed BFS.
namespace CLRSopen Finset Classicalnamespace Chapter26variable {W : Type*} [Fintype W] [DecidableEq W] {N : FlowNetwork W}Every residual edge is supported by a nonzero capacity in its forward or reverse direction.
theorem Flow.residualEdge_implies_capacity_support (φ : Flow W N) {u v : W}
(hres : Flow.residualEdge φ u v) : N.c u v ≠ 0 ∨ N.c v u ≠ 0 := by
by_contra h
rw [not_or] at h
have huv : N.c u v = 0 := not_ne_iff.mp h.1
have hvu : N.c v u = 0 := not_ne_iff.mp h.2
have hnonneg : 0 ≤ φ.f u v := Flow.nonneg_of_zero_reverse_cap φ u v hvu
unfold Flow.residualEdge Flow.residualCapacity at hres
rw [huv] at hres
linarithend Chapter26namespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]Source-to-left support arcs.
noncomputable def matchingFlowSourceSupport (G : BipartiteGraph V) :
Finset ((V ⊕ Bool) × (V ⊕ Bool)) :=
G.L.image fun l => (Sum.inr true, Sum.inl l)Embedded left-to-right graph arcs.
noncomputable def matchingFlowGraphSupport (G : BipartiteGraph V) :
Finset ((V ⊕ Bool) × (V ⊕ Bool)) :=
G.E.image fun e => (Sum.inl e.1, Sum.inl e.2)Right-to-sink support arcs.
noncomputable def matchingFlowSinkSupport (G : BipartiteGraph V) :
Finset ((V ⊕ Bool) × (V ⊕ Bool)) :=
G.R.image fun r => (Sum.inl r, Sum.inr false)All forward support arcs of the matching flow network.
noncomputable def matchingFlowForwardSupport (G : BipartiteGraph V) :
Finset ((V ⊕ Bool) × (V ⊕ Bool)) :=
matchingFlowSourceSupport G ∪ matchingFlowGraphSupport G ∪
matchingFlowSinkSupport GReverse one directed arc.
def reverseArc {α : Type*} (e : α × α) : α × α := (e.2, e.1)@[simp]
theorem reverseArc_reverseArc {α : Type*} (e : α × α) :
reverseArc (reverseArc e) = e := by
rcases e with ⟨u, v⟩
rfltheorem reverseArc_injective {α : Type*} : Function.Injective (@reverseArc α) :=
Function.LeftInverse.injective reverseArc_reverseArcCandidate residual arcs: both orientations of every forward support arc.
noncomputable def matchingFlowResidualSupport (G : BipartiteGraph V) :
Finset ((V ⊕ Bool) × (V ⊕ Bool)) :=
matchingFlowForwardSupport G ∪
(matchingFlowForwardSupport G).image reverseArctheorem matchingFlowSourceSupport_card (G : BipartiteGraph V) :
(matchingFlowSourceSupport G).card = G.L.card := by
exact Finset.card_image_of_injective G.L (by
intro a b h
exact Sum.inl.inj (Prod.mk.inj h).2)theorem matchingFlowGraphSupport_card (G : BipartiteGraph V) :
(matchingFlowGraphSupport G).card = G.E.card := by
exact Finset.card_image_of_injective G.E (by
intro a b h
exact Prod.ext (Sum.inl.inj (Prod.mk.inj h).1)
(Sum.inl.inj (Prod.mk.inj h).2))theorem matchingFlowSinkSupport_card (G : BipartiteGraph V) :
(matchingFlowSinkSupport G).card = G.R.card := by
exact Finset.card_image_of_injective G.R (by
intro a b h
exact Sum.inl.inj (Prod.mk.inj h).1)
theorem matchingFlowSourceSupport_disjoint_graph (G : BipartiteGraph V) :
Disjoint (matchingFlowSourceSupport G) (matchingFlowGraphSupport G) := by
rw [Finset.disjoint_left]
intro e hs hg
rcases Finset.mem_image.mp hs with ⟨l, _, rfl⟩
rcases Finset.mem_image.mp hg with ⟨e, _, h⟩
simp at h
theorem matchingFlowSourceSupport_disjoint_sink (G : BipartiteGraph V) :
Disjoint (matchingFlowSourceSupport G) (matchingFlowSinkSupport G) := by
rw [Finset.disjoint_left]
intro e hs ht
rcases Finset.mem_image.mp hs with ⟨l, _, rfl⟩
rcases Finset.mem_image.mp ht with ⟨r, _, h⟩
simp at h
theorem matchingFlowGraphSupport_disjoint_sink (G : BipartiteGraph V) :
Disjoint (matchingFlowGraphSupport G) (matchingFlowSinkSupport G) := by
rw [Finset.disjoint_left]
intro e hg ht
rcases Finset.mem_image.mp hg with ⟨e, _, rfl⟩
rcases Finset.mem_image.mp ht with ⟨r, _, h⟩
simp at hExact number of forward support arcs.
theorem matchingFlowForwardSupport_card (G : BipartiteGraph V) :
(matchingFlowForwardSupport G).card = flowArcCount G := by
have hsg := matchingFlowSourceSupport_disjoint_graph G
have hst := matchingFlowSourceSupport_disjoint_sink G
have hgt := matchingFlowGraphSupport_disjoint_sink G
have hus : Disjoint
(matchingFlowSourceSupport G ∪ matchingFlowGraphSupport G)
(matchingFlowSinkSupport G) :=
Finset.disjoint_union_left.mpr ⟨hst, hgt⟩
rw [matchingFlowForwardSupport,
Finset.card_union_of_disjoint hus,
Finset.card_union_of_disjoint hsg,
matchingFlowSourceSupport_card,
matchingFlowGraphSupport_card,
matchingFlowSinkSupport_card]
rflA forward support never contains the reverse of one of its arcs.
theorem matchingFlowForwardSupport_no_reverse (G : BipartiteGraph V) {u v : V ⊕ Bool}
(h : (u, v) ∈ matchingFlowForwardSupport G) :
(v, u) ∉ matchingFlowForwardSupport G := by
rw [matchingFlowForwardSupport] at h
rcases Finset.mem_union.mp h with hsg | ht
· rcases Finset.mem_union.mp hsg with hs | hg
· rcases Finset.mem_image.mp hs with ⟨l, hl, huv⟩
have hu : Sum.inr true = u := congrArg Prod.fst huv
have hv : Sum.inl l = v := congrArg Prod.snd huv
subst u
subst v
simp [matchingFlowForwardSupport, matchingFlowSourceSupport,
matchingFlowGraphSupport, matchingFlowSinkSupport]
· rcases Finset.mem_image.mp hg with ⟨e, he, huv⟩
have heL := (G.hE_subset e he).1
have heR := (G.hE_subset e he).2
have hu : Sum.inl e.1 = u := congrArg Prod.fst huv
have hv : Sum.inl e.2 = v := congrArg Prod.snd huv
subst u
subst v
intro hrev
have hrevE : (e.2, e.1) ∈ G.E := by
simpa [matchingFlowForwardSupport, matchingFlowSourceSupport,
matchingFlowGraphSupport, matchingFlowSinkSupport] using hrev
exact G.not_mem_L_of_mem_R heR (G.hE_subset _ hrevE).1
· rcases Finset.mem_image.mp ht with ⟨r, hr, huv⟩
have hu : Sum.inl r = u := congrArg Prod.fst huv
have hv : Sum.inr false = v := congrArg Prod.snd huv
subst u
subst v
simp [matchingFlowForwardSupport, matchingFlowSourceSupport,
matchingFlowGraphSupport, matchingFlowSinkSupport]
theorem matchingFlowForwardSupport_disjoint_reverse (G : BipartiteGraph V) :
Disjoint (matchingFlowForwardSupport G)
((matchingFlowForwardSupport G).image reverseArc) := by
rw [Finset.disjoint_left]
intro e he hre
rcases Finset.mem_image.mp hre with ⟨x, hx, hxe⟩
have hxe' : x = reverseArc e := by
have := congrArg reverseArc hxe
simpa using this
subst x
exact matchingFlowForwardSupport_no_reverse G he hxExact number of oriented residual candidates.
theorem matchingFlowResidualSupport_card (G : BipartiteGraph V) :
(matchingFlowResidualSupport G).card = 2 * flowArcCount G := by
rw [matchingFlowResidualSupport,
Finset.card_union_of_disjoint (matchingFlowForwardSupport_disjoint_reverse G),
Finset.card_image_of_injective _ reverseArc_injective,
matchingFlowForwardSupport_card]
omegatheorem capacity_ne_zero_iff_mem_matchingFlowForwardSupport
(G : BipartiteGraph V) (u v : V ⊕ Bool) :
(toFlowNetwork V G).c u v ≠ 0 ↔ (u, v) ∈ matchingFlowForwardSupport G := by
cases u with
| inl a =>
cases v with
| inl b =>
simp [toFlowNetwork, capFunc, matchingFlowForwardSupport,
matchingFlowSourceSupport, matchingFlowGraphSupport,
matchingFlowSinkSupport]
| inr b =>
cases b <;>
simp [toFlowNetwork, capFunc, matchingFlowForwardSupport,
matchingFlowSourceSupport, matchingFlowGraphSupport,
matchingFlowSinkSupport]
| inr a =>
cases a <;> cases v with
| inl b =>
simp [toFlowNetwork, capFunc, matchingFlowForwardSupport,
matchingFlowSourceSupport, matchingFlowGraphSupport,
matchingFlowSinkSupport]
| inr b =>
cases b <;>
simp [toFlowNetwork, capFunc, matchingFlowForwardSupport,
matchingFlowSourceSupport, matchingFlowGraphSupport,
matchingFlowSinkSupport]Every residual edge of a matching flow lies in the fixed oriented support.
theorem matchingFlowResidualSupport_covers {G : BipartiteGraph V}
(M : Matching V G) {u v : V ⊕ Bool}
(hres : Flow.residualEdge (matchingToFlow M) u v) :
(u, v) ∈ matchingFlowResidualSupport G := by
rcases Flow.residualEdge_implies_capacity_support (matchingToFlow M) hres with
hforward | hreverse
· exact Finset.mem_union_left _
((capacity_ne_zero_iff_mem_matchingFlowForwardSupport G u v).1 hforward)
· apply Finset.mem_union_right
apply Finset.mem_image.mpr
exact ⟨(v, u),
(capacity_ne_zero_iff_mem_matchingFlowForwardSupport G v u).1 hreverse,
rfl⟩
Indexed oriented support for all matching states of G.
noncomputable def matchingFlowAdjacency (G : BipartiteGraph V) :
SupportBuild (V ⊕ Bool) :=
buildSupportAdjacency (matchingFlowResidualSupport G)
theorem matchingFlowAdjacency_work (G : BipartiteGraph V) :
(matchingFlowAdjacency G).work = 2 * flowArcCount G := by
rw [matchingFlowAdjacency, buildSupportAdjacency_work,
matchingFlowResidualSupport_card]
theorem matchingFlowAdjacency_storage (G : BipartiteGraph V) :
(matchingFlowAdjacency G).adjacency.storage = 2 * flowArcCount G := by
rw [matchingFlowAdjacency, buildSupportAdjacency_storage,
matchingFlowResidualSupport_card]Filtering a pre-indexed bucket by the current matching-flow residual predicate gives exactly the old semantic residual neighborhood.
theorem matchingFlowAdjacency_residualAdj {G : BipartiteGraph V}
(M : Matching V G) (u : V ⊕ Bool) :
((matchingFlowAdjacency G).adjacency.bucket u).filter
(fun v => Flow.residualEdge (matchingToFlow M) u v) =
residualAdj (matchingToFlow M) u := by
ext v
simp only [Finset.mem_filter, mem_residualAdj]
constructor
· exact fun h => h.2
· intro hres
refine ⟨?_, hres⟩
rw [matchingFlowAdjacency, mem_buildSupportAdjacency]
exact matchingFlowResidualSupport_covers M hresend Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.CostedBFS
Costed residual BFS for matching flows
This file specializes support-indexed residual BFS to the bipartite matching network. It also recovers the parent chain produced by that same BFS run and translates that concrete residual path to a graph augmenting path. No second reachability search or arbitrary path choice occurs in the translation.
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]The precomputed matching-flow adjacency covers the residual edges of every matching state.
theorem matchingFlowSupportsResidual {G : BipartiteGraph V}
(M : Matching V G) :
SupportsResidual (matchingFlowAdjacency G).adjacency (matchingToFlow M) := by
intro u v hres
rw [matchingFlowAdjacency, mem_buildSupportAdjacency]
exact matchingFlowResidualSupport_covers M hresMatching residual BFS over an already-built support adjacency.
noncomputable def matchingCostedBFSWith {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G) :
CostedBFSRun (V ⊕ Bool) :=
costedResidualBFS A (matchingToFlow M)theorem matchingCostedBFSWith_state {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) :
(matchingCostedBFSWith A M).state = residualBFS (matchingToFlow M) := by
exact costedResidualBFS_state A _ covertheorem matchingCostedBFSWith_work_le {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) :
(matchingCostedBFSWith A M).work ≤ flowVertexCount V + 4 * A.storage := by
simpa [matchingCostedBFSWith, flowVertexCount] using
costedResidualBFS_work_le A (matchingToFlow M) cover
theorem matchingCostedBFSWith_distance {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
(residualBFS (matchingToFlow M)).distance (Sum.inr false) = some d := by
rw [← matchingCostedBFSWith_state A M cover]
exact hd
One support-indexed BFS execution for the residual network of M.
noncomputable def matchingCostedBFS {G : BipartiteGraph V} (M : Matching V G) :
CostedBFSRun (V ⊕ Bool) :=
matchingCostedBFSWith (matchingFlowAdjacency G).adjacency MErasing the counter gives the established semantic residual BFS state.
theorem matchingCostedBFS_state {G : BipartiteGraph V} (M : Matching V G) :
(matchingCostedBFS M).state = residualBFS (matchingToFlow M) := by
exact costedResidualBFS_state _ _ (matchingFlowSupportsResidual M)The actual bucket-scanning execution is linear in the flow vertices and the two orientations of each capacity-support arc.
theorem matchingCostedBFS_work_le {G : BipartiteGraph V} (M : Matching V G) :
(matchingCostedBFS M).work ≤ flowVertexCount V + 8 * flowArcCount G := by
have h := costedResidualBFS_work_le (matchingFlowAdjacency G).adjacency
(matchingToFlow M) (matchingFlowSupportsResidual M)
rw [matchingFlowAdjacency_storage] at h
change (matchingCostedBFS M).work ≤
Fintype.card (V ⊕ Bool) + 8 * flowArcCount G
change (costedResidualBFS (matchingFlowAdjacency G).adjacency
(matchingToFlow M)).work ≤ _
omegaTransport a sink-distance observation from the costed state to the semantic residual BFS state.
theorem matchingCostedBFS_distance {G : BipartiteGraph V} (M : Matching V G)
{d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
(residualBFS (matchingToFlow M)).distance (Sum.inr false) = some d := by
rw [← matchingCostedBFS_state M]
exact hdThe exact residual parent path recovered from a matching BFS run, together with the work used to build its vertex list.
structure MatchingBFSPathRecovery {G : BipartiteGraph V} (M : Matching V G)
where
path : Flow.ResidualPath (matchingToFlow M) (Sum.inr true) (Sum.inr false)
work : NatRecover a parent path from a BFS over an explicitly supplied, already built support adjacency.
noncomputable def matchingBFSPathRecoveryWith {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
MatchingBFSPathRecovery M := by
let hd' := matchingCostedBFSWith_distance A M cover hd
let invariant := residualBFS_distanceInvariant (matchingToFlow M)
let parentPath := invariant.parentPath_of_distance hd'
let recovered := BFSParentPath.verticesWithCost parentPath
exact
{ path :=
{ vertices := recovered.vertices
chain := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_chain invariant
head_eq := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_head
last_eq := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_getLast
nodup := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_nodup invariant }
work := recovered.work }theorem matchingBFSPathRecoveryWith_work {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
(matchingBFSPathRecoveryWith A M cover hd).work = 2 * (d + 1) := by
simp [matchingBFSPathRecoveryWith, BFSParentPath.verticesWithCost_work]
theorem matchingBFSPathRecoveryWith_work_le {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
(matchingBFSPathRecoveryWith A M cover hd).work ≤
2 * flowVertexCount V := by
rw [matchingBFSPathRecoveryWith_work]
let parentPath :=
(residualBFS_distanceInvariant (matchingToFlow M)).parentPath_of_distance
(matchingCostedBFSWith_distance A M cover hd)
have hnodup := parentPath.vertices_nodup
(residualBFS_distanceInvariant (matchingToFlow M))
have hlength : (BFSParentPath.vertices parentPath).length = d + 1 :=
by simpa [parentPath] using BFSParentPath.vertices_length (h := parentPath)
have hcard : (BFSParentPath.vertices parentPath).length ≤
Fintype.card (V ⊕ Bool) :=
List.Nodup.length_le_card hnodup
rw [hlength] at hcard
simpa [flowVertexCount] using Nat.mul_le_mul_left 2 hcardRecover the source-to-sink parent chain selected by the same costed BFS state. List construction uses cons followed by one reversal.
noncomputable def matchingBFSPathRecovery {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
MatchingBFSPathRecovery M := by
let hd' := matchingCostedBFS_distance M hd
let invariant := residualBFS_distanceInvariant (matchingToFlow M)
let parentPath := invariant.parentPath_of_distance hd'
let recovered := BFSParentPath.verticesWithCost parentPath
exact
{ path :=
{ vertices := recovered.vertices
chain := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_chain invariant
head_eq := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_head
last_eq := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_getLast
nodup := by
rw [BFSParentPath.verticesWithCost_vertices]
exact parentPath.vertices_nodup invariant }
work := recovered.work }The recovered list is definitionally tied, modulo the verified erasure, to the semantic BFS parent chain.
theorem matchingBFSPathRecovery_vertices {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
(matchingBFSPathRecovery M hd).path.vertices =
BFSParentPath.vertices
((residualBFS_distanceInvariant (matchingToFlow M)).parentPath_of_distance
(matchingCostedBFS_distance M hd)) := by
simp [matchingBFSPathRecovery, BFSParentPath.verticesWithCost_vertices]Exact work charged for parent-chain construction and final reversal.
theorem matchingBFSPathRecovery_work {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
(matchingBFSPathRecovery M hd).work = 2 * (d + 1) := by
simp [matchingBFSPathRecovery, BFSParentPath.verticesWithCost_work]Parent recovery is linear in the flow-network vertex count.
theorem matchingBFSPathRecovery_work_le {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
(matchingBFSPathRecovery M hd).work ≤ 2 * flowVertexCount V := by
rw [matchingBFSPathRecovery_work]
let parentPath :=
(residualBFS_distanceInvariant (matchingToFlow M)).parentPath_of_distance
(matchingCostedBFS_distance M hd)
have hnodup := parentPath.vertices_nodup
(residualBFS_distanceInvariant (matchingToFlow M))
have hlength : (BFSParentPath.vertices parentPath).length = d + 1 :=
by simpa [parentPath] using BFSParentPath.vertices_length (h := parentPath)
have hcard : (BFSParentPath.vertices parentPath).length ≤ Fintype.card (V ⊕ Bool) :=
List.Nodup.length_le_card hnodup
rw [hlength] at hcard
simpa [flowVertexCount] using Nat.mul_le_mul_left 2 hcardA concrete residual source-to-sink path in the matching network induces a graph augmenting path. The proof consumes the supplied path itself; it does not replace it with a separately chosen reachability witness.
theorem augmentingPathProjection_of_residualPath {G : BipartiteGraph V}
(M : Matching V G)
(q : Flow.ResidualPath (matchingToFlow M) (Sum.inr true) (Sum.inr false)) :
∃ p : List V, IsAugmentingPath G M p ∧
p = projectGraphVertices q.vertices := by
cases hq : q.vertices with
| nil =>
have hhead := q.head_eq
simp [hq] at hhead
| cons x rest =>
have hq0 : x = Sum.inr true := by
simpa [hq] using q.head_eq
subst x
cases rest with
| nil =>
have hend := q.last_eq
simp [hq] at hend
| cons y rest' =>
have hstep0 :
Flow.residualEdge (matchingToFlow M) (Sum.inr true) y := by
have hc := (List.isChain_iff_getElem.mp q.chain) 0 (by simp [hq])
simpa [hq, toFlowNetwork] using hc
cases y with
| inl l =>
have ⟨hl, hlu⟩ :=
(matchingToFlow_residualEdge_source M l).mp hstep0
have hw : (Sum.inl l :: rest').IsChain
(Flow.residualEdge (matchingToFlow M)) := by
have hchain := q.chain
rw [List.isChain_iff_getElem] at hchain ⊢
intro i hi
have hc := hchain (i + 1) (by simp [hq] at hi ⊢; omega)
simpa [hq, toFlowNetwork] using hc
have hwnd : (Sum.inl l :: rest').Nodup := by
have hnd := q.nodup
rw [hq] at hnd
exact hnd.of_cons
have hw0 : (Sum.inl l :: rest')[0]? = some (Sum.inl l) := rfl
have hwlast :
(Sum.inl l :: rest')[(Sum.inl l :: rest').length - 1]? =
some (Sum.inr false) := by
have h1 :
(Sum.inr true :: Sum.inl l :: rest')[
(Sum.inr true :: Sum.inl l :: rest').length - 1]? =
(Sum.inl l :: rest')[(Sum.inl l :: rest').length - 1]? := by
simp [List.length_cons]
have hend := q.last_eq
rw [hq, List.getLast?_eq_getElem?, h1] at hend
exact hend
have hwns : Sum.inr true ∉ Sum.inl l :: rest' := by
have hnd := q.nodup
rw [hq, List.nodup_cons] at hnd
exact hnd.1
obtain ⟨p, hpn, hpe, hpge, hphead, hplast, hpfw, hpbw, -,
hproject⟩ :=
translation_inner M l hl (Sum.inl l :: rest') hw hwnd hw0
hwlast hwns
have hpne : p ≠ [] := fun h => by simp [h] at hpge
refine ⟨p, ?_, by simpa [projectGraphVertices] using hproject⟩
refine ⟨hpn, hpe, hpge, ?_, ?_, ?_, ?_, hpfw, hpbw⟩
· intro h
have h1 : p.head h = l := by
have h2 : p.head? = some (p.head h) :=
List.head?_eq_some_head _
rw [hphead] at h2
exact (Option.some.inj h2).symm
rw [h1]
exact hl
· intro h r
have h1 : p.head h = l := by
have h2 : p.head? = some (p.head h) :=
List.head?_eq_some_head _
rw [hphead] at h2
exact (Option.some.inj h2).symm
rw [h1]
exact hlu r
· intro h
have h1 : p.getLast? = some (p.getLast h) :=
List.getLast?_eq_some_getLast hpne
exact (hplast _ h1).1
· intro h l'
have h1 : p.getLast? = some (p.getLast h) :=
List.getLast?_eq_some_getLast hpne
exact (hplast _ h1).2 l'
| inr b =>
exact absurd hstep0
(matchingToFlow_not_residualEdge_source_inr M b)The graph projection of a concrete matching residual path is itself an augmenting path.
theorem projectGraphVertices_isAugmentingPath {G : BipartiteGraph V}
(M : Matching V G)
(q : Flow.ResidualPath (matchingToFlow M) (Sum.inr true) (Sum.inr false)) :
IsAugmentingPath G M (projectGraphVertices q.vertices) := by
obtain ⟨p, hp, hproject⟩ := augmentingPathProjection_of_residualPath M q
simpa [hproject] using hpCompatibility existential form of the concrete residual-path translation.
theorem augmentingPath_of_residualPath {G : BipartiteGraph V}
(M : Matching V G)
(q : Flow.ResidualPath (matchingToFlow M) (Sum.inr true) (Sum.inr false)) :
∃ p : List V, IsAugmentingPath G M p :=
⟨projectGraphVertices q.vertices,
projectGraphVertices_isAugmentingPath M q⟩Result of the one-pass projection from residual-network vertices to graph vertices.
structure CostedGraphPathProjection (V : Type*) where
vertices : List V
work : NatExecute the graph-vertex projection, charging one case inspection per residual-path vertex.
def projectGraphVerticesWithCost : List (V ⊕ Bool) →
CostedGraphPathProjection V
| [] => ⟨[], 0⟩
| x :: rest =>
let tail := projectGraphVerticesWithCost rest
match x with
| Sum.inl v => ⟨v :: tail.vertices, tail.work + 1⟩
| Sum.inr _ => ⟨tail.vertices, tail.work + 1⟩omit [Fintype V] [DecidableEq V] in
theorem projectGraphVerticesWithCost_vertices (w : List (V ⊕ Bool)) :
(projectGraphVerticesWithCost w).vertices = projectGraphVertices w := by
induction w with
| nil => rfl
| cons x rest ih =>
cases x <;> simp [projectGraphVerticesWithCost, projectGraphVertices, ih]omit [Fintype V] [DecidableEq V] in
theorem projectGraphVerticesWithCost_work (w : List (V ⊕ Bool)) :
(projectGraphVerticesWithCost w).work = w.length := by
induction w with
| nil => rfl
| cons x rest ih =>
cases x <;> simp [projectGraphVerticesWithCost, ih]Execute graph projection for the path recovered from an explicitly supplied, already-built support adjacency.
noncomputable def matchingBFSGraphProjectionWith {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
CostedGraphPathProjection V :=
projectGraphVerticesWithCost
(matchingBFSPathRecoveryWith A M cover hd).path.vertices
theorem matchingBFSGraphProjectionWith_isAugmenting {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
IsAugmentingPath G M
(matchingBFSGraphProjectionWith A M cover hd).vertices := by
rw [matchingBFSGraphProjectionWith, projectGraphVerticesWithCost_vertices]
exact projectGraphVertices_isAugmentingPath M
(matchingBFSPathRecoveryWith A M cover hd).pathThe graph projection from an explicitly indexed BFS run is linear in the flow-network vertex count.
theorem matchingBFSGraphProjectionWith_work_le {G : BipartiteGraph V}
(A : SupportAdjacency (V ⊕ Bool)) (M : Matching V G)
(cover : SupportsResidual A (matchingToFlow M)) {d : Nat}
(hd : (matchingCostedBFSWith A M).state.distance (Sum.inr false) = some d) :
(matchingBFSGraphProjectionWith A M cover hd).work ≤
flowVertexCount V := by
rw [matchingBFSGraphProjectionWith, projectGraphVerticesWithCost_work]
exact List.Nodup.length_le_card
(matchingBFSPathRecoveryWith A M cover hd).path.nodupExecute the graph projection of the exact recovered matching-BFS path.
noncomputable def matchingBFSGraphProjection {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
CostedGraphPathProjection V :=
projectGraphVerticesWithCost (matchingBFSPathRecovery M hd).path.vertices
theorem matchingBFSGraphProjection_isAugmenting {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
IsAugmentingPath G M (matchingBFSGraphProjection M hd).vertices := by
rw [matchingBFSGraphProjection, projectGraphVerticesWithCost_vertices]
exact projectGraphVertices_isAugmentingPath M
(matchingBFSPathRecovery M hd).pathThe one-pass path projection is linear in the flow-network vertex count.
theorem matchingBFSGraphProjection_work_le {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
(matchingBFSGraphProjection M hd).work ≤ flowVertexCount V := by
rw [matchingBFSGraphProjection, projectGraphVerticesWithCost_work]
exact List.Nodup.length_le_card
(matchingBFSPathRecovery M hd).path.nodupThe exact parent path recovered from the costed BFS translates to a graph augmenting path.
theorem augmentingPath_of_matchingBFSPathRecovery {G : BipartiteGraph V}
(M : Matching V G) {d : Nat}
(hd : (matchingCostedBFS M).state.distance (Sum.inr false) = some d) :
∃ p : List V, IsAugmentingPath G M p :=
⟨(matchingBFSGraphProjection M hd).vertices,
matchingBFSGraphProjection_isAugmenting M hd⟩end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.MatchingAugment
Concrete matching augmentation
The textbook augmentation proof is refined here to return the matching built by its insert/swap execution. The attached counter is accumulated by that same recursion: one unit for a final insertion and two units for each erase/insert swap.
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V] {G : BipartiteGraph V}Insert a single augmenting edge into a matching.
noncomputable def insertAugmentingEdge (M : Matching V G) {l r : V}
(hE : (l, r) ∈ G.E) (_hM : (l, r) ∉ M.edges)
(hl : M.IsUnmatchedLeft l) (hr : M.IsUnmatchedRight r) : Matching V G :=
{ edges := insert (l, r) M.edges
h_subset := Finset.insert_subset hE M.h_subset
h_unique_left := by
intro l₂ r₁ r₂ h₁ h₂
simp only [Finset.mem_insert, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | h₁ <;>
rcases h₂ with ⟨e2a, e2b⟩ | h₂
· exact e1b.trans e2b.symm
· exact (hl r₂ (e1a ▸ h₂)).elim
· exact (hl r₁ (e2a ▸ h₁)).elim
· exact M.h_unique_left l₂ r₁ r₂ h₁ h₂
h_unique_right := by
intro l₁ l₂ r₃ h₁ h₂
simp only [Finset.mem_insert, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | h₁ <;>
rcases h₂ with ⟨e2a, e2b⟩ | h₂
· exact e1a.trans e2a.symm
· exact (hr l₂ (e1b ▸ h₂)).elim
· exact (hr l₁ (e2b ▸ h₁)).elim
· exact M.h_unique_right l₁ l₂ r₃ h₁ h₂ }
theorem insertAugmentingEdge_size (M : Matching V G) {l r : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges)
(hl : M.IsUnmatchedLeft l) (hr : M.IsUnmatchedRight r) :
(insertAugmentingEdge M hE hM hl hr).size = M.size + 1 := by
show (insert (l, r) M.edges).card = M.size + 1
rw [Finset.card_insert_of_notMem hM]
rfl
Replace the matched edge (l',r) by the nonmatching edge (l,r).
noncomputable def swapAugmentingEdge (M : Matching V G) {l r l' : V}
(hE : (l, r) ∈ G.E) (_hM : (l, r) ∉ M.edges)
(hM' : (l', r) ∈ M.edges) (hl : M.IsUnmatchedLeft l)
(_hne : l ≠ l') : Matching V G :=
{ edges := insert (l, r) (M.edges.erase (l', r))
h_subset := Finset.insert_subset hE
((Finset.erase_subset _ _).trans M.h_subset)
h_unique_left := by
intro l₂ r₁ r₂ h₁ h₂
simp only [Finset.mem_insert, Finset.mem_erase, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | ⟨-, h₁⟩ <;>
rcases h₂ with ⟨e2a, e2b⟩ | ⟨-, h₂⟩
· exact e1b.trans e2b.symm
· exact (hl r₂ (e1a ▸ h₂)).elim
· exact (hl r₁ (e2a ▸ h₁)).elim
· exact M.h_unique_left l₂ r₁ r₂ h₁ h₂
h_unique_right := by
intro l₁ l₂ r₃ h₁ h₂
simp only [Finset.mem_insert, Finset.mem_erase, Prod.mk.injEq] at h₁ h₂
rcases h₁ with ⟨e1a, e1b⟩ | ⟨hne₁, h₁⟩ <;>
rcases h₂ with ⟨e2a, e2b⟩ | ⟨hne₂, h₂⟩
· exact e1a.trans e2a.symm
· exact (hne₂
(Prod.ext (M.h_unique_right l₂ l' r (e1b ▸ h₂) hM') e1b)).elim
· exact (hne₁
(Prod.ext (M.h_unique_right l₁ l' r (e2b ▸ h₁) hM') e2b)).elim
· exact M.h_unique_right l₁ l₂ r₃ h₁ h₂ }
theorem swapAugmentingEdge_size (M : Matching V G) {l r l' : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges)
(hM' : (l', r) ∈ M.edges) (hl : M.IsUnmatchedLeft l)
(hne : l ≠ l') :
(swapAugmentingEdge M hE hM hM' hl hne).size = M.size := by
show (insert (l, r) (M.edges.erase (l', r))).card = M.size
have hnotin : (l, r) ∉ M.edges.erase (l', r) := fun h =>
hM (Finset.mem_of_mem_erase h)
rw [Finset.card_insert_of_notMem hnotin, Finset.card_erase_of_mem hM',
Nat.sub_add_cancel (Finset.card_pos.mpr ⟨(l', r), hM'⟩)]
rflThe left endpoint removed by a swap is unmatched afterwards.
theorem swapAugmentingEdge_unmatched (M : Matching V G) {l r l' : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges)
(hM' : (l', r) ∈ M.edges) (hl : M.IsUnmatchedLeft l)
(hne : l ≠ l') :
(swapAugmentingEdge M hE hM hM' hl hne).IsUnmatchedLeft l' := by
intro r₂ h
simp only [swapAugmentingEdge, Finset.mem_insert, Finset.mem_erase,
Prod.mk.injEq] at h
rcases h with ⟨e1, -⟩ | ⟨hne2, hmem⟩
· exact hne e1.symm
· exact hne2
(Prod.ext rfl (M.h_unique_left l' r r₂ hM' hmem).symm)theorem mem_swapAugmentingEdge_iff (M : Matching V G) {l r l' : V}
(hE : (l, r) ∈ G.E) (hM : (l, r) ∉ M.edges)
(hM' : (l', r) ∈ M.edges) (hl : M.IsUnmatchedLeft l)
(hne : l ≠ l') (e : V × V) :
e ∈ (swapAugmentingEdge M hE hM hM' hl hne).edges ↔
e = (l, r) ∨ (e ∈ M.edges ∧ e ≠ (l', r)) := by
simp only [swapAugmentingEdge, Finset.mem_insert, Finset.mem_erase]
constructor
· rintro (h | ⟨h1, h2⟩)
· exact Or.inl h
· exact Or.inr ⟨h2, h1⟩
· rintro (h | ⟨h1, h2⟩)
· exact Or.inl h
· exact Or.inr ⟨h2, h1⟩Result of the concrete alternating-path update. Its correctness and linear work bound travel with the returned execution.
structure MatchingAugmentRun (G : BipartiteGraph V) (M : Matching V G)
(p : List V) where
matching : Matching V G
work : Nat
size_eq : matching.size = M.size + 1
work_le : work ≤ p.lengthThe concrete first swap of a nontrivial augmenting path, packaged with the proof that its remaining suffix is augmenting for the new matching.
structure AugmentingSwapStep (G : BipartiteGraph V) (M : Matching V G)
(rest : List V) where
matching : Matching V G
size_eq : matching.size = M.size
tail_isAugmenting : IsAugmentingPath G matching restExecute the first erase/insert swap of a path with at least four vertices.
noncomputable def augmentingSwapStep {M : Matching V G} {l r l' : V}
{rest : List V} (hp : IsAugmentingPath G M (l :: r :: l' :: rest)) :
AugmentingSwapStep G M (l' :: rest) := by
have hnePath : l :: r :: l' :: rest ≠ [] := by simp
have hnd := hp.nodup
rw [List.nodup_cons] at hnd
obtain ⟨hlNotin, hnd⟩ := hnd
rw [List.nodup_cons] at hnd
obtain ⟨hrNotin, hnd⟩ := hnd
have hfw := hp.forward (l, r) List.mem_cons_self
have hbw := hp.backward (l', r) List.mem_cons_self
have hlu : M.IsUnmatchedLeft l := hp.head_unmatched hnePath
have hll : l ≠ l' := fun h =>
hlNotin (h ▸ List.mem_cons_of_mem _ List.mem_cons_self)
let M₁ := swapAugmentingEdge M hfw.1 hfw.2 hbw hlu hll
have hM₁size : M₁.size = M.size := by
exact swapAugmentingEdge_size M hfw.1 hfw.2 hbw hlu hll
have hM₁un : M₁.IsUnmatchedLeft l' := by
exact swapAugmentingEdge_unmatched M hfw.1 hfw.2 hbw hlu hll
have hM₁mem (e : V × V) : e ∈ M₁.edges ↔
e = (l, r) ∨ (e ∈ M.edges ∧ e ≠ (l', r)) := by
exact mem_swapAugmentingEdge_iff M hfw.1 hfw.2 hbw hlu hll e
have hlast : (l :: r :: l' :: rest).getLast hnePath =
(l' :: rest).getLast (by simp) := by
simp [List.getLast_cons]
refine
{ matching := M₁
size_eq := hM₁size
tail_isAugmenting := ?_ }
refine ⟨hnd, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· have heven := hp.length_even
have hge := hp.length_ge
simp only [List.length_cons] at heven hge ⊢
obtain ⟨k, hk⟩ := heven
exact ⟨k - 1, by omega⟩
· have heven := hp.length_even
have hge := hp.length_ge
simp only [List.length_cons] at heven hge ⊢
obtain ⟨k, hk⟩ := heven
omega
· intro _
exact (G.hE_subset _ (M.h_subset hbw)).1
· intro _ r₂ h
exact hM₁un r₂ h
· intro _
have h := hp.getLast_mem_R hnePath
rwa [hlast] at h
· intro _ l₂ h
rw [hM₁mem] at h
rcases h with h | ⟨hmem, -⟩
· obtain ⟨-, heq⟩ := Prod.mk.inj h
have hrmem : r ∈ l' :: rest := by
have hlastMem := List.getLast_mem (l := l' :: rest) (by simp)
rwa [heq] at hlastMem
exact absurd hrmem hrNotin
· exact hp.getLast_unmatched hnePath l₂ (hlast ▸ hmem)
· intro e he
have hf := hp.forward e (List.mem_cons_of_mem _ he)
refine ⟨hf.1, fun hmem => ?_⟩
rw [hM₁mem] at hmem
rcases hmem with h | ⟨hmem, -⟩
· obtain ⟨e1, -⟩ := Prod.mk.inj h
have hm := fst_mem_of_mem_altEdges_left he
rw [e1] at hm
exact hlNotin (List.mem_cons_of_mem _ hm)
· exact hf.2 hmem
· intro e he
have hb := hp.backward e (List.mem_cons_of_mem _ he)
have hne : e ≠ (l', r) := by
intro hcontra
have hm := snd_mem_of_mem_altEdges_right he
rw [hcontra] at hm
exact hrNotin hm
exact (hM₁mem e).mpr (Or.inr ⟨hb, hne⟩)Execute all swaps and the final insertion along an augmenting path.
noncomputable def augmentMatchingAlong (M : Matching V G) (p : List V)
(hp : IsAugmentingPath G M p) : MatchingAugmentRun G M p :=
match p with
| [] => by
exfalso
simpa using hp.length_ge
| [_] => by
exfalso
simpa using hp.length_ge
| [l, r] => by
have hfw := hp.forward (l, r) List.mem_cons_self
have hne : l :: [r] ≠ [] := by simp
let M' := insertAugmentingEdge M hfw.1 hfw.2
(hp.head_unmatched hne) (hp.getLast_unmatched hne)
exact
{ matching := M'
work := 1
size_eq := by
exact insertAugmentingEdge_size M hfw.1 hfw.2
(hp.head_unmatched hne) (hp.getLast_unmatched hne)
work_le := by simp }
| l :: r :: l' :: rest => by
let step := augmentingSwapStep hp
let tail := augmentMatchingAlong step.matching (l' :: rest)
step.tail_isAugmenting
exact
{ matching := tail.matching
work := 2 + tail.work
size_eq := by
calc
tail.matching.size = step.matching.size + 1 := tail.size_eq
_ = M.size + 1 := by rw [step.size_eq]
work_le := by
have htail := tail.work_le
simp only [List.length_cons] at htail ⊢
omega }
termination_by p.lengthConcrete augmentation increases the matching size by exactly one.
theorem augmentMatchingAlong_size (M : Matching V G) (p : List V)
(hp : IsAugmentingPath G M p) :
(augmentMatchingAlong M p hp).matching.size = M.size + 1 :=
(augmentMatchingAlong M p hp).size_eqThe attached update work is at most the path's number of vertices.
theorem augmentMatchingAlong_work_le (M : Matching V G) (p : List V)
(hp : IsAugmentingPath G M p) :
(augmentMatchingAlong M p hp).work ≤ p.length :=
(augmentMatchingAlong M p hp).work_leA simple augmenting path update uses at most one unit per graph vertex.
theorem augmentMatchingAlong_work_le_vertexCard (M : Matching V G)
(p : List V) (hp : IsAugmentingPath G M p) :
(augmentMatchingAlong M p hp).work ≤ Fintype.card V := by
exact (augmentMatchingAlong_work_le M p hp).trans
(List.Nodup.length_le_card hp.nodup)end Matchingsend CLRSCLRSLean.FourthEdition.Chapter_25.Section_25_1_Maximum_Bipartite_Matching.FlowExecution.CostedRun
Attached-cost bipartite matching run
This module closes the adjacency-list execution promised by CLRS §25.1. Each attempt runs the support-indexed BFS, inspects its returned sink label, recovers that run's parent path, and executes the concrete matching update. The counter is accumulated in the same recursion and includes the one-time support-index construction.
The full run binds that support index once and threads it through every recursive attempt. Work is stated in the explicit unit-cost RAM model of the support-BFS layer, not as Lean kernel or compiled-container evaluation time.
Proof witnesses and erasure/translation proofs carry no RAM charge. The charged data operations are precisely support construction, bucket scans, parent-list construction/reversal, residual-to-graph projection, and matching-edge erase/insert updates.
namespace CLRSopen Finset Classicalnamespace Matchingsopen Chapter26variable {V : Type*} [Fintype V] [DecidableEq V]omit [Fintype V] in
theorem matchingFlowFunSummand_integral (e : V × V) (u v : V ⊕ Bool) :
∃ n : Int, matchingFlowFunSummand e u v = (n : Real) := by
let n : Int :=
match u, v with
| Sum.inr true, Sum.inl l => if e.1 = l then 1 else 0
| Sum.inl a, Sum.inl b =>
(if e = (a, b) then 1 else 0) + (if e = (b, a) then -1 else 0)
| Sum.inl r, Sum.inr false => if e.2 = r then 1 else 0
| Sum.inl l, Sum.inr true => if e.1 = l then -1 else 0
| Sum.inr false, Sum.inl r => if e.2 = r then -1 else 0
| _, _ => 0
refine ⟨n, ?_⟩
cases u with
| inl a =>
cases v with
| inl b =>
by_cases hab : e = (a, b) <;> by_cases hba : e = (b, a) <;>
simp [n, matchingFlowFunSummand, hab, hba]
| inr b =>
cases b <;> simp [n, matchingFlowFunSummand]
| inr a =>
cases a <;> cases v with
| inl b => simp [n, matchingFlowFunSummand]
| inr b => cases b <;> simp [n, matchingFlowFunSummand]Every matching-derived semantic flow is integral.
theorem matchingToFlow_integral {G : BipartiteGraph V} (M : Matching V G) :
(matchingToFlow M).IsIntegral := by
intro u v
change ∃ n : Int, matchingFlowFun M u v = (n : Real)
unfold matchingFlowFun
induction M.edges using Finset.induction_on with
| empty => exact ⟨0, by simp⟩
| @insert e support he ih =>
obtain ⟨n, hn⟩ := ih
obtain ⟨m, hm⟩ := matchingFlowFunSummand_integral e u v
refine ⟨m + n, ?_⟩
simp [he, hm, hn]Uniform work allowance for one attempted augmentation.
def matchingAttemptWorkBudget (G : BipartiteGraph V) : Nat :=
5 * flowVertexCount V + 8 * flowArcCount GEvery matching has at most one edge per left vertex.
theorem Matching.size_le_left_card {G : BipartiteGraph V}
(M : Matching V G) : M.size ≤ G.L.card := by
rw [← M.matchedLeft_card]
apply Finset.card_le_card
intro l hl
exact M.mem_L_of_isMatchedLeft ((M.mem_matchedLeft_iff l).1 hl)A missing sink label in a BFS using an explicitly supplied support adjacency certifies maximality of the current matching.
theorem isMaximum_of_matchingCostedBFSWith_distance_none
{G : BipartiteGraph V} (A : SupportAdjacency (V ⊕ Bool))
(M : Matching V G) (cover : SupportsResidual A (matchingToFlow M))
(hnone : (matchingCostedBFSWith A M).state.distance
(Sum.inr false) = none) :
M.IsMaximum := by
have hno : ¬ (matchingToFlow M).hasAugmentingPath := by
intro hpath
have hex : ∃ d, (residualBFS (matchingToFlow M)).distance
(Sum.inr false) = some d :=
(bfsState_distance_defined_iff_reachable (matchingToFlow M)
(Sum.inr false)).2 hpath
rw [← matchingCostedBFSWith_state A M cover] at hex
rcases hex with ⟨d, hd⟩
rw [hnone] at hd
simp at hd
have hmaxFlow := Flow.maximal_of_noAugmentingPath (matchingToFlow M) hno
intro M'
have hle := hmaxFlow (matchingToFlow M')
rw [matchingToFlow_value, matchingToFlow_value] at hle
exact_mod_cast hleSpecialized maximality wrapper for the canonical matching support.
theorem isMaximum_of_matchingCostedBFS_distance_none
{G : BipartiteGraph V} (M : Matching V G)
(hnone : (matchingCostedBFS M).state.distance (Sum.inr false) = none) :
M.IsMaximum :=
isMaximum_of_matchingCostedBFSWith_distance_none
(matchingFlowAdjacency G).adjacency M (matchingFlowSupportsResidual M) hnone
Result of at most fuel costed augmentation attempts from initial.
structure CostedMatchingRunFrom (G : BipartiteGraph V)
(initial : Matching V G) (fuel : Nat) where
matching : Matching V G
work : Nat
augmentations : Nat
size_eq : matching.size = initial.size + augmentations
augmentations_le : augmentations ≤ fuel
maximum_or_full : matching.IsMaximum ∨ augmentations = fuel
work_le : work ≤ fuel * matchingAttemptWorkBudget GRun the attached-cost matching loop from an arbitrary matching while reusing one explicitly supplied support adjacency throughout the recursion.
noncomputable def costedMatchingRunFrom (G : BipartiteGraph V)
(A : SupportAdjacency (V ⊕ Bool))
(hA : A = (matchingFlowAdjacency G).adjacency) :
(fuel : Nat) → (initial : Matching V G) →
CostedMatchingRunFrom G initial fuel
| 0, initial =>
{ matching := initial
work := 0
augmentations := 0
size_eq := by simp
augmentations_le := by simp
maximum_or_full := Or.inr rfl
work_le := by simp }
| fuel + 1, initial =>
let cover : SupportsResidual A (matchingToFlow initial) := by
rw [hA]
exact matchingFlowSupportsResidual initial
let bfs := matchingCostedBFSWith A initial
match hdistance : bfs.state.distance (Sum.inr false) with
| none =>
{ matching := initial
work := bfs.work
augmentations := 0
size_eq := by simp
augmentations_le := by simp
maximum_or_full := Or.inl
(isMaximum_of_matchingCostedBFSWith_distance_none
A initial cover hdistance)
work_le := by
have hbfs : bfs.work ≤
flowVertexCount V + 8 * flowArcCount G := by
have h := matchingCostedBFSWith_work_le A initial cover
have hstorage : A.storage = 2 * flowArcCount G := by
rw [hA, matchingFlowAdjacency_storage]
rw [hstorage] at h
simp only [bfs, flowVertexCount] at h ⊢
omega
simp only [matchingAttemptWorkBudget]
rw [Nat.add_mul]
simp only [one_mul]
omega }
| some d =>
let recovery := matchingBFSPathRecoveryWith A initial cover hdistance
let projection :=
matchingBFSGraphProjectionWith A initial cover hdistance
let p := projection.vertices
let hp := matchingBFSGraphProjectionWith_isAugmenting
A initial cover hdistance
let update := augmentMatchingAlong initial p hp
let tail := costedMatchingRunFrom G A hA fuel update.matching
{ matching := tail.matching
work := bfs.work + recovery.work + projection.work + update.work +
tail.work
augmentations := tail.augmentations + 1
size_eq := by
calc
tail.matching.size = update.matching.size + tail.augmentations :=
tail.size_eq
_ = initial.size + (tail.augmentations + 1) := by
rw [update.size_eq]
omega
augmentations_le := by
have htail := tail.augmentations_le
omega
maximum_or_full := by
rcases tail.maximum_or_full with hmax | hfull
· exact Or.inl hmax
· exact Or.inr (by omega)
work_le := by
have hbfs : bfs.work ≤
flowVertexCount V + 8 * flowArcCount G := by
have h := matchingCostedBFSWith_work_le A initial cover
have hstorage : A.storage = 2 * flowArcCount G := by
rw [hA, matchingFlowAdjacency_storage]
rw [hstorage] at h
simp only [bfs, flowVertexCount] at h ⊢
omega
have hrecovery : recovery.work ≤ 2 * flowVertexCount V := by
simpa [recovery] using
matchingBFSPathRecoveryWith_work_le A initial cover hdistance
have hprojection : projection.work ≤ flowVertexCount V := by
simpa [projection] using
matchingBFSGraphProjectionWith_work_le
A initial cover hdistance
have hupdate : update.work ≤ Fintype.card V := by
simpa [update] using
augmentMatchingAlong_work_le_vertexCard initial p hp
have htail := tail.work_le
simp only [matchingAttemptWorkBudget] at htail ⊢
have hflowVertices : Fintype.card V ≤ flowVertexCount V := by
simp [flowVertexCount]
rw [Nat.add_mul]
simp only [one_mul]
omega }Final result, including one-time adjacency-support construction.
structure CostedMatchingRun (G : BipartiteGraph V) where
matching : Matching V G
flow : Flow (V ⊕ Bool) (toFlowNetwork V G)
flow_eq : flow = matchingToFlow matching
work : Nat
augmentations : NatThe full textbook run starts from the empty matching and permits one successful augmentation per left vertex.
noncomputable def costedMatchingRun (G : BipartiteGraph V) :
CostedMatchingRun G :=
let built := matchingFlowAdjacency G
let core := costedMatchingRunFrom G built.adjacency rfl
G.L.card (Matching.empty G)
{ matching := core.matching
flow := matchingToFlow core.matching
flow_eq := rfl
work := built.work + core.work
augmentations := core.augmentations }The returned matching is maximum.
theorem costedMatchingRun_maximum (G : BipartiteGraph V) :
(costedMatchingRun G).matching.IsMaximum := by
let built := matchingFlowAdjacency G
let core := costedMatchingRunFrom G built.adjacency rfl
G.L.card (Matching.empty G)
change core.matching.IsMaximum
rcases core.maximum_or_full with hmax | hfull
· exact hmax
· intro M'
have hsize : core.matching.size = G.L.card := by
rw [core.size_eq, Matching.empty_size, zero_add, hfull]
rw [hsize]
exact Matching.size_le_left_card M'theorem costedMatchingRun_flow_eq (G : BipartiteGraph V) :
(costedMatchingRun G).flow =
matchingToFlow (costedMatchingRun G).matching :=
(costedMatchingRun G).flow_eqThe semantic flow attached definitionally to the returned matching is maximal.
theorem costedMatchingRun_flow_maximal (G : BipartiteGraph V) :
(costedMatchingRun G).flow.isMaximal := by
rw [costedMatchingRun_flow_eq]
apply Flow.maximal_of_noAugmentingPath
intro hpath
have hnoGraph :=
(berge_maximum_iff_no_augmentingPath (costedMatchingRun G).matching).1
(costedMatchingRun_maximum G)
exact hnoGraph
(augmentingPath_of_hasAugmentingPath (costedMatchingRun G).matching hpath)
theorem costedMatchingRun_flow_integral (G : BipartiteGraph V) :
(costedMatchingRun G).flow.IsIntegral := by
rw [costedMatchingRun_flow_eq]
exact matchingToFlow_integral _
theorem costedMatchingRun_flow_value (G : BipartiteGraph V) :
(costedMatchingRun G).flow.value =
((costedMatchingRun G).matching.size : Real) := by
rw [costedMatchingRun_flow_eq, matchingToFlow_value]
Exact attached bound: support construction once, followed by at most
|L| linear support-BFS/path-update attempts.
theorem costedMatchingRun_work_le (G : BipartiteGraph V) :
(costedMatchingRun G).work ≤
2 * flowArcCount G + G.L.card * matchingAttemptWorkBudget G := by
let built := matchingFlowAdjacency G
let core := costedMatchingRunFrom G built.adjacency rfl
G.L.card (Matching.empty G)
have hcore := core.work_le
have hbuild := matchingFlowAdjacency_work G
change built.work + core.work ≤ _
change (matchingFlowAdjacency G).work = _ at hbuild
rw [hbuild]
omega
A conventional constant-factor product form of the adjacency-list
bound: the run is O(V_f E_f) for the constructed flow network.
theorem costedMatchingRun_work_le_product (G : BipartiteGraph V) :
(costedMatchingRun G).work ≤
20 * flowVertexCount V * (flowArcCount G + 1) := by
refine (costedMatchingRun_work_le G).trans ?_
let vf := flowVertexCount V
let ef := flowArcCount G
have hvf : vf ≤ 2 * (ef + 1) := by
dsimp [vf, ef]
rw [flowVertexCount_eq, flowArcCount_eq]
omega
have hvone : 1 ≤ vf := by
dsimp [vf]
rw [flowVertexCount_eq]
omega
have hleft : G.L.card ≤ vf := by
exact (left_card_le_vertex_card G).trans (by
dsimp [vf]
rw [flowVertexCount_eq]
omega)
have hleftMul :
G.L.card * (5 * vf + 8 * ef) ≤ vf * (5 * vf + 8 * ef) :=
Nat.mul_le_mul_right _ hleft
have hvfSquare : 5 * vf * vf ≤ 10 * vf * (ef + 1) := by
have h := Nat.mul_le_mul_left (5 * vf) hvf
calc
5 * vf * vf ≤ 5 * vf * (2 * (ef + 1)) := h
_ = 10 * vf * (ef + 1) := by ring
have hefLinear : 8 * vf * ef ≤ 8 * vf * (ef + 1) := by
exact Nat.mul_le_mul_left (8 * vf) (Nat.le_succ ef)
have hefBuild : 2 * ef ≤ 2 * vf * (ef + 1) := by
have h := Nat.mul_le_mul_right (ef + 1) hvone
have h' : ef ≤ vf * (ef + 1) :=
(Nat.le_succ ef).trans (by simpa using h)
calc
2 * ef ≤ 2 * (vf * (ef + 1)) := Nat.mul_le_mul_left 2 h'
_ = 2 * vf * (ef + 1) := by ring
change 2 * ef + G.L.card * (5 * vf + 8 * ef) ≤
20 * vf * (ef + 1)
calc
2 * ef + G.L.card * (5 * vf + 8 * ef) ≤
2 * ef + vf * (5 * vf + 8 * ef) :=
Nat.add_le_add_left hleftMul _
_ = 2 * ef + 5 * vf * vf + 8 * vf * ef := by ring
_ ≤ 2 * vf * (ef + 1) + 10 * vf * (ef + 1) +
8 * vf * (ef + 1) := by
exact Nat.add_le_add (Nat.add_le_add hefBuild hvfSquare) hefLinear
_ = 20 * vf * (ef + 1) := by ringThe run performs no more successful augmentations than left vertices.
theorem costedMatchingRun_augmentations_le (G : BipartiteGraph V) :
(costedMatchingRun G).augmentations ≤ G.L.card := by
let built := matchingFlowAdjacency G
exact (costedMatchingRunFrom G built.adjacency rfl
G.L.card (Matching.empty G)).augmentations_leAttached-cost flow-method headline (CLRS §25.1). The returned value is a maximum matching produced by the support-indexed BFS/update execution, and its same-execution work satisfies the displayed adjacency-list product bound.
theorem flowMethod_finds_maximum_matching_with_attached_cost
(G : BipartiteGraph V) :
let run := costedMatchingRun G
run.matching.IsMaximum ∧
run.flow.isMaximal ∧
run.flow.IsIntegral ∧
run.flow.value = (run.matching.size : Real) ∧
run.work ≤ 2 * flowArcCount G + G.L.card * matchingAttemptWorkBudget G ∧
run.augmentations ≤ G.L.card := by
dsimp only
exact ⟨costedMatchingRun_maximum G, costedMatchingRun_flow_maximal G,
costedMatchingRun_flow_integral G, costedMatchingRun_flow_value G,
costedMatchingRun_work_le G,
costedMatchingRun_augmentations_le G⟩end Matchingsend CLRS