CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 25. Matchings in Bipartite Graphs
25.2. The stable-marriage problem

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S1_Preference_Model
import CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S2_Gale_Shapley
import CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S3_Optimality

25.2. The stable-marriage problem

This section formalizes the stable-marriage problem of CLRS §25.2 and the Gale–Shapley proposal algorithm: the preference model (rank functions, pairings, blocking pairs, stability), the functional proposal loop with well-founded termination, and the stability theorems for its output.

Main results:

PreferenceProfile / Pairing: the preference and pairing model
Pairing.Stable: absence of blocking pairs (CLRS eq. (25.10))
gs: the Gale–Shapley output pairing
gs_terminates_le_n_sq: the proposal loop terminates within |M| · |W| proposals
gs_stable (Theorem 25.5): the Gale–Shapley output is stable
stable_matching_exists: every preference profile has a stable pairing
gs_perfect: equal-size sides yield a perfect Gale–Shapley pairing
gs_man_optimal (Theorem 25.6): every man receives his best valid partner
gs_woman_pessimal: the same output is woman-pessimal among stable pairings

Current gaps:

None for the finite preference model and the textbook optimality theorems.

Notation conventions used in this section:

M : men, W : women (finite types, DecidableEq)
P : preference profile with rank functions mRank / wRank (smaller ranks are better)
μ : pairing with partner functions mPartner / wPartner

Implementation details

The section is split into the following sub-modules:

Definitions and proofs

CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S1_Preference_Model

S1. Preference model

The combinatorial model of the stable-marriage problem of CLRS §25.2: a preference profile assigns every man a strict total order over the women and every woman a strict total order over the men, represented by distinct numeric ranks; a pairing records who is matched to whom; and stability is the absence of blocking pairs.

Main results:

PreferenceProfile: men's and women's rank functions (with distinct ranks)
PreferenceProfile.mPrefers / PreferenceProfile.wPrefers: strict preference relations derived from the ranks
Pairing: a consistent pair of partner functions (CLRS §25.2)
Pairing.IsPerfect: every man and every woman is matched
BlockingPair: a pair that would rather be together than with its current partners (CLRS eq. (25.9))
Stable: a pairing with no blocking pair (CLRS eq. (25.10))

namespace CLRSnamespace Matchings

A preference profile for the stable-marriage problem (CLRS §25.2): each man m ranks every woman by mRank m and each woman w ranks every man by wRank w, where smaller ranks mean higher preference. The rank functions are injective in the opposite argument, so every agent's preferences form a strict total order.

The rank man m assigns to woman w: smaller is better.

The rank woman w assigns to man m: smaller is better.

Every man ranks distinct women distinctly.

Every woman ranks distinct men distinctly.

              structure PreferenceProfile (M W : Type*) [Fintype M] [DecidableEq M]
    [Fintype W] [DecidableEq W] where  mRank : M → W → ℕ  wRank : W → M → ℕ  h_mRank_injective : ∀ m : M, Function.Injective (mRank m)  h_wRank_injective : ∀ w : W, Function.Injective (wRank w)

Man m prefers woman w₁ to woman w₂.

def PreferenceProfile.mPrefers {M W : Type*} [Fintype M] [DecidableEq M]
    [Fintype W] [DecidableEq W] (P : PreferenceProfile M W) (m : M) (w₁ w₂ : W) : Prop :=
  P.mRank m w₁ < P.mRank m w₂

Woman w prefers man m₁ to man m₂.

def PreferenceProfile.wPrefers {M W : Type*} [Fintype M] [DecidableEq M]
    [Fintype W] [DecidableEq W] (P : PreferenceProfile M W) (w : W) (m₁ m₂ : M) : Prop :=
  P.wRank w m₁ < P.wRank w m₂

A pairing of men and women (CLRS §25.2): mPartner m is the woman man m is matched to (if any) and wPartner w is the man woman w is matched to (if any), and the two sides agree: man m is matched to woman w if and only if woman w is matched to man m.

The woman each man is matched to, if any.

The man each woman is matched to, if any.

Mutual consistency: m is matched to w iff w is matched to m.

              structure Pairing (M W : Type*) where  mPartner : M → Option W  wPartner : W → Option M  h_consistency : ∀ m w, mPartner m = some w ↔ wPartner w = some m

namespace Pairing

A pairing is perfect when every man and every woman is matched (CLRS §25.2).

def IsPerfect {M W : Type*} (μ : Pairing M W) : Prop :=
  (∀ m, ∃ w, μ.mPartner m = some w) ∧ (∀ w, ∃ m, μ.wPartner w = some m)

(m, w) is a blocking pair for the pairing μ when m and w are not matched to each other and each of them either is unmatched or strictly prefers the other to its current partner (CLRS eq. (25.9)).

