EconCSLib.MarketDesign.Matching.GaleShapley

Standard Gale-Shapley deferred-acceptance algorithm for two-sided matching markets.

Replaces the earlier batched-proposal (Boston-mechanism) gs_aux that committed women in round 1 with no ability to upgrade — verified unstable via #eval (commit 1e14bf9: blocking pair (b, A) on the n=3 counterexample).

Scope (MT-L0 + MT-L1, #202 + #203)

• GS.Preferences n — list-based preference type for the algorithmic layer.
• Standard DA: GS.daStep, GS.daRun, GS.finalState, GS.gs.
• gs_bijective — proved via injectivity + pigeonhole.
• galeShapley_isStable — stability via the standard deferred-acceptance argument.
• Bridge types: MatchingMarket.ofEquivData, Matching.ofGS.

Algorithm design

Standard men-proposing DA with explicit state (nextChoice, holding):

• holding j = some i: woman j currently holds man i tentatively.
• nextChoice i = k: man i's next proposal is (m.prefs i)[k].
• A man is free when no woman holds him.
• Each step: every free man proposes his next-best woman; each woman keeps the best of {held, new proposers} by her preference list rank; free men advance nextChoice.
• Termination: structural recursion on fuel n*n + 1. At most n*n proposals total (n men × n proposals each).

Key invariants

All preserved by every daStep (preservation lemmas listed in parentheses).

1. Rank monotonicity — a woman's held man's rank only decreases over time; once she upgrades, she never downgrades (holding_rank_mono_step / _run).
2. Holding injectivity — at most one woman holds any given man at any time (holding_injective_step / _run).
3. JInv — proposed ⇒ held: every woman who has ever been proposed to is currently held by someone (jinv_step).
4. HoldInv — held ⇒ proposed: every currently-held pair (p, j) has j having already proposed to p (holdinv_step).
5. RSInv — the deferred-acceptance rank invariant (the stability engine): every woman a man has proposed to is currently holding someone at least as preferred as that man (rsinv_step).
6. At termination: all men held → all women hold someone (by pigeonhole on holding_injective).

Proof strategy (from primitives to stability)

            initState
                │
                │  daStep (preserves all six invariants)
                ▼
            finalState
            │   │   │
            │   │   └─► holding_injective  ──┐
            │   │                            ├─► gs_bijective ──┐
            │   └─────► all men held        ─┘                  │
            │                                                   ▼
            └─────► RSInv@finalState ──► no blocking pair (stability)
                       │       └────── HoldInv@finalState
                       │
                       └── relies on rank-mono + JInv

Roughly: cursors and holdings stay in two-sided correspondence (JInv

• HoldInv); a held pair only upgrades (holding_rank_mono); at most one woman holds any man (holding_injective); cursors are bounded by n (nc_le_n_run) and grow monotonically (nc_sum_grows), so the fuel n*n + 1 always suffices for termination (finalState_no_free_men); and at termination RSInv rules out blocking pairs (rsinv_stability).

References

• [Gale-Shapley 1962] Am. Math. Monthly 69(1):9-15 — original existence proof.
• [Roth-Sotomayor 1990] Two-Sided Matching, Ch. 2-3 — textbook treatment of deferred acceptance and stability.
• [MSZ Ch.22, Alg 22.6 + Thm 22.7] Maschler, Solan, Zamir, Game Theory — the deferred-acceptance algorithm and its stability theorem.

Preference type

structure GS.Preferences (n : ℕ) : Type

List-based preferences: prefs i is a full permutation of Fin n, ordered from most to least preferred.

• prefs : Fin n → List (Fin n)
• valid (i : Fin n) : (self.prefs i).Nodup ∧ (self.prefs i).length = n

Helper lemmas

theorem GS.pref_list_mem {n : ℕ} (l : List (Fin n)) (hnd : l.Nodup) (hlen : l.length = n) (x : Fin n) : x ∈ l

Every element of Fin n appears in a full-permutation list.

DA state

structure GS.DAState (n : ℕ) : Type

DA state: per-man proposal cursor + per-woman tentative hold.

• nextChoice : Fin n → ℕ
• holding : Fin n → Option (Fin n)

def GS.initState (n : ℕ) : DAState n

Initial state: all women free, all men start at proposal index 0.

Equations

• GS.initState n = { nextChoice := fun (x : Fin n) => 0, holding := fun (x : Fin n) => none }

Free-man predicate

def GS.isFree {n : ℕ} (s : DAState n) (i : Fin n) : Bool

Man i is free in s iff no woman holds him.

Equations

• GS.isFree s i = decide (∀ (j : Fin n), s.holding j ≠ some i)

theorem GS.isFree_iff {n : ℕ} (s : DAState n) (i : Fin n) : isFree s i = true ↔ ∀ (j : Fin n), s.holding j ≠ some i

theorem GS.not_isFree_iff {n : ℕ} (s : DAState n) (i : Fin n) : isFree s i = false ↔ ∃ (j : Fin n), s.holding j = some i

def GS.freeMenSet {n : ℕ} (s : DAState n) : Finset (Fin n)

The finset of all free men in s.

Equations

• GS.freeMenSet s = {i : Fin n | GS.isFree s i = true}

theorem GS.mem_freeMenSet {n : ℕ} {s : DAState n} {i : Fin n} : i ∈ freeMenSet s ↔ isFree s i = true

Proposal target

def GS.propTarget {n : ℕ} (m : Preferences n) (i : Fin n) (k : ℕ) : Option (Fin n)

The woman man i proposes to at cursor index k (none if out of bounds).

Equations

• GS.propTarget m i k = (m.prefs i)[k]?

theorem GS.propTarget_lt {n : ℕ} (m : Preferences n) (i : Fin n) {k : ℕ} (hk : k < n) : ∃ (j : Fin n), propTarget m i k = some j

propTarget returns some when k < n.

DA step

noncomputable def GS.daStep {n : ℕ} (w m : Preferences n) (s : DAState n) : DAState n

One step of standard men-proposing DA.

All free men propose; women pick the best of {held, new proposers} by rank; free men advance their cursor by 1.

Equations

• One or more equations did not get rendered due to their size.

theorem GS.daStep_nc_free {n : ℕ} {w m : Preferences n} {s : DAState n} {i : Fin n} (hi : isFree s i = true) : (daStep w m s).nextChoice i = s.nextChoice i + 1

theorem GS.daStep_nc_held {n : ℕ} {w m : Preferences n} {s : DAState n} {i : Fin n} (hi : isFree s i = false) : (daStep w m s).nextChoice i = s.nextChoice i

theorem GS.daStep_holding {n : ℕ} (w m : Preferences n) (s : DAState n) (p : Fin n) : (daStep w m s).holding p = match s.holding p, List.argmin (fun (i : Fin n) => List.idxOf i (w.prefs p)) {i : Fin n | (isFree s i && propTarget m i (s.nextChoice i) == some p) = true}.val.toList with | none, none => none | some h, none => some h | none, some q => some q | some h, some q => if List.idxOf q (w.prefs p) < List.idxOf h (w.prefs p) then some q else some h

One step of DA: woman p's new holding, expanded once.

This is the workhorse rewrite for any proof that needs to case-split on what (daStep w m s).holding p is. It unfolds the outermost match inside daStep's newHolding. The statement does inline the auxiliary proposerList / bestNew formulae verbatim; downstream proofs re-abbreviate them with set after rewriting (see holdinv_step).

The match shape is:

match s.holding p, bestNew p with
| none,   none   => none                                  -- still free
| some h, none   => some h                                -- old hold kept
| none,   some q => some q                                -- new proposer
| some h, some q => if rank q < rank h then q else h      -- upgrade?

where bestNew p = (proposerList p).argmin (rank in w.prefs p) and proposerList p is the list of free men who proposed to p this step.

Provable by rfl because daStep is noncomputable def and the body is a sequence of lets ending in a structure literal whose .holding p projects directly to the inner match.

DA run (structurally recursive, no WF needed)

noncomputable def GS.daRun {n : ℕ} (w m : Preferences n) : ℕ → DAState n → DAState n

Run DA for at most fuel steps, stopping early if no free men remain.

Equations

• GS.daRun w m 0 x✝ = x✝
• GS.daRun w m fuel.succ x✝ = if (GS.freeMenSet x✝).Nonempty then GS.daRun w m fuel (GS.daStep w m x✝) else x✝

noncomputable def GS.finalState {n : ℕ} (w m : Preferences n) : DAState n

finalState: run daRun with fuel n*n + 1 from initState.

Equations

• GS.finalState w m = GS.daRun w m (n * n + 1) (GS.initState n)

noncomputable def GS.gs {n : ℕ} [NeZero n] (w m : Preferences n) : Fin n → Fin n

The Gale-Shapley function: woman j's partner at termination.

Equations

• GS.gs w m j = ((GS.finalState w m).holding j).getD default

Bridge to EconCSLib native types

noncomputable def MatchingMarket.ofEquivData {n : ℕ} (wPrefs mPrefs : GS.Preferences n) : MatchingMarket (Fin n) (Fin n)

Build a MatchingMarket (Fin n) (Fin n) from list-based preference data. some j ≻ some k iff j appears earlier in the list; none is worst.

Side transposition (read carefully). ofEquivData a b puts a on the market's MEN (prefM) and b on the market's WOMEN (prefW). Hence when it is applied as ofEquivData w m with the algorithm's w (women's / choosing preferences) and m (men's / proposing preferences), the market's "men" are the algorithm's women and the market's "women" are the algorithm's men — the two sides are transposed. Stability is symmetric, so this is harmless, but be aware that a market-M index corresponds to an algorithm woman (and vice versa); the stability proof reasons in the algorithm frame.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Matching.ofGS {n : ℕ} (f : Fin n → Fin n) (hf : Function.Bijective f) : Matching (Fin n) (Fin n)

Coerce a bijective f : Fin n → Fin n into Matching (Fin n) (Fin n).

Equations

• Matching.ofGS f hf = { matchM := fun (w : Fin n) => some (f w), matchW := fun (m : Fin n) => some ((Equiv.ofBijective f hf).symm m), consistent := ⋯ }

Correctness (MT-L1 #203)

Invariant 1: holding rank monotonically improves

theorem holding_rank_mono_step {n : ℕ} [NeZero n] (w m : GS.Preferences n) (s : GS.DAState n) (j : Fin n) {hval : Fin n} (hh : s.holding j = some hval) : ∃ (h' : Fin n), (GS.daStep w m s).holding j = some h' ∧ List.idxOf h' (w.prefs j) ≤ List.idxOf hval (w.prefs j)

After one daStep, woman j's held man's rank can only decrease (she only upgrades).

theorem holding_rank_mono_run {n : ℕ} [NeZero n] (w m : GS.Preferences n) (fuel : ℕ) (s : GS.DAState n) (j : Fin n) {hval : Fin n} (hh : s.holding j = some hval) : ∃ (h' : Fin n), (GS.daRun w m fuel s).holding j = some h' ∧ List.idxOf h' (w.prefs j) ≤ List.idxOf hval (w.prefs j)

Rank-mono over any daRun.

theorem held_preserved_run {n : ℕ} [NeZero n] (w m : GS.Preferences n) (fuel : ℕ) (s : GS.DAState n) (j : Fin n) {hval : Fin n} (hh : s.holding j = some hval) : ∃ (h' : Fin n), (GS.daRun w m fuel s).holding j = some h'

Once held, always held over daRun.

Invariant 2: holding is injective

theorem holding_injective_step {n : ℕ} [NeZero n] (w m : GS.Preferences n) (s : GS.DAState n) (hinj : ∀ (j1 j2 i : Fin n), s.holding j1 = some i → s.holding j2 = some i → j1 = j2) (j1 j2 i : Fin n) : (GS.daStep w m s).holding j1 = some i → (GS.daStep w m s).holding j2 = some i → j1 = j2

In daStep, holding remains injective.

theorem holding_injective_run {n : ℕ} [NeZero n] (w m : GS.Preferences n) (fuel : ℕ) (s : GS.DAState n) (hinj : ∀ (j1 j2 i : Fin n), s.holding j1 = some i → s.holding j2 = some i → j1 = j2) (j1 j2 i : Fin n) : (GS.daRun w m fuel s).holding j1 = some i → (GS.daRun w m fuel s).holding j2 = some i → j1 = j2

Over daRun, holding remains injective.

theorem initState_injective {n : ℕ} [NeZero n] (j1 j2 i : Fin n) : (GS.initState n).holding j1 = some i → (GS.initState n).holding j2 = some i → j1 = j2

initState has trivially injective holding (all none).

Invariant 3: fuel sufficiency

The following private lemmas are defined outside section GS_Correctness to avoid implicit section variable clutter. All parameters are explicit.

Proposal rank bound: the core of Roth-Sotomayor

Roth–Sotomayor rank invariant

def HoldInv {n : ℕ} (m : GS.Preferences n) (s : GS.DAState n) : Prop

HoldInv (Held → Proposed): if woman p currently holds man j, then j must already have proposed to p — i.e., p is in the proposed-prefix (m.prefs j).take (s.nextChoice j) of j's preference list.

This is the converse direction of [JInv]: JInv says proposed ⇒ held; HoldInv says held ⇒ proposed. Together they make the two-sided correspondence between cursors and holdings airtight.

HoldInv is the one the stability proof's "the holder must be at least as preferred as the blocker" step relies on, via RSInv — see the proof sketch of [galeShapley_isStable] and the preservation lemma [holdinv_step].

Equations

• HoldInv m s = ∀ (j p : Fin n), s.holding p = some j → p ∈ List.take (s.nextChoice j) (m.prefs j)

theorem holdinv_init {n : ℕ} [NeZero n] (m : GS.Preferences n) : HoldInv m (GS.initState n)

theorem holdinv_step {n : ℕ} [NeZero n] (w m : GS.Preferences n) (s : GS.DAState n) (hhold : HoldInv m s) : HoldInv m (GS.daStep w m s)

HoldInv is preserved by one DA step.

Proof structure: case-analyze on the pair (s.holding p, bestNew p) that drives daStep's decision for woman p. There are four cases, two of which (old hold preserved and new free-man wins) recur in mirrored form depending on whether s.holding p was some h or none. We extract those two arguments into the local helpers preserve_hold and new_hold and dispatch each of the four cases with a single line.

Throughout, the key external lemmas are:

• pl_free_props — anyone in proposerList p was free and proposed to p.
• daStep_nc_free / daStep_nc_held — nextChoice j advances by 1 if j was free, stays put otherwise.
• not_isFree_iff — j is not free in s iff some woman holds j.

theorem holdinv_finalState {n : ℕ} [NeZero n] (w m : GS.Preferences n) : HoldInv m (GS.finalState w m)

Invariant 1: holding rank monotonically improves

Invariant 3: termination

theorem finalState_no_free_men {n : ℕ} [NeZero n] (w m : GS.Preferences n) (i : Fin n) : GS.isFree (GS.finalState w m) i = false

At termination, every man is held (no free man remains). Proof: if a free man remained, nc_sum_grows would give n*n + 1 ≤ n*n, contradiction.

Total matching

theorem final_all_men_held {n : ℕ} [NeZero n] (w m : GS.Preferences n) (i : Fin n) : ∃ (j : Fin n), (GS.finalState w m).holding j = some i

At termination, every man is held by some woman.

theorem final_holding_injective {n : ℕ} [NeZero n] (w m : GS.Preferences n) (j1 j2 i : Fin n) : (GS.finalState w m).holding j1 = some i → (GS.finalState w m).holding j2 = some i → j1 = j2

finalState holding is injective.

theorem final_all_women_hold {n : ℕ} [NeZero n] (w m : GS.Preferences n) (j : Fin n) : ∃ (i : Fin n), (GS.finalState w m).holding j = some i

At termination, every woman holds some man.

Bijectivity

theorem gs_injective {n : ℕ} [NeZero n] (w m : GS.Preferences n) : Function.Injective (GS.gs w m)

gs w m is injective.

theorem gs_bijective {n : ℕ} [NeZero n] (w m : GS.Preferences n) : Function.Bijective (GS.gs w m)

gs w m is a bijection on Fin n.

Stability

theorem galeShapley_isStable {n : ℕ} [NeZero n] (w m : GS.Preferences n) : Matching.IsStable (MatchingMarket.ofEquivData w m) (Matching.ofGS (GS.gs w m) ⋯)

Gale-Shapley stability: the DA output has no blocking pair.

The statement is in the market frame (IsBlocking … (i : M) (j : W)). But MatchingMarket.ofEquivData w m transposes the two sides (see its docstring), so the market-M index i is an algorithm woman and the market-W index j is an algorithm man. The proof therefore reads in the algorithm frame — i a woman, j a man — matching the inline comments.

Proof (standard deferred acceptance): suppose (i, j) blocks. In algorithm terms man j strictly prefers woman i to his wife, so j proposed to i at some round: his wife is in his proposed-prefix (holdinv_finalState) and i is ranked at least as early (hprefJ). Then rsinv_stability (RSInv) gives that at termination woman i holds a man she ranks at least as high as j, so she does not strictly prefer j to her partner — contradicting the blocking assumption.