Maximum bipartite matching

StructureMatching in a bipartite graph#✓fully proved

Let a bipartite graph have left vertices \(0, \dots, a-1\), right vertices \(0, \dots, b-1\) and an adjacency list for each left vertex. A finite set \(M\) of pairs \((i, j)\) of a left vertex \(i\) and a right vertex \(j\) is a matching when every pair in \(M\) is an edge (\(j\) is in the adjacency list of \(i\)), no two distinct pairs of \(M\) have the same left vertex, and no two distinct pairs of \(M\) have the same right vertex.

structure IsMatching (M : Finset (Fin a × Fin b)) : Prop where
  /-- Every pair is an edge. -/
  edge : ∀ p ∈ M, p.2 ∈ adj p.1
  /-- No left vertex is matched twice. -/
  left : ∀ p ∈ M, ∀ q ∈ M, p.1 = q.1 → p = q
  /-- No right vertex is matched twice. -/
  right : ∀ p ∈ M, ∀ q ∈ M, p.2 = q.2 → p = q

Used by 16

Used byOne round of the layered search bounds the deficit · Correctness of Hopcroft–Karp · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Hopcroft and Karp's bound on the number of phases · Optimality of the augmenting-path matching algorithm · Kőnig's certificate · Correctness of the phase loop · Hopcroft–Karp returns a matching · The augmenting-path algorithm returns a matching · A valid partner array gives a matching · Enough augmentations reach a maximum matching · The deficit is at most \(b / d\) · Greedy online matching is 1/2-competitive · The \(1/2\) lower bound with a matching of the arrivals' graph · Perfect matchings of the arrivals are matchings of their graph · The greedy online matching is a matching

DefinitionMatched pairs of a partner assignment#✓fully proved

Given a partner assignment \(\mathrm{mate}\) that sends each right vertex \(j < b\) to a left vertex \(i < a\) or to nothing, the matched pairs of \(\mathrm{mate}\) form the set of all pairs \((i, j)\) of a left vertex \(i < a\) and a right vertex \(j < b\) with \(\mathrm{mate}(j) = i\).

def pairs (mate : Fin b → Option (Fin a)) : Finset (Fin a × Fin b) :=
  Finset.univ.filter fun p => mate p.2 = some p.1

Used by 16

Used byOne round of the layered search bounds the deficit · Correctness of Hopcroft–Karp · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Hopcroft and Karp's bound on the number of phases · Optimality of the augmenting-path matching algorithm · Kőnig's certificate · Matched pairs and matched right vertices are equinumerous · Correctness of the phase loop · Hopcroft–Karp returns a matching · The augmenting-path algorithm returns a matching · A valid partner array gives a matching · Enough augmentations reach a maximum matching · The deficit is at most \(b / d\) · Greedy online matching is 1/2-competitive · Greedy online matching is within a factor \(2\) of the maximum · The greedy online matching is a matching

StructurePartner arrays that describe a matching#✓fully proved

Consider a bipartite graph with left vertices \(\{0, \dots, a-1\}\), right vertices \(\{0, \dots, b-1\}\) and, for each left vertex \(i\), a list of its neighbours. A partner array assigns to each right vertex \(j\) either no partner or a left vertex as its partner. It is valid when every partner is a neighbour (if \(i\) is the partner of \(j\), then \(j\) is in the list of neighbours of \(i\)) and no left vertex is the partner of two different right vertices (if \(i\) is the partner of both \(j\) and \(j'\), then \(j = j'\)).

structure Valid (mate : Fin b → Option (Fin a)) : Prop where
  /-- Partners are neighbours. -/
  edge : ∀ i j, mate j = some i → j ∈ adj i
  /-- No left vertex is the partner of two right vertices. -/
  inj : ∀ i j j', mate j = some i → mate j' = some i → j = j'

Used by 40

Used byA successful augmentation grows the matching by one edge · One round of the layered search bounds the deficit · Correctness of Hopcroft–Karp · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Hopcroft and Karp's bound on the number of phases · Optimality of the augmenting-path matching algorithm · Kőnig's certificate · Shortest chains from a vertex whose level a phase keeps were chains before it · Each phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · Correctness of the phase loop · Hopcroft–Karp returns a matching · The augmenting-path algorithm returns a matching · A valid partner array gives a matching · Distances do not decrease across a phase · The first free round does not decrease across a phase · Phases use shortest augmenting paths · The next phase's paths are strictly longer · Enough augmentations reach a maximum matching · A matched right vertex is reached no later than its partner · The deficit is at most \(b / d\) · Levels of the pairs of a phase · Partners of predecessors lie one level earlier · The walk back from an unmatched reached vertex is an augmenting path · The walk back is an alternating path · Invariant of a phase · Phase paths are disjoint augmenting paths · Phases are maximal · A phase finds a path when an unmatched right vertex is reached · The paths of a phase are vertex-disjoint augmenting paths · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Search paths are alternating paths through unused vertices · Flipping an alternating path keeps a matching · Flipping disjoint alternating paths at once keeps a matching · The greedy matching is maximal · Invariants of the greedy run · The greedy online matching is a matching

DefinitionUnmatched left vertex#✓fully proved

Given a partner array \(\mu\), which assigns to each right vertex \(j\) either a left vertex \(\mu(j)\) as partner or no partner, a left vertex \(i\) is unmatched (free) when no right vertex \(j\) has \(\mu(j) = i\).

def Free (mate : Fin b → Option (Fin a)) (i : Fin a) : Prop := ∀ j, mate j ≠ some i

Used by 34

Used byAlternating path · One round of the layered search bounds the deficit · Kőnig's certificate · Shortest chains from a vertex whose level a phase keeps were chains before it · Matched reached left vertices are reached through a partner · A phase leaves no new unmatched left vertex · Alternating chain to an unmatched left vertex · Alternating breadth-first layers · Distances do not decrease across a phase · No augmenting path is shorter than a phase's · The next phase's paths are strictly longer · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds · A matched right vertex is reached no later than its partner · Shortest chains avoiding earlier paths contain no dead vertex · Levels along a shortest alternating chain · Levels of the pairs of a phase · Partners of predecessors lie one level earlier · The walk back is an alternating path · Invariant of a phase · Phases are maximal · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Search paths are alternating paths through unused vertices · The second pair of a shortest alternating chain · Flipping an alternating path keeps a matching · Flipping disjoint alternating paths at once keeps a matching · Greedy online matching is 1/2-competitive · Done right vertices · The greedy matching is maximal · Invariants of the greedy run · The greedy online matching is a matching · Greedy step of online bipartite matching · Greedy step on an array · Earlier partners survive an arrival

DefinitionAlternating breadth-first layers#✓fully proved

Let \(\mu\) give each right vertex \(j\) of a bipartite graph at most one partner \(\mu(j)\) among the left vertices. The layers are pairs \((Z_k, R_k)\) of a set \(Z_k\) of left vertices and a set \(R_k\) of right vertices, defined by recursion on \(k\): \(Z_0\) is the set of unmatched left vertices (those that are the partner of no right vertex) and \(R_0 = \emptyset\); \(R_{k+1}\) is the set of right vertices \(j\) adjacent to some \(i \in Z_k\) with \(\mu(j) \ne i\), and \(Z_{k+1}\) is \(Z_k\) together with the left vertices \(\mu(j)\) for \(j \in R_{k+1}\).

The layers are cumulative on both sides: \(Z_k\) holds the left vertices reached within \(k\) rounds and \(R_k\) the right vertices reached within \(k\) rounds. The round where a vertex is first reached is its breadth-first level.

def layers (mate : Fin b → Option (Fin a)) : ℕ → Finset (Fin a) × Finset (Fin b)
  | 0 => (Finset.univ.filter fun i => Free mate i, ∅)
  | k + 1 =>
      let Z := (layers mate k).1
      let R := Finset.univ.filter fun j => ∃ i ∈ Z, j ∈ adj i ∧ mate j ≠ some i
      (Z ∪ Finset.univ.filter (fun i => ∃ j ∈ R, mate j = some i), R)

Uses 1 · Used by 47

Statement usesUnmatched left vertex

Used byAlternating path · One augmentation step · A failed augmentation reaches no unmatched right vertex · A successful augmentation grows the matching by one edge · One round of the layered search bounds the deficit · Hopcroft and Karp's bound on the number of phases · Kőnig's certificate · Shortest chains from a vertex whose level a phase keeps were chains before it · Exact level of a right vertex · Matched reached left vertices are reached through a partner · First free round · When there is no first free round · Characterization of the first free round · Each phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · The left layers stop growing once two consecutive ones agree · Rounds \(a\) and \(a + 1\) reach the same left vertices · The first free round does not decrease across a phase · No augmenting path is shorter than a phase's · Phases use shortest augmenting paths · The next phase's paths are strictly longer · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds · A matched right vertex is reached no later than its partner · The deficit is at most \(b / d\) · Levels along a shortest alternating chain · Levels of the pairs of a phase · Partners of predecessors lie one level earlier · Walking the layers back · The walk back from an unmatched reached vertex is an augmenting path · The walk back is an alternating path · Hopcroft–Karp phase · Invariant of a phase · Phase paths are disjoint augmenting paths · Phases are maximal · A phase finds a path when an unmatched right vertex is reached · The paths of a phase are vertex-disjoint augmenting paths · Depth-first search of a Hopcroft–Karp phase · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Length bound for search paths · The dead set of a search only grows · A failed search marks its start dead · Search paths are alternating paths through unused vertices · The second pair of a shortest alternating chain

TheoremMatched reached left vertices are reached through a partner#✓fully proved

Let \(\mu\) be a partner array and \(k\) a natural number. If a left vertex \(i\) is reached within \(k\) rounds of the layered search and is matched (some right vertex has partner \(i\)), then some right vertex \(j\) reached within \(k\) rounds has partner \(i\), that is, \(\mu(j) = i\).

theorem exists_mate_of_mem_layers {k : ℕ} {i : Fin a} (hi : i ∈ (layers adj mate k).1)
    (hfree : ¬ Free mate i) : ∃ j ∈ (layers adj mate k).2, mate j = some i

Uses 2 · Used by 6

Statement usesUnmatched left vertex · Alternating breadth-first layers

Used byKőnig's certificate · A matched right vertex is reached no later than its partner · Partners of predecessors lie one level earlier · The walk back is an alternating path · Searches from reached vertices succeed when nothing is used or dead · Search paths are alternating paths through unused vertices

TheoremThe left layers stop growing once two consecutive ones agree#✓fully proved

For any partner array, if the layered search reaches the same left vertices within \(k\) rounds as within \(k + 1\) rounds, then for every \(m \ge k\) it reaches exactly those left vertices within \(m\) rounds.

theorem layers_fst_eq_of_eq {k : ℕ} (h : (layers adj mate k).1 = (layers adj mate (k + 1)).1) :
    ∀ m, k ≤ m → (layers adj mate m).1 = (layers adj mate k).1

Uses 1 · Used by 1

Statement usesAlternating breadth-first layers

Used byRounds \(a\) and \(a + 1\) reach the same left vertices

TheoremRounds \(a\) and \(a + 1\) reach the same left vertices#✓fully proved

In a bipartite graph with \(a\) left vertices, for every partner array \(\mu\), the alternating layered search for \(\mu\) reaches the same left vertices within \(a + 1\) rounds as within \(a\) rounds.

theorem layers_fst_stable : (layers adj mate (a + 1)).1 = (layers adj mate a).1

Uses 2 · Used by 1

Statement usesAlternating breadth-first layers

Proof usesThe left layers stop growing once two consecutive ones agree

Used byKőnig's certificate

91 fully proved

Augmenting paths

DefinitionWalking the layers back#✓fully proved

Given the adjacency lists \(\mathrm{adj}\) of a bipartite graph, a partner assignment \(\mathrm{mate}\), a level \(k\) and a right vertex \(j\), the walk back from \(j\) at level \(k\) is a list of pairs defined by recursion on \(k\). At level \(0\) it is \([(i, j)]\) for the least unmatched left vertex \(i\) with \(j \in \mathrm{adj}(i)\) and \(\mathrm{mate}(j) \ne i\), and empty if there is none. At level \(k + 1\), if \(j\) is reached within \(k + 1\) rounds of the alternating layered search, it is the walk back from \(j\) at level \(k\). Otherwise take the least left vertex \(i\) reached within \(k + 1\) rounds with \(j \in \mathrm{adj}(i)\) and \(\mathrm{mate}(j) \ne i\) (the walk is empty if there is none): if no right vertex has partner \(i\) the walk is \([(i, j)]\), and otherwise it is \((i, j)\) followed by the walk back at level \(k\) from the least right vertex \(j'\) with \(\mathrm{mate}(j') = i\).

When \(j\) is reached within \(k + 1\) rounds, the walk descends to the round where \(j\) is first reached and lists the pairs to match, \(j\) first.

Cslib.Algorithms.Lean.BipartiteMatching.pathTo · 17 lines

def pathTo (mate : Fin b → Option (Fin a)) : ℕ → Fin b → List (Fin a × Fin b)
  | 0, j =>
      let Z := (layers adj mate 0).1
      match (List.finRange a).find? (fun i => decide (i ∈ Z ∧ j ∈ adj i ∧ mate j ≠ some i)) with
      | none => []
      | some i => [(i, j)]
  | k + 1, j =>
      let L := layers adj mate (k + 1)
      if j ∈ L.2 then pathTo mate k j
      else
        match (List.finRange a).find? (fun i =>
          decide (i ∈ L.1 ∧ j ∈ adj i ∧ mate j ≠ some i)) with
        | none => []
        | some i =>
            match (List.finRange b).find? (fun j' => decide (mate j' = some i)) with
            | none => [(i, j)]
            | some j' => (i, j) :: pathTo mate k j'

Uses 1 · Used by 5

Statement usesAlternating breadth-first layers

Used byOne augmentation step · A failed augmentation reaches no unmatched right vertex · A successful augmentation grows the matching by one edge · The walk back from an unmatched reached vertex is an augmenting path · The walk back is an alternating path

