Gale–Shapley algorithm

30 fully proved

Preferences

DefinitionPreference order of a ranking#✓fully proved

A permutation \(\sigma\) of \(\{0, \dots, n-1\}\), read as a ranking (\(\sigma(k)\) is the \(k\)-th choice, \(\sigma(0)\) the best), gives the strict total order on \(\{0, \dots, n-1\}\) in which \(a\) is preferred to \(b\) when \(\sigma^{-1}(a) < \sigma^{-1}(b)\).

def toOrder (σ : Equiv.Perm (Fin n)) : MathlibExt.Order.StrictTotalOrder (Fin n) where
  lt a b := σ.symm a < σ.symm b
  irrefl _ := lt_irrefl _
  trans h1 h2 := lt_trans h1 h2
  total h := lt_or_gt_of_ne fun e => h (σ.symm.injective e)

Uses 1 · Used by 4

Statement usesStrict total order

Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Every strict total order on \(\{0, \dots, n-1\}\) is given by a ranking · Proposers' preferences from rankings · Receivers' preference profile from rankings

DefinitionProposers' preferences from rankings#✓fully proved

Given for each proposer \(m\) a ranking \(\sigma_m\) of the \(n\) receivers (\(\sigma_m(k)\) is the choice of \(m\) of rank \(k\), rank \(0\) the best), the proposers' preference profile assigns to \(m\) the strict total order in which \(m\) prefers \(w\) to \(w'\) when \(\sigma_m^{-1}(w) < \sigma_m^{-1}(w')\).

def mprefs (mp : Fin n → Equiv.Perm (Fin n)) : MPrefs (Fin n) (Fin n) := fun m => toOrder (mp m)

Uses 2 · Used by 10

Statement usesPreference order of a ranking · Men's preferences

Used byA proposer's final partner is his last proposal · Gale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · The Gale-Shapley matching · Proposer-optimality · Receiver-pessimality · Invariant of deferred acceptance · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · A stable matching has no blocking pair · Deferred acceptance makes at most n² proposals

DefinitionReceivers' preference profile from rankings#✓fully proved

Given for each receiver \(w\) a ranking \(\sigma_w\) of the \(n\) proposers (a permutation of \(\{0, \dots, n-1\}\), with \(\sigma_w(0)\) her first choice), the receivers' preference profile assigns to \(w\) the preference order of \(\sigma_w\): \(w\) prefers \(a\) to \(b\) when \(\sigma_w^{-1}(a) < \sigma_w^{-1}(b)\).

def wprefs (wp : Fin n → Equiv.Perm (Fin n)) : WPrefs (Fin n) (Fin n) := fun w => toOrder (wp w)

Uses 2 · Used by 10

Statement usesPreference order of a ranking · Women's preference profile

Used byA proposer's final partner is his last proposal · Gale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · The Gale-Shapley matching · Proposer-optimality · Receiver-pessimality · Invariant of deferred acceptance · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · A stable matching has no blocking pair · Deferred acceptance makes at most n² proposals

The algorithm

StructureDeferred-acceptance state#✓fully proved

A state of deferred acceptance with \(n\) proposers and \(n\) receivers, both numbered \(0, \dots, n-1\), records for each proposer a natural number, the number of proposals he has made (his next proposal goes to his choice of that rank), and for each receiver either the proposer she currently holds or that she holds nobody.

structure State (n : ℕ) where
  /-- The number of proposals made by each proposer. -/
  next : Vector ℕ n
  /-- The proposer each receiver holds, if any. -/
  holder : Vector (Option (Fin n)) n

Used by 21

Used byChoosing the next proposer · A proposer's final partner is his last proposal · Free proposer · Deferred acceptance · The Gale-Shapley matching · Proposer-optimality · When deferred acceptance stops, every proposer is held · Every receiver holds someone once every proposer is held · Initial state of deferred acceptance · Invariant of deferred acceptance · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · Receiver's holder after a proposal · Cases of the receiver's new holder · Proposer's partner · Receiver's partner · A proposal · Remaining proposals · Running deferred acceptance · Deferred acceptance makes at most n² proposals · A proposal adds one to the proposal count

DefinitionInitial state of deferred acceptance#✓fully proved

The initial state with \(n\) proposers and \(n\) receivers: every proposer has made \(0\) proposals and no receiver holds anyone.

def init (n : ℕ) : State n := ⟨Vector.replicate n 0, Vector.replicate n none⟩

Uses 1 · Used by 6

Statement usesDeferred-acceptance state

Used byA proposer's final partner is his last proposal · Deferred acceptance · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

DefinitionFree proposer#✓fully proved

A proposer \(m\) is free in a state \(s\) of deferred acceptance when no receiver holds \(m\) in \(s\).

def Free (s : State n) (m : Fin n) : Prop := ∀ w : Fin n, s.holder[w] ≠ some m

Uses 1 · Used by 7

Statement usesDeferred-acceptance state

Used byChoosing the next proposer · A proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · When deferred acceptance stops, every proposer is held · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

DefinitionReceiver's holder after a proposal#✓fully proved

In a state \(s\) of deferred acceptance, the proposer whom receiver \(w\) holds after proposer \(m\) proposes to her is \(m\) if she holds nobody in \(s\) or ranks \(m\) strictly better than her current holder \(m'\) in her ranking, and \(m'\) otherwise.

def newHolder (s : State n) (m w : Fin n) : Option (Fin n) :=
  match s.holder[w] with
  | none => some m
  | some m' => if (wp w).symm m < (wp w).symm m' then some m else some m'

Uses 1 · Used by 8

Statement usesDeferred-acceptance state

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Cases of the receiver's new holder · A proposal · Deferred acceptance makes at most n² proposals · A proposal adds one to the proposal count

DefinitionA proposal#✓fully proved

Fix, for each proposer, a ranking of the \(n\) receivers and, for each receiver, a ranking of the \(n\) proposers (rank \(0\) is the first choice). Let \(s\) be a state of deferred acceptance in which proposer \(m\) has made \(k\) proposals. If \(k < n\), then \(m\) proposes to the receiver \(w\) of rank \(k\) in his ranking: his number of proposals becomes \(k + 1\), and \(w\) now holds \(m\) if she held nobody or ranks \(m\) strictly above the proposer she held, and keeps her old holder otherwise; all other counts and holders are unchanged. If \(k \ge n\), the state is unchanged.

def propose (s : State n) (m : Fin n) : State n :=
  if h : s.next[m] < n then
    ⟨s.next.set m (s.next[m] + 1),
      s.holder.set (mp m ⟨s.next[m], h⟩) (newHolder wp s m (mp m ⟨s.next[m], h⟩))⟩
  else s

Uses 2 · Used by 7

Statement usesDeferred-acceptance state · Receiver's holder after a proposal

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Running deferred acceptance · Deferred acceptance makes at most n² proposals · A proposal adds one to the proposal count

DefinitionChoosing the next proposer#✓fully proved

In a state \(s\) of deferred acceptance with proposers \(0, 1, \dots, n-1\), the chooser returns the least proposer \(m\) who is free in \(s\) and has made fewer than \(n\) proposals in \(s\), or no proposer if there is none.

def chooser (s : State n) : Option (Fin n) :=
  (List.finRange n).find? fun m => decide (Free s m) && decide (s.next[m] < n)

Uses 2 · Used by 7

Statement usesFree proposer · Deferred-acceptance state

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · When deferred acceptance stops, every proposer is held · The Gale-Shapley matching is stable · Running deferred acceptance · Deferred acceptance makes at most n² proposals

DefinitionRunning deferred acceptance#✓fully proved

Fix rankings for \(n\) proposers and \(n\) receivers, both numbered \(0, \dots, n-1\). Starting from a state \(s\) with a budget of \(f\) proposals: if \(f = 0\), or if no proposer is both free (held by no receiver) and has made fewer than \(n\) proposals, the run returns \(s\); otherwise the lowest-numbered such proposer makes a proposal, and the run continues from the resulting state with budget \(f - 1\).

def run : ℕ → State n → State n
  | 0, s => s
  | fuel + 1, s =>
      match chooser s with
      | none => s
      | some m => run fuel (propose mp wp s m)

Uses 3 · Used by 6

Statement usesDeferred-acceptance state · Choosing the next proposer · A proposal

Used byA proposer's final partner is his last proposal · Deferred acceptance · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

DefinitionDeferred acceptance#✓fully proved

Let each of \(n\) proposers rank the \(n\) receivers, and each receiver rank the \(n\) proposers, with rank \(0\) the best. Deferred acceptance is the state reached from the initial state, in which no one has proposed and no receiver holds anyone, by repeating the following step at most \(n^2\) times, stopping early once no proposer is both free and has made fewer than \(n\) proposals: the least such proposer, having made \(p\) proposals so far, proposes to the receiver of rank \(p\) in his ranking, and she then holds whichever of him and her current holder she ranks better, or him if she held no one.

These \(n^2\) steps always suffice: in the resulting state no proposer is both free and has made fewer than \(n\) proposals.

def galeShapley : State n := run mp wp (n * n) (init n)

Uses 3 · Used by 5

Statement usesDeferred-acceptance state · Initial state of deferred acceptance · Running deferred acceptance

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

The invariant

StructureInvariant of deferred acceptance#✓fully proved

Let each proposer \(m\) have a ranking \(\sigma_m\) of the \(n\) receivers and each receiver \(w\) a ranking \(\tau_w\) of the \(n\) proposers, where \(\sigma_m(k)\) is the choice of \(m\) of rank \(k\) (rank \(0\) is the best) and \(\tau_w^{-1}(x)\) is the rank of \(x\) for \(w\). A state \(s\) of deferred acceptance satisfies the invariant when: every proposer has made at most \(n\) proposals; if \(w\) holds \(m\), then \(m\) has made \(k + 1\) proposals for some rank \(k\) with \(\sigma_m(k) = w\); no proposer is held by two different receivers; for every proposer \(m\) and every rank \(k\) less than the number of proposals of \(m\), the receiver \(w = \sigma_m(k)\) holds some \(m'\) with \(\tau_w^{-1}(m') \le \tau_w^{-1}(m)\); and for such \(m\) and \(k\), if \(\sigma_m(k)\) does not hold \(m\), then no perfect matching that is stable for the preferences given by the rankings matches \(m\) with \(\sigma_m(k)\).

structure Inv (s : State n) : Prop where
  /-- Nobody proposes more than `n` times. -/
  next_le : ∀ m : Fin n, s.next[m] ≤ n
  /-- A held proposer is held by his latest proposal. -/
  last : ∀ w m : Fin n, s.holder[w] = some m → ∃ k : Fin n, k.val + 1 = s.next[m] ∧ mp m k = w
  /-- A proposer is held by at most one receiver. -/
  inj : ∀ w w' m : Fin n, s.holder[w] = some m → s.holder[w'] = some m → w = w'
  /-- A receiver who was proposed to holds someone at least as good as each of her proposers. -/
  held : ∀ m k : Fin n, k.val < s.next[m] →
    ∃ m', s.holder[mp m k] = some m' ∧ (wp (mp m k)).symm m' ≤ (wp (mp m k)).symm m
  /-- **No proposer is rejected by a stable partner** (Gale and Shapley's optimality argument). -/
  opt : ∀ m k : Fin n, k.val < s.next[m] → s.holder[mp m k] ≠ some m →
    ∀ ν : PerfectMatching (Fin n) (Fin n), IsStable (mprefs mp) (wprefs wp) ν → ν m ≠ mp m k

Uses 5 · Used by 7

Statement usesDeferred-acceptance state · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · When deferred acceptance stops, every proposer is held · The Gale-Shapley matching is stable · Rejected proposals bound stable partners · Deferred acceptance makes at most n² proposals

TheoremA stable matching has no blocking pair#✓fully proved

Let each proposer \(m\) have a ranking \(\sigma_m\) of the \(n\) receivers and each receiver \(w\) a ranking \(\tau_w\) of the \(n\) proposers, where \(\sigma_m^{-1}(x)\) and \(\tau_w^{-1}(x)\) are ranks (\(0\) the best). If \(\nu\) is a perfect matching that is stable for the preferences given by these rankings, there are no proposer \(m\) and receiver \(w\) with \(\sigma_m^{-1}(w) < \sigma_m^{-1}(\nu(m))\) and \(\tau_w^{-1}(m) < \tau_w^{-1}(\nu^{-1}(w))\).

theorem not_blocking {ν : PerfectMatching (Fin n) (Fin n)}
    (hν : IsStable (mprefs mp) (wprefs wp) ν) {m w : Fin n}
    (h1 : (mp m).symm w < (mp m).symm (ν m)) (h2 : (wp w).symm m < (wp w).symm (ν.symm w)) :
    False

Uses 5 · Used by 6

Statement usesProposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching

Proof usesRelation of a strict total order

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · Receiver-pessimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

TheoremRejected proposals bound stable partners#✓fully proved

Let each proposer \(m\) have a ranking \(\sigma_m\) of the \(n\) receivers (\(\sigma_m(k)\) is the choice of \(m\) of rank \(k\), rank \(0\) the best), and each receiver a ranking of the \(n\) proposers. Let \(s\) be a state of deferred acceptance satisfying the invariant, let \(\nu\) be a perfect matching that is stable for the preferences given by the rankings, let \(m\) be a proposer, and let \(b\) be a natural number at most the number of proposals \(m\) has made in \(s\). If for every rank \(k < b\) the receiver \(\sigma_m(k)\) does not hold \(m\) in \(s\), then \(\sigma_m^{-1}(\nu(m)) \ge b\).

theorem le_rank_of_rejected {s : State n} (hI : Inv mp wp s) {ν : PerfectMatching (Fin n) (Fin n)}
    (hν : IsStable (mprefs mp) (wprefs wp) ν) (m : Fin n) {b : ℕ} (hb : b ≤ s.next[m])
    (hrej : ∀ k : Fin n, k.val < b → s.holder[mp m k] ≠ some m) :
    b ≤ ((mp m).symm (ν m)).val

Uses 6 · Used by 5

Statement usesInvariant of deferred acceptance · Deferred-acceptance state · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

TheoremCases of the receiver's new holder#✓fully proved

Let \(s\) be a state of deferred acceptance, \(m\) a proposer and \(w\) a receiver with ranking \(\tau_w\) of the proposers (\(\tau_w^{-1}(x)\) is the rank of \(x\), rank \(0\) the best). Then one of the following holds: \(w\) holds nobody in \(s\) and holds \(m\) after \(m\) proposes to her; or \(w\) holds some \(y\) in \(s\) with \(\tau_w^{-1}(m) < \tau_w^{-1}(y)\) and holds \(m\) after \(m\) proposes to her; or \(w\) holds some \(y\) in \(s\) with \(\tau_w^{-1}(m) \ge \tau_w^{-1}(y)\) and holds \(y\) after \(m\) proposes to her.

theorem newHolder_cases (s : State n) (m w : Fin n) :
    (s.holder[w] = none ∧ newHolder wp s m w = some m) ∨
    (∃ y, s.holder[w] = some y ∧ (wp w).symm m < (wp w).symm y ∧ newHolder wp s m w = some m) ∨
    (∃ y, s.holder[w] = some y ∧ ¬ (wp w).symm m < (wp w).symm y ∧
      newHolder wp s m w = some y)

Uses 2 · Used by 5

Statement usesDeferred-acceptance state · Receiver's holder after a proposal

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

Termination within n² proposals

DefinitionRemaining proposals#✓fully proved

For a state \(s\) of deferred acceptance with \(n\) proposers and \(n\) receivers, in which each proposer \(m\) has made \(k_m\) proposals, the number of proposals still available is \(\sum_{m} \max(n - k_m, 0)\), the sum running over all \(n\) proposers.

def remaining (s : State n) : ℕ := ∑ m : Fin n, (n - s.next[m])

Uses 1 · Used by 5

Statement usesDeferred-acceptance state

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality · The Gale-Shapley matching is stable · Deferred acceptance makes at most n² proposals

TheoremA proposal adds one to the proposal count#✓fully proved

Fix rankings for \(n\) proposers and \(n\) receivers. If proposer \(m\) has made fewer than \(n\) proposals in a state \(s\) of deferred acceptance, then after \(m\) proposes, the total number of proposals made by all proposers is one more than in \(s\).

theorem sum_next_propose {s : State n} {m : Fin n} (h : s.next[m] < n) :
    ∑ m' : Fin n, (propose mp wp s m).next[m'] = ∑ m' : Fin n, s.next[m'] + 1

