Theory Sotomayor
theory Sotomayor
imports
Main
begin
section‹ \<^citet>‹"Sotomayor:1996"›: A non-constructive proof of the existence of stable marriages \label{sec:sotomayor} ›
text‹
We set the scene with a non-constructive proof of the existence of
stable matches due to \<^citet>‹"Sotomayor:1996"›. This approach is
pleasantly agnostic about the strictness of preferences, and moreover
avoids getting bogged down in reasoning about programs; most existing
proofs involve such but omit formal treatments of the requisite
assertions. This tradition started with \<^citet>‹"GaleShapley:1962"›; see
\<^citet>‹"Bijlsma:1991"› for a rigorous treatment.
The following contains the full details of an Isabelle/HOL
formalization of her proof, and aims to introduce the machinery we
will make heavy use of later. Further developments will elide many of
the more tedious technicalities that we include here.
The scenario consists of disjoint finite sets of men @{term "M"} and
women @{term "W"}, represented as types ‹'m::finite"› and
‹'w::finite› respectively. We diverge from
\citeauthor{Sotomayor:1996} by having each man and woman rank only
acceptable partners in a way that is transitive and complete. (Here
completeness requires @{const "Refl"} in addition to @{const "Total"}
as the latter does not imply the former, and so we end up with a total
preorder.) Such orders therefore include cycles of indifference, i.e.,
are not antisymmetric.
Also matches are treated as relations rather than functions.
We model this scenario in a @{theory_text "locale"}, a sectioning
mechanism for stating a series of lemmas relative to a set of fixed
variables (@{theory_text "fixes"}) and assumptions (@{theory_text
"assumes"}) that can later be instantiated and discharged.
›
type_synonym ('m, 'w) match = "('m × 'w) set"
locale StableMarriage =
fixes Pm :: "'m::finite ⇒ 'w::finite rel"
fixes Pw :: "'w ⇒ 'm rel"
assumes Pm_pref: "∀m. Preorder (Pm m) ∧ Total (Pm m)"
assumes Pw_pref: "∀w. Preorder (Pw w) ∧ Total (Pw w)"
begin
text‹
A @{emph ‹match›} assigns at most one man to each woman, and
vice-versa. It is also @{emph ‹individually rational›}, i.e., the
partners are acceptable to each other. The constant @{const "Field"}
is the union of the @{const "Domain"} and @{const "Range"} of a
relation.
›
definition match :: "('m, 'w) match ⇒ bool" where
"match μ ⟷ inj_on fst μ ∧ inj_on snd μ ∧ μ ⊆ (⋃m. {m} × Field (Pm m)) ∩ (⋃w. Field (Pw w) × {w})"
text‹
A woman @{emph ‹prefers›} one man to another if her preference order
ranks the former over the latter, and @{emph ‹strictly prefers›} him if
additionally the latter is not ranked over the former, and similarly
for the men.
›
abbreviation (input) "m_for w μ ≡ {m. (m, w) ∈ μ}"
abbreviation (input) "w_for m μ ≡ {w. (m, w) ∈ μ}"
definition m_prefers :: "'m ⇒ ('m, 'w) match ⇒ 'w set" where
"m_prefers m μ = {w' ∈ Field (Pm m). ∀w∈w_for m μ. (w, w') ∈ Pm m}"
definition w_prefers :: "'w ⇒ ('m, 'w) match ⇒ 'm set" where
"w_prefers w μ = {m' ∈ Field (Pw w). ∀m∈m_for w μ. (m, m') ∈ Pw w}"
definition m_strictly_prefers :: "'m ⇒ ('m, 'w) match ⇒ 'w set" where
"m_strictly_prefers m μ = {w' ∈ Field (Pm m). ∀w∈w_for m μ. (w, w') ∈ Pm m ∧ (w', w) ∉ Pm m}"
definition w_strictly_prefers :: "'w ⇒ ('m, 'w) match ⇒ 'm set" where
"w_strictly_prefers w μ = {m' ∈ Field (Pw w). ∀m∈m_for w μ. (m, m') ∈ Pw w ∧ (m', m) ∉ Pw w}"
text‹
A couple @{emph ‹blocks›} a match ‹μ› if both strictly
prefer each other to anyone they are matched with in
‹μ›.
›
definition blocks :: "'m ⇒ 'w ⇒ ('m, 'w) match ⇒ bool" where
"blocks m w μ ⟷ w ∈ m_strictly_prefers m μ ∧ m ∈ w_strictly_prefers w μ"
text‹
We say a match is @{emph ‹stable›} if there are no blocking couples.
›
definition stable :: "('m, 'w) match ⇒ bool" where
"stable μ ⟷ match μ ∧ (∀m w. ¬ blocks m w μ)"
lemma stable_match:
assumes "stable μ"
shows "match μ"
using assms unfolding stable_def by blast
text‹
Our goal is to show that for every preference order there is a stable
match. Stable matches in this scenario form a lattice, and this proof
implicitly adopts the traditional view that men propose and women
choose.
The definitions above form the trust basis for this existence theorem;
the following are merely part of the proof apparatus, and Isabelle/HOL
enforces their soundness with respect to the argument. We will see
these concepts again in later developments.
Firstly, a match is @{emph ‹simple›} if every woman party to a blocking
pair is single. The most obvious such match leaves everyone single.
›
definition simple :: "('m, 'w) match ⇒ bool" where
"simple μ ⟷ match μ ∧ (∀m w. blocks m w μ ⟶ w ∉ Range μ)"
lemma simple_match:
assumes "simple μ"
shows "match μ"
using assms unfolding simple_def by blast
lemma simple_ex:
"∃μ. simple μ"
unfolding simple_def blocks_def match_def by auto
text‹
\citeauthor{Sotomayor:1996} observes the following:
›
lemma simple_no_single_women_stable:
assumes "simple μ"
assumes "∀w. w ∈ Range μ"
shows "stable μ"
using assms unfolding simple_def stable_def by blast
lemma stable_simple:
assumes "stable μ"
shows "simple μ"
using assms unfolding simple_def stable_def by blast
text‹
Secondly, a @{emph ‹weakly Pareto optimal match for men (among all
simple matches)›} is one for which there is no other match that all men
like as much and some man likes more.
›
definition m_weakly_prefers :: "'m ⇒ ('m, 'w) match ⇒ 'w set" where
"m_weakly_prefers m μ = {w' ∈ Field (Pm m). ∀w∈w_for m μ. (w, w') ∈ Pm m}"
definition weakly_preferred_by_men :: "('m, 'w) match ⇒ ('m, 'w) match ⇒ bool" where
"weakly_preferred_by_men μ μ'
⟷ (∀m. ∀w∈w_for m μ. ∃w'∈w_for m μ'. w' ∈ m_weakly_prefers m μ)"
definition strictly_preferred_by_a_man :: "('m, 'w) match ⇒ ('m, 'w) match ⇒ bool" where
"strictly_preferred_by_a_man μ μ'
⟷ (∃m. ∃w∈w_for m μ'. w ∈ m_strictly_prefers m μ)"
definition weakly_Pareto_optimal_for_men :: "('m, 'w) match ⇒ bool" where
"weakly_Pareto_optimal_for_men μ
⟷ simple μ ∧ ¬(∃μ'. simple μ' ∧ weakly_preferred_by_men μ μ' ∧ strictly_preferred_by_a_man μ μ')"
text‹
We will often provide @{emph ‹introduction rules›} for more complex
predicates, and sometimes derive these by elementary syntactic
manipulations expressed by the @{emph ‹attributes›}
enclosed in square brackets after a use-mention of a lemma. The
@{command "lemmas"} command binds a name to the result. To conform
with the Isar structured proof language, we use meta-logic (``Pure''
in Isabelle terminology) connectives: ‹⋀› denotes
universal quantification, and ‹⟹›
implication.
›
lemma weakly_preferred_by_menI:
assumes "⋀m w. (m, w) ∈ μ ⟹ ∃w'. (m, w') ∈ μ' ∧ w' ∈ m_weakly_prefers m μ"
shows "weakly_preferred_by_men μ μ'"
using assms unfolding weakly_preferred_by_men_def by blast
lemmas simpleI = iffD2[OF simple_def, unfolded conj_imp_eq_imp_imp, rule_format]
lemma weakly_Pareto_optimal_for_men_simple:
assumes "weakly_Pareto_optimal_for_men μ"
shows "simple μ"
using assms unfolding weakly_Pareto_optimal_for_men_def by simp
text‹
Later we will elide obvious technical lemmas like the following. The
more obscure proofs are typically generated automatically by
sledgehammer \<^citep>‹"Blanchette:2016"›.
›
lemma m_weakly_prefers_Pm:
assumes "match μ"
assumes "(m, w) ∈ μ"
shows "w' ∈ m_weakly_prefers m μ ⟷ (w, w') ∈ Pm m"
using spec[OF Pm_pref, where x=m] assms unfolding m_weakly_prefers_def match_def preorder_on_def
by simp (metis (no_types, opaque_lifting) FieldI2 fst_conv inj_on_contraD snd_conv)
lemma match_Field:
assumes "match μ"
assumes "(m, w) ∈ μ"
shows "w ∈ Field (Pm m)"
and "m ∈ Field (Pw w)"
using assms unfolding match_def by blast+
lemma weakly_preferred_by_men_refl:
assumes "match μ"
shows "weakly_preferred_by_men μ μ"
using assms unfolding weakly_preferred_by_men_def m_weakly_prefers_def
by clarsimp (meson Pm_pref m_weakly_prefers_Pm match_Field(1) preorder_on_def refl_onD)
text‹
\citeauthor[p137]{Sotomayor:1996} provides an alternative definition
of @{const "weakly_preferred_by_men"}. The syntax @{theory_text "(is
?lhs ⟷ pat)"} binds the @{emph ‹schematic
variables›} ‹?lhs› and ‹?rhs› to the terms
separated by ‹⟷›.
›
lemma weakly_preferred_by_men_strictly_preferred_by_a_man:
assumes "match μ"
assumes "match μ'"
shows "weakly_preferred_by_men μ μ' ⟷ ¬strictly_preferred_by_a_man μ' μ" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs then show ?rhs
unfolding weakly_preferred_by_men_def strictly_preferred_by_a_man_def
m_weakly_prefers_def m_strictly_prefers_def by fastforce
next
assume ?rhs show ?lhs
proof(rule weakly_preferred_by_menI)
fix m w assume "(m, w) ∈ μ"
from assms ‹?rhs› ‹(m, w) ∈ μ› obtain w' where XXX: "(m, w') ∈ μ'" "(w', w) ∈ Pm m ⟶ (w, w') ∈ Pm m"
unfolding match_def strictly_preferred_by_a_man_def m_strictly_prefers_def by blast
with spec[OF Pm_pref, where x=m] assms ‹(m, w) ∈ μ›
show "∃w'. (m, w') ∈ μ' ∧ w' ∈ m_weakly_prefers m μ"
unfolding preorder_on_def total_on_def by (metis m_weakly_prefers_Pm match_Field(1) refl_onD)
qed
qed
lemma weakly_Pareto_optimal_for_men_def2:
"weakly_Pareto_optimal_for_men μ
⟷ simple μ ∧ (∀μ'. simple μ' ∧ strictly_preferred_by_a_man μ μ' ⟶ strictly_preferred_by_a_man μ' μ)"
unfolding weakly_Pareto_optimal_for_men_def simple_def
by (meson weakly_preferred_by_men_strictly_preferred_by_a_man)
text‹
\citeauthor{Sotomayor:1996} claims that the existence of such a weakly
Pareto optimal match for men is ``guaranteed by the fact that
@{emph ‹the set of simple matchings is nonempty›} [our @{thm [source]
"simple_ex"} lemma] @{emph ‹and finite and the preferences are
transitive.›}'' The following lemmas express this intuition:
›
lemma trans_finite_has_maximal_elt:
assumes "trans r"
assumes "finite (Field r)"
assumes "Field r ≠ {}"
shows "∃x∈Field r. (∀y∈Field r. (x, y) ∈ r ⟶ (y, x) ∈ r)"
using assms(2,1,3) by induct (auto elim: transE)
lemma weakly_Pareto_optimal_for_men_ex:
"∃μ. weakly_Pareto_optimal_for_men μ"
proof -
let ?r = "{(μ, μ'). simple μ ∧ simple μ' ∧ weakly_preferred_by_men μ μ'}"
from trans_finite_has_maximal_elt[where r="?r"]
obtain x where "x ∈ Field ?r" "∀y∈Field ?r. (x, y) ∈ ?r ⟶ (y, x) ∈ ?r"
proof
from Pm_pref show "trans ?r"
unfolding trans_def weakly_preferred_by_men_def m_weakly_prefers_def m_strictly_prefers_def
by simp (meson order_on_defs(1) transE)
from simple_ex weakly_preferred_by_men_refl[OF simple_match] show "Field ?r ≠ {}"
unfolding Field_def by force
qed simp_all
then show ?thesis
unfolding weakly_Pareto_optimal_for_men_def Field_def
using simple_match weakly_preferred_by_men_strictly_preferred_by_a_man by auto
qed
text‹
The main result proceeds by contradiction.
›
lemma weakly_Pareto_optimal_for_men_stable:
assumes "weakly_Pareto_optimal_for_men μ"
shows "stable μ"
proof(rule ccontr)
assume "¬stable μ"
from ‹weakly_Pareto_optimal_for_men μ› have "simple μ" by (rule weakly_Pareto_optimal_for_men_simple)
from ‹¬stable μ› ‹simple μ› obtain m' w where "blocks m' w μ" and "w ∉ Range μ"
unfolding simple_def stable_def by blast+
let ?r = "Restr (Pw w) {m. w ∈ m_strictly_prefers m μ}"
from trans_finite_has_maximal_elt[where r="?r"]
obtain m where "m ∈ Field ?r" "∀m'∈Field ?r. (m, m') ∈ ?r ⟶ (m', m) ∈ ?r"
proof
from Pw_pref show "trans ?r"
unfolding preorder_on_def by (blast intro: trans_Restr)
from Pw_pref ‹blocks m' w μ› have "(m', m') ∈ ?r"
unfolding blocks_def w_strictly_prefers_def preorder_on_def by (blast dest: refl_onD)
then show "Field ?r ≠ {}" by (metis FieldI2 empty_iff)
qed simp_all
with ‹blocks m' w μ› ‹w ∉ Range μ›
have "blocks m w μ" and "∀m'. blocks m' w μ ∧ (m, m') ∈ Pw w ⟶ (m', m) ∈ Pw w"
unfolding blocks_def w_strictly_prefers_def Field_def by auto
let ?μ' = "μ - {(m, w') |w'. True} ∪ {(m, w)}"
have "simple ?μ'"
proof(rule simpleI)
from ‹simple μ› ‹blocks m w μ› show "match ?μ'"
unfolding blocks_def match_def simple_def m_strictly_prefers_def w_strictly_prefers_def
by (safe; clarsimp simp: inj_on_diff; blast)
fix m' w' assume "blocks m' w' ?μ'"
from ‹blocks m' w' ?μ'› ‹∀m'. blocks m' w μ ∧ (m, m') ∈ Pw w ⟶ (m', m) ∈ Pw w›
have "w' ≠ w"
unfolding blocks_def m_strictly_prefers_def w_strictly_prefers_def by auto
show "w' ∉ Range ?μ'"
proof(cases "(m, w') ∈ μ")
case True
from ‹simple μ› ‹blocks m' w' ?μ'› ‹w' ≠ w› ‹(m, w') ∈ μ›
show ?thesis
unfolding simple_def match_def
by clarsimp (metis (no_types, opaque_lifting) fst_conv inj_on_contraD snd_conv)
next
case False
from Pm_pref ‹blocks m w μ› ‹blocks m' w' ?μ'› ‹(m, w') ∉ μ›
have "blocks m' w' μ"
unfolding preorder_on_def blocks_def m_strictly_prefers_def w_strictly_prefers_def
by simp (metis transE)
with ‹simple μ› ‹w' ≠ w› show ?thesis unfolding simple_def by blast
qed
qed
moreover have "weakly_preferred_by_men μ ?μ'"
proof(rule weakly_preferred_by_menI)
fix m' w' assume "(m', w') ∈ μ"
then show "∃w'. (m', w') ∈ ?μ' ∧ w' ∈ m_weakly_prefers m' μ"
proof(cases "m' = m")
case True
from ‹blocks m w μ› ‹(m', w') ∈ μ› ‹m' = m› show ?thesis
unfolding m_weakly_prefers_def blocks_def m_strictly_prefers_def by blast
next
case False
from Pm_pref ‹simple μ› ‹(m', w') ∈ μ› ‹m' ≠ m› show ?thesis
by clarsimp (meson m_weakly_prefers_Pm match_Field preorder_on_def refl_onD simple_match)
qed
qed
moreover from ‹blocks m w μ› have "strictly_preferred_by_a_man μ ?μ'"
unfolding strictly_preferred_by_a_man_def blocks_def by blast
moreover note ‹weakly_Pareto_optimal_for_men μ›
ultimately show False
unfolding weakly_Pareto_optimal_for_men_def by blast
qed
theorem stable_ex:
"∃μ. stable μ"
using weakly_Pareto_optimal_for_men_stable weakly_Pareto_optimal_for_men_ex by blast
text‹
We can exit the locale context and later re-enter it.
›
end
text‹
We @{emph ‹interpret›} the locale by supplying constants that instantiate
the variables we fixed earlier, and proving that these satisfy the
assumptions. In this case we provide concrete preference orders, and
by doing so we demonstrate that our theory is non-vacuous. We
arbitrarily choose \<^citet>‹‹Example~2.15› in "RothSotomayor:1990"› which
demonstrates the non-existence of man- or woman-optimal matches if
preferences are non-strict. (We define optimality shortly.) The
following bunch of types eases the description of this particular
scenario.
›