DefinitionFlipping a list of pairs#✓fully proved

Let \(\mu\) be a partner array, assigning to each right vertex either a left partner or none, and let \(P\) be a list of pairs \((i, j)\) of a left vertex \(i\) and a right vertex \(j\). The flip of \(\mu\) along \(P\) sends each right vertex \(j\) to the left vertex of the first pair in \(P\) whose right vertex is \(j\), and to \(\mu(j)\) (a partner or none) when no pair of \(P\) has right vertex \(j\).

def flip (mate : Fin b → Option (Fin a)) (P : List (Fin a × Fin b)) : Fin b → Option (Fin a) :=
  fun j => match P.find? (fun p => decide (p.2 = j)) with
    | some p => some p.1
    | none => mate j

Used by 17

Used byOne augmentation step · A failed augmentation reaches no unmatched right vertex · A successful augmentation grows the matching by one edge · Flipping an augmenting path adds one matched vertex · Flipping disjoint augmenting paths matches at least one more vertex · Shortest chains from a vertex whose level a phase keeps were chains before it · Each phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · Hopcroft–Karp step · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · The first free round does not decrease across a phase · The next phase's paths are strictly longer · Flipping an alternating path matches its first vertex · Flipping an alternating path keeps a matching · Flipping disjoint alternating paths at once keeps a matching

StructureAlternating path#✓fully proved