Uses 3

Statement usesDeferred-acceptance state · A proposal

Proof usesReceiver's holder after a proposal

TheoremDeferred acceptance makes at most n² proposals#✓fully proved

For any rankings of the \(n\) receivers by each of the \(n\) proposers and of the proposers by each receiver, in the final state of deferred acceptance the numbers of proposals made by the proposers sum to at most \(n \cdot n\).

No proposer proposes more than \(n\) times.

theorem sum_next_galeShapley_le : ∑ m : Fin n, (galeShapley mp wp).next[m] ≤ n * n

Uses 17

Statement usesDeferred-acceptance state · Deferred acceptance

Proof usesFree proposer · Invariant of deferred acceptance · Choosing the next proposer · Initial state of deferred acceptance · Rejected proposals bound stable partners · Proposers' preferences from rankings · Receiver's holder after a proposal · Cases of the receiver's new holder · A stable matching has no blocking pair · A proposal · Remaining proposals · Running deferred acceptance · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching

The output is a perfect matching

TheoremWhen deferred acceptance stops, every proposer is held#✓fully proved

Fix rankings of the \(n\) receivers by each of \(n\) proposers and of the proposers by each receiver. Let \(s\) be a state of deferred acceptance that satisfies the invariant of deferred acceptance for these rankings, and suppose that no proposer is both free in \(s\) and has made fewer than \(n\) proposals in \(s\). Then every proposer is held by some receiver in \(s\).

