This repository is formalization of some results about stable matchings and the Gale-Shapley algorithm.
We follow Dumont's paper (in French) as it contains more advanced results than other sources.
An introduction to the subject can be found in Gale and Shapley's original paper. Many other sources have introductory material on the topic as well.
We do not handle the case of incomplete preference lists. However, we do allow different cardinalities on the two sides, so matchings are implemented as partial functions M → Option W.
In the main library GaleShapley, only one proposer, arbitarily chosen using choose, proposes on each round. This gives maximal generality of the results, since it shows they do not depend on who proposes each round. For a computable implementation, see the Computable Implementation section.
Implements the Gale-Shapley algorithm galeShapley which gives a stable matching given an initial set of preferences. The proof of stability is from Gale and Shapley's original paper, also given in Section 1.2 of Dumont, and many other sources.
proposerOptimal: The Gale-Shapley algorithm gives the optimal stable matching for the proposing side. The proof is from Gale and Shapley's original paper, also available in many other sources.
The dual result receiverPessimal follows as a corollary.
hwangTheorem: Hwang's theorem as stated in Dumont's paper section 1.5 in terms of revendicateurs. We follow the proof in Dumont. This gives three corollaries:
proposerOptimal': An alternative proof of proposer optimality.paretoOptimality: There is no matching (whether stable or not) in which all proposers do better than in the proposer-optimal stable matching.menShouldntLie: The Dubins-Freedman result that "men shouldn't lie", with the proof given in Theorem 2.3 of Dumont. Using Hwang's theorem, the proof is much simpler than the original proof from Dubins and Freedman's paper.
A collection of results about the interaction of 2 stable matchings for the same set of preferences, found in sections 1.3 and 1.4 of Dumont.
It culminates with Conway's result that the set of stable matchings for a fixed set of preferences form a complete lattice under the natural inf and sup operations (supMatchingClosed, supMatchingStable, infMatchingClosed, infMatchingStable)
mPref_stableCompleteLattice: Construct the complete lattice mentioned above on the set of stable matchings, using the results from GaleShapley.TwoStableMatchings.
gsEqualsTop: Yet another version of proposer optimality, saying that the stable matching given by the Gale-Shapley algorithm is the top element of the complete lattice. We derive the result in a straightforward way from the main result in Optimality.
The subdirectory GaleShapley/Compute contains a computable implementation of the algorithm which can be compiled and executed. We assume DecidableEq M and DecidableEq W to allow computation.
Basic contains the same implementation as in the main library, except that instead of choosing a proposer arbitrarily, we assume LinearOrder M and choose the lowest eligible proposer each round. This is a minimal version of the library where all proofs have been removed except those necessary to define the algorithm.
BasicAlt contains an alternate "parallel" implementation in which all eligible proposers propose each round. However, for reasons I don't really understand, this code runs extremely slowly starting at n=4. Ideas for resolving this issue, or at least understanding it, would be appreciated.
Compute contains a sample definition of some preferences and computations. The n=4 example is taken from Gale and Shapley's original paper. Some computations are done with #eval, and there is also a Main function doing the computation for n=4 which can be compiled with lake build GaleShapleyCompute. The compiled binary is at .lake/build/bin/GaleShapleyCompute.
You can see the n=4 slowdown for BasicAlt if you change the import in Compute from Basic to BasicAlt, and look at the #eval statement towards the bottom of the file.