Let \(\mu\) be a partner array, giving each right vertex at most one left vertex as its partner, let \(k\) be a natural number and \(j\) a right vertex. A list \(P\) of pairs \((i, j')\) of a left vertex \(i\) and a right vertex \(j'\) is an alternating path from \(j\) within round \(k\) when all of the following hold: \(P\) is nonempty and its first pair has right vertex \(j\); for every pair \((i, j')\) of \(P\), \(j'\) is a neighbour of \(i\) but \(i\) is not the partner of \(j'\); for every pair \((i, j')\) of \(P\), the alternating search from the unmatched left vertices reaches \(i\) within \(k\) rounds and \(j'\) within \(k + 1\) rounds; no left vertex and no right vertex occurs twice in \(P\); for any two consecutive pairs \((i, j')\) and \((i', j'')\) of \(P\), \(i\) is the partner of \(j''\); and the left vertex of the last pair of \(P\) is the partner of no right vertex.

When \(j\) is unmatched as well, \(P\) is an augmenting path.

Cslib.Algorithms.Lean.BipartiteMatching.AltPath · 16 lines

structure AltPath (mate : Fin b → Option (Fin a)) (k : ℕ) (j : Fin b)
    (P : List (Fin a × Fin b)) : Prop where
  /-- It starts at `j`. -/
  head : P.head?.map Prod.snd = some j
  /-- Its pairs are non-matching edges. -/
  edge : ∀ p ∈ P, p.2 ∈ adj p.1 ∧ mate p.2 ≠ some p.1
  /-- Its vertices are reached. -/
  layer : ∀ p ∈ P, p.1 ∈ (layers adj mate k).1 ∧ p.2 ∈ (layers adj mate (k + 1)).2
  /-- No left vertex twice. -/
  nodup_fst : (P.map Prod.fst).Nodup
  /-- No right vertex twice. -/
  nodup_snd : (P.map Prod.snd).Nodup
  /-- Each right vertex after the first is matched to the previous left vertex. -/
  chain : List.IsChain (fun p q => mate q.2 = some p.1) P
  /-- The last left vertex is unmatched. -/
  last : ∀ p ∈ P.getLast?, Free mate p.1

Uses 2 · Used by 18

Statement usesUnmatched left vertex · Alternating breadth-first layers

Used byA successful augmentation grows the matching by one edge · Flipping an augmenting path adds one matched vertex · Flipping disjoint augmenting paths matches at least one more vertex · A phase leaves no new unmatched left vertex · A successful Hopcroft–Karp step grows the matching · Augmenting path · No augmenting path is shorter than a phase's · The next phase's paths are strictly longer · Flipping an alternating path matches its first vertex · Levels of the pairs of a phase · The walk back from an unmatched reached vertex is an augmenting path · The walk back is an alternating path · Invariant of a phase · Phase paths are disjoint augmenting paths · Phases are maximal · Search paths are alternating paths through unused vertices · Flipping an alternating path keeps a matching · Flipping disjoint alternating paths at once keeps a matching

StructureAugmenting path#✓fully proved

Let \(\mu\) be a partner array, \(k\) a natural number and \(j\) a right vertex. A list \(P\) of pairs of a left vertex and a right vertex is an augmenting path from \(j\) within round \(k\) when \(P\) is an alternating path from \(j\) within round \(k\) and \(j\) is unmatched: \(\mu\) gives \(j\) no partner.

Since the last left vertex of an alternating path is unmatched, both endpoints of an augmenting path are unmatched.

structure IsAugmentingPath (mate : Fin b → Option (Fin a)) (k : ℕ) (j : Fin b)
    (P : List (Fin a × Fin b)) : Prop extends AltPath adj mate k j P where
  /-- The starting right vertex is unmatched. -/
  start_free : mate j = none

Uses 1 · Used by 15

Statement usesAlternating path

Used byA successful augmentation grows the matching by one edge · Flipping an augmenting path adds one matched vertex · Flipping disjoint augmenting paths matches at least one more vertex · Shortest chains from a vertex whose level a phase keeps were chains before it · A phase leaves no new unmatched left vertex · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · No augmenting path is shorter than a phase's · Phases use shortest augmenting paths · The next phase's paths are strictly longer · Levels of the pairs of a phase · The walk back from an unmatched reached vertex is an augmenting path · Phase paths are disjoint augmenting paths · Phases are maximal · The paths of a phase are vertex-disjoint augmenting paths

TheoremThe walk back is an alternating path#✓fully proved

Let \(\mathrm{mate}\) be a valid partner assignment. For every level \(k\) and every right vertex \(j\) reached within \(k + 1\) rounds of the alternating layered search, the walk back from \(j\) at level \(k\) is an alternating path from \(j\) at level \(k\): it starts at \(j\), its pairs are non-matching edges, its left vertices are reached within \(k\) rounds and its right vertices within \(k + 1\) rounds, no vertex occurs twice, each right vertex after the first is the partner of the previous left vertex, and the last left vertex is unmatched.

theorem pathTo_spec (hv : Valid adj mate) : ∀ (k : ℕ) (j : Fin b),
    j ∈ (layers adj mate (k + 1)).2 → AltPath adj mate k j (pathTo adj mate k j)

Uses 6 · Used by 1

Statement usesAlternating path · Partner arrays that describe a matching · Alternating breadth-first layers · Walking the layers back

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner

Used byThe walk back from an unmatched reached vertex is an augmenting path

TheoremFlipping an alternating path keeps a matching#✓fully proved

Let \(\mu\) be a valid partner array (partners are neighbours and no left vertex is the partner of two right vertices), and let \(P\) be an alternating path for \(\mu\) from a right vertex \(j\) with round bound \(k\). Then the partner array obtained from \(\mu\) by matching each pair of \(P\) and keeping the other partners is valid.

theorem valid_flip (hv : Valid adj mate) {k : ℕ} {j : Fin b} {P : List (Fin a × Fin b)}
    (hP : AltPath adj mate k j P) : Valid adj (flip mate P)

Uses 4 · Used by 1

Statement usesAlternating path · Partner arrays that describe a matching · Flipping a list of pairs

Proof usesUnmatched left vertex

Used byA successful augmentation grows the matching by one edge

DefinitionMatched right vertices#✓fully proved

Let \(\mu\) give each right vertex \(j\) of a bipartite graph at most one partner \(\mu(j)\) among the left vertices. The matched right vertices of \(\mu\) are the right vertices \(j\) that have a partner \(\mu(j)\).

def matched (mate : Fin b → Option (Fin a)) : Finset (Fin b) :=
  Finset.univ.filter fun j => (mate j).isSome

Used by 14

Used byA successful augmentation grows the matching by one edge · Correctness of Hopcroft–Karp · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Optimality of the augmenting-path matching algorithm · Flipping an augmenting path adds one matched vertex · Flipping disjoint augmenting paths matches at least one more vertex · Matched pairs and matched right vertices are equinumerous · Each phase lengthens the shortest augmenting paths · A successful Hopcroft–Karp step grows the matching · Correctness of the phase loop · Hopcroft–Karp returns a matching · The augmenting-path algorithm returns a matching · Flipping an alternating path matches its first vertex · Enough augmentations reach a maximum matching

TheoremFlipping an alternating path matches its first vertex#✓fully proved

Let \(\mu\) give each right vertex of a bipartite graph at most one partner among the left vertices, and let \(P\) be an alternating path for \(\mu\) starting at the right vertex \(j\). Then the right vertices matched after flipping \(P\) are exactly \(j\) and the right vertices matched under \(\mu\).

The other right vertices of \(P\) change partners but stay matched.

theorem matched_flip {k : ℕ} {j : Fin b} {P : List (Fin a × Fin b)} (hP : AltPath adj mate k j P) :
    matched (flip mate P) = insert j (matched mate)

Uses 3 · Used by 1

Statement usesAlternating path · Flipping a list of pairs · Matched right vertices

Used byFlipping an augmenting path adds one matched vertex

TheoremThe walk back from an unmatched reached vertex is an augmenting path#✓fully proved

Let \(\mu\) be a valid partner array, \(k\) a natural number and \(j\) a right vertex that is unmatched and is reached within \(k + 1\) rounds of the alternating layered search for \(\mu\). Then the walk back from \(j\) at level \(k\) is an augmenting path from \(j\) within round \(k\).

theorem pathTo_isAugmentingPath (hv : Valid adj mate) {k : ℕ} {j : Fin b}
    (hj : j ∈ (layers adj mate (k + 1)).2) (hfree : mate j = none) :
    IsAugmentingPath adj mate k j (pathTo adj mate k j)

Uses 6 · Used by 1

Statement usesAugmenting path · Partner arrays that describe a matching · Alternating breadth-first layers · Walking the layers back

Proof usesAlternating path · The walk back is an alternating path

Used byA successful augmentation grows the matching by one edge

TheoremFlipping an augmenting path adds one matched vertex#✓fully proved

If \(P\) is an augmenting path for a partner array \(\mu\), then flipping \(P\) in \(\mu\) gives a partner array with exactly one more matched right vertex than \(\mu\).

theorem card_matched_flip {k : ℕ} {j : Fin b} {P : List (Fin a × Fin b)}
    (hP : IsAugmentingPath adj mate k j P) :
    (matched (flip mate P)).card = (matched mate).card + 1

Uses 5 · Used by 1

Statement usesAugmenting path · Flipping a list of pairs · Matched right vertices

Proof usesAlternating path · Flipping an alternating path matches its first vertex

Used byA successful augmentation grows the matching by one edge

The algorithm

DefinitionOne augmentation step#✓fully proved

Let \(\mu\) be a partner array on a bipartite graph with \(a\) left vertices and \(b\) right vertices. Run the alternating search from the unmatched left vertices for \(a + 1\) rounds and take the first right vertex \(j\), in the order \(0, \dots, b - 1\), that is unmatched and reached. If there is none, the step fails. Otherwise it returns the partner array obtained from \(\mu\) by flipping the path found by walking back from \(j\) through the search layers: every right vertex \(j'\) on the path gets as partner the left vertex paired with it on the path, and every other right vertex keeps its partner.

def augment (mate : Fin b → Option (Fin a)) : Option (Fin b → Option (Fin a)) :=
  let R := (layers adj mate (a + 1)).2
  match (List.finRange b).find? (fun j => decide (mate j = none ∧ j ∈ R)) with
  | none => none
  | some j => some (flip mate (pathTo adj mate a j))

Uses 3 · Used by 4

Statement usesFlipping a list of pairs · Alternating breadth-first layers · Walking the layers back

Used byA failed augmentation reaches no unmatched right vertex · A successful augmentation grows the matching by one edge · Augmentation loop · Enough augmentations reach a maximum matching

DefinitionAugmentation loop#✓fully proved

Given a fuel \(f \in \mathbb{N}\) and a partner array \(\mu\) (assigning to each right vertex at most one left partner), the loop returns \(\mu\) when \(f = 0\). When \(f \ge 1\) it performs one augmentation step on \(\mu\): if the layered search reaches no unmatched right vertex, the loop returns \(\mu\); otherwise it runs with fuel \(f - 1\) on the array that this step returns, obtained by flipping the pairs walked back through the layers from the least-indexed unmatched right vertex that the search reaches. Thus it augments while possible, at most \(f\) times.

def maxMatchingAux : ℕ → (Fin b → Option (Fin a)) → Fin b → Option (Fin a)
  | 0, mate => mate
  | fuel + 1, mate =>
      match augment adj mate with
      | none => mate
      | some mate' => maxMatchingAux fuel mate'

Uses 1 · Used by 4

Statement usesOne augmentation step

Used byOptimality of the augmenting-path matching algorithm · The augmenting-path algorithm returns a matching · The augmenting-path maximum matching · Enough augmentations reach a maximum matching

DefinitionThe augmenting-path maximum matching#✓fully proved

In a bipartite graph with right vertices \(0, \dots, b-1\), the partner array obtained by running the augmentation loop with fuel \(b + 1\) from the empty matching, in which no right vertex has a partner.

def maxMatching : Fin b → Option (Fin a) := maxMatchingAux adj (b + 1) fun _ => none

Uses 1 · Used by 3

Statement usesAugmentation loop

Used byOptimality of the augmenting-path matching algorithm · The augmenting-path algorithm returns a matching · Greedy online matching is within a factor \(2\) of the maximum

TheoremMatched pairs and matched right vertices are equinumerous#✓fully proved

For every partner array \(\mu\), the number of matched pairs \((i, j)\) of \(\mu\), those with \(\mu(j) = i\), equals the number of matched right vertices of \(\mu\).

theorem card_pairs (mate : Fin b → Option (Fin a)) : (pairs mate).card = (matched mate).card

Uses 2 · Used by 1

Statement usesMatched right vertices · Matched pairs of a partner assignment

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases

TheoremA valid partner array gives a matching#✓fully proved

Let each right vertex \(j\) of a bipartite graph have at most one partner, a left vertex. If the partners are valid for the graph (each partner of \(j\) is adjacent to \(j\), and no left vertex is the partner of two right vertices), then the set of pairs \((i, j)\) with \(i\) the partner of \(j\) is a matching of the graph.

theorem isMatching_pairs (hv : Valid adj mate) : IsMatching adj (pairs mate)

Uses 3 · Used by 3

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Matched pairs of a partner assignment

Used byHopcroft–Karp returns a matching · The augmenting-path algorithm returns a matching · The greedy online matching is a matching

TheoremA successful augmentation grows the matching by one edge#✓fully proved

Let \(\mu\) be a partner array that describes a matching. If the augmentation step on \(\mu\) returns a partner array \(\mu'\), then \(\mu'\) also describes a matching, and \(\mu'\) has exactly one more matched right vertex than \(\mu\).

theorem augment_some (hv : Valid adj mate) {mate' : Fin b → Option (Fin a)}
    (h : augment adj mate = some mate') :
    Valid adj mate' ∧ (matched mate').card = (matched mate).card + 1

Uses 11 · Used by 1

Statement usesPartner arrays that describe a matching · One augmentation step · Matched right vertices

Proof usesAlternating path · Augmenting path · Flipping an augmenting path adds one matched vertex · Flipping a list of pairs · Alternating breadth-first layers · Walking the layers back · The walk back from an unmatched reached vertex is an augmenting path · Flipping an alternating path keeps a matching

Used byEnough augmentations reach a maximum matching

TheoremA failed augmentation reaches no unmatched right vertex#✓fully proved

Let \(\mu\) be a partner array on a bipartite graph with \(a\) left vertices. If the augmentation step on \(\mu\) fails, then no unmatched right vertex is reached within \(a + 1\) rounds of the alternating search from the unmatched left vertices.

theorem augment_none (h : augment adj mate = none) :
    ∀ j, mate j = none → j ∉ (layers adj mate (a + 1)).2

Uses 4 · Used by 1

Statement usesOne augmentation step · Alternating breadth-first layers

Proof usesFlipping a list of pairs · Walking the layers back

Used byEnough augmentations reach a maximum matching

TheoremKőnig's certificate#✓fully proved

Let \(\mu\) be a partner array on a bipartite graph with \(a\) left vertices that describes a matching. If no unmatched right vertex is reached within \(a + 1\) rounds of the alternating search from the unmatched left vertices, then no matching has more edges than the matching of \(\mu\): the unreached left vertices and the reached right vertices cover every edge, and each of them is matched, to distinct matching edges.

theorem card_le_of_no_free (hv : Valid adj mate)
    (h : ∀ j, mate j = none → j ∉ (layers adj mate (a + 1)).2) {M : Finset (Fin a × Fin b)}
    (hM : IsMatching adj M) : M.card ≤ (pairs mate).card

Uses 7 · Used by 4

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Alternating breadth-first layers · Matched pairs of a partner assignment

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner · Rounds \(a\) and \(a + 1\) reach the same left vertices

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Hopcroft and Karp's bound on the number of phases · Correctness of the phase loop · Enough augmentations reach a maximum matching

TheoremEnough augmentations reach a maximum matching#✓fully proved

In a bipartite graph with right vertices \(0, \dots, b-1\), let \(\mu\) be a valid partner array (it assigns to each right vertex at most one left partner, partners are neighbours, and no left vertex is the partner of two right vertices). Let \(f \in \mathbb{N}\) satisfy \(b < |\mathrm{matched}(\mu)| + f\), where \(\mathrm{matched}(\mu)\) is the set of right vertices with a partner, and let \(\mu'\) be the result of the augmentation loop from \(\mu\) with fuel \(f\). Then \(\mu'\) is valid, and every matching \(M\) of the graph satisfies \(|M| \le |\mathrm{pairs}(\mu')|\), where \(\mathrm{pairs}(\mu')\) is the set of pairs \((i, j)\) with \(\mu'(j) = i\).

theorem maxMatchingAux_spec : ∀ (fuel : ℕ) (mate : Fin b → Option (Fin a)), Valid adj mate →
    b < (matched mate).card + fuel →
    Valid adj (maxMatchingAux adj fuel mate) ∧
      ∀ M, IsMatching adj M → M.card ≤ (pairs (maxMatchingAux adj fuel mate)).card

Uses 9 · Used by 2

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Matched right vertices · Augmentation loop · Matched pairs of a partner assignment

Proof usesOne augmentation step · A failed augmentation reaches no unmatched right vertex · A successful augmentation grows the matching by one edge · Kőnig's certificate

Used byOptimality of the augmenting-path matching algorithm · The augmenting-path algorithm returns a matching

TheoremThe augmenting-path algorithm returns a matching#✓fully proved

For every bipartite graph with left vertices \(0, \dots, a-1\), right vertices \(0, \dots, b-1\) and an adjacency list for each left vertex, the pairs \((i, j)\) such that the augmenting-path maximum matching algorithm (from the empty matching, repeatedly flip an augmenting path found by the layered search) makes \(i\) the partner of \(j\) form a matching of the graph: each pair is an edge, and no two distinct pairs share a left or a right vertex.

theorem isMatching_maxMatching : IsMatching adj (pairs (maxMatching adj))

Uses 8 · Used by 1

Statement usesMatching in a bipartite graph · The augmenting-path maximum matching · Matched pairs of a partner assignment

Proof usesPartner arrays that describe a matching · A valid partner array gives a matching · Matched right vertices · Augmentation loop · Enough augmentations reach a maximum matching

Used byGreedy online matching is within a factor \(2\) of the maximum

TheoremOptimality of the augmenting-path matching algorithm#✓fully proved

In a bipartite graph with \(b\) right vertices, start from the empty matching and repeat the augmentation step until it fails, at most \(b + 1\) times. No matching of the graph has more edges than the resulting matching.

theorem card_le_maxMatching {M : Finset (Fin a × Fin b)} (hM : IsMatching adj M) :
    M.card ≤ (pairs (maxMatching adj)).card

Uses 7

Statement usesMatching in a bipartite graph · The augmenting-path maximum matching · Matched pairs of a partner assignment

Proof usesPartner arrays that describe a matching · Matched right vertices · Augmentation loop · Enough augmentations reach a maximum matching

Hopcroft–Karp phases

DefinitionPartner of a left vertex#✓fully proved

Given a partner assignment \(\mathrm{mate}\) that sends each right vertex \(j < b\) to a left vertex \(i < a\) or to nothing, the partner of a left vertex \(i\) is the least right vertex \(j\) with \(\mathrm{mate}(j) = i\); it is undefined when there is no such \(j\), that is, when \(i\) is unmatched.

def partnerOf (mate : Fin b → Option (Fin a)) (i : Fin a) : Option (Fin b) :=
  (List.finRange b).find? fun j' => decide (mate j' = some i)

Used by 7

Used byDepth-first search of a Hopcroft–Karp phase · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Length bound for search paths · The dead set of a search only grows · A failed search marks its start dead · Search paths are alternating paths through unused vertices

DefinitionMarking a right vertex dead#✓fully proved

Given a set \(D\) of right vertices, represented by its indicator function, and a right vertex \(j\), the result is the indicator function of \(D \cup \{j\}\).

def markDead (dead : Fin b → Bool) (j : Fin b) : Fin b → Bool :=
  fun x => dead x || decide (x = j)

Used by 1

Used byTrying the candidate predecessors of a right vertex

DefinitionTrying the candidate predecessors of a right vertex#✓fully proved

Let \(j\) be a right vertex, \(\mathrm{ok}\) a test on left vertices, \(\pi\) a map giving each left vertex an optional right vertex (its partner, if any), and \(s\) a search taking a right vertex and a dead set (a set of right vertices) to an optional path, a list of pairs of a left and a right vertex, and a new dead set. Given a list of left vertices and a dead set \(D\), the procedure goes through the list in order, skipping the vertices that fail \(\mathrm{ok}\). At the first remaining vertex \(i\): if \(\pi(i)\) is undefined, it returns the path \([(i, j)]\) and \(D\); if \(\pi(i) = j'\) and \(s(j', D)\) finds a path \(P\), it returns the path \((i, j)\) followed by \(P\), with the dead set returned by \(s\); if \(s(j', D)\) finds no path, it continues with the rest of the list from the dead set returned by \(s\). When the list is exhausted, it fails and returns the current dead set with \(j\) added.

def tryPreds (ok : Fin a → Bool) (partner : Fin a → Option (Fin b))
    (search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool))
    (j : Fin b) : List (Fin a) → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)
  | [], dead => (none, markDead dead j)
  | i :: is, dead =>
      if ok i then
        match partner i with
        | none => (some [(i, j)], dead)
        | some j' =>
            match search j' dead with
            | (some P, dead') => (some ((i, j) :: P), dead')
            | (none, dead') => tryPreds ok partner search j is dead'
      else tryPreds ok partner search j is dead

Uses 1 · Used by 12

Statement usesMarking a right vertex dead

Used byDepth-first search of a Hopcroft–Karp phase · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Length bound for search paths · The dead set of a search only grows · A failed search marks its start dead · Search paths are alternating paths through unused vertices · Where newly dead vertices come from · When trying candidates finds a path · Trying candidates keeps dead vertices dead · When trying candidates fails · A path found by trying candidates comes from one candidate

DefinitionDepth-first search of a Hopcroft–Karp phase#✓fully proved

Fix a partner array \(\mu\) assigning each right vertex at most one left partner, and a set \(U\) of used left vertices. Write \(L_n\) and \(R_n\) for the left and right vertices reached within \(n\) rounds of the alternating breadth-first layers of \(\mu\) (so \(R_0 = \emptyset\)). A left vertex \(i\) is unmatched if no right vertex has partner \(i\); otherwise its partner is the least right vertex \(j'\) with \(\mu(j') = i\). The search from a right vertex \(j\) with bound \(n\) and a set \(D\) of dead right vertices returns an optional path (a list of pairs of a left and a right vertex) together with a new dead set:

• if \(j \in D\), it fails and returns \(D\) unchanged;
• otherwise, if \(j \in R_n\), it is the search from \(j\) with bound \(n - 1\) and dead set \(D\);
• otherwise it goes through the candidates, the left vertices \(i \in L_n\) in increasing order with \(j\) adjacent to \(i\), \(\mu(j) \ne i\) and \(i \notin U\). For an unmatched candidate \(i\) it returns the path \([(i, j)]\) and the current dead set. For a matched candidate \(i\) it searches from the partner of \(i\) with bound \(n - 1\) and the current dead set (when \(n = 0\) this search fails and returns the dead set unchanged); if that search finds a path \(P\), it returns \((i, j)\) followed by \(P\), with the dead set that search returned, and otherwise it moves on to the next candidate with the dead set that search returned. If every candidate fails, it fails and returns the current dead set with \(j\) added.

This is the pruning of Hopcroft and Karp: a right vertex from which the search fails is marked dead and not searched again.

Cslib.Algorithms.Lean.BipartiteMatching.searchPath · 15 lines

def searchPath (mate : Fin b → Option (Fin a)) (usedL : Fin a → Bool) :
    ℕ → Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)
  | 0, j, dead =>
      let Z := (layers adj mate 0).1
      if dead j then (none, dead)
      else
        tryPreds (fun i => decide (i ∈ Z ∧ j ∈ adj i ∧ mate j ≠ some i ∧ usedL i = false))
          (partnerOf mate) (fun _ d => (none, d)) j (List.finRange a) dead
  | k + 1, j, dead =>
      let L := layers adj mate (k + 1)
      if dead j then (none, dead)
      else if j ∈ L.2 then searchPath mate usedL k j dead
      else
        tryPreds (fun i => decide (i ∈ L.1 ∧ j ∈ adj i ∧ mate j ≠ some i ∧ usedL i = false))
          (partnerOf mate) (fun j' d => searchPath mate usedL k j' d) j (List.finRange a) dead

Uses 3 · Used by 12

Statement usesAlternating breadth-first layers · Partner of a left vertex · Trying the candidate predecessors of a right vertex

Used byThe next phase's paths are strictly longer · Phase search over candidates · Length bound for phase paths · Invariant of a phase · Phase paths are disjoint augmenting paths · A phase finds a path when an unmatched right vertex is reached · Dead vertices have no escape · Searches from reached vertices succeed when nothing is used or dead · Length bound for search paths · The dead set of a search only grows · A failed search marks its start dead · Search paths are alternating paths through unused vertices

TheoremTrying candidates keeps dead vertices dead#✓fully proved

For a right vertex \(j\), a test \(\mathrm{ok}\) on left vertices, a map \(\pi\) giving each left vertex an optional right vertex, and a search \(s\) taking a right vertex and a dead set (a set of right vertices) to an optional path and a new dead set, write \(T(l, D)\) for the optional path and the dead set returned by trying the left vertices of the list \(l\) as predecessors of \(j\), starting from the dead set \(D\). Suppose \(s\) never shrinks the dead set: for every right vertex \(j'\) and every dead set \(d\), the dead set returned by \(s(j', d)\) contains \(d\). Then for every list \(l\) of left vertices and every dead set \(D\), the dead set of \(T(l, D)\) contains \(D\).

theorem tryPreds_mono {ok : Fin a → Bool} {partner : Fin a → Option (Fin b)}
    {search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)}
    (hs : ∀ j' d x, d x = true → (search j' d).2 x = true) (j : Fin b) :
    ∀ (is : List (Fin a)) (dead : Fin b → Bool) (x : Fin b), dead x = true →
      (tryPreds ok partner search j is dead).2 x = true

Uses 1 · Used by 3

Statement usesTrying the candidate predecessors of a right vertex