theorem held_of_done {s : State n} (hI : Inv mp wp s) (hc : chooser s = none) (m : Fin n) :
    ∃ w : Fin n, s.holder[w] = some m

Uses 4 · Used by 3

Statement usesInvariant of deferred acceptance · Deferred-acceptance state · Choosing the next proposer

Proof usesFree proposer

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality

TheoremEvery receiver holds someone once every proposer is held#✓fully proved

Let \(s\) be a state of deferred acceptance with \(n\) proposers and \(n\) receivers. If every proposer is held by some receiver in \(s\), then every receiver holds some proposer in \(s\).

theorem holds_of_held {s : State n}
    (hall : ∀ m : Fin n, ∃ w : Fin n, s.holder[w] = some m)
    (w : Fin n) : ∃ m, s.holder[w] = some m

Uses 1 · Used by 1

Statement usesDeferred-acceptance state

Used byThe Gale-Shapley matching

DefinitionReceiver's partner#✓fully proved

In a state \(s\) of deferred acceptance with \(n\) proposers and \(n\) receivers, both numbered \(0, \dots, n-1\), the partner of a receiver \(w\) is the proposer she holds in \(s\); if she holds nobody, it is the proposer numbered \(w\) (a default value).

def partnerW (s : State n) (w : Fin n) : Fin n := s.holder[w].getD w