def BlockingPair {M W : Type*} [Fintype M] [DecidableEq M] [Fintype W] [DecidableEq W]
    (P : PreferenceProfile M W) (μ : Pairing M W) (m : M) (w : W) : Prop :=
  (μ.wPartner w = none ∨ ∃ m', μ.wPartner w = some m' ∧ P.wPrefers w m m') ∧
    (μ.mPartner m = none ∨ ∃ w', μ.mPartner m = some w' ∧ P.mPrefers m w w')

A pairing is stable when it has no blocking pair (CLRS eq. (25.10)).

def Stable {M W : Type*} [Fintype M] [DecidableEq M] [Fintype W] [DecidableEq W]
    (P : PreferenceProfile M W) (μ : Pairing M W) : Prop :=
  ∀ m w, ¬ BlockingPair P μ m w

              end Pairingend Matchingsend CLRS

CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S2_Gale_Shapley

S2. The Gale–Shapley proposal algorithm

A functional formulation of the Gale–Shapley algorithm of CLRS §25.2 as a loop over proposal steps: at each step a free man proposes to the woman he has not yet proposed to whom he ranks highest, and the woman accepts him exactly when she is free or prefers him to her current partner (in which case her current partner is freed). Each man proposes to each woman at most once, so the loop terminates within |M| · |W| proposals.

Main results:

GSState: the algorithm state (a pairing plus per-man proposed sets)
nextWoman: the most preferred woman a man has not yet proposed to
proposalStep / step: the one-step proposal/accept transition
Invariant: the loop invariants (matched women always prefer their current partner to any proposer; proposed sets are rank prefixes; a man's partner is always proposed to)
step_partner_improves: a woman's partner only improves over time
pendingCount / gsLoopN / gs: the well-founded loop and its final state
ProposedAt and proposedAt_before_of_prefers: proposals proceed in decreasing preference order

              namespace CLRSnamespace StableMarriageopen Finset Classical Matchingsvariable {M : Type*} [Fintype M] [DecidableEq M]variable {W : Type*} [Fintype W] [DecidableEq W]variable {P : PreferenceProfile M W}

The state of the Gale–Shapley proposal algorithm (CLRS §25.2): a pairing, together with the set of women each man has already proposed to.

The woman each man is currently matched to, if any.

The man each woman is currently matched to, if any.

Mutual consistency of the two partner functions.

The set of women each man has already proposed to.

              structure GSState (P : PreferenceProfile M W) where  mPartner : M → Option W  wPartner : W → Option M  h_consistency : ∀ m w, mPartner m = some w ↔ wPartner w = some m  proposed : M → Finset W

A proposal is pending when some free man has not yet proposed to every woman.

def hasPending (σ : GSState P) : Prop :=
  ∃ m, σ.mPartner m = none ∧ σ.proposed m ≠ Finset.univ

Woman w accepts man m when she is free or prefers him to her current partner.

def accepts (σ : GSState P) (m : M) (w : W) : Prop :=
  σ.wPartner w = none ∨ ∃ m₁, σ.wPartner w = some m₁ ∧ P.wPrefers w m m₁

A woman who has never been proposed to is free, and a man who has proposed to every woman has no next proposal.


lemma nextWoman_witness (σ : GSState P) (m : M) (hpend : σ.proposed m ≠ Finset.univ) :
    ∃ w : W, w ∈ Finset.univ \ σ.proposed m ∧
      ∀ w' ∈ Finset.univ \ σ.proposed m, P.mRank m w ≤ P.mRank m w' := by
  classical
  let S : Finset ℕ := (Finset.univ \ σ.proposed m).image (P.mRank m)
  have hSne : S.Nonempty := by
    have hcm : (Finset.univ \ σ.proposed m).Nonempty := by
      by_contra hcm
      have hEq : Finset.univ \ σ.proposed m = ∅ := Finset.not_nonempty_iff_eq_empty.mp hcm
      apply hpend
      ext x
      by_cases hx : x ∈ σ.proposed m
      · simp [hx]
      · exfalso
        have hx' : x ∈ Finset.univ \ σ.proposed m := by simp [hx]
        rw [hEq] at hx'
        simp at hx'
    rcases hcm with ⟨x, hx⟩
    exact ⟨P.mRank m x, Finset.mem_image.mpr ⟨x, hx, rfl⟩⟩
  let r : ℕ := S.min' hSne
  have hmin : r ∈ S ∧ ∀ b ∈ S, r ≤ b :=
    (Finset.min'_eq_iff (s := S) (H := hSne) r).mp rfl
  rcases Finset.mem_image.mp hmin.1 with ⟨w, hw, hrank⟩
  refine ⟨w, hw, ?_⟩
  intro w' hw'
  have hw'_rank : P.mRank m w' ∈ S := Finset.mem_image.mpr ⟨w', hw', rfl⟩
  have hle : r ≤ P.mRank m w' := hmin.2 (P.mRank m w') hw'_rank
  rw [← hrank] at hle
  exact hle

The woman a man proposes to next: the woman he has not yet proposed to whom he ranks highest (CLRS §25.2).

noncomputable def nextWoman (σ : GSState P) (m : M) (hpend : σ.proposed m ≠ Finset.univ) : W :=
  Classical.choose (nextWoman_witness σ m hpend)

The next woman a man proposes to has not been proposed to yet, so each man proposes to each woman at most once.

lemma nextWoman_not_proposed (σ : GSState P) (m : M) (hpend : σ.proposed m ≠ Finset.univ) :
    nextWoman σ m hpend ∉ σ.proposed m :=
  (Finset.mem_sdiff.mp (Classical.choose_spec (nextWoman_witness σ m hpend)).1).2

Every woman a man has not yet proposed to is ranked at least as high (that is, at most as preferred) as his next proposal.

lemma nextWoman_min_rank (σ : GSState P) (m : M) (hpend : σ.proposed m ≠ Finset.univ)
    {w' : W} (hw' : w' ∈ Finset.univ \ σ.proposed m) :
    P.mRank m (nextWoman σ m hpend) ≤ P.mRank m w' :=
  (Classical.choose_spec (nextWoman_witness σ m hpend)).2 w' hw'

The proposal step of a single free man m: he proposes to the woman he has not yet proposed to whom he ranks highest; she accepts him exactly when she is free or prefers him to her current partner, in which case her current partner is freed.

Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
noncomputable def proposalStep (σ : GSState P) (m : M) (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) : GSState P :=
  let w := nextWoman σ m hpend
  { mPartner := fun m' =>
      if accepts σ m w ∧ m' = m then some w
      else if accepts σ m w ∧ σ.wPartner w = some m' then none
      else σ.mPartner m'
    wPartner := fun w' =>
      if w' = w then (if accepts σ m w then some m else σ.wPartner w) else σ.wPartner w'
    h_consistency := by
      intro m' w'
      by_cases hacc : accepts σ m w
      · by_cases hmm : m' = m
        · by_cases hww : w' = w
          · simp [hacc, hmm, hww]
          · have hnot : σ.wPartner w' ≠ some m := by
              intro hw
              have hm := (σ.h_consistency m w').mpr hw
              simp [hfree] at hm
            have hwne : w ≠ w' := by
              intro h
              exact hww h.symm
            simp [hacc, hmm, hww, hnot, hwne]
        · by_cases hww : w' = w
          · subst w'
            by_cases hwm : σ.wPartner w = some m'
            · have hmne : m ≠ m' := by
                intro h
                exact hmm h.symm
              constructor
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hwm, hmne] using h
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hwm, hmne] using h
            · have hmw : σ.mPartner m' ≠ some w := by
                intro h
                exact hwm ((σ.h_consistency m' w).mp h)
              have hmne : m ≠ m' := by
                intro h
                exact hmm h.symm
              constructor
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hwm, hmw, hmne] using h
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hwm, hmw, hmne] using h
          · by_cases hwm : σ.wPartner w = some m'
            · have hnotw' : σ.wPartner w' ≠ some m' := by
                intro hw'
                have hm1 : σ.mPartner m' = some w := (σ.h_consistency m' w).mpr hwm
                have hm2 : σ.mPartner m' = some w' := (σ.h_consistency m' w').mpr hw'
                have hww' : w = w' := by
                  rw [hm1] at hm2
                  simpa using hm2
                exact hww hww'.symm
              constructor
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hwm] using h
              · intro h
                Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hacc, hmm, hww, hwm, hnotw'] using h
            · simp [hacc, hmm, hww, hwm]
              exact σ.h_consistency m' w'
      · by_cases hmm : m' = m
        · by_cases hww : w' = w
          · have hnot : σ.wPartner w ≠ some m := by
              intro hw
              have hm := (σ.h_consistency m w).mpr hw
              simp [hfree] at hm
            simp [hacc, hmm, hww, hnot, hfree]
          · have hnot : σ.wPartner w' ≠ some m := by
              intro hw
              have hm := (σ.h_consistency m w').mpr hw
              simp [hfree] at hm
            have hwne : w ≠ w' := by
              intro h
              exact hww h.symm
            simp [hacc, hmm, hww, hnot, This simp argument is unused:
  hwne

Hint: Omit it from the simp argument list.
  simp [hacc, hmm, hww, hnot, hw̵n̵e̵,̵ ̵h̵free]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hwne, hfree]
        · by_cases hww : w' = w
          · subst w'
            simp [hacc, hmm]
            exact σ.h_consistency m' w
          · simp [hacc, hmm, hww]
            exact σ.h_consistency m' w'
    proposed := fun m' => if m' = m then insert w (σ.proposed m') else σ.proposed m' }

In a proposal step, the proposing man's proposed set gains exactly the target woman.

lemma proposalStep_proposed_self {σ : GSState P} {m : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) :
    (proposalStep σ m hfree hpend).proposed m =
      insert (nextWoman σ m hpend) (σ.proposed m) := by
  simp [proposalStep]

Other men's proposed sets are unchanged by a proposal step.

lemma proposalStep_proposed_other {σ : GSState P} {m m' : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) (hmm : m' ≠ m) :
    (proposalStep σ m hfree hpend).proposed m' = σ.proposed m' := by
  simp [proposalStep, hmm]

The target woman's partner after a proposal step: she accepts exactly when she is free or prefers the proposer.

lemma proposalStep_wPartner_target {σ : GSState P} {m : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) :
    (proposalStep σ m hfree hpend).wPartner (nextWoman σ m hpend) =
      if accepts σ m (nextWoman σ m hpend) then some m
      else σ.wPartner (nextWoman σ m hpend) := by
  simp [proposalStep]

Other women's partners are unchanged by a proposal step.

lemma proposalStep_wPartner_other {σ : GSState P} {m : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) {w' : W} (hww : w' ≠ nextWoman σ m hpend) :
    (proposalStep σ m hfree hpend).wPartner w' = σ.wPartner w' := by
  simp [proposalStep, hww]

The proposing man's partner after a proposal step: the target woman when she accepts, and unmatched otherwise.


lemma proposalStep_mPartner_self {σ : GSState P} {m : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) :
    (proposalStep σ m hfree hpend).mPartner m =
      if accepts σ m (nextWoman σ m hpend) then some (nextWoman σ m hpend) else none := by
  by_cases hacc : accepts σ m (nextWoman σ m hpend)
  · simp [proposalStep, hacc, This simp argument is unused:
  hfree

Hint: Omit it from the simp argument list.
  simp [proposalStep, hacc,̵ ̵h̵f̵r̵e̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hfree]
  · simp [proposalStep, hacc, hfree]

When a woman accepts a new man, her current partner is freed.

lemma proposalStep_mPartner_dump {σ : GSState P} {m m' : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) (hmm : m' ≠ m)
    (hacc : accepts σ m (nextWoman σ m hpend))
    (hwm : σ.wPartner (nextWoman σ m hpend) = some m') :
    (proposalStep σ m hfree hpend).mPartner m' = none := by
  simp [proposalStep, hmm, hacc, hwm]

A man who is neither the proposer nor freed keeps his partner.

lemma proposalStep_mPartner_other {σ : GSState P} {m m' : M} (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) (hmm : m' ≠ m)
    (hnot : ¬ (accepts σ m (nextWoman σ m hpend) ∧
      σ.wPartner (nextWoman σ m hpend) = some m')) :
    (proposalStep σ m hfree hpend).mPartner m' = σ.mPartner m' := by
  simp [proposalStep, hmm, hnot]

One proposal step of the algorithm: an arbitrary free man with a pending proposal proposes to his most preferred unproposed woman. If no proposal is pending, the state is unchanged.

noncomputable def step (σ : GSState P) : GSState P :=
  if h : hasPending σ then
    proposalStep σ (Classical.choose h) (Classical.choose_spec h).1 (Classical.choose_spec h).2
  else σ

Without a pending proposal, a step changes nothing.

lemma step_eq_self_of_no_pending {σ : GSState P} (h : ¬ hasPending σ) : step σ = σ := by
  simp [step, h]

The loop invariants of the proposal algorithm: every woman who has been proposed to is matched, every matched woman prefers her current partner to every man who has proposed to her, every man's proposed set is a rank prefix (a woman of smaller rank implies all even more preferred women were proposed to), and every man has proposed to his current partner.

def Invariant (σ : GSState P) : Prop :=
  (∀ w m, w ∈ σ.proposed m → σ.wPartner w ≠ none) ∧
    (∀ w m₀, σ.wPartner w = some m₀ →
      ∀ m, w ∈ σ.proposed m → P.wRank w m₀ ≤ P.wRank w m) ∧
    (∀ m w₁ w₂, w₁ ∈ σ.proposed m → P.mRank m w₂ < P.mRank m w₁ → w₂ ∈ σ.proposed m) ∧
    (∀ m w, σ.mPartner m = some w → w ∈ σ.proposed m)

Every woman who has been proposed to is matched.

lemma Invariant.w_proposed_matched {σ : GSState P} (hσ : Invariant σ) {w : W} {m : M}
    (h : w ∈ σ.proposed m) : σ.wPartner w ≠ none :=
  hσ.1 w m h

A matched woman prefers her current partner to every man who has proposed to her.

lemma Invariant.best_among_proposers {σ : GSState P} (hσ : Invariant σ) {w : W} {m₀ : M}
    (hw : σ.wPartner w = some m₀) {m : M} (hm : w ∈ σ.proposed m) :
    P.wRank w m₀ ≤ P.wRank w m :=
  hσ.2.1 w m₀ hw m hm

Every man's proposed set is a rank prefix.

lemma Invariant.downward_closed {σ : GSState P} (hσ : Invariant σ) {m : M} {w₁ w₂ : W}
    (h₁ : w₁ ∈ σ.proposed m) (h₂ : P.mRank m w₂ < P.mRank m w₁) : w₂ ∈ σ.proposed m :=
  hσ.2.2.1 m w₁ w₂ h₁ h₂

Every man has proposed to his current partner.

lemma Invariant.partner_proposed {σ : GSState P} (hσ : Invariant σ) {m : M} {w : W}
    (h : σ.mPartner m = some w) : w ∈ σ.proposed m :=
  hσ.2.2.2 m w h

The initial state: nobody is matched and nobody has proposed.

def init : GSState P :=
  { mPartner := fun _ => none
    wPartner := fun _ => none
    h_consistency := by simp
    proposed := fun _ => ∅ }

The initial state satisfies the invariants.

lemma init_invariant : Invariant (init : GSState P) := by
  unfold Invariant init
  simp

A proposal step preserves the invariants.


lemma step_preserves_invariant {σ : GSState P} (hσ : Invariant σ) : Invariant (step σ) := by
  by_cases h : hasPending σ
  · have hstep : step σ = proposalStep σ (Classical.choose h) (Classical.choose_spec h).1
        (Classical.choose_spec h).2 := by
      simp [step, h]
    rw [hstep]
    let m := Classical.choose h
    have hspec := Classical.choose_spec h
    let w := nextWoman σ m hspec.2
    have hw_not : w ∉ σ.proposed m := nextWoman_not_proposed σ m hspec.2
    have hw_min : ∀ w' ∈ Finset.univ \ σ.proposed m, P.mRank m w ≤ P.mRank m w' := by
      intro w'' hw''
      exact nextWoman_min_rank σ m hspec.2 hw''
    unfold Invariant
    refine ⟨?_, ?_, ?_, ?_⟩
    · intro w' m' hmem
      by_cases hmm' : m' = m
      · subst m'
        have hmem' : w' ∈ insert w (σ.proposed m) := by
          rwa [proposalStep_proposed_self hspec.1 hspec.2] at hmem
        rcases Finset.mem_insert.mp hmem' with hw' | hw'
        · subst w'
          rw [proposalStep_wPartner_target hspec.1 hspec.2]
          change (if accepts σ m w then some m else σ.wPartner w) ≠ none
          by_cases hacc : accepts σ m w
          · simp [hacc]
          · simp [hacc]
            intro hnone
            exact hacc (Or.inl hnone)
        · have hwn : σ.wPartner w' ≠ none := hσ.w_proposed_matched hw'
          by_cases hww' : w' = w
          · subst w'
            exact False.elim (hw_not hw')
          · rw [proposalStep_wPartner_other hspec.1 hspec.2 hww']
            exact hwn
      · have hmem' : w' ∈ σ.proposed m' := by
          rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm'] at hmem
        have hwn : σ.wPartner w' ≠ none := hσ.w_proposed_matched hmem'
        by_cases hww' : w' = w
        · subst w'
          rw [proposalStep_wPartner_target hspec.1 hspec.2]
          change (if accepts σ m w then some m else σ.wPartner w) ≠ none
          by_cases hacc : accepts σ m w
          · simp [hacc]
          · simp [hacc]
            exact hwn
        · rw [proposalStep_wPartner_other hspec.1 hspec.2 hww']
          exact hwn
    · intro w' m₀ hwm₀
      by_cases hww' : w' = w
      · subst w'
        rw [proposalStep_wPartner_target hspec.1 hspec.2] at hwm₀
        change (if accepts σ m w then some m else σ.wPartner w) = some m₀ at hwm₀
        by_cases hacc : accepts σ m w
        · have hm₀ : m = m₀ := by
            simp [hacc] at hwm₀
            simpa using hwm₀
          subst m₀
          intro m'' hmem''
          by_cases hmm'' : m'' = m
          · subst m''
            rfl
          · have hmemσ : w ∈ σ.proposed m'' := by
              rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm''] at hmem''
            by_cases hwfree : σ.wPartner w = none
            · exact False.elim ((hσ.w_proposed_matched hmemσ) hwfree)
            · have hacc' : ∃ m₁, σ.wPartner w = some m₁ ∧ P.wPrefers w m m₁ := by
                rcases hacc with hnone | hpref
                · exact False.elim (hwfree hnone)
                · exact hpref
              rcases hacc' with ⟨m₁, hwm₁, hpref⟩
              have hle : P.wRank w m₁ ≤ P.wRank w m'' := hσ.best_among_proposers hwm₁ hmemσ
              exact le_trans (le_of_lt hpref) hle
        · have hwm₀' : σ.wPartner w = some m₀ := by
            simp [hacc] at hwm₀
            exact hwm₀
          have hnotpref : ¬ ∃ m₁, σ.wPartner w = some m₁ ∧ P.wPrefers w m m₁ := by
            intro hpref
            exact hacc (Or.inr hpref)
          have hnotw : ¬ P.wPrefers w m m₀ := by
            intro hpref
            exact hnotpref ⟨m₀, hwm₀', hpref⟩
          intro m'' hmem''
          by_cases hmm'' : m'' = m
          · subst m''
            exact le_of_not_gt hnotw
          · have hmemσ : w ∈ σ.proposed m'' := by
              rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm''] at hmem''
            exact hσ.best_among_proposers hwm₀' hmemσ
      · have hwmσ : σ.wPartner w' = some m₀ := by
          rwa [proposalStep_wPartner_other hspec.1 hspec.2 hww'] at hwm₀
        intro m'' hmem''
        by_cases hmm'' : m'' = m
        · subst m''
          have hmem' : w' ∈ insert w (σ.proposed m) := by
            rwa [proposalStep_proposed_self hspec.1 hspec.2] at hmem''
          rcases Finset.mem_insert.mp hmem' with hw' | hw'
          · subst w'
            exact False.elim (hww' rfl)
          · exact hσ.best_among_proposers hwmσ hw'
        · have hmemσ : w' ∈ σ.proposed m'' := by
            rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm''] at hmem''
          exact hσ.best_among_proposers hwmσ hmemσ
    · intro m' w₁ w₂ hmem₁ hlt
      by_cases hmm' : m' = m
      · subst m'
        have hmem₁' : w₁ ∈ insert w (σ.proposed m) := by
          rwa [proposalStep_proposed_self hspec.1 hspec.2] at hmem₁
        rcases Finset.mem_insert.mp hmem₁' with hw₁ | hw₁
        · subst w₁
          by_cases hw₂ : w₂ = w
          · subst w₂
            rw [proposalStep_proposed_self hspec.1 hspec.2]
            exact Finset.mem_insert_self w (σ.proposed m)
          · have hw₂' : w₂ ∈ σ.proposed m := by
              by_contra hnot
              have hw₂c : w₂ ∈ Finset.univ \ σ.proposed m :=
                Finset.mem_sdiff.mpr ⟨Finset.mem_univ w₂, hnot⟩
              exact (lt_irrefl (P.mRank m w)) (lt_of_le_of_lt (hw_min w₂ hw₂c) hlt)
            rw [proposalStep_proposed_self hspec.1 hspec.2]
            exact Finset.mem_insert_of_mem hw₂'
        · have hw₂' : w₂ ∈ σ.proposed m := hσ.downward_closed hw₁ hlt
          rw [proposalStep_proposed_self hspec.1 hspec.2]
          exact Finset.mem_insert_of_mem hw₂'
      · have hmem₁' : w₁ ∈ σ.proposed m' := by
          rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm'] at hmem₁
        have hw₂' : w₂ ∈ σ.proposed m' := hσ.downward_closed hmem₁' hlt
        rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm']
    · intro m' w' hm
      by_cases hmm' : m' = m
      · subst m'
        rw [proposalStep_mPartner_self hspec.1 hspec.2] at hm
        change (if accepts σ m w then some w else none) = some w' at hm
        by_cases hacc : accepts σ m w
        · simp [hacc] at hm
          have hEq : w = w' := by
            simpa using hm
          rw [← hEq]
          rw [proposalStep_proposed_self hspec.1 hspec.2]
          exact Finset.mem_insert_self w (σ.proposed m)
        · simp [hacc] at hm
      · by_cases hdump : accepts σ m w ∧ σ.wPartner w = some m'
        · rcases hdump with ⟨hacc, hwm⟩
          rw [proposalStep_mPartner_dump hspec.1 hspec.2 hmm' hacc hwm] at hm
          simp at hm
        · have hmσ : σ.mPartner m' = some w' := by
            rwa [proposalStep_mPartner_other hspec.1 hspec.2 hmm' hdump] at hm
          have hprop : w' ∈ σ.proposed m' := hσ.partner_proposed hmσ
          rwa [proposalStep_proposed_other hspec.1 hspec.2 hmm']
  · simp [step, h]
    exact hσ

Invariant (women only improve). When a woman changes partner in a proposal step, she strictly prefers the new partner to the old one.


lemma step_partner_improves {σ : GSState P} {w : W} {m₁ m₂ : M}
    (hold : σ.wPartner w = some m₁) (hnew : (step σ).wPartner w = some m₂)
    (hne : m₁ ≠ m₂) : P.wPrefers w m₂ m₁ := by
  by_cases h : hasPending σ
  · rw [step, dif_pos h] at hnew
    let m := Classical.choose h
    have hspec := Classical.choose_spec h
    by_cases hww : w = nextWoman σ m hspec.2
    · subst w
      rw [proposalStep_wPartner_target hspec.1 hspec.2] at hnew
      change (if accepts σ m (nextWoman σ m hspec.2) then some m
          else σ.wPartner (nextWoman σ m hspec.2)) = some m₂ at hnew
      by_cases hacc : accepts σ m (nextWoman σ m hspec.2)
      · simp [hacc] at hnew
        have hm₂ : m₂ = m := by
          exact hnew.symm
        subst m₂
        have hacc' : ∃ m₃, σ.wPartner (nextWoman σ m hspec.2) = some m₃ ∧
            P.wPrefers (nextWoman σ m hspec.2) m m₃ := by
          rcases hacc with hnone | hpref
          · exfalso
            rw [hold] at hnone
            simp at hnone
          · exact hpref
        rcases hacc' with ⟨m₃, hw₃, hpref⟩
        have hm₃ : m₃ = m₁ := by
          rw [hold] at hw₃
          exact Option.some.inj hw₃.symm
        simpa [hm₃] using hpref
      · simp [hacc] at hnew
        rw [hold] at hnew
        exact False.elim (hne (by simpa using hnew))
    · rw [proposalStep_wPartner_other hspec.1 hspec.2 hww] at hnew
      rw [hold] at hnew
      exact False.elim (hne (by simpa using hnew))
  · simp [step, h] at hnew
    rw [hold] at hnew
    exact False.elim (hne (by simpa using hnew))

Forget the proposal bookkeeping: a GS state is a pairing.

def GSState.toPairing (σ : GSState P) : Pairing M W :=
  { mPartner := σ.mPartner, wPartner := σ.wPartner, h_consistency := σ.h_consistency }

The number of proposals still to be made: the total count of women each man has not yet proposed to.

noncomputable def pendingCount (σ : GSState P) : ℕ :=
  ∑ m : M, (Fintype.card W - (σ.proposed m).card)

The proposed sets of a proposal step: the proposing man gains exactly the target woman, everyone else is unchanged.


lemma proposalStep_proposed (σ : GSState P) (m : M) (hfree : σ.mPartner m = none)
    (hpend : σ.proposed m ≠ Finset.univ) (m' : M) :
    (proposalStep σ m hfree hpend).proposed m' =
      if m' = m then insert (nextWoman σ m hpend) (σ.proposed m') else σ.proposed m' := by
  by_cases hmm' : m' = m
  · subst m'
    rw [proposalStep_proposed_self hfree hpend]
    simp
  · rw [proposalStep_proposed_other hfree hpend hmm']
    simp [hmm']

A proposal step strictly decreases the number of pending proposals.


lemma pendingCount_step_lt (σ : GSState P) (h : hasPending σ) :
    pendingCount (step σ) < pendingCount σ := by
  let m := Classical.choose h
  have hspec := Classical.choose_spec h
  have hstep : step σ = proposalStep σ m hspec.1 hspec.2 := by
    simp [step, h, m, This simp argument is unused:
  hspec

Hint: Omit it from the simp argument list.
  simp [step, h, m,̵ ̵h̵s̵p̵e̵c̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hspec]
  rw [hstep]
  unfold pendingCount
  have hdecrease : ∀ m' : M,
      (Fintype.card W - ((proposalStep σ m hspec.1 hspec.2).proposed m').card) ≤
        (Fintype.card W - (σ.proposed m').card) := by
    intro m'
    by_cases hmm' : m' = m
    · subst m'
      rw [proposalStep_proposed_self hspec.1 hspec.2]
      have hcard : (insert (nextWoman σ m hspec.2) (σ.proposed m)).card =
          (σ.proposed m).card + 1 :=
        Finset.card_insert_of_notMem (nextWoman_not_proposed σ m hspec.2)
      rw [hcard]
      omega
    · rw [proposalStep_proposed_other hspec.1 hspec.2 hmm']
  have hstrict : (Fintype.card W - ((proposalStep σ m hspec.1 hspec.2).proposed m).card) <
      (Fintype.card W - (σ.proposed m).card) := by
    rw [proposalStep_proposed_self hspec.1 hspec.2]
    have hcard : (insert (nextWoman σ m hspec.2) (σ.proposed m)).card =
        (σ.proposed m).card + 1 :=
      Finset.card_insert_of_notMem (nextWoman_not_proposed σ m hspec.2)
    rw [hcard]
    have hlt : (σ.proposed m).card < Fintype.card W := by
      exact Finset.card_lt_card
        (Finset.ssubset_iff_subset_ne.mpr ⟨Finset.subset_univ _, hspec.2⟩)
    omega
  exact Finset.sum_lt_sum (fun m' hm' => hdecrease m') ⟨m, Finset.mem_univ m, hstrict⟩

Iterating the proposal step n times.

noncomputable def gsLoopN : ℕ → GSState P → GSState P
  | 0, σ => σ
  | n + 1, σ => gsLoopN n (step σ)

The loop preserves the invariants.

lemma gsLoopN_invariant (σ : GSState P) (hσ : Invariant σ) (n : ℕ) :
    Invariant (gsLoopN n σ) := by
  induction n generalizing σ with
  | zero => simpa [gsLoopN]
  | succ n ih => simpa [gsLoopN] using ih (step σ) (step_preserves_invariant hσ)

Once no proposal is pending, further steps change nothing.

lemma gsLoopN_eq_self_of_no_pending {σ : GSState P} (h : ¬ hasPending σ) (n : ℕ) :
    gsLoopN n σ = σ := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp [gsLoopN, step_eq_self_of_no_pending h, ih]

The Gale–Shapley proposal loop (CLRS §25.2): repeat the proposal step until no proposal is pending. The recursion is well-founded on the pending count, which strictly decreases at every pending step, so the loop is guaranteed to halt.

noncomputable def gsLoop (σ : GSState P) : GSState P :=
  if Variable name `h` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`h : hasPending σ then gsLoop (step σ) else σ
termination_by pendingCount σ
decreasing_by
  exact pendingCount_step_lt σ h

The proposal loop halts: its output has no pending proposal.


lemma gsLoop_no_pending (σ : GSState P) : ¬ hasPending (gsLoop σ) := by
  rw [gsLoop]
  by_cases h : hasPending σ
  · simpa [h] using gsLoop_no_pending (step σ)
  · simp [h]
termination_by pendingCount σ
decreasing_by
  exact pendingCount_step_lt σ h

The proposal loop preserves the invariants.


lemma gsLoop_invariant (σ : GSState P) (hσ : Invariant σ) :
    Invariant (gsLoop σ) := by
  rw [gsLoop]
  by_cases h : hasPending σ
  · simpa [h] using gsLoop_invariant (step σ) (step_preserves_invariant hσ)
  · simpa [h]
termination_by pendingCount σ
decreasing_by
  exact pendingCount_step_lt σ h

The Gale–Shapley output pairing (CLRS §25.2): run the proposal loop from the empty state.

noncomputable def gs (P : PreferenceProfile M W) : Pairing M W :=
  (gsLoop (init : GSState P)).toPairing

end StableMarriageend CLRS

CLRSLean.FourthEdition.Chapter_25.Section_25_2_Stable_Marriage.S3_Optimality

S3. Optimality of the Gale–Shapley output

The stable-marriage theorems of CLRS §25.2: the Gale–Shapley output is a stable pairing, every preference profile admits a stable pairing, the output is a perfect pairing when the two sides have equal size, and the output is man-optimal and woman-pessimal.

Main results:

gs_stable: the Gale–Shapley output is stable (CLRS Theorem 25.5)
stable_matching_exists: every preference profile has a stable pairing
gs_perfect: with equal numbers of men and women, the Gale–Shapley output is a perfect pairing
gs_man_optimal: every man is matched to his best valid partner (CLRS Theorem 25.6)
gs_man_optimal_perfect: with equal numbers, every man is matched to his best valid partner
gs_woman_pessimal: every woman is matched to her worst valid partner
unmatched_man_proposes_to_all: at the final state an unmatched man has proposed to every woman

The man-optimality proof is time-indexed: runAt n is the state after n steps, proposesAt n m w detects that m proposes to w at step n+1 (w leaves his unproposed set), and rejectedAt n m w detects that w rejects m at step n+1. no_rejection_of_valid shows that no man is ever rejected by a valid partner: a rejection at step n+1 forces an earlier rejection of a valid partner (rejected_valid_earlier), contradicting minimality of the first such rejection. The proposal loop is placed on the timeline by gsLoop_eq_gsLoopN, which identifies the final state with the indexed run at its pending count.

              namespace CLRSnamespace StableMarriageopen Finset Classical Matchingsvariable {M : Type*} [Fintype M] [DecidableEq M]variable {W : Type*} [Fintype W] [DecidableEq W]variable (P : PreferenceProfile M W)

At the final state of the proposal loop, an unmatched man has proposed to every woman.

lemma unmatched_man_proposes_to_all (P : PreferenceProfile M W) {m : M}
    (hm : (gsLoop (init : GSState P)).mPartner m = none) :
    (gsLoop (init : GSState P)).proposed m = Finset.univ := by
  by_contra hnot
  exact gsLoop_no_pending (init : GSState P) ⟨m, hm, hnot⟩

Stability of the Gale–Shapley output (CLRS Theorem 25.5): the pairing produced by the proposal algorithm is stable.


theorem gs_stable (P : PreferenceProfile M W) : Pairing.Stable P (gs P) := by
  let σ : GSState P := gsLoop (init : GSState P)
  have hσ : Invariant σ := by
    unfold σ
    exact gsLoop_invariant (init : GSState P) init_invariant
  have hhalt : ¬ hasPending σ := by
    unfold σ
    exact gsLoop_no_pending (init : GSState P)
  intro m w hblock
  rcases hblock with ⟨hwside, hmside⟩
  have hwprop : w ∈ σ.proposed m := by
    by_cases hmfree : σ.mPartner m = none
    · have hpropall : σ.proposed m = Finset.univ := by
        by_contra hnot
        exact hhalt ⟨m, hmfree, hnot⟩
      rw [hpropall]
      exact Finset.mem_univ w
    · rcases hmside with hmun | ⟨w₀, hw₀, hpref⟩
      · exfalso
        exact hmfree (by simpa [σ, gs, GSState.toPairing] using hmun)
      · have hw₀prop : w₀ ∈ σ.proposed m :=
          hσ.partner_proposed (by simpa [σ, gs, GSState.toPairing] using hw₀)
        exact hσ.downward_closed hw₀prop hpref
  have hwmatched : σ.wPartner w ≠ none := hσ.w_proposed_matched hwprop
  rcases hwside with hwun | ⟨m₀, hwm₀, hpref_w⟩
  · exact False.elim (hwmatched (by simpa [σ, gs, GSState.toPairing] using hwun))
  · have hbest : P.wRank w m₀ ≤ P.wRank w m :=
      hσ.best_among_proposers (by simpa [σ, gs, GSState.toPairing] using hwm₀) hwprop
    exact (lt_irrefl (P.wRank w m₀)) (lt_of_le_of_lt hbest hpref_w)

Existence of stable matchings (CLRS §25.2): every preference profile admits a stable pairing — the Gale–Shapley output is one.

theorem stable_matching_exists (P : PreferenceProfile M W) :
    ∃ μ : Pairing M W, Pairing.Stable P μ :=
  ⟨gs P, gs_stable P⟩

A non-none option is some its value.

lemma ne_none_iff_exists {α : Type*} {a : Option α} (h : a ≠ none) :
    ∃ x, a = some x := by
  cases a with
  | none => exact False.elim (h (by rfl))
  | some x => exact ⟨x, rfl⟩

The matched women and the matched men of a consistent pairing have the same cardinality: the partner map w ↦ wPartner w is a bijection between them.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma matched_card_eq {σ : GSState P} (hM : Nonempty M) :
    (Finset.univ.filter fun w : W => σ.wPartner w ≠ none).card =
      (Finset.univ.filter fun m : M => σ.mPartner m ≠ none).card := by
  let f : W → M := fun w =>
    if hw : σ.wPartner w ≠ none then
      Classical.choose (ne_none_iff_exists hw)
    else Classical.choice hM
  refine Finset.card_bij (fun w hw => f w) ?_ ?_ ?_
  · intro a ha
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha ⊢
    have hf : f a = Classical.choose (ne_none_iff_exists ha) := by simp [f, ha]
    rw [hf]
    have hs : σ.wPartner a = some (Classical.choose (ne_none_iff_exists ha)) :=
      Classical.choose_spec (ne_none_iff_exists ha)
    intro hnot
    have hm := (σ.h_consistency (Classical.choose (ne_none_iff_exists ha)) a).mpr hs
    simp [hnot] at hm
  · intro a ha b hb hf
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb
    have hfa : f a = Classical.choose (ne_none_iff_exists ha) := by simp [f, ha]
    have hfb : f b = Classical.choose (ne_none_iff_exists hb) := by simp [f, hb]
    rw [hfa, hfb] at hf
    have hsa : σ.wPartner a = some (Classical.choose (ne_none_iff_exists ha)) :=
      Classical.choose_spec (ne_none_iff_exists ha)
    have hsb : σ.wPartner b = some (Classical.choose (ne_none_iff_exists hb)) :=
      Classical.choose_spec (ne_none_iff_exists hb)
    have hma : σ.mPartner (Classical.choose (ne_none_iff_exists ha)) = some a :=
      (σ.h_consistency (Classical.choose (ne_none_iff_exists ha)) a).mpr hsa
    have hmb : σ.mPartner (Classical.choose (ne_none_iff_exists hb)) = some b :=
      (σ.h_consistency (Classical.choose (ne_none_iff_exists hb)) b).mpr hsb
    have : some a = some b := by
      rw [← hma]
      rw [hf]
      rw [hmb]
    exact Option.some.inj this
  · intro b hb
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hb
    rcases ne_none_iff_exists hb with ⟨w, hw⟩
    have hwm : σ.wPartner w = some b := (σ.h_consistency b w).mp hw
    have hw' : σ.wPartner w ≠ none := by
      rw [hwm]
      simp
    refine ⟨w, ?_, ?_⟩
    · simp only [Finset.mem_filter, Finset.mem_univ, true_and]
      intro hnot
      have hmw := (σ.h_consistency b w).mp hw
      simp [hnot] at hmw
    · have hf : f w = Classical.choose (ne_none_iff_exists hw') := by simp [f, hw']
      rw [hf]
      have hs : σ.wPartner w = some (Classical.choose (ne_none_iff_exists hw')) :=
        Classical.choose_spec (ne_none_iff_exists hw')
      have hs' : some b = some (Classical.choose (ne_none_iff_exists hw')) := by
        try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hwm] using hs
      have hEq : Classical.choose (ne_none_iff_exists hw') = b := by
        exact Option.some.inj hs'.symm
      exact hEq

The matched set of a side is everything when its cardinality forces it.


lemma filter_eq_univ_of_card_eq {α : Type*} [Fintype α] [DecidableEq α]
    (p : α → Prop) [DecidablePred p] (h : (Finset.univ.filter p).card = Fintype.card α) :
    ∀ a : α, p a := by
  intro a
  by_contra hnot
  have hlt : (Finset.univ.filter p).card < Fintype.card α := by
    exact Finset.card_lt_card
      (Finset.ssubset_iff_subset_ne.mpr ⟨Finset.subset_univ _, by
        intro heq
        have hmem : a ∈ Finset.univ.filter p := by
          rw [heq]
          exact Finset.mem_univ a
        exact hnot (Finset.mem_filter.mp hmem).2⟩)
  omega

Perfectness of the Gale–Shapley output (CLRS §25.2): with equally many men and women, the algorithm terminates with a perfect pairing.


theorem gs_perfect (P : PreferenceProfile M W) (hcard : Fintype.card M = Fintype.card W) :
    (gs P).IsPerfect := by
  by_cases hM : Nonempty M
  · let σ : GSState P := gsLoop (init : GSState P)
    have hσ : Invariant σ := by
      unfold σ
      exact gsLoop_invariant (init : GSState P) init_invariant
    have hhalt : ¬ hasPending σ := by
      unfold σ
      exact gsLoop_no_pending (init : GSState P)
    have hbij : (Finset.univ.filter fun w : W => σ.wPartner w ≠ none).card =
        (Finset.univ.filter fun m : M => σ.mPartner m ≠ none).card :=
      matched_card_eq P hM
    have hmmatched : ∀ m : M, ∃ w : W, σ.mPartner m = some w := by
      intro m
      by_contra hnot
      have hmfree : σ.mPartner m = none := by
        by_contra hnotnone
        exact hnot (ne_none_iff_exists hnotnone)
      have hpropall : σ.proposed m = Finset.univ := by
        by_contra h
        exact hhalt ⟨m, hmfree, h⟩
      have hwmatched : ∀ w : W, σ.wPartner w ≠ none := by
        intro w
        have hwprop : w ∈ σ.proposed m := by
          rw [hpropall]
          exact Finset.mem_univ w
        exact hσ.w_proposed_matched hwprop
      have hcardW : (Finset.univ.filter fun w : W => σ.wPartner w ≠ none).card =
          Fintype.card W := by
        rw [show (Finset.univ.filter fun w : W => σ.wPartner w ≠ none) = Finset.univ by
          apply Finset.eq_univ_iff_forall.mpr
          intro w
          simp [hwmatched w]]
        simp
      have hcardM : (Finset.univ.filter fun m : M => σ.mPartner m ≠ none).card =
          Fintype.card M := by
        rw [← hbij, hcardW, hcard]
      have hall : ∀ m' : M, σ.mPartner m' ≠ none :=
        filter_eq_univ_of_card_eq (fun m : M => σ.mPartner m ≠ none) hcardM
      exact hnot (ne_none_iff_exists (hall m))
    have hwmatched : ∀ w : W, ∃ m : M, σ.wPartner w = some m := by
      intro w
      have hcardM : (Finset.univ.filter fun m : M => σ.mPartner m ≠ none).card =
          Fintype.card M := by
        rw [show (Finset.univ.filter fun m : M => σ.mPartner m ≠ none) = Finset.univ by
          apply Finset.eq_univ_iff_forall.mpr
          intro m
          rcases hmmatched m with ⟨w, hw⟩
          simp [hw]]
        simp
      have hcardW : (Finset.univ.filter fun w : W => σ.wPartner w ≠ none).card =
          Fintype.card W := by
        rw [hbij, hcardM, hcard]
      have hall : ∀ w' : W, σ.wPartner w' ≠ none :=
        filter_eq_univ_of_card_eq (fun w : W => σ.wPartner w ≠ none) hcardW
      exact ne_none_iff_exists (hall w)
    constructor
    · intro m
      exact hmmatched m
    · intro w
      exact hwmatched w
  · constructor
    · intro m
      exfalso
      exact hM ⟨m⟩
    · intro w
      exfalso
      have hW : ¬ Nonempty W := by
        intro hW
        have hcardW : Fintype.card W = 0 := by
          rw [← hcard]
          letI : IsEmpty M := not_nonempty_iff.mp hM
          exact Fintype.card_eq_zero (α := M)
        have hpos : 0 < Fintype.card W := (Fintype.card_pos_iff).mpr hW
        omega
      exact hW ⟨w⟩

A woman w is a valid partner of man m when some stable pairing matches m with w (CLRS §25.2).

def validPartner (P : PreferenceProfile M W) (m : M) (w : W) : Prop :=
  ∃ μ : Pairing M W, Pairing.Stable P μ ∧ μ.mPartner m = some w

The state of the proposal loop after exactly n steps from the initial state.

noncomputable def runAt (P : PreferenceProfile M W) (n : ℕ) : GSState P :=
  gsLoopN n (init : GSState P)

Running the loop n+1 times from σ is stepping the n-step run.

lemma gsLoopN_step_comm (σ : GSState P) (n : ℕ) :
    gsLoopN (n+1) σ = step (gsLoopN n σ) := by
  induction n generalizing σ with
  | zero => rfl
  | succ n ih =>
      calc
        gsLoopN (n+2) σ = gsLoopN (n+1) (step σ) := rfl
        _ = step (gsLoopN n (step σ)) := ih (step σ)
        _ = step (gsLoopN (n+1) σ) := by rfl

One more step of the indexed run steps the current state.

lemma runAt_succ (n : ℕ) : runAt P (n+1) = step (runAt P n) := by
  unfold runAt
  exact gsLoopN_step_comm P (init : GSState P) n

From a state with pending proposals, the pending count is positive.


lemma pendingCount_pos_of_hasPending (σ : GSState P) (h : hasPending σ) :
    1 ≤ pendingCount σ := by
  classical
  rcases h with ⟨m, hmfree, hpropne⟩
  unfold pendingCount
  have hlt : (σ.proposed m).card < Fintype.card W := by
    exact Finset.card_lt_card
      (Finset.ssubset_iff_subset_ne.mpr ⟨Finset.subset_univ _, hpropne⟩)
  have hterm : 1 ≤ Fintype.card W - (σ.proposed m).card := by omega
  have hsum : Fintype.card W - (σ.proposed m).card ≤
      ∑ m : M, (Fintype.card W - (σ.proposed m).card) := by
    exact Finset.single_le_sum
      (fun m' hm' => Nat.zero_le (Fintype.card W - (σ.proposed m').card))
      (Finset.mem_univ m)
  omega

The proposal loop is the indexed run at its pending count: after pendingCount σ steps the loop has halted.


lemma gsLoopN_eq_gsLoop_of_ge (σ : GSState P) (k : ℕ) (hk : pendingCount σ ≤ k) :
    gsLoopN k σ = gsLoop σ := by
  rw [gsLoop]
  by_cases h : hasPending σ
  · rw [dif_pos h]
    have hk1 : 1 ≤ k := le_trans (pendingCount_pos_of_hasPending P σ h) hk
    have hlt : pendingCount (step σ) < pendingCount σ := pendingCount_step_lt σ h
    have hk' : k = (k - 1) + 1 := by omega
    calc
      gsLoopN k σ = gsLoopN ((k - 1) + 1) σ := by rw [← hk']
      _ = gsLoopN (k - 1) (step σ) := rfl
      _ = gsLoop (step σ) := by
        exact gsLoopN_eq_gsLoop_of_ge (step σ) (k - 1) (by omega)
  · rw [dif_neg h]
    exact gsLoopN_eq_self_of_no_pending h k
termination_by pendingCount σ
decreasing_by
  exact pendingCount_step_lt σ h

The Gale–Shapley loop from σ equals the indexed run of length pendingCount σ.

lemma gsLoop_eq_gsLoopN (σ : GSState P) : gsLoop σ = gsLoopN (pendingCount σ) σ := by
  exact (gsLoopN_eq_gsLoop_of_ge P σ (pendingCount σ) le_rfl).symm

Man m proposes to woman w at step n+1: w leaves the unproposed set between the n-th and (n+1)-st states.

def proposesAt (n : ℕ) (m : M) (w : W) : Prop :=
  w ∉ (runAt P n).proposed m ∧ w ∈ (runAt P (n+1)).proposed m

Man m is rejected by woman w at step n+1: w either drops m between the two states, or rejects his proposal.

def rejectedAt (n : ℕ) (m : M) (w : W) : Prop :=
  ((runAt P n).mPartner m = some w ∧ (runAt P (n+1)).mPartner m ≠ some w) ∨
    (proposesAt P n m w ∧ ¬ accepts (runAt P n) m w)

A proposal at step n+1 is exactly the proposal step of m to his next woman.


lemma proposesAt_extract (n : ℕ) (m : M) (w : W) (hp : proposesAt P n m w) :
    ∃ hfree : (runAt P n).mPartner m = none,
      ∃ hpend : (runAt P n).proposed m ≠ Finset.univ,
        w = nextWoman (runAt P n) m hpend ∧ runAt P (n+1) = proposalStep (runAt P n) m hfree hpend := by
  classical
  unfold proposesAt at hp
  rw [runAt_succ P n] at hp ⊢
  by_cases h : hasPending (runAt P n)
  · let c := Classical.choose h
    have hspec := Classical.choose_spec h
    have hstep : step (runAt P n) = proposalStep (runAt P n) c hspec.1 hspec.2 := by
      simp [step, h, c]
    have hmem : w ∈ (step (runAt P n)).proposed m := hp.2
    have hmc : m = c := by
      by_contra hmc
      have h' : (proposalStep (runAt P n) c hspec.1 hspec.2).proposed m =
          (runAt P n).proposed m := by
        exact proposalStep_proposed_other hspec.1 hspec.2 hmc
      exact hp.1 (by simpa [hstep, h'] using hmem)
    subst m
    have hmem' : w ∈ insert (nextWoman (runAt P n) c hspec.2) ((runAt P n).proposed c) := by
      rw [← proposalStep_proposed_self hspec.1 hspec.2]
      rw [← hstep]
      exact hmem
    have hw : w = nextWoman (runAt P n) c hspec.2 := by
      rcases Finset.mem_insert.mp hmem' with hw | hmem''
      · exact hw
      · exact False.elim (hp.1 (by simpa using hmem''))
    refine ⟨hspec.1, hspec.2, hw, ?_⟩
    exact hstep
  · have h' : step (runAt P n) = runAt P n := step_eq_self_of_no_pending h
    rw [h'] at hp
    exact False.elim (hp.1 hp.2)

A man proposing at step n+1 is free at time n.

lemma proposesAt_free (n : ℕ) (m : M) (w : W) (hp : proposesAt P n m w) :
    (runAt P n).mPartner m = none := by
  rcases proposesAt_extract P n m w hp with ⟨hfree, hpend, hw, hstep⟩
  exact hfree

The proposer's partner after a proposal step: the target woman when she accepts, and unmatched otherwise.


lemma proposesAt_self (n : ℕ) (m : M) (w : W) (hp : proposesAt P n m w) :
    (runAt P (n+1)).mPartner m = if accepts (runAt P n) m w then some w else none := by
  rcases proposesAt_extract P n m w hp with ⟨hfree, hpend, hw, hstep⟩
  rw [hstep]
  simpa [← hw] using proposalStep_mPartner_self hfree hpend

The target woman's partner after a proposal step: the proposer when she accepts, and unchanged otherwise.


lemma proposesAt_target (n : ℕ) (m : M) (w : W) (hp : proposesAt P n m w) :
    (runAt P (n+1)).wPartner w = if accepts (runAt P n) m w then some m else (runAt P n).wPartner w := by
  rcases proposesAt_extract P n m w hp with ⟨hfree, hpend, hw, hstep⟩
  rw [hstep]
  simpa [← hw] using proposalStep_wPartner_target hfree hpend

If w is in a man's proposed set at time b ≥ 1, he proposed to her at some earlier step.


lemma proposesAt_exists (b : ℕ) (m : M) (w : W) (Variable name `hb` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hb : 1 ≤ b)
    (h : w ∈ (runAt P b).proposed m) : ∃ n < b, proposesAt P n m w := by
  classical
  have hnonempty : ∃ t : ℕ, w ∈ (runAt P t).proposed m := ⟨b, h⟩
  let t₀ : ℕ := Nat.find hnonempty
  have ht₀ : w ∈ (runAt P t₀).proposed m := Nat.find_spec hnonempty
  have htmin : ∀ t < t₀, w ∉ (runAt P t).proposed m := by
    intro t ht
    exact Nat.find_min hnonempty ht
  have ht₀ge : 1 ≤ t₀ := by
    by_contra ht0
    have ht₀' : t₀ = 0 := by omega
    rw [ht₀'] at ht₀
    have hfalse : False := by
      simp [runAt, gsLoopN, init] at ht₀
    exact hfalse
  have ht₀le : t₀ ≤ b := by
    by_contra htle
    exact htmin b (by omega) h
  refine ⟨t₀ - 1, by omega, ?_⟩
  constructor
  · exact htmin (t₀ - 1) (by omega)
  · have ht₀' : t₀ - 1 + 1 = t₀ := by omega
    rw [ht₀']
    exact ht₀

At a rejection step, the rejecting woman is matched to a man she strictly prefers to the rejected man.

Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at hwm` instead of `simpa using hwm`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma rejectedAt_new_partner (n : ℕ) (m : M) (w : W) (hrej : rejectedAt P n m w) :
    ∃ m₀, (runAt P (n+1)).wPartner w = some m₀ ∧ P.wPrefers w m₀ m := by
  rcases hrej with hB | hA
  · rcases hB with ⟨hwm, hnotm⟩
    by_cases h : hasPending (runAt P n)
    · let c := Classical.choose h
      have hspec := Classical.choose_spec h
      have hstep : step (runAt P n) = proposalStep (runAt P n) c hspec.1 hspec.2 := by
        simp [step, h, c]
      let w₀ : W := nextWoman (runAt P n) c hspec.2
      have hmc : m ≠ c := by
        intro hmc
        have hc : (runAt P n).mPartner m = none := by simpa [hmc] using hspec.1
        exact (by Try `simp at hwm` instead of `simpa using hwm`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hc] using hwm)
      have hacc : accepts (runAt P n) c w₀ ∧ (runAt P n).wPartner w₀ = some m := by
        by_contra hnot'
        have hm' : (proposalStep (runAt P n) c hspec.1 hspec.2).mPartner m =
            (runAt P n).mPartner m := by
          exact proposalStep_mPartner_other hspec.1 hspec.2 hmc hnot'
        have hm'w : (runAt P (n+1)).mPartner m = some w := by
          rw [runAt_succ P n, hstep, hm', hwm]
        exact hnotm hm'w
      have hw₀ : w₀ = w := by
        have h1 : (runAt P n).mPartner m = some w₀ :=
          ((runAt P n).h_consistency m w₀).mpr hacc.2
        exact Option.some.inj (by rw [← h1, hwm])
      have hwnew : (runAt P (n+1)).wPartner w = some c := by
        rw [runAt_succ P n, hstep]
        have htarget : (proposalStep (runAt P n) c hspec.1 hspec.2).wPartner
            (nextWoman (runAt P n) c hspec.2) = some c := by
          simpa [w₀, hacc.1] using proposalStep_wPartner_target (σ := runAt P n) (m := c)
            hspec.1 hspec.2
        rw [← hw₀]
        exact htarget
      have hwmn : (runAt P n).wPartner w = some m := ((runAt P n).h_consistency m w).mp hwm
      have hpref : P.wPrefers w c m := by
        rcases hacc.1 with hfree' | hpref'
        · exact False.elim (by simp [← hw₀, hfree'] at hwmn)
        · rcases hpref' with ⟨m₁, hwm₁, hp'⟩
          have hm₁ : m₁ = m := Option.some.inj (by rw [← hwm₁, hw₀, hwmn])
          simpa [hw₀, hm₁] using hp'
      exact ⟨c, hwnew, hpref⟩
    · have hstep : step (runAt P n) = runAt P n := step_eq_self_of_no_pending h
      have hm' : (runAt P (n+1)).mPartner m = (runAt P n).mPartner m := by
        rw [runAt_succ P n, hstep]
      exact False.elim (hnotm (by simpa [hm'] using hwm))
  · rcases hA with ⟨hp, hnotacc⟩
    rcases proposesAt_extract P n m w hp with ⟨hfree, hpend, hw, hstep⟩
    have hwne : (runAt P n).wPartner w ≠ none := by
      intro hnone
      exact hnotacc (Or.inl hnone)
    rcases ne_none_iff_exists hwne with ⟨m₀, hwm₀⟩
    refine ⟨m₀, ?_, ?_⟩
    · rw [hstep, hw]
      have hnotacc' : ¬ accepts (runAt P n) m (nextWoman (runAt P n) m hpend) := by
        simpa [hw] using hnotacc
      have htarget : (proposalStep (runAt P n) m hfree hpend).wPartner
          (nextWoman (runAt P n) m hpend) =
          (runAt P n).wPartner (nextWoman (runAt P n) m hpend) := by
        rw [proposalStep_wPartner_target hfree hpend]
        rw [if_neg hnotacc']
      rw [htarget, hw.symm]
      exact hwm₀
    · have hnotpref : ¬ P.wPrefers w m m₀ := by
        intro hp'
        exact hnotacc (Or.inr ⟨m₀, hwm₀, hp'⟩)
      have hm₀ne : m₀ ≠ m := by
        intro hm₀
        have h : (runAt P n).mPartner m = some w := ((runAt P n).h_consistency m w).mpr
          (by simpa [hm₀] using hwm₀)
        exact False.elim (by Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hfree] using h)
      have hle : P.wRank w m₀ ≤ P.wRank w m := le_of_not_gt hnotpref
      have hne : P.wRank w m₀ ≠ P.wRank w m := Function.Injective.ne (P.h_wRank_injective w) hm₀ne
      exact lt_of_le_of_ne hle hne

After a rejection step the new partner m₀ of the rejecting woman has already proposed to every woman w₀ he strictly prefers to her by time n: his proposed set does not gain w₀ at the rejection step, and he is not matched to w₀ at time n.

Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try `simp at hwm` instead of `simpa using hwm`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
lemma rejection_partner_facts (n : ℕ) (m : M) (w : W) (m₀ : M) (w₀ : W)
    (hrej : rejectedAt P n m w) (hwm₀new : (runAt P (n+1)).wPartner w = some m₀)
    (hm₀ne : m₀ ≠ m) (hw₀ne : w₀ ≠ w) (hw₀part : w₀ ∈ (runAt P (n+1)).proposed m₀) :
    w₀ ∈ (runAt P n).proposed m₀ ∧ (runAt P n).mPartner m₀ ≠ some w₀ := by
  rcases hrej with hB | hA
  · rcases hB with ⟨hwm, hnotm⟩
    by_cases h : hasPending (runAt P n)
    · let c := Classical.choose h
      have hspec := Classical.choose_spec h
      have hstep : step (runAt P n) = proposalStep (runAt P n) c hspec.1 hspec.2 := by
        simp [step, h, c]
      let w₀' : W := nextWoman (runAt P n) c hspec.2
      have hmc : m ≠ c := by
        intro hmc
        have hc : (runAt P n).mPartner m = none := by simpa [hmc] using hspec.1
        exact (by Try `simp at hwm` instead of `simpa using hwm`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hc] using hwm)
      have hacc : accepts (runAt P n) c w₀' ∧ (runAt P n).wPartner w₀' = some m := by
        by_contra hnot'
        have hm' : (proposalStep (runAt P n) c hspec.1 hspec.2).mPartner m =
            (runAt P n).mPartner m := by
          exact proposalStep_mPartner_other hspec.1 hspec.2 hmc hnot'
        have hm'w : (runAt P (n+1)).mPartner m = some w := by
          rw [runAt_succ P n, hstep, hm', hwm]
        exact hnotm hm'w
      have hw₀' : w₀' = w := by
        have h1 : (runAt P n).mPartner m = some w₀' :=
          ((runAt P n).h_consistency m w₀').mpr hacc.2
        exact Option.some.inj (by rw [← h1, hwm])
      have hm₀c : m₀ = c := by
        have hwnew : (runAt P (n+1)).wPartner w = some c := by
          rw [runAt_succ P n, hstep]
          have htarget : (proposalStep (runAt P n) c hspec.1 hspec.2).wPartner
              (nextWoman (runAt P n) c hspec.2) = some c := by
            simpa [w₀', hacc.1] using proposalStep_wPartner_target (σ := runAt P n) (m := c)
              hspec.1 hspec.2
          rw [← hw₀']
          exact htarget
        exact Option.some.inj (by rw [← hwnew, hwm₀new])
      have hw₀partn : w₀ ∈ (runAt P n).proposed m₀ := by
        have hprop : (runAt P (n+1)).proposed m₀ = insert w ((runAt P n).proposed m₀) := by
          rw [runAt_succ P n, hstep]
          rw [hm₀c]
          rw [proposalStep_proposed_self hspec.1 hspec.2]
          change insert (w₀' : W) ((runAt P n).proposed c) = insert w ((runAt P n).proposed c)
          rw [hw₀']
        rw [hprop] at hw₀part
        rcases Finset.mem_insert.mp hw₀part with hw₀eq | hw₀in
        · exact False.elim (hw₀ne hw₀eq)
        · exact hw₀in
      have hmn₀ : (runAt P n).mPartner m₀ ≠ some w₀ := by
        have hm₀none : (runAt P n).mPartner m₀ = none := by simpa [hm₀c] using hspec.1
        intro h
        exact (by Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hm₀none] using h)
      exact ⟨hw₀partn, hmn₀⟩
    · have hstep : step (runAt P n) = runAt P n := step_eq_self_of_no_pending h
      have hm' : (runAt P (n+1)).mPartner m = (runAt P n).mPartner m := by
        rw [runAt_succ P n, hstep]
      exact False.elim (hnotm (by simpa [hm'] using hwm))
  · rcases hA with ⟨hp, hnotacc⟩
    rcases proposesAt_extract P n m w hp with ⟨hfree, hpend, hw, hstep⟩
    have hw₀partn : w₀ ∈ (runAt P n).proposed m₀ := by
      have hprop : (runAt P (n+1)).proposed m₀ = (runAt P n).proposed m₀ := by
        rw [hstep]
        exact proposalStep_proposed_other hfree hpend hm₀ne
      rwa [← hprop]
    have hmn₀ : (runAt P n).mPartner m₀ ≠ some w₀ := by
      have hnot' : ¬ (accepts (runAt P n) m (nextWoman (runAt P n) m hpend) ∧
          (runAt P n).wPartner (nextWoman (runAt P n) m hpend) = some m₀) := by
        intro hc
        have hwm' : (runAt P (n+1)).wPartner w = some m := by
          rw [hstep, hw]
          have htarget : (proposalStep (runAt P n) m hfree hpend).wPartner
              (nextWoman (runAt P n) m hpend) = some m := by
            simpa [hc.1] using proposalStep_wPartner_target (σ := runAt P n) (m := m) hfree hpend
          exact htarget
        exact hm₀ne (Option.some.inj (by rw [← hwm', hwm₀new]))
      have hm' : (runAt P n).mPartner m₀ = some w := by
        have hmm' : (proposalStep (runAt P n) m hfree hpend).mPartner m₀ =
            (runAt P n).mPartner m₀ :=
          proposalStep_mPartner_other hfree hpend hm₀ne hnot'
        have hcons : (proposalStep (runAt P n) m hfree hpend).mPartner m₀ = some w :=
          ((proposalStep (runAt P n) m hfree hpend).h_consistency m₀ w).mpr
            (by simpa [hstep] using hwm₀new)
        rw [← hmm', hcons]
      intro h
      have hw₀eq : w = w₀ := Option.some.inj (by rw [← h, hm'])
      exact hw₀ne hw₀eq.symm
    exact ⟨hw₀partn, hmn₀⟩

A rejection of a valid partner implies an earlier rejection of a valid partner: from a rejection at step n+1 one can construct a rejection at an earlier step.


lemma rejected_valid_earlier (n : ℕ) (m : M) (w : W) (hrej : rejectedAt P n m w)
    (hval : validPartner P m w) : ∃ n' < n, ∃ m' w', rejectedAt P n' m' w' ∧ validPartner P m' w' := by
  rcases hval with ⟨μ, hstable, hμm⟩
  rcases rejectedAt_new_partner P n m w hrej with ⟨m₀, hwm₀new, hpref₀⟩
  have hm₀ne : m₀ ≠ m := by
    intro hm₀
    have h : P.wRank w m < P.wRank w m := by
      rw [hm₀] at hpref₀
      exact hpref₀
    exact (lt_irrefl (P.wRank w m)) h
  have hμm₀ne : μ.mPartner m₀ ≠ none := by
    intro hm₀none
    have hblock : Pairing.BlockingPair P μ m₀ w := by
      constructor
      · exact Or.inr ⟨m, (μ.h_consistency m w).mp hμm, hpref₀⟩
      · exact Or.inl hm₀none
    exact hstable m₀ w hblock
  rcases ne_none_iff_exists hμm₀ne with ⟨w₀, hμm₀⟩
  have hw₀ne : w₀ ≠ w := by
    intro hw₀
    have h1 : μ.wPartner w = some m₀ := (μ.h_consistency m₀ w).mp (by simpa [hw₀] using hμm₀)
    have h2 : μ.wPartner w = some m := (μ.h_consistency m w).mp hμm
    exact hm₀ne (Option.some.inj (by rw [← h1, h2]))
  have hpref₀' : P.mPrefers m₀ w₀ w := by
    have hnotm : ¬ (μ.mPartner m₀ = none ∨ ∃ w₁, μ.mPartner m₀ = some w₁ ∧ P.mPrefers m₀ w w₁) := by
      intro hm
      exact hstable m₀ w ⟨Or.inr ⟨m, (μ.h_consistency m w).mp hμm, hpref₀⟩, hm⟩
    have hnotpref : ¬ P.mPrefers m₀ w w₀ := by
      intro hp
      exact hnotm (Or.inr ⟨w₀, hμm₀, hp⟩)
    have hle : P.mRank m₀ w₀ ≤ P.mRank m₀ w := le_of_not_gt hnotpref
    have hne : P.mRank m₀ w₀ ≠ P.mRank m₀ w := Function.Injective.ne (P.h_mRank_injective m₀) hw₀ne
    exact lt_of_le_of_ne hle hne
  have hσ₁ : Invariant (runAt P (n+1)) := by
    unfold runAt
    exact gsLoopN_invariant (init : GSState P) init_invariant (n+1)
  have hwm₀part : w ∈ (runAt P (n+1)).proposed m₀ := by
    have hm₀w : (runAt P (n+1)).mPartner m₀ = some w :=
      ((runAt P (n+1)).h_consistency m₀ w).mpr hwm₀new
    exact hσ₁.partner_proposed hm₀w
  have hw₀part : w₀ ∈ (runAt P (n+1)).proposed m₀ := hσ₁.downward_closed hwm₀part hpref₀'
  have hpair : w₀ ∈ (runAt P n).proposed m₀ ∧ (runAt P n).mPartner m₀ ≠ some w₀ :=
    rejection_partner_facts P n m w m₀ w₀ hrej hwm₀new hm₀ne hw₀ne hw₀part
  rcases hpair with ⟨hw₀partn, hmn₀⟩
  have hn1 : 1 ≤ n := by
    by_contra hn
    have hn' : n = 0 := by omega
    rw [hn'] at hw₀partn
    simp [runAt, gsLoopN, init] at hw₀partn
  rcases proposesAt_exists P n m₀ w₀ hn1 hw₀partn with ⟨n', hn'lt, hprop'⟩
  by_cases hacc : accepts (runAt P n') m₀ w₀
  · have hself : (runAt P (n'+1)).mPartner m₀ = some w₀ := by
      simpa [hacc] using proposesAt_self P n' m₀ w₀ hprop'
    let p : ℕ → Prop := fun t => n' + 1 < t ∧ (runAt P t).mPartner m₀ ≠ some w₀
    have hwitness : p (n+1) := by
      constructor
      · omega
      · have hcons : (runAt P (n+1)).mPartner m₀ = some w :=
          ((runAt P (n+1)).h_consistency m₀ w).mpr hwm₀new
        intro h
        exact hw₀ne (Option.some.inj (by rw [← h, hcons]))
    have hT : ∃ t, p t := ⟨n+1, hwitness⟩
    let T : ℕ := Nat.find hT
    have hTspec : p T := Nat.find_spec hT
    have hTmin : ∀ t < T, ¬ p t := by
      intro t ht
      exact Nat.find_min hT ht
    have hTle : T ≤ n + 1 := by
      by_contra hlt
      exact hTmin (n+1) (by omega) hwitness
    have hTne : T ≠ n + 1 := by
      intro hT'
      by_cases hn'lt : n' + 1 < n
      · exact hTmin n (by omega) ⟨hn'lt, hmn₀⟩
      · have hn'eq : n' + 1 = n := by omega
        exact hmn₀ (by simpa [hn'eq] using hself)
    have hT1 : T - 1 < n := by omega
    have hrej' : rejectedAt P (T-1) m₀ w₀ := by
      have hm₁ : (runAt P (T-1)).mPartner m₀ = some w₀ := by
        by_cases hT1eq : T - 1 = n' + 1
        · rwa [hT1eq]
        · have hT1gt : n' + 1 < T - 1 := by omega
          have hnotp : ¬ p (T-1) := hTmin (T-1) (by omega)
          by_cases hm' : (runAt P (T-1)).mPartner m₀ = some w₀
          · exact hm'
          · exact False.elim (hnotp ⟨hT1gt, hm'⟩)
      have hT' : (runAt P (T - 1 + 1)).mPartner m₀ ≠ some w₀ := by
        simpa [show T - 1 + 1 = T by omega] using hTspec.2
      exact Or.inl ⟨hm₁, hT'⟩
    exact ⟨T - 1, hT1, m₀, w₀, hrej', ⟨μ, hstable, hμm₀⟩⟩
  · have hrej' : rejectedAt P n' m₀ w₀ := Or.inr ⟨hprop', hacc⟩
    exact ⟨n', hn'lt, m₀, w₀, hrej', ⟨μ, hstable, hμm₀⟩⟩

No man is ever rejected by a valid partner during the proposal run: rejections of valid partners would descend to strictly earlier steps.


theorem no_rejection_of_valid : ¬ ∃ n m w, rejectedAt P n m w ∧ validPartner P m w := by
  classical
  intro h
  let p : ℕ → Prop := fun n => ∃ m w, rejectedAt P n m w ∧ validPartner P m w
  have hnonempty : ∃ n, p n := h
  let n₀ : ℕ := Nat.find hnonempty
  have h₀ : p n₀ := Nat.find_spec hnonempty
  have hmin : ∀ n < n₀, ¬ p n := by
    intro n hn
    exact Nat.find_min hnonempty hn
  rcases h₀ with ⟨m, w, hrej, hval⟩
  rcases rejected_valid_earlier P n₀ m w hrej hval with ⟨n', hn'lt, m', w', hrej', hval'⟩
  exact hmin n' hn'lt ⟨m', w', hrej', hval'⟩

A man matched at the end of the run cannot strictly prefer a valid partner to his final partner.


lemma better_valid_contradiction (k : ℕ) (m : M) (w : W) (hm : (runAt P k).mPartner m = some w)
    {w' : W} (hval : validPartner P m w') (hpref : P.mPrefers m w' w) : False := by
  have hk1 : 1 ≤ k := by
    by_contra hk
    have hk' : k = 0 := by omega
    rw [hk'] at hm
    simp [runAt, gsLoopN, init] at hm
  have hσ : Invariant (runAt P k) := by
    unfold runAt
    exact gsLoopN_invariant (init : GSState P) init_invariant k
  have hwprop : w ∈ (runAt P k).proposed m := hσ.partner_proposed hm
  have hw'prop : w' ∈ (runAt P k).proposed m := hσ.downward_closed hwprop hpref
  rcases proposesAt_exists P k m w' hk1 hw'prop with ⟨n, hnlt, hp⟩
  by_cases hacc : accepts (runAt P n) m w'
  · have hself : (runAt P (n+1)).mPartner m = some w' := by
      simpa [hacc] using proposesAt_self P n m w' hp
    have hww' : w' ≠ w := by
      intro h
      have h₁ : P.mRank m w < P.mRank m w := by
        rw [h] at hpref
        exact hpref
      exact (lt_irrefl (P.mRank m w)) h₁
    let p : ℕ → Prop := fun t => n + 1 < t ∧ (runAt P t).mPartner m ≠ some w'
    have hwitness : p k := by
      constructor
      · by_contra hnk
        have hkeq : k = n + 1 := by omega
        have hm' : (runAt P (n+1)).mPartner m = some w := by simpa [hkeq] using hm
        exact hww' (Option.some.inj (by rw [← hself, hm']))
      · intro h
        exact hww' (Option.some.inj (by rw [← h, hm]))
    have hT : ∃ t, p t := ⟨k, hwitness⟩
    let T : ℕ := Nat.find hT
    have hTspec : p T := Nat.find_spec hT
    have hTmin : ∀ t < T, ¬ p t := by
      intro t ht
      exact Nat.find_min hT ht
    have hT1 : T - 1 < k := by
      have hTle : T ≤ k := by
        by_contra hlt
        exact hTmin k (by omega) hwitness
      have hTpos : 1 ≤ T := by
        have h : n + 1 < T := hTspec.1
        omega
      omega
    have hrej : rejectedAt P (T-1) m w' := by
      have hm₁ : (runAt P (T-1)).mPartner m = some w' := by
        by_cases hT1eq : T - 1 = n + 1
        · rwa [hT1eq]
        · have hT1gt : n + 1 < T - 1 := by omega
          have hnotp : ¬ p (T-1) := hTmin (T-1) (by omega)
          by_cases hm' : (runAt P (T-1)).mPartner m = some w'
          · exact hm'
          · exact False.elim (hnotp ⟨hT1gt, hm'⟩)
      have hT' : (runAt P (T - 1 + 1)).mPartner m ≠ some w' := by
        simpa [show T - 1 + 1 = T by omega] using hTspec.2
      exact Or.inl ⟨hm₁, hT'⟩
    exact no_rejection_of_valid P ⟨T - 1, m, w', hrej, hval⟩
  · have hrej : rejectedAt P n m w' := Or.inr ⟨hp, hacc⟩
    exact no_rejection_of_valid P ⟨n, m, w', hrej, hval⟩

Man-optimality of the Gale–Shapley output (CLRS Theorem 25.6): every man is matched to his best valid partner — no stable matching pairs him with a woman he strictly prefers to his Gale–Shapley partner.


theorem gs_man_optimal (P : PreferenceProfile M W) :
    ∀ m w, (gs P).mPartner m = some w →
      ∀ w', validPartner P m w' → ¬ P.mPrefers m w' w := by
  intro m w hm w' hval
  by_contra hpref
  have hσeq : gsLoop (init : GSState P) = runAt P (pendingCount (init : GSState P)) := by
    unfold runAt
    exact gsLoop_eq_gsLoopN P (init : GSState P)
  have hm' : (runAt P (pendingCount (init : GSState P))).mPartner m = some w := by
    simp [gs, GSState.toPairing, hσeq] at hm
    exact hm
  exact better_valid_contradiction P (pendingCount (init : GSState P)) m w hm' hval hpref

Man-optimality with equal cardinality (CLRS Theorem 25.6): with equally many men and women, every man is matched to his best valid partner.

theorem gs_man_optimal_perfect (P : PreferenceProfile M W)
    (hcard : Fintype.card M = Fintype.card W) :
    ∀ m, ∃ w, (gs P).mPartner m = some w ∧
      ∀ w', validPartner P m w' → ¬ P.mPrefers m w' w := by
  intro m
  rcases (gs_perfect P hcard).1 m with ⟨w, hw⟩
  exact ⟨w, hw, gs_man_optimal P m w hw⟩

Woman-pessimality of the Gale–Shapley output (CLRS §25.2): each woman who receives a partner does not strictly prefer that Gale–Shapley partner to any partner she receives in another stable pairing. Thus her Gale–Shapley partner is her worst valid partner. With equal cardinalities, perfectness discharges the matched-woman premise.


theorem gs_woman_pessimal (P : PreferenceProfile M W) :
    ∀ w m₀, (gs P).wPartner w = some m₀ →
      ∀ μ : Pairing M W, Pairing.Stable P μ →
        ∀ m', μ.wPartner w = some m' → ¬ P.wPrefers w m₀ m' := by
  intro w m₀ hwm₀ μ hstable m' hμm'
  by_contra hpref
  have hnot : ¬ Pairing.BlockingPair P μ m₀ w := hstable m₀ w
  have hwside : μ.wPartner w = none ∨ ∃ m₁, μ.wPartner w = some m₁ ∧ P.wPrefers w m₀ m₁ :=
    Or.inr ⟨m', hμm', hpref⟩
  have hnotm : ¬ (μ.mPartner m₀ = none ∨ ∃ w', μ.mPartner m₀ = some w' ∧ P.mPrefers m₀ w w') := by
    intro hm
    exact hnot ⟨hwside, hm⟩
  have hm₀ne : μ.mPartner m₀ ≠ none := by
    intro hn
    exact hnotm (Or.inl hn)
  rcases ne_none_iff_exists hm₀ne with ⟨w₀, hm₀w₀⟩
  have hnotpref : ¬ P.mPrefers m₀ w w₀ := by
    intro hp
    exact hnotm (Or.inr ⟨w₀, hm₀w₀, hp⟩)
  have hw₀ne : w₀ ≠ w := by
    intro h
    have h1 : μ.wPartner w = some m₀ := (μ.h_consistency m₀ w).mp (by simpa [h] using hm₀w₀)
    have hmm' : m₀ = m' := Option.some.inj (by rw [← h1, hμm'])
    have h : P.wRank w m₀ < P.wRank w m₀ := by
      rw [← hmm'] at hpref
      exact hpref
    exact (lt_irrefl (P.wRank w m₀)) h
  have hpref₀ : P.mPrefers m₀ w₀ w := by
    have hle : P.mRank m₀ w₀ ≤ P.mRank m₀ w := le_of_not_gt hnotpref
    have hne : P.mRank m₀ w₀ ≠ P.mRank m₀ w := Function.Injective.ne (P.h_mRank_injective m₀) hw₀ne
    exact lt_of_le_of_ne hle hne
  have hσm₀ : (gs P).mPartner m₀ = some w := ((gs P).h_consistency m₀ w).mpr hwm₀
  have hvalidw₀ : validPartner P m₀ w₀ := ⟨μ, hstable, hm₀w₀⟩
  exact gs_man_optimal P m₀ w hσm₀ w₀ hvalidw₀ hpref₀

end StableMarriageend CLRS