Used byThe dead set of a search only grows · Where newly dead vertices come from · When trying candidates fails

TheoremA path found by trying candidates comes from one candidate#✓fully proved

For a right vertex \(j\), a test \(\mathrm{ok}\) on left vertices, a map \(\pi\) giving each left vertex an optional right vertex, and a search \(s\) taking a right vertex and a dead set (a set of right vertices) to an optional path and a new dead set, write \(T(l, D)\) for the optional path and the dead set returned by trying the left vertices of the list \(l\) as predecessors of \(j\), starting from the dead set \(D\). Suppose \(s\) never shrinks the dead set: for every right vertex \(j'\) and every dead set \(d\), the dead set returned by \(s(j', d)\) contains \(d\). If \(T(l, D)\) returns a path \(P\), then there are a vertex \(i\) of \(l\) with \(\mathrm{ok}(i)\) and a dead set \(D_0\) containing \(D\) such that either \(\pi(i)\) is undefined and \(P = [(i, j)]\), or \(\pi(i) = j'\) for a right vertex \(j'\) and \(s(j', D_0)\) returns a path \(P'\) with \(P\) equal to \((i, j)\) followed by \(P'\).

theorem tryPreds_some {ok : Fin a → Bool} {partner : Fin a → Option (Fin b)}
    {search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)}
    (hs : ∀ j' d x, d x = true → (search j' d).2 x = true) (j : Fin b) :
    ∀ (is : List (Fin a)) (dead : Fin b → Bool) (P : List (Fin a × Fin b)),
      (tryPreds ok partner search j is dead).1 = some P →
      ∃ i ∈ is, ok i = true ∧ ∃ dead₀ : Fin b → Bool, (∀ x, dead x = true → dead₀ x = true) ∧
        ((partner i = none ∧ P = [(i, j)]) ∨
          ∃ j' P', partner i = some j' ∧ (search j' dead₀).1 = some P' ∧ P = (i, j) :: P')

Uses 1 · Used by 2

Statement usesTrying the candidate predecessors of a right vertex

Used byLength bound for search paths · Search paths are alternating paths through unused vertices

TheoremWhen trying candidates finds a path#✓fully proved