Uses 1 · Used by 2

Statement usesDeferred-acceptance state

Used byThe Gale-Shapley matching · The Gale-Shapley matching is stable

DefinitionProposer's partner#✓fully proved

In a state \(s\) of deferred acceptance with \(n\) proposers and \(n\) receivers, both numbered \(0, \dots, n-1\), the partner of a proposer \(m\) is the lowest-numbered receiver that holds \(m\) in \(s\); if no receiver holds \(m\), it is the receiver numbered \(m\) (a default value).

def partnerM (s : State n) (m : Fin n) : Fin n :=
  ((List.finRange n).find? fun w : Fin n => s.holder[w] == some m).getD m

Uses 1 · Used by 3

Statement usesDeferred-acceptance state

Used byA proposer's final partner is his last proposal · The Gale-Shapley matching · Proposer-optimality

DefinitionThe Gale-Shapley matching#✓fully proved

Each proposer with the receiver who holds him at the end.

def gsMatching : PerfectMatching (Fin n) (Fin n) where
  toFun := partnerM (galeShapley mp wp)
  invFun := partnerW (galeShapley mp wp)
  left_inv m := by
    obtain ⟨hI, hc⟩ := galeShapley_spec mp wp
    obtain ⟨w, hw⟩ := held_of_done hI hc m
    rw [partnerM_eq hI hw, partnerW_eq hw]
  right_inv w := by
    obtain ⟨hI, hc⟩ := galeShapley_spec mp wp
    obtain ⟨m, hm⟩ := holds_of_held (held_of_done hI hc) w
    rw [partnerW_eq hm, partnerM_eq hI hm]