For a right vertex \(j\), a test \(\mathrm{ok}\) on left vertices, a map \(\pi\) giving each left vertex an optional right vertex, and a search \(s\) taking a right vertex and a dead set (a set of right vertices) to an optional path and a new dead set, write \(T(l, D)\) for the optional path and the dead set returned by trying the left vertices of the list \(l\) as predecessors of \(j\), starting from the dead set \(D\). Suppose some vertex of \(l\) passes \(\mathrm{ok}\), and for every vertex \(i\) of \(l\) passing \(\mathrm{ok}\) and every right vertex \(j'\) with \(\pi(i) = j'\), the search \(s(j', D)\) finds a path. Then \(T(l, D)\) finds a path.

Only the initial dead set matters: it does not change before the first vertex passing \(\mathrm{ok}\).

theorem tryPreds_isSome {ok : Fin a → Bool} {partner : Fin a → Option (Fin b)}
    {search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)}
    (j : Fin b) (dead : Fin b → Bool) : ∀ (is : List (Fin a)), (∃ i ∈ is, ok i = true) →
      (∀ i ∈ is, ok i = true → ∀ j', partner i = some j' → (search j' dead).1.isSome) →
      (tryPreds ok partner search j is dead).1.isSome

Uses 1 · Used by 1

Statement usesTrying the candidate predecessors of a right vertex

Used bySearches from reached vertices succeed when nothing is used or dead

TheoremThe dead set of a search only grows#✓fully proved

For every set of used left vertices, every level \(k\), every right vertex \(j\) and every set of dead right vertices, each right vertex that is dead before the search at level \(k\) from \(j\) is still dead after it.

theorem searchPath_mono (usedL : Fin a → Bool) : ∀ (k : ℕ) (j : Fin b) (dead : Fin b → Bool)
    (x : Fin b), dead x = true → (searchPath adj mate usedL k j dead).2 x = true

Uses 5 · Used by 6

Statement usesDepth-first search of a Hopcroft–Karp phase

Proof usesAlternating breadth-first layers · Partner of a left vertex · Trying the candidate predecessors of a right vertex · Trying candidates keeps dead vertices dead

Used byInvariant of a phase · Phase paths are disjoint augmenting paths · Dead vertices have no escape · Length bound for search paths · A failed search marks its start dead · Search paths are alternating paths through unused vertices

TheoremSearch paths are alternating paths through unused vertices#✓fully proved

Suppose the partner array describes a matching, \(k\) is a level and \(j\) is a right vertex reached within \(k + 1\) rounds of the alternating breadth-first search. For every set of used left vertices and every set of dead right vertices, if the search at level \(k\) from \(j\) finds a path \(P\), then \(P\) is an alternating path at level \(k\) from \(j\), no left vertex of \(P\) is used, and no right vertex of \(P\) was dead before the search.

theorem searchPath_spec (hv : Valid adj mate) (usedL : Fin a → Bool) :
    ∀ (k : ℕ) (j : Fin b) (dead : Fin b → Bool) (P : List (Fin a × Fin b)),
      j ∈ (layers adj mate (k + 1)).2 → (searchPath adj mate usedL k j dead).1 = some P →
      AltPath adj mate k j P ∧ ∀ p ∈ P, usedL p.1 = false ∧ dead p.2 = false

Uses 10 · Used by 3

Statement usesAlternating path · Partner arrays that describe a matching · Alternating breadth-first layers · Depth-first search of a Hopcroft–Karp phase

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner · Partner of a left vertex · The dead set of a search only grows · Trying the candidate predecessors of a right vertex · A path found by trying candidates comes from one candidate

Used byThe next phase's paths are strictly longer · Invariant of a phase · Phase paths are disjoint augmenting paths

TheoremSearches from reached vertices succeed when nothing is used or dead#✓fully proved

If the partner array describes a matching, then for every \(k\) and every right vertex \(j\) reached within \(k + 1\) rounds of the alternating breadth-first search, the search at level \(k\) from \(j\), with no left vertex used and no right vertex dead, finds a path.

theorem searchPath_isSome (hv : Valid adj mate) : ∀ (k : ℕ) (j : Fin b),
    j ∈ (layers adj mate (k + 1)).2 →
      (searchPath adj mate (fun _ => false) k j (fun _ => false)).1.isSome

Uses 8 · Used by 2

Statement usesPartner arrays that describe a matching · Alternating breadth-first layers · Depth-first search of a Hopcroft–Karp phase

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner · Partner of a left vertex · Trying the candidate predecessors of a right vertex · When trying candidates finds a path

Used byThe next phase's paths are strictly longer · A phase finds a path when an unmatched right vertex is reached

DefinitionMarking the left vertices of a path used#✓fully proved

Given a set \(U\) of left vertices, represented by its indicator function, and a list \(P\) of pairs \((i, j)\) of a left vertex \(i\) and a right vertex \(j\), the result is the indicator function of \(U\) together with the left vertices of the pairs of \(P\).

def markL (used : Fin a → Bool) (P : List (Fin a × Fin b)) : Fin a → Bool :=
  fun i => used i || decide (i ∈ P.map Prod.fst)

Used by 5

Used byPhase search over candidates · Length bound for phase paths · Invariant of a phase · Phase paths are disjoint augmenting paths · A phase finds a path when an unmatched right vertex is reached

DefinitionMarking the right vertices of a path used#✓fully proved

Given a set \(U\) of right vertices, represented by its indicator function, and a list \(P\) of pairs \((i, j)\) of a left vertex \(i\) and a right vertex \(j\), the result is the indicator function of \(U\) together with the right vertices of the pairs of \(P\).

def markR (used : Fin b → Bool) (P : List (Fin a × Fin b)) : Fin b → Bool :=
  fun j => used j || decide (j ∈ P.map Prod.snd)

Used by 5

Used byPhase search over candidates · Length bound for phase paths · Invariant of a phase · Phase paths are disjoint augmenting paths · A phase finds a path when an unmatched right vertex is reached

DefinitionPhase search over candidates#✓fully proved

Given a partner assignment \(\mathrm{mate}\), a level \(k\), a list of candidate right vertices, a set \(U\) of used left vertices and a set \(D\) of used or dead right vertices, the phase search tries the candidates in order. For a candidate \(j\) it runs the layered depth-first search from \(j\) at level \(k\) with used left vertices \(U\) and dead set \(D\), which returns an optional path and an enlarged dead set \(D'\). If it finds no path, the phase search continues with the remaining candidates, \(U\) and \(D'\); if it finds a path \(P\), it records \(P\) and continues with the remaining candidates, \(U\) together with the left vertices of \(P\), and \(D'\) together with the right vertices of \(P\). The result is the list of the recorded paths.

def phaseAux (mate : Fin b → Option (Fin a)) (k : ℕ) :
    List (Fin b) → (Fin a → Bool) → (Fin b → Bool) → List (List (Fin a × Fin b))
  | [], _, _ => []
  | j :: js, usedL, usedR =>
      match searchPath adj mate usedL k j usedR with
      | (none, dead) => phaseAux mate k js usedL dead
      | (some P, dead) => P :: phaseAux mate k js (markL usedL P) (markR dead P)

Uses 3 · Used by 14

Statement usesMarking the left vertices of a path used · Marking the right vertices of a path used · Depth-first search of a Hopcroft–Karp phase

Used byEach phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · Phases use shortest augmenting paths · The next phase's paths are strictly longer · Levels of the pairs of a phase · Hopcroft–Karp phase · Length bound for phase paths · Invariant of a phase · Phase paths are disjoint augmenting paths · Phases are maximal · A phase finds a path when an unmatched right vertex is reached · The paths of a phase are vertex-disjoint augmenting paths

DefinitionFirst free round#✓fully proved

For a partner array \(\mu\) of a bipartite graph with \(a\) left vertices, the first free round of \(\mu\) is the least \(d \le a\) such that some unmatched right vertex is reached within \(d + 1\) rounds of the layered search; it is undefined if there is no such \(d\).

def firstFreeRound (mate : Fin b → Option (Fin a)) : Option ℕ :=
  (List.range (a + 1)).find? fun k => decide (∃ j, mate j = none ∧ j ∈ (layers adj mate (k + 1)).2)

Uses 1 · Used by 17

Statement usesAlternating breadth-first layers

Used byHopcroft and Karp's bound on the number of phases · Shortest chains from a vertex whose level a phase keeps were chains before it · When there is no first free round · Characterization of the first free round · Each phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · The first free round does not decrease across a phase · No augmenting path is shorter than a phase's · Phases use shortest augmenting paths · The next phase's paths are strictly longer · Levels of the pairs of a phase · Hopcroft–Karp phase · Phases are maximal · A phase finds a path when an unmatched right vertex is reached · The paths of a phase are vertex-disjoint augmenting paths

DefinitionHopcroft–Karp phase#✓fully proved

If no round of the alternating breadth-first search reaches an unmatched right vertex, the phase finds no path. Otherwise let \(d\) be the earliest round such that round \(d + 1\) reaches one. The phase runs the search at level \(d\) from each unmatched right vertex reached within \(d + 1\) rounds, in increasing order, starting with no left vertex used and no right vertex dead, and lists the paths found. After each search, the left vertices of the path found become used and its right vertices become dead, and right vertices that the search marked dead stay dead for the later searches.

def phase (mate : Fin b → Option (Fin a)) : List (List (Fin a × Fin b)) :=
  match firstFreeRound adj mate with
  | none => []
  | some d =>
      let R := (layers adj mate (d + 1)).2
      phaseAux adj mate d ((List.finRange b).filter fun j => decide (mate j = none ∧ j ∈ R))
        (fun _ => false) (fun _ => false)

Uses 3 · Used by 14

Statement usesFirst free round · Alternating breadth-first layers · Phase search over candidates

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Each phase lengthens the shortest augmenting paths · A phase leaves no new unmatched left vertex · Hopcroft–Karp step · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · The first free round does not decrease across a phase · Phases use shortest augmenting paths · The next phase's paths are strictly longer · Levels of the pairs of a phase · Phases are maximal · A phase finds a path when an unmatched right vertex is reached · The paths of a phase are vertex-disjoint augmenting paths

DefinitionHopcroft–Karp step#✓fully proved

Given a partner array \(\mu\), consider the phase of \(\mu\), a list of paths, each a list of pairs. If the phase is empty, the step returns nothing; otherwise it returns the flip of \(\mu\) along the concatenation of all the paths of the phase.

def hkStep (mate : Fin b → Option (Fin a)) : Option (Fin b → Option (Fin a)) :=
  let Ps := phase adj mate
  if Ps.isEmpty then none else some (flip mate Ps.flatten)

Uses 2 · Used by 8

Statement usesFlipping a list of pairs · Hopcroft–Karp phase

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Each phase lengthens the shortest augmenting paths · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · Hopcroft–Karp phase loop · Fuel adds up in the phase loop · The phase loop stops when a step finds nothing · Correctness of the phase loop

DefinitionHopcroft–Karp phase loop#✓fully proved

Given a fuel \(n \in \mathbb{N}\) and a partner array \(\mu\), the loop returns \(\mu\) when \(n = 0\) or when the Hopcroft–Karp step on \(\mu\) returns nothing; when \(n \ge 1\) and the step returns a partner array \(\mu'\), it returns the loop with fuel \(n - 1\) run from \(\mu'\). So it runs Hopcroft–Karp steps while they find paths, at most \(n\) times.

def hopcroftKarpAux : ℕ → (Fin b → Option (Fin a)) → Fin b → Option (Fin a)
  | 0, mate => mate
  | fuel + 1, mate =>
      match hkStep adj mate with
      | none => mate
      | some mate' => hopcroftKarpAux fuel mate'

Uses 1 · Used by 9

Statement usesHopcroft–Karp step

Used byCorrectness of Hopcroft–Karp · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Hopcroft and Karp's bound on the number of phases · Each phase lengthens the shortest augmenting paths · Hopcroft–Karp · Fuel adds up in the phase loop · The phase loop stops when a step finds nothing · Correctness of the phase loop · Hopcroft–Karp returns a matching

DefinitionHopcroft–Karp#✓fully proved

Let a bipartite graph have left vertices \(0, \dots, a-1\), right vertices \(0, \dots, b-1\) and an adjacency list for each left vertex. Starting from the empty matching, the Hopcroft–Karp algorithm runs phases, at most \(b + 1\) of them, and stops early at the first phase that finds no path: each phase computes the layered search once, collects vertex-disjoint augmenting paths from the unmatched right vertices reached in the earliest round that reaches any, and flips all of them at once. The result is the final matching, given as the partner (or the absence of one) of each right vertex.

The result is a maximum matching.

def hopcroftKarp : Fin b → Option (Fin a) := hopcroftKarpAux adj (b + 1) fun _ => none

Uses 1 · Used by 2

Statement usesHopcroft–Karp phase loop

Used byCorrectness of Hopcroft–Karp · Hopcroft–Karp returns a matching

TheoremCharacterization of the first free round#✓fully proved

For a partner array \(\mu\) of a bipartite graph with \(a\) left vertices and a natural number \(d\), the first free round of \(\mu\) equals \(d\) if and only if \(d \le a\), some unmatched right vertex is reached within \(d + 1\) rounds of the layered search, and for every \(k < d\) no unmatched right vertex is reached within \(k + 1\) rounds.

theorem firstFreeRound_eq_some {d : ℕ} : firstFreeRound adj mate = some d ↔
    d ≤ a ∧ (∃ j, mate j = none ∧ j ∈ (layers adj mate (d + 1)).2) ∧
      ∀ k < d, ∀ j, mate j = none → j ∉ (layers adj mate (k + 1)).2

Uses 2 · Used by 7

Statement usesFirst free round · Alternating breadth-first layers

Used byHopcroft and Karp's bound on the number of phases · The first free round does not decrease across a phase · No augmenting path is shorter than a phase's · The next phase's paths are strictly longer · Levels of the pairs of a phase · Phases are maximal · A phase finds a path when an unmatched right vertex is reached

TheoremWhen there is no first free round#✓fully proved

For a partner array \(\mu\) of a bipartite graph with \(a\) left vertices, the first free round of \(\mu\) is undefined if and only if no unmatched right vertex is reached within \(a + 1\) rounds of the layered search.

theorem firstFreeRound_eq_none : firstFreeRound adj mate = none ↔
    ∀ j, mate j = none → j ∉ (layers adj mate (a + 1)).2

Uses 2 · Used by 3

Statement usesFirst free round · Alternating breadth-first layers

Used byHopcroft and Karp's bound on the number of phases · Each phase lengthens the shortest augmenting paths · A phase finds a path when an unmatched right vertex is reached

TheoremPhase paths are disjoint augmenting paths#✓fully proved

Let \(\mathrm{mate}\) be a valid partner assignment, \(k\) a level, \(J\) a list of right vertices each unmatched and reached within \(k + 1\) rounds of the alternating layered search, and \(U_L\), \(U_R\) sets of left and right vertices. Then every path that the phase search at level \(k\) collects from \(J\) with used left vertices \(U_L\) and used right vertices \(U_R\) is an augmenting path from some right vertex, with left vertices reached within \(k\) rounds and right vertices within \(k + 1\) rounds; no left vertex and no right vertex occurs twice among all pairs of all these paths; and every pair \((i, j)\) of these paths has \(i \notin U_L\) and \(j \notin U_R\).

theorem phaseAux_spec (hv : Valid adj mate) (k : ℕ) : ∀ (js : List (Fin b))
    (usedL : Fin a → Bool) (usedR : Fin b → Bool),
    (∀ j ∈ js, mate j = none ∧ j ∈ (layers adj mate (k + 1)).2) →
    (∀ P ∈ phaseAux adj mate k js usedL usedR, ∃ j, IsAugmentingPath adj mate k j P) ∧
      ((phaseAux adj mate k js usedL usedR).flatten.map Prod.fst).Nodup ∧
      ((phaseAux adj mate k js usedL usedR).flatten.map Prod.snd).Nodup ∧
      ∀ p ∈ (phaseAux adj mate k js usedL usedR).flatten, usedL p.1 = false ∧ usedR p.2 = false

Uses 10 · Used by 6

Statement usesAugmenting path · Partner arrays that describe a matching · Alternating breadth-first layers · Phase search over candidates

Proof usesAlternating path · Marking the left vertices of a path used · Marking the right vertices of a path used · Depth-first search of a Hopcroft–Karp phase · The dead set of a search only grows · Search paths are alternating paths through unused vertices

Used byA phase leaves no new unmatched left vertex · A successful Hopcroft–Karp step grows the matching · Distances do not decrease across a phase · Phases use shortest augmenting paths · Levels of the pairs of a phase · The paths of a phase are vertex-disjoint augmenting paths

TheoremFlipping disjoint alternating paths at once keeps a matching#✓fully proved

Let \(\mu\) be a valid partner array (partners are neighbours and no left vertex is the partner of two right vertices), \(k\) a natural number, and \(P_1, \dots, P_r\) paths each of which is an alternating path for \(\mu\), with round bound \(k\), from some right vertex. Suppose no left vertex and no right vertex occurs twice in the concatenation \(P_1 \cdots P_r\). Then the partner array obtained from \(\mu\) by matching each pair of the concatenation and keeping the other partners is valid.

theorem valid_flip_flatten (hv : Valid adj mate) {k : ℕ} {Ps : List (List (Fin a × Fin b))}
    (hPs : ∀ P ∈ Ps, ∃ j, AltPath adj mate k j P) (h1 : (Ps.flatten.map Prod.fst).Nodup)
    (h2 : (Ps.flatten.map Prod.snd).Nodup) : Valid adj (flip mate Ps.flatten)

Uses 4 · Used by 2

Statement usesAlternating path · Partner arrays that describe a matching · Flipping a list of pairs

Proof usesUnmatched left vertex

Used byA successful Hopcroft–Karp step grows the matching · The next phase's paths are strictly longer

TheoremFlipping disjoint augmenting paths matches at least one more vertex#✓fully proved

Let \(\mu\) be a partner array and let \(P_1, \dots, P_n\), with \(n \ge 1\), be augmenting paths for \(\mu\), all for the same number \(k\) of search rounds, such that no right vertex occurs twice in the concatenation \(P_1 P_2 \cdots P_n\). Then flipping this concatenation in \(\mu\) gives a partner array with at least one more matched right vertex than \(\mu\): the right vertices matched before stay matched, and so does the start of the first path.

theorem card_matched_flip_flatten {k : ℕ} {Ps : List (List (Fin a × Fin b))}
    (hPs : ∀ P ∈ Ps, ∃ j, IsAugmentingPath adj mate k j P) (h2 : (Ps.flatten.map Prod.snd).Nodup)
    (hne : Ps ≠ []) : (matched mate).card + 1 ≤ (matched (flip mate Ps.flatten)).card

Uses 4 · Used by 1

Statement usesAugmenting path · Flipping a list of pairs · Matched right vertices

Proof usesAlternating path

Used byA successful Hopcroft–Karp step grows the matching

TheoremA phase finds a path when an unmatched right vertex is reached#✓fully proved

If the partner array describes a matching and some unmatched right vertex is reached within \(a + 1\) rounds of the alternating breadth-first search, where \(a\) is the number of left vertices, then the phase finds at least one path.

The search from the first candidate always yields a path.

theorem phase_ne_nil (hv : Valid adj mate) {j : Fin b} (hj : mate j = none)
    (hR : j ∈ (layers adj mate (a + 1)).2) : phase adj mate ≠ []

Uses 11 · Used by 1

Statement usesPartner arrays that describe a matching · Alternating breadth-first layers · Hopcroft–Karp phase

Proof usesFirst free round · When there is no first free round · Characterization of the first free round · Marking the left vertices of a path used · Marking the right vertices of a path used · Phase search over candidates · Depth-first search of a Hopcroft–Karp phase · Searches from reached vertices succeed when nothing is used or dead

Used byA Hopcroft–Karp step that finds nothing

TheoremA successful Hopcroft–Karp step grows the matching#✓fully proved

Let \(\mu\) be a valid partner array (a matching of the graph). If the Hopcroft–Karp step on \(\mu\) returns a partner array \(\mu'\), then \(\mu'\) is valid and \(|\mathrm{matched}(\mu)| + 1 \le |\mathrm{matched}(\mu')|\), where \(\mathrm{matched}(\nu)\) is the set of right vertices that have a partner in \(\nu\).

theorem hkStep_some (hv : Valid adj mate) {mate' : Fin b → Option (Fin a)}
    (h : hkStep adj mate = some mate') :
    Valid adj mate' ∧ (matched mate).card + 1 ≤ (matched mate').card

Uses 13 · Used by 3

Statement usesPartner arrays that describe a matching · Hopcroft–Karp step · Matched right vertices

Proof usesAlternating path · Augmenting path · Flipping disjoint augmenting paths matches at least one more vertex · First free round · Flipping a list of pairs · Alternating breadth-first layers · Hopcroft–Karp phase · Phase search over candidates · Phase paths are disjoint augmenting paths · Flipping disjoint alternating paths at once keeps a matching

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Each phase lengthens the shortest augmenting paths · Correctness of the phase loop

TheoremA Hopcroft–Karp step that finds nothing#✓fully proved

Let \(\mu\) be a valid partner array (a matching of the graph, whose left vertices number \(a\)). If the Hopcroft–Karp step on \(\mu\) returns nothing, then no right vertex without a partner in \(\mu\) is reached within \(a + 1\) rounds of the alternating breadth-first layers of \(\mu\).

theorem hkStep_none (hv : Valid adj mate) (h : hkStep adj mate = none) :
    ∀ j, mate j = none → j ∉ (layers adj mate (a + 1)).2

Uses 6 · Used by 3

Statement usesPartner arrays that describe a matching · Hopcroft–Karp step · Alternating breadth-first layers

Proof usesFlipping a list of pairs · Hopcroft–Karp phase · A phase finds a path when an unmatched right vertex is reached

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Each phase lengthens the shortest augmenting paths · Correctness of the phase loop

TheoremCorrectness of the phase loop#✓fully proved

Let \(\mu\) be a valid partner array (a matching of the graph) on \(b\) right vertices, and let \(n \in \mathbb{N}\) be a fuel with \(b < |\mathrm{matched}(\mu)| + n\), where \(\mathrm{matched}(\mu)\) is the set of right vertices with a partner in \(\mu\); so \(n\) exceeds the number of unmatched right vertices. Let \(\mu'\) be the result of the Hopcroft–Karp phase loop with fuel \(n\) from \(\mu\). Then \(\mu'\) is valid, and every matching \(M\) of the graph satisfies \(|M| \le |\mathrm{pairs}(\mu')|\), where \(\mathrm{pairs}(\mu')\) is the set of pairs \((i, j)\) with \(\mu'(j) = i\).

theorem hopcroftKarpAux_spec : ∀ (fuel : ℕ) (mate : Fin b → Option (Fin a)), Valid adj mate →
    b < (matched mate).card + fuel →
    Valid adj (hopcroftKarpAux adj fuel mate) ∧
      ∀ M, IsMatching adj M → M.card ≤ (pairs (hopcroftKarpAux adj fuel mate)).card

Uses 9 · Used by 2

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Hopcroft–Karp phase loop · Matched right vertices · Matched pairs of a partner assignment

Proof usesKőnig's certificate · Hopcroft–Karp step · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching

Used byCorrectness of Hopcroft–Karp · Hopcroft–Karp returns a matching

TheoremHopcroft–Karp returns a matching#✓fully proved

For every bipartite graph with left vertices \(0, \dots, a-1\), right vertices \(0, \dots, b-1\) and an adjacency list for each left vertex, the pairs \((i, j)\) such that the Hopcroft–Karp algorithm makes \(i\) the partner of \(j\) form a matching of the graph: each pair is an edge, and no two distinct pairs share a left or a right vertex.

theorem isMatching_hopcroftKarp : IsMatching adj (pairs (hopcroftKarp adj))

Uses 8

Statement usesMatching in a bipartite graph · Hopcroft–Karp · Matched pairs of a partner assignment

Proof usesPartner arrays that describe a matching · Hopcroft–Karp phase loop · Correctness of the phase loop · A valid partner array gives a matching · Matched right vertices

TheoremCorrectness of Hopcroft–Karp#✓fully proved

No matching is larger than the result.

theorem card_le_hopcroftKarp {M : Finset (Fin a × Fin b)} (hM : IsMatching adj M) :
    M.card ≤ (pairs (hopcroftKarp adj)).card

Uses 7

Statement usesMatching in a bipartite graph · Hopcroft–Karp · Matched pairs of a partner assignment

Proof usesPartner arrays that describe a matching · Hopcroft–Karp phase loop · Correctness of the phase loop · Matched right vertices

Phases use shortest augmenting paths

TheoremThe start of an alternating chain of \(L\) pairs is reached within \(L\) rounds#✓fully proved

Let \(\mu\) be a partner array, let \(L \ge 1\), and let \((i_1, j_1), \dots, (i_L, j_L)\) be pairs of a left and a right vertex such that each \(j_t\) is adjacent to \(i_t\) with \(\mu(j_t) \ne i_t\), each \(j_{t+1}\) has partner \(\mu(j_{t+1}) = i_t\) for \(t < L\), and \(i_L\) is unmatched. Then \(j_1\) is among the right vertices reached within \(L\) rounds of the alternating layered search for \(\mu\).

From the unmatched end, each pair advances one round.

theorem mem_layers_length : ∀ (P : List (Fin a × Fin b)),
    (∀ p ∈ P, p.2 ∈ adj p.1 ∧ mate p.2 ≠ some p.1) →
    List.IsChain (fun p q => mate q.2 = some p.1) P → (∀ p ∈ P.getLast?, Free mate p.1) →
    ∀ p ∈ P.head?, p.2 ∈ (layers adj mate P.length).2

Uses 2 · Used by 5

Statement usesUnmatched left vertex · Alternating breadth-first layers

Used byNo augmenting path is shorter than a phase's · Levels of the pairs of a phase · Phases are maximal · Dead vertices have no escape · The second pair of a shortest alternating chain

TheoremNo augmenting path is shorter than a phase's#✓fully proved

Let \(\mu\) give each right vertex of a bipartite graph at most one partner among the left vertices. If the first free round of \(\mu\) is \(d\), then every augmenting path for \(\mu\) has at least \(d + 1\) pairs.

theorem le_length_of_isAugmentingPath {d k : ℕ} (hd : firstFreeRound adj mate = some d)
    {j : Fin b} {P : List (Fin a × Fin b)} (hP : IsAugmentingPath adj mate k j P) :
    d + 1 ≤ P.length

Uses 7 · Used by 2

Statement usesAugmenting path · First free round

Proof usesAlternating path · Unmatched left vertex · Characterization of the first free round · Alternating breadth-first layers · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds

Used byPhases use shortest augmenting paths · The next phase's paths are strictly longer

TheoremLength bound for search paths#✓fully proved

For every set of used left vertices, every level \(k\), every right vertex \(j\) and every set of dead right vertices, a path found by the search at level \(k\) from \(j\) has at most \(k + 1\) pairs.

theorem searchPath_length_le (usedL : Fin a → Bool) : ∀ (k : ℕ) (j : Fin b)
    (dead : Fin b → Bool) (P : List (Fin a × Fin b)),
    (searchPath adj mate usedL k j dead).1 = some P → P.length ≤ k + 1

Uses 6 · Used by 2

Statement usesDepth-first search of a Hopcroft–Karp phase

Proof usesAlternating breadth-first layers · Partner of a left vertex · The dead set of a search only grows · Trying the candidate predecessors of a right vertex · A path found by trying candidates comes from one candidate

Used byThe next phase's paths are strictly longer · Length bound for phase paths

TheoremLength bound for phase paths#✓fully proved

For every partner assignment \(\mathrm{mate}\), level \(k\), list of candidate right vertices and sets of used left and right vertices, every path that the phase search at level \(k\) collects from these candidates has at most \(k + 1\) pairs.

theorem phaseAux_length_le (k : ℕ) : ∀ (js : List (Fin b)) (usedL : Fin a → Bool)
    (usedR : Fin b → Bool), ∀ P ∈ phaseAux adj mate k js usedL usedR, P.length ≤ k + 1

Uses 5 · Used by 1

Statement usesPhase search over candidates

Proof usesMarking the left vertices of a path used · Marking the right vertices of a path used · Depth-first search of a Hopcroft–Karp phase · Length bound for search paths

Used byPhases use shortest augmenting paths

TheoremPhases use shortest augmenting paths#✓fully proved

Let \(\mu\) be a valid partner assignment of a bipartite graph (a matching) whose first free round is \(d\). Then every path of the phase of \(\mu\) has exactly \(d + 1\) pairs.

Every augmenting path for \(\mu\) has at least \(d + 1\) pairs, so these paths are shortest augmenting paths.

theorem length_of_mem_phase (hv : Valid adj mate) {d : ℕ} (hd : firstFreeRound adj mate = some d)
    {P : List (Fin a × Fin b)} (hP : P ∈ phase adj mate) : P.length = d + 1

Uses 9 · Used by 1

Statement usesPartner arrays that describe a matching · First free round · Hopcroft–Karp phase

Proof usesAugmenting path · Alternating breadth-first layers · No augmenting path is shorter than a phase's · Phase search over candidates · Length bound for phase paths · Phase paths are disjoint augmenting paths

Used byLevels of the pairs of a phase

Phases find maximal sets of shortest augmenting paths

DefinitionExact level of a right vertex#✓fully proved

For a partner array \(\mu\), a natural number \(m\) and a right vertex \(z\), \(z\) has exact level \(m\) when \(z\) is first reached in round \(m + 1\) of the layered search for \(\mu\): it is reached within \(m + 1\) rounds but not within \(m\) rounds.

def ExactLevel (mate : Fin b → Option (Fin a)) (m : ℕ) (z : Fin b) : Prop :=
  z ∈ (layers adj mate (m + 1)).2 ∧ z ∉ (layers adj mate m).2

Uses 1 · Used by 12

Statement usesAlternating breadth-first layers

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Distances do not decrease across a phase · The next phase's paths are strictly longer · No shortest escape · Shortest chains avoiding earlier paths contain no dead vertex · Levels along a shortest alternating chain · Levels of the pairs of a phase · Partners of predecessors lie one level earlier · Invariant of a phase · Phases are maximal · Dead vertices have no escape · The second pair of a shortest alternating chain

DefinitionAlternating chain to an unmatched left vertex#✓fully proved

In a bipartite graph, let each right vertex have at most one partner, a left vertex (the partners need not form a matching), and let \(z\) be a right vertex. A list \(Q\) of pairs (left vertex, right vertex) is an alternating chain from \(z\) when its first pair has right vertex \(z\), each of its pairs \((i, j)\) is an edge with \(i\) not the partner of \(j\), each right vertex after the first is the partner of the preceding left vertex, and its last left vertex is the partner of no right vertex.

Unlike an augmenting path, \(z\) may be matched, the vertices need not lie in the layers of the search, and a vertex may occur more than once.

def IsChainFrom (mate : Fin b → Option (Fin a)) (z : Fin b) (Q : List (Fin a × Fin b)) : Prop :=
  Q.head?.map Prod.snd = some z ∧ (∀ q ∈ Q, q.2 ∈ adj q.1 ∧ mate q.2 ≠ some q.1) ∧
    List.IsChain (fun p q => mate q.2 = some p.1) Q ∧ ∀ q ∈ Q.getLast?, Free mate q.1

Uses 1 · Used by 9

Statement usesUnmatched left vertex

Used byShortest chains from a vertex whose level a phase keeps were chains before it · The next phase's paths are strictly longer · No shortest escape · Shortest chains avoiding earlier paths contain no dead vertex · Levels along a shortest alternating chain · Invariant of a phase · Phases are maximal · Dead vertices have no escape · The second pair of a shortest alternating chain

DefinitionNo shortest escape#✓fully proved

Let \(\mu\) be a partner array, \(U\) a set of left vertices, \(D\) a set of right vertices and \(z\) a right vertex. Then \(z\) has no escape avoiding \(U\) and \(D\) when there are no \(m \in \mathbb{N}\) and no list of pairs \((i_1, j_1), \dots, (i_{m+1}, j_{m+1})\) such that \(z\) is first reached in round \(m + 1\) of the alternating layered search for \(\mu\), the list is an alternating chain from \(z\), no \(i_t\) lies in \(U\), and no \(j_t\) with \(t \ge 2\) lies in \(D\). Here the list is an alternating chain from \(z\) when \(j_1 = z\), each \(j_t\) is adjacent to \(i_t\) with \(\mu(j_t) \ne i_t\), \(\mu(j_{t+1}) = i_t\) for \(t \le m\), and \(i_{m+1}\) is unmatched.

A phase gives this property to every right vertex it marks dead after a failed search.

def NoEscape (mate : Fin b → Option (Fin a)) (U : Fin a → Bool) (D : Fin b → Bool) (z : Fin b) :
    Prop :=
  ∀ (m : ℕ) (Q : List (Fin a × Fin b)), ExactLevel adj mate m z → IsChainFrom adj mate z Q →
    Q.length = m + 1 → (∀ q ∈ Q, U q.1 = false) → (∀ q ∈ Q.tail, D q.2 = false) → False

Uses 2 · Used by 5

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex

Used byThe next phase's paths are strictly longer · Shortest chains avoiding earlier paths contain no dead vertex · Invariant of a phase · Phases are maximal · Dead vertices have no escape

TheoremThe second pair of a shortest alternating chain#✓fully proved

Let \(\mu\) be a partner array and \(z\) a right vertex first reached in round \(m + 1\) of the alternating breadth-first layers of \(\mu\), and let \(Q\) be an alternating chain for \(\mu\) from \(z\) ending at an unmatched left vertex, with exactly \(m + 1\) pairs, at least two of them. Let \((i', j')\) be the second pair of \(Q\). Then \(m \ge 1\), the right vertex \(j'\) is first reached in round \(m\), and \(Q\) without its first pair is an alternating chain for \(\mu\) from \(j'\) ending at an unmatched left vertex.

theorem ExactLevel.tail {m : ℕ} {z : Fin b} {s s' : Fin a × Fin b} {S : List (Fin a × Fin b)}
    (hz : ExactLevel adj mate m z) (hQ : IsChainFrom adj mate z (s :: s' :: S))
    (hlen : (s :: s' :: S).length = m + 1) :
    ∃ m', m = m' + 1 ∧ ExactLevel adj mate m' s'.2 ∧ IsChainFrom adj mate s'.2 (s' :: S)

Uses 5 · Used by 3

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex

Proof usesUnmatched left vertex · Alternating breadth-first layers · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Shortest chains avoiding earlier paths contain no dead vertex · Levels along a shortest alternating chain

TheoremPartners of predecessors lie one level earlier#✓fully proved

Let \(\mathrm{mate}\) be a valid partner assignment for the bipartite graph with adjacency lists \(\mathrm{adj}\). Let \(z\) be a right vertex first reached in round \(k + 2\) of the alternating layered search, let \(i\) be a left vertex reached within \(k + 1\) rounds with \(z \in \mathrm{adj}(i)\) and \(\mathrm{mate}(z) \ne i\), and let \(j'\) be a right vertex with \(\mathrm{mate}(j') = i\). Then \(j'\) is first reached in round \(k + 1\).

theorem ExactLevel.partner (hv : Valid adj mate) {k : ℕ} {z j' : Fin b} {i : Fin a}
    (hz : ExactLevel adj mate (k + 1) z) (hi : i ∈ (layers adj mate (k + 1)).1)
    (hadj : z ∈ adj i) (hm : mate z ≠ some i) (hp : mate j' = some i) :
    ExactLevel adj mate k j'

Uses 5 · Used by 1

Statement usesExact level of a right vertex · Partner arrays that describe a matching · Alternating breadth-first layers

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner

Used byDead vertices have no escape

TheoremWhere newly dead vertices come from#✓fully proved

For a right vertex \(j\), a test \(\mathrm{ok}\) on left vertices, a map \(\pi\) giving each left vertex an optional right vertex, and a search \(s\) taking a right vertex and a dead set (a set of right vertices) to an optional path and a new dead set, write \(T(l, D)\) for the optional path and the dead set returned by trying the left vertices of the list \(l\) as predecessors of \(j\), starting from the dead set \(D\). Suppose \(s\) never shrinks the dead set: for every right vertex \(j'\) and every dead set \(d\), the dead set returned by \(s(j', d)\) contains \(d\). Let \(E\) be the dead set of \(T(l, D)\) and let \(y\) be a right vertex in \(E\) but not in \(D\). Then either \(T(l, D)\) finds no path and \(y = j\), or there are a vertex \(i\) of \(l\) passing \(\mathrm{ok}\), a right vertex \(j'\) and a dead set \(d\) containing \(D\) such that \(\pi(i) = j'\), \(y \notin d\), \(y\) is in the dead set returned by \(s(j', d)\), and that dead set is contained in \(E\).

theorem tryPreds_dead {ok : Fin a → Bool} {partner : Fin a → Option (Fin b)}
    {search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)}
    (hs : ∀ j' d x, d x = true → (search j' d).2 x = true) (j : Fin b) :
    ∀ (is : List (Fin a)) (D : Fin b → Bool) (y : Fin b),
      (tryPreds ok partner search j is D).2 y = true → D y = false →
      ((tryPreds ok partner search j is D).1 = none ∧ y = j) ∨
        ∃ i ∈ is, ok i = true ∧ ∃ j' d, partner i = some j' ∧ (∀ x, D x = true → d x = true) ∧
          (search j' d).2 y = true ∧ d y = false ∧
          ∀ x, (search j' d).2 x = true → (tryPreds ok partner search j is D).2 x = true

Uses 2 · Used by 1

Statement usesTrying the candidate predecessors of a right vertex

Proof usesTrying candidates keeps dead vertices dead

Used byDead vertices have no escape

TheoremWhen trying candidates fails#✓fully proved

For a right vertex \(j\), a test \(\mathrm{ok}\) on left vertices, a map \(\pi\) giving each left vertex an optional right vertex, and a search \(s\) taking a right vertex and a dead set (a set of right vertices) to an optional path and a new dead set, write \(T(l, D)\) for the optional path and the dead set returned by trying the left vertices of the list \(l\) as predecessors of \(j\), starting from the dead set \(D\). Suppose \(s\) never shrinks the dead set: for every right vertex \(j'\) and every dead set \(d\), the dead set returned by \(s(j', d)\) contains \(d\). If \(T(l, D)\) finds no path, then \(j\) is in the dead set \(E\) of \(T(l, D)\), and for every vertex \(i\) of \(l\) passing \(\mathrm{ok}\) there are a right vertex \(j'\) and a dead set \(d\) such that \(\pi(i) = j'\), \(s(j', d)\) finds no path, and the dead set returned by \(s(j', d)\) is contained in \(E\).

theorem tryPreds_none {ok : Fin a → Bool} {partner : Fin a → Option (Fin b)}
    {search : Fin b → (Fin b → Bool) → Option (List (Fin a × Fin b)) × (Fin b → Bool)}
    (hs : ∀ j' d x, d x = true → (search j' d).2 x = true) (j : Fin b) :
    ∀ (is : List (Fin a)) (D : Fin b → Bool), (tryPreds ok partner search j is D).1 = none →
      (tryPreds ok partner search j is D).2 j = true ∧
      ∀ i ∈ is, ok i = true → ∃ j' d, partner i = some j' ∧ (search j' d).1 = none ∧
        ∀ x, (search j' d).2 x = true → (tryPreds ok partner search j is D).2 x = true

Uses 2 · Used by 2

Statement usesTrying the candidate predecessors of a right vertex

Proof usesTrying candidates keeps dead vertices dead

Used byDead vertices have no escape · A failed search marks its start dead

TheoremA failed search marks its start dead#✓fully proved

For every set of used left vertices, every level \(k\), every right vertex \(z\) and every set of dead right vertices, if the search at level \(k\) from \(z\) finds no path, then \(z\) is dead after it.

theorem searchPath_none_marks (U : Fin a → Bool) : ∀ (k : ℕ) (z : Fin b) (D : Fin b → Bool),
    (searchPath adj mate U k z D).1 = none → (searchPath adj mate U k z D).2 z = true

Uses 6 · Used by 2

Statement usesDepth-first search of a Hopcroft–Karp phase

Proof usesAlternating breadth-first layers · Partner of a left vertex · The dead set of a search only grows · Trying the candidate predecessors of a right vertex · When trying candidates fails

Used byInvariant of a phase · Dead vertices have no escape

TheoremDead vertices have no escape#✓fully proved

Suppose the partner array describes a matching. Run the search at level \(k\) from a right vertex \(z\) first reached in round \(k + 1\), with a set \(U\) of used left vertices and an initial set \(D\) of dead right vertices, and let \(D'\) be the dead set after it. Then every right vertex \(y\) in \(D'\) but not in \(D\) has no escape avoiding \(U\) and \(D'\): if \(y\) is first reached in round \(m + 1\), no alternating chain from \(y\) to an unmatched left vertex with \(m + 1\) pairs has all its left vertices outside \(U\) and all its right vertices after \(y\) outside \(D'\).

So Hopcroft and Karp's pruning loses no path.

theorem searchPath_dead (hv : Valid adj mate) (U : Fin a → Bool) : ∀ (k : ℕ) (z : Fin b)
    (D : Fin b → Bool), ExactLevel adj mate k z → ∀ y,
      (searchPath adj mate U k z D).2 y = true → D y = false →
      NoEscape adj mate U (searchPath adj mate U k z D).2 y

Uses 15 · Used by 1

Statement usesExact level of a right vertex · No shortest escape · Partner arrays that describe a matching · Depth-first search of a Hopcroft–Karp phase

Proof usesPartners of predecessors lie one level earlier · Unmatched left vertex · Alternating chain to an unmatched left vertex · Alternating breadth-first layers · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds · Partner of a left vertex · The dead set of a search only grows · A failed search marks its start dead · Trying the candidate predecessors of a right vertex · Where newly dead vertices come from · When trying candidates fails

Used byInvariant of a phase

TheoremShortest chains avoiding earlier paths contain no dead vertex#✓fully proved

Let \(\mu\) be a partner array, \(U\) a set of left vertices and \(D\) a set of right vertices, and let \(L\) be a set of left vertices and \(R\) a set of right vertices such that every vertex of \(U\) lies in \(L\) and every vertex of \(D\) lies in \(R\) or has no escape avoiding \(U\) and \(D\). Let \(m \in \mathbb{N}\), let \(z\) be a right vertex first reached in round \(m + 1\) of the alternating layered search for \(\mu\), and let \(S\) be an alternating chain from \(z\) with \(m + 1\) pairs such that no left vertex of \(S\) lies in \(L\) and no right vertex of \(S\) lies in \(R\). Then no right vertex of \(S\) lies in \(D\).

In a phase, \(L\) and \(R\) are the left and right vertices of the paths found so far.

theorem not_dead_of_chain {U : Fin a → Bool} {D : Fin b → Bool} {Lf : Fin a → Prop}
    {Rf : Fin b → Prop} (hU : ∀ i, U i = true → Lf i)
    (hD : ∀ y, D y = true → NoEscape adj mate U D y ∨ Rf y) :
    ∀ (S : List (Fin a × Fin b)) (z : Fin b) (m : ℕ), IsChainFrom adj mate z S →
      ExactLevel adj mate m z → S.length = m + 1 → (∀ q ∈ S, ¬ Lf q.1 ∧ ¬ Rf q.2) →
      ∀ q ∈ S, D q.2 = false

Uses 5 · Used by 1

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex · No shortest escape

Proof usesThe second pair of a shortest alternating chain · Unmatched left vertex

Used byInvariant of a phase

TheoremInvariant of a phase#✓fully proved

Let \(\mathrm{mate}\) be a valid partner assignment, let \(j\) be a right vertex first reached in round \(d + 1\) of the alternating layered search, and let \(Q\) be an alternating chain from \(j\) with \(d + 1\) pairs. Let \(J\) be a list of right vertices each first reached in round \(d + 1\), \(U\) a set of left vertices, \(D\) a set of right vertices and \(F\) a list of paths, such that every vertex in \(U\) is a left vertex of a path in \(F\), and every vertex in \(D\) either has no escape avoiding \(U\) and \(D\) or is a right vertex of a path in \(F\). If \(j\) is in \(J\) or in \(D\), then some path in \(F\), or among the paths that the phase search at level \(d\) collects from \(J\) with used left vertices \(U\) and used right vertices \(D\), shares a left vertex or a right vertex with \(Q\).

theorem phaseAux_maximal (hv : Valid adj mate) (d : ℕ) {j : Fin b} {Q : List (Fin a × Fin b)}
    (hQ : IsChainFrom adj mate j Q) (hj : ExactLevel adj mate d j) (hlen : Q.length = d + 1) :
    ∀ (js : List (Fin b)) (U : Fin a → Bool) (D : Fin b → Bool) (F : List (List (Fin a × Fin b))),
      (∀ j' ∈ js, ExactLevel adj mate d j') →
      (∀ i, U i = true → ∃ P ∈ F, i ∈ P.map Prod.fst) →
      (∀ y, D y = true → NoEscape adj mate U D y ∨ ∃ P ∈ F, y ∈ P.map Prod.snd) →
      (j ∈ js ∨ D j = true) →
      (∀ P ∈ F ++ phaseAux adj mate d js U D, ∀ q ∈ Q,
        q.1 ∉ P.map Prod.fst ∧ q.2 ∉ P.map Prod.snd) → False

Uses 16 · Used by 2

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex · No shortest escape · Partner arrays that describe a matching · Phase search over candidates

Proof usesAlternating path · Unmatched left vertex · Alternating breadth-first layers · Marking the left vertices of a path used · Marking the right vertices of a path used · Shortest chains avoiding earlier paths contain no dead vertex · Depth-first search of a Hopcroft–Karp phase · Dead vertices have no escape · The dead set of a search only grows · A failed search marks its start dead · Search paths are alternating paths through unused vertices

Used byThe next phase's paths are strictly longer · Phases are maximal

TheoremPhases are maximal#✓fully proved

Suppose the partner array describes a matching and \(d\) is the earliest round such that round \(d + 1\) of the alternating breadth-first search reaches an unmatched right vertex. Then for every \(k\), every augmenting path \(Q\) at level \(k\) with exactly \(d + 1\) pairs shares a vertex with some path \(P\) of the phase: some pair of \(Q\) has its left vertex among the left vertices of \(P\) or its right vertex among the right vertices of \(P\).

Every augmenting path has at least \(d + 1\) pairs, so these are the shortest augmenting paths, and the phase's vertex-disjoint shortest augmenting paths form a maximal set, as Hopcroft and Karp require.

theorem phase_maximal (hv : Valid adj mate) {d k : ℕ} (hd : firstFreeRound adj mate = some d)
    {j : Fin b} {Q : List (Fin a × Fin b)} (hQ : IsAugmentingPath adj mate k j Q)
    (hlen : Q.length = d + 1) :
    ∃ P ∈ phase adj mate, ∃ q ∈ Q, q.1 ∈ P.map Prod.fst ∨ q.2 ∈ P.map Prod.snd

Uses 14

Statement usesAugmenting path · Partner arrays that describe a matching · First free round · Hopcroft–Karp phase

Proof usesAlternating path · Exact level of a right vertex · Unmatched left vertex · Alternating chain to an unmatched left vertex · No shortest escape · Characterization of the first free round · Alternating breadth-first layers · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds · Phase search over candidates · Invariant of a phase

Distances do not decrease across a phase

TheoremA matched right vertex is reached no later than its partner#✓fully proved

Let \(\mu\) be a valid partner array (partners are neighbours, and no left vertex is the partner of two right vertices), let \(j\) be a right vertex with partner \(\mu(j) = i\), and let \(k \in \mathbb{N}\). If \(i\) is among the left vertices reached within \(k\) rounds of the alternating layered search for \(\mu\), then \(j\) is among the right vertices reached within \(k\) rounds.

theorem mem_layers_snd_of_mate (hv : Valid adj mate) {k : ℕ} {i : Fin a} {j : Fin b}
    (hm : mate j = some i) (hi : i ∈ (layers adj mate k).1) : j ∈ (layers adj mate k).2

Uses 4 · Used by 3

Statement usesPartner arrays that describe a matching · Alternating breadth-first layers

Proof usesUnmatched left vertex · Matched reached left vertices are reached through a partner

Used byOne round of the layered search bounds the deficit · Shortest chains from a vertex whose level a phase keeps were chains before it · Distances do not decrease across a phase

TheoremLevels along a shortest alternating chain#✓fully proved

Let \(\mu\) be a partner array, let \(m \in \mathbb{N}\), let \(z\) be a right vertex first reached in round \(m + 1\) of the alternating layered search for \(\mu\), and let \(S\) be an alternating chain from \(z\) with \(m + 1\) pairs. Then for every pair \((i, j)\) of \(S\) there is \(m' \in \mathbb{N}\) such that \(j\) is first reached in round \(m' + 1\) and \(i\) is reached within \(m'\) rounds.

theorem pair_levels_of_chain : ∀ (S : List (Fin a × Fin b)) (z : Fin b) (m : ℕ),
    IsChainFrom adj mate z S → ExactLevel adj mate m z → S.length = m + 1 →
    ∀ p ∈ S, ∃ m', ExactLevel adj mate m' p.2 ∧ p.1 ∈ (layers adj mate m').1

Uses 5 · Used by 2

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex · Alternating breadth-first layers

Proof usesThe second pair of a shortest alternating chain · Unmatched left vertex

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Levels of the pairs of a phase

TheoremLevels of the pairs of a phase#✓fully proved

In a bipartite graph with left vertices \(0, \dots, a-1\), let \(\mu\) be a valid partner array (partners are neighbours, and no left vertex is the partner of two right vertices), and let \(d \le a\) be such that round \(d + 1\) of the alternating layered search for \(\mu\) reaches an unmatched right vertex and no earlier round does. Then for every pair \((i, j)\) on a path of the Hopcroft–Karp phase for \(\mu\) there is \(m \in \mathbb{N}\) such that \(j\) is first reached in round \(m + 1\) and \(i\) is among the left vertices reached within \(m\) rounds.

theorem pair_levels_of_mem_phase (hv : Valid adj mate) {d : ℕ}
    (hd : firstFreeRound adj mate = some d) {p : Fin a × Fin b}
    (hp : p ∈ (phase adj mate).flatten) :
    ∃ m, ExactLevel adj mate m p.2 ∧ p.1 ∈ (layers adj mate m).1

Uses 14 · Used by 2

Statement usesExact level of a right vertex · Partner arrays that describe a matching · First free round · Alternating breadth-first layers · Hopcroft–Karp phase

Proof usesAlternating path · Unmatched left vertex · Augmenting path · Characterization of the first free round · Phases use shortest augmenting paths · The start of an alternating chain of \(L\) pairs is reached within \(L\) rounds · Levels along a shortest alternating chain · Phase search over candidates · Phase paths are disjoint augmenting paths

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Distances do not decrease across a phase

TheoremA phase leaves no new unmatched left vertex#✓fully proved

Let \(\mu\) be a valid partner array (a matching of the graph) whose first free round is defined, equal to some \(d\). If a left vertex \(i\) is unmatched in the flip of \(\mu\) along the concatenation of all the paths of the phase of \(\mu\), then \(i\) is unmatched in \(\mu\).

The first pair of each path starts at an unmatched right vertex, and every other right vertex of a path had the previous left vertex as partner, which the phase rematches.

theorem free_of_free_flip (hv : Valid adj mate) {d : ℕ} (hd : firstFreeRound adj mate = some d)
    {i : Fin a} (h : Free (flip mate (phase adj mate).flatten) i) : Free mate i

Uses 10 · Used by 2

Statement usesUnmatched left vertex · Partner arrays that describe a matching · First free round · Flipping a list of pairs · Hopcroft–Karp phase

Proof usesAlternating path · Augmenting path · Alternating breadth-first layers · Phase search over candidates · Phase paths are disjoint augmenting paths

Used byShortest chains from a vertex whose level a phase keeps were chains before it · Distances do not decrease across a phase

TheoremDistances do not decrease across a phase#✓fully proved

Let the partner array of a bipartite graph with \(a\) left vertices be valid, and suppose that some round \(r \le a + 1\) of the layered search reaches an unmatched right vertex, so that a phase runs from the earliest such round. After flipping all the paths that phase finds, for every \(k \in \mathbb{N}\) the left vertices and the right vertices reached within \(k\) rounds of the layered search were already reached within \(k\) rounds before the flip.

This is a step of Hopcroft and Karp's analysis.

theorem layers_flip_phase_subset (hv : Valid adj mate) {d : ℕ}
    (hd : firstFreeRound adj mate = some d) : ∀ k : ℕ,
    (layers adj (flip mate (phase adj mate).flatten) k).1 ⊆ (layers adj mate k).1 ∧
      (layers adj (flip mate (phase adj mate).flatten) k).2 ⊆ (layers adj mate k).2

Uses 13 · Used by 3

Statement usesPartner arrays that describe a matching · First free round · Flipping a list of pairs · Alternating breadth-first layers · Hopcroft–Karp phase

Proof usesExact level of a right vertex · Unmatched left vertex · Augmenting path · A phase leaves no new unmatched left vertex · A matched right vertex is reached no later than its partner · Levels of the pairs of a phase · Phase search over candidates · Phase paths are disjoint augmenting paths

Used byShortest chains from a vertex whose level a phase keeps were chains before it · The first free round does not decrease across a phase · The next phase's paths are strictly longer

TheoremThe first free round does not decrease across a phase#✓fully proved

Let \(\mu\) be a valid partner assignment of a bipartite graph (a matching), and let \(\mu'\) be obtained from \(\mu\) by flipping all the paths of the phase of \(\mu\) at once. If the first free round of \(\mu\) is \(d\) and the first free round of \(\mu'\) is \(d'\), then \(d \le d'\).

theorem le_firstFreeRound_flip_phase (hv : Valid adj mate) {d d' : ℕ}
    (hd : firstFreeRound adj mate = some d)
    (hd' : firstFreeRound adj (flip mate (phase adj mate).flatten) = some d') : d ≤ d'

Uses 7 · Used by 1

Statement usesPartner arrays that describe a matching · First free round · Flipping a list of pairs · Hopcroft–Karp phase

Proof usesCharacterization of the first free round · Alternating breadth-first layers · Distances do not decrease across a phase

Used byThe next phase's paths are strictly longer

TheoremThe paths of a phase are vertex-disjoint augmenting paths#✓fully proved

Suppose the partner array describes a matching and \(d\) is the earliest round such that round \(d + 1\) of the alternating breadth-first search reaches an unmatched right vertex. Then every path of the phase is an augmenting path at level \(d\) from some right vertex, and no left vertex and no right vertex occurs twice among the pairs of all the paths of the phase.

theorem phase_spec (hv : Valid adj mate) {d : ℕ} (hd : firstFreeRound adj mate = some d) :
    (∀ P ∈ phase adj mate, ∃ j, IsAugmentingPath adj mate d j P) ∧
      ((phase adj mate).flatten.map Prod.fst).Nodup ∧
      ((phase adj mate).flatten.map Prod.snd).Nodup

Uses 7 · Used by 2

Statement usesAugmenting path · Partner arrays that describe a matching · First free round · Hopcroft–Karp phase

Proof usesAlternating breadth-first layers · Phase search over candidates · Phase paths are disjoint augmenting paths

Used byShortest chains from a vertex whose level a phase keeps were chains before it · The next phase's paths are strictly longer

TheoremShortest chains from a vertex whose level a phase keeps were chains before it#✓fully proved

Let \(\mu\) be a valid partner array whose first free round is defined, and let \(\mu'\) be obtained from \(\mu\) by flipping all the paths of the phase of \(\mu\). Let \(z\) be a right vertex and \(m\) a natural number such that \(z\) is first reached in round \(m + 1\) of the layered search both for \(\mu\) and for \(\mu'\), and let \(S\) be an alternating chain for \(\mu'\) from \(z\) to an unmatched left vertex with exactly \(m + 1\) pairs. Then \(S\) is also an alternating chain for \(\mu\) from \(z\) to an unmatched left vertex, and for every pair of \(S\) after the first, its right vertex is not the right vertex of any pair on the paths of the phase.

A flipped edge would step back a round, which a chain of this length cannot afford.

theorem chain_of_chain_flip_phase (hv : Valid adj mate) {d : ℕ}
    (hd : firstFreeRound adj mate = some d) :
    ∀ (S : List (Fin a × Fin b)) (z : Fin b) (m : ℕ),
      IsChainFrom adj (flip mate (phase adj mate).flatten) z S → S.length = m + 1 →
      ExactLevel adj mate m z → ExactLevel adj (flip mate (phase adj mate).flatten) m z →
      IsChainFrom adj mate z S ∧ ∀ q ∈ S.tail, ∀ p ∈ (phase adj mate).flatten, p.2 ≠ q.2

Uses 16 · Used by 1

Statement usesExact level of a right vertex · Alternating chain to an unmatched left vertex · Partner arrays that describe a matching · First free round · Flipping a list of pairs · Hopcroft–Karp phase

Proof usesThe second pair of a shortest alternating chain · Unmatched left vertex · Augmenting path · A phase leaves no new unmatched left vertex · Alternating breadth-first layers · Distances do not decrease across a phase · A matched right vertex is reached no later than its partner · Levels along a shortest alternating chain · Levels of the pairs of a phase · The paths of a phase are vertex-disjoint augmenting paths

Used byThe next phase's paths are strictly longer

TheoremThe next phase's paths are strictly longer#✓fully proved

The next phase's paths are strictly longer (Hopcroft and Karp). Let \(\mu\) be a valid partner assignment of a bipartite graph (a matching), and let \(\mu'\) be obtained from \(\mu\) by flipping all the paths of the phase of \(\mu\) at once. If the first free round of \(\mu\) is \(d\) and the first free round of \(\mu'\) is \(d'\), then \(d < d'\).

A shortest augmenting path for \(\mu'\) of the same length would be a shortest augmenting chain for \(\mu\) that is disjoint from the paths of the phase, contradicting the maximality of the phase.

theorem lt_firstFreeRound_flip_phase (hv : Valid adj mate) {d d' : ℕ}
    (hd : firstFreeRound adj mate = some d)
    (hd' : firstFreeRound adj (flip mate (phase adj mate).flatten) = some d') : d < d'

Uses 24 · Used by 1

Statement usesPartner arrays that describe a matching · First free round · Flipping a list of pairs · Hopcroft–Karp phase

Proof usesAlternating path · Exact level of a right vertex · Unmatched left vertex · Augmenting path · Alternating chain to an unmatched left vertex · No shortest escape · Shortest chains from a vertex whose level a phase keeps were chains before it · Characterization of the first free round · Alternating breadth-first layers · Distances do not decrease across a phase · The first free round does not decrease across a phase · No augmenting path is shorter than a phase's · Phase search over candidates · Invariant of a phase · The paths of a phase are vertex-disjoint augmenting paths · Depth-first search of a Hopcroft–Karp phase · Searches from reached vertices succeed when nothing is used or dead · Length bound for search paths · Search paths are alternating paths through unused vertices · Flipping disjoint alternating paths at once keeps a matching

Used byEach phase lengthens the shortest augmenting paths

O(√V) phases

TheoremOne round of the layered search bounds the deficit#✓fully proved

If no unmatched right vertex is reached by round k + 1, every matching has at most as many edges as the current one plus the right vertices first reached in round k + 1: the unreached left vertices and the right vertices reached by round k + 1 cover every edge.

theorem card_le_card_pairs_add (hv : Valid adj mate) {M : Finset (Fin a × Fin b)}
    (hM : IsMatching adj M) {k : ℕ}
    (hk : ∀ j, mate j = none → j ∉ (layers adj mate (k + 1)).2) :
    M.card ≤ (pairs mate).card +
      ((layers adj mate (k + 1)).2 \ (layers adj mate k).2).card

Uses 6 · Used by 1

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Alternating breadth-first layers · Matched pairs of a partner assignment

Proof usesUnmatched left vertex · A matched right vertex is reached no later than its partner

Used byThe deficit is at most \(b / d\)

TheoremThe deficit is at most \(b / d\)#✓fully proved

In a bipartite graph with right vertices \(0, \dots, b-1\), let \(\mu\) be a valid partner array (partners are neighbours, and no left vertex is the partner of two right vertices), let \(M\) be any matching of the graph, and let \(d \in \mathbb{N}\). Suppose that for every \(k < d\), no unmatched right vertex is among the right vertices reached within \(k + 1\) rounds of the alternating layered search for \(\mu\). Then \(d \cdot \max(|M| - |P_\mu|, 0) \le |R_d|\), where \(P_\mu\) is the set of pairs \((i, j)\) with \(\mu(j) = i\) and \(R_d\) is the set of right vertices reached within \(d\) rounds.

This is the counting step of Hopcroft and Karp's bound: since \(R_d\) has at most \(b\) elements, the deficit of the current matching against any matching is at most \(b / d\) when \(d \ge 1\).

theorem mul_card_sub_le (hv : Valid adj mate) {M : Finset (Fin a × Fin b)}
    (hM : IsMatching adj M) : ∀ d : ℕ,
    (∀ k < d, ∀ j, mate j = none → j ∉ (layers adj mate (k + 1)).2) →
    d * (M.card - (pairs mate).card) ≤ (layers adj mate d).2.card

Uses 5 · Used by 1

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Alternating breadth-first layers · Matched pairs of a partner assignment

Proof usesOne round of the layered search bounds the deficit

Used byHopcroft and Karp's bound on the number of phases

TheoremThe phase loop stops when a step finds nothing#✓fully proved

If the Hopcroft–Karp step on a partner array \(\mu\) returns nothing, then for every fuel \(f \in \mathbb{N}\) the Hopcroft–Karp phase loop with fuel \(f\) from \(\mu\) returns \(\mu\).

theorem hopcroftKarpAux_of_hkStep_none (h : hkStep adj mate = none) :
    ∀ f, hopcroftKarpAux adj f mate = mate

Uses 2 · Used by 3

Statement usesHopcroft–Karp step · Hopcroft–Karp phase loop

Used byClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Each phase lengthens the shortest augmenting paths · Fuel adds up in the phase loop

TheoremFuel adds up in the phase loop#✓fully proved

For all \(f, g \in \mathbb{N}\) and every partner array \(\mu\), the Hopcroft–Karp phase loop with fuel \(f + g\) from \(\mu\) returns the same partner array as the loop with fuel \(g\) run from the result of the loop with fuel \(f\) from \(\mu\).

theorem hopcroftKarpAux_add : ∀ (f g : ℕ) (mate : Fin b → Option (Fin a)),
    hopcroftKarpAux adj (f + g) mate = hopcroftKarpAux adj g (hopcroftKarpAux adj f mate)

Uses 3 · Used by 1

Statement usesHopcroft–Karp phase loop

Proof usesHopcroft–Karp step · The phase loop stops when a step finds nothing

Used byHopcroft and Karp's bound on the number of phases

TheoremEach phase lengthens the shortest augmenting paths#✓fully proved

Let \(\mu\) be a valid partner array and \(c\) a natural number such that the first free round of \(\mu\), if defined, is at least \(c\). For every natural number \(f\), running at most \(f\) Hopcroft–Karp phases from \(\mu\), stopping early when a phase finds no path, gives a valid partner array whose first free round, if defined, is at least \(c + f\).

theorem firstFreeRound_hopcroftKarpAux : ∀ (f c : ℕ) (mate : Fin b → Option (Fin a)),
    Valid adj mate → (∀ d, firstFreeRound adj mate = some d → c ≤ d) →
    Valid adj (hopcroftKarpAux adj f mate) ∧
      ∀ d, firstFreeRound adj (hopcroftKarpAux adj f mate) = some d → c + f ≤ d

Uses 14 · Used by 1

Statement usesPartner arrays that describe a matching · First free round · Hopcroft–Karp phase loop

Proof usesWhen there is no first free round · Flipping a list of pairs · Hopcroft–Karp step · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · The phase loop stops when a step finds nothing · Alternating breadth-first layers · The next phase's paths are strictly longer · Matched right vertices · Hopcroft–Karp phase · Phase search over candidates

Used byHopcroft and Karp's bound on the number of phases

TheoremClosing a deficit of \(f\) in \(f\) Hopcroft–Karp phases#✓fully proved

Let \(\mu\) be a valid partner array, \(M\) a matching of the bipartite graph and \(f \in \mathbb{N}\). If \(M\) has at most \(f\) more pairs than the matched pairs of \(\mu\), then \(M\) has at most as many pairs as the matched pairs of the partner array returned by the Hopcroft–Karp phase loop with fuel \(f\) from \(\mu\).

Each phase that finds a path adds at least one edge, and a phase that finds none leaves a maximum matching.

theorem card_le_hopcroftKarpAux_of_le : ∀ (f : ℕ) (mate : Fin b → Option (Fin a)),
    Valid adj mate → ∀ M, IsMatching adj M → M.card ≤ (pairs mate).card + f →
      M.card ≤ (pairs (hopcroftKarpAux adj f mate)).card

Uses 11 · Used by 1

Statement usesMatching in a bipartite graph · Partner arrays that describe a matching · Hopcroft–Karp phase loop · Matched pairs of a partner assignment

Proof usesKőnig's certificate · Matched pairs and matched right vertices are equinumerous · Hopcroft–Karp step · A Hopcroft–Karp step that finds nothing · A successful Hopcroft–Karp step grows the matching · The phase loop stops when a step finds nothing · Matched right vertices

Used byHopcroft and Karp's bound on the number of phases

TheoremHopcroft and Karp's bound on the number of phases#✓fully proved

In a bipartite graph with \(b\) right vertices, run at most \(2 \lfloor \sqrt{b} \rfloor + 2\) Hopcroft–Karp phases from the empty matching, stopping early when a phase finds no augmenting path. Then no matching of the graph has more edges than the resulting one.

After the first \(\lfloor \sqrt{b} \rfloor + 1\) phases every augmenting path has more than \(\lfloor \sqrt{b} \rfloor\) pairs, so the deficit against any matching is at most \(\lfloor \sqrt{b} \rfloor\), and each further phase adds an edge.

theorem card_le_hopcroftKarpAux_sqrt {M : Finset (Fin a × Fin b)} (hM : IsMatching adj M) :
    M.card ≤ (pairs (hopcroftKarpAux adj (2 * Nat.sqrt b + 2) fun _ => none)).card

Uses 13

Statement usesMatching in a bipartite graph · Hopcroft–Karp phase loop · Matched pairs of a partner assignment

Proof usesPartner arrays that describe a matching · Closing a deficit of \(f\) in \(f\) Hopcroft–Karp phases · Kőnig's certificate · First free round · When there is no first free round · Characterization of the first free round · Each phase lengthens the shortest augmenting paths · Fuel adds up in the phase loop · Alternating breadth-first layers · The deficit is at most \(b / d\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.