Uses 21 · Used by 5

Statement usesFree proposer · Invariant of deferred acceptance · Deferred-acceptance state · Choosing the next proposer · Deferred acceptance · When deferred acceptance stops, every proposer is held · Every receiver holds someone once every proposer is held · Initial state of deferred acceptance · Rejected proposals bound stable partners · Proposers' preferences from rankings · Receiver's holder after a proposal · Cases of the receiver's new holder · A stable matching has no blocking pair · Proposer's partner · Receiver's partner · A proposal · Remaining proposals · Running deferred acceptance · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching

Used byA proposer's final partner is his last proposal · Gale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Proposer-optimality · Receiver-pessimality · The Gale-Shapley matching is stable

Stability and optimality

TheoremA proposer's final partner is his last proposal#✓fully proved

Let each proposer \(m\) rank the \(n\) receivers by a permutation \(\sigma_m\) of \(\{0, \dots, n-1\}\), where \(\sigma_m(k)\) is his choice of rank \(k\), let each receiver rank the \(n\) proposers, and let \(p_m\) be the number of proposals \(m\) has made in the final state of deferred acceptance. Then \(p_m \ge 1\), and the Gale-Shapley partner \(\mu(m)\) of \(m\) has rank \(p_m - 1\) in his ranking, that is, \(\sigma_m^{-1}(\mu(m)) = p_m - 1\).

theorem exists_rank_gsMatching (m : Fin n) : ∃ k : Fin n,
    k.val + 1 = (galeShapley mp wp).next[m] ∧ (mp m).symm (gsMatching mp wp m) = k

Uses 20 · Used by 2

Statement usesDeferred-acceptance state · Deferred acceptance · The Gale-Shapley matching · Perfect matching

Proof usesFree proposer · Invariant of deferred acceptance · Choosing the next proposer · When deferred acceptance stops, every proposer is held · Initial state of deferred acceptance · Rejected proposals bound stable partners · Proposers' preferences from rankings · Receiver's holder after a proposal · Cases of the receiver's new holder · A stable matching has no blocking pair · Proposer's partner · A proposal · Remaining proposals · Running deferred acceptance · Receivers' preference profile from rankings · Stable perfect matching

Used byProposer-optimality · The Gale-Shapley matching is stable

TheoremThe Gale-Shapley matching is stable#✓fully proved

For \(n\) proposers and \(n\) receivers, each with a ranking of the other side, the perfect matching computed by deferred acceptance is stable for the strict preferences given by these rankings.

theorem isStable_gsMatching : IsStable (mprefs mp) (wprefs wp) (gsMatching mp wp)

Uses 22 · Used by 1

Statement usesThe Gale-Shapley matching · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching

Proof usesFree proposer · Invariant of deferred acceptance · Deferred-acceptance state · Choosing the next proposer · A proposer's final partner is his last proposal · Deferred acceptance · Initial state of deferred acceptance · Rejected proposals bound stable partners · Receiver's holder after a proposal · Cases of the receiver's new holder · A stable matching has no blocking pair · Receiver's partner · A proposal · Remaining proposals · Running deferred acceptance · Blocking pair · Perfect matching · Relation of a strict total order

Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers

TheoremProposer-optimality#✓fully proved

No stable matching gives a proposer a partner he prefers to his Gale-Shapley partner.

theorem gsMatching_proposer_optimal {ν : PerfectMatching (Fin n) (Fin n)}
    (hν : IsStable (mprefs mp) (wprefs wp) ν) (m : Fin n) :
    ¬ (mprefs mp m).lt (ν m) (gsMatching mp wp m)

Uses 22 · Used by 2

Statement usesThe Gale-Shapley matching · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching · Relation of a strict total order

Proof usesFree proposer · Invariant of deferred acceptance · Deferred-acceptance state · Choosing the next proposer · A proposer's final partner is his last proposal · Deferred acceptance · When deferred acceptance stops, every proposer is held · Initial state of deferred acceptance · Rejected proposals bound stable partners · Receiver's holder after a proposal · Cases of the receiver's new holder · A stable matching has no blocking pair · Proposer's partner · A proposal · Remaining proposals · Running deferred acceptance

Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Receiver-pessimality

TheoremReceiver-pessimality#✓fully proved

No stable matching gives a receiver a partner she likes less than her Gale-Shapley partner.

theorem gsMatching_receiver_pessimal {ν : PerfectMatching (Fin n) (Fin n)}
    (hν : IsStable (mprefs mp) (wprefs wp) ν) (w : Fin n) :
    ¬ (wprefs wp w).lt ((gsMatching mp wp).symm w) (ν.symm w)

Uses 8

Statement usesThe Gale-Shapley matching · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Perfect matching · Relation of a strict total order

Proof usesProposer-optimality · A stable matching has no blocking pair

Strict total orders as rankings

DefinitionRank under a strict total order#✓fully proved

For a strict total order \(<\) on \(\{0, \dots, n-1\}\), the rank of an element \(a\) is the number of elements \(b\) with \(b < a\) (the elements preferred to \(a\)), as an element of \(\{0, \dots, n-1\}\).

def orderRank (T : MathlibExt.Order.StrictTotalOrder (Fin n)) [DecidableRel T.lt] (a : Fin n) :
    Fin n :=
  ⟨(Finset.univ.filter fun b => T.lt b a).card, by
    calc (Finset.univ.filter fun b => T.lt b a).card < (Finset.univ : Finset (Fin n)).card :=
          Finset.card_lt_card ⟨Finset.filter_subset _ _, fun h => T.irrefl a
            (Finset.mem_filter.1 (h (Finset.mem_univ a))).2⟩
      _ = n := Finset.card_fin n⟩

Uses 1 · Used by 1

Statement usesStrict total order

Used byEvery strict total order on \(\{0, \dots, n-1\}\) is given by a ranking

TheoremEvery strict total order on \(\{0, \dots, n-1\}\) is given by a ranking#✓fully proved

For every strict total order \(\prec\) on \(\{0, \dots, n-1\}\) there is a permutation \(\sigma\) of \(\{0, \dots, n-1\}\) such that, for all \(a\) and \(b\), \(a \prec b\) holds exactly when \(\sigma^{-1}(a) < \sigma^{-1}(b)\).

Hence the Gale-Shapley algorithm on rankings applies to every preference on \(\{0, \dots, n-1\}\).

theorem exists_toOrder_eq (T : MathlibExt.Order.StrictTotalOrder (Fin n)) :
    ∃ σ : Equiv.Perm (Fin n), toOrder σ = T

Uses 4 · Used by 1

Statement usesPreference order of a ranking · Strict total order

Proof usesRank under a strict total order · Strict total orders are determined by their relation

Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers

TheoremGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers#✓fully proved

Let the \(n\) proposers and the \(n\) receivers both be numbered \(0, \dots, n-1\). Let each proposer \(m\) have a strict total order \(\lt _m\) of preference on the receivers and each receiver \(w\) a strict total order \(\lt _w\) of preference on the proposers, where \(x \lt _m y\) means that \(m\) prefers \(x\) to \(y\), and likewise for \(\lt _w\). Then there are permutations \(\sigma_m\) (one for each proposer \(m\)) and \(\tau_w\) (one for each receiver \(w\)) of \(\{0, \dots, n-1\}\), read as rankings, such that \(w \lt _m w'\) exactly when \(\sigma_m^{-1}(w) < \sigma_m^{-1}(w')\) and \(a \lt _w b\) exactly when \(\tau_w^{-1}(a) < \tau_w^{-1}(b)\), and the Gale-Shapley matching \(\mu\) of the rankings \(\sigma\) and \(\tau\) is stable for these preferences and proposer-optimal: for every perfect matching \(\nu\) that is stable for these preferences and every proposer \(m\), it is not the case that \(\nu(m) \lt _m \mu(m)\).

theorem exists_rankings_gsMatching (mp' : MPrefs (Fin n) (Fin n)) (wp' : WPrefs (Fin n) (Fin n)) :
    ∃ σ τ : Fin n → Equiv.Perm (Fin n), mprefs σ = mp' ∧ wprefs τ = wp' ∧
      IsStable mp' wp' (gsMatching σ τ) ∧
      ∀ ν : PerfectMatching (Fin n) (Fin n), IsStable mp' wp' ν →
        ∀ m, ¬ (mp' m).lt (ν m) (gsMatching σ τ m)

Uses 14

Statement usesThe Gale-Shapley matching · Proposers' preferences from rankings · Receivers' preference profile from rankings · Stable perfect matching · Men's preferences · Perfect matching · Relation of a strict total order · Women's preference profile

Proof usesEvery strict total order on \(\{0, \dots, n-1\}\) is given by a ranking · Proposer-optimality · The Gale-Shapley matching is stable · Preference order of a ranking · Strict preference order · Strict total order

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.