diff --git a/thys/Gale_Shapley/Gale_Shapley1.thy b/thys/Gale_Shapley/Gale_Shapley1.thy --- a/thys/Gale_Shapley/Gale_Shapley1.thy +++ b/thys/Gale_Shapley/Gale_Shapley1.thy @@ -1,1298 +1,1293 @@ (* Stepwise refinement of the Gale-Shapley algorithm down to executable functional code. Part 1: Refinement down to lists. Author: Tobias Nipkow *) theory Gale_Shapley1 imports Main "HOL-Hoare.Hoare_Logic" "List-Index.List_Index" "HOL-Library.While_Combinator" "HOL-Library.LaTeXsugar" begin lemmas conj12 = conjunct1 conjunct2 (* TODO: mv *) theorem while_rule2: "[| P s; !!s. [| P s; b s |] ==> P (c s) \ (c s, s) \ r; !!s. [| P s; \ b s |] ==> Q s; wf r |] ==> Q (while b c s)" using while_rule[of P] by metis -(* by now in Map *) -lemma ran_map_upd_Some: - "\ m x = Some y; inj_on m (dom m); z \ ran m \ \ ran(m(x := Some z)) = ran m - {y} \ {z}" -by(force simp add: ran_def domI inj_onD) - syntax "_assign_list" :: "idt \ nat \ 'b \ 'com" ("(2_[_] :=/ _)" [70, 0, 65] 61) translations "xs[n] := e" \ "xs := CONST list_update xs n e" abbreviation upt_set :: "nat \ nat set" ("{<_}") where "{ {0.. 'a \ 'a \ bool" where "prefers P x y = (index P x < index P y)" abbreviation prefa :: "'a list \ 'a \ 'a \ bool" ("(_ \/ _ < _)" [50,50,50] 50) where "P \ x < y \ prefers P x y" lemma prefers_asym: "P \ x < y \ \ P \ y < x" by(simp add: prefers_def) lemma prefers_trans: "P \ x < y \ P \ y < z \ P \ x < z" by (meson order_less_trans prefers_def) fun rk_of_pref :: "nat \ nat list \ nat list \ nat list" where "rk_of_pref r rs (n#ns) = (rk_of_pref (r+1) rs ns)[n := r]" | "rk_of_pref r rs [] = rs" definition ranking :: "nat list \ nat list" where "ranking P = rk_of_pref 0 (replicate (length P) 0) P" lemma length_rk_of_pref[simp]: "length(rk_of_pref v vs P) = length vs" by(induction P arbitrary: v)(auto) lemma nth_rk_of_pref: "\ length P \ length rs; i \ set P; distinct P; set P \ { \ rk_of_pref r rs P ! i = index P i + r" by(induction P arbitrary: r i) (auto simp add: nth_list_update) lemma ranking_iff_pref: "\ set P = { \ ranking P ! i < ranking P ! j \ P \ i < j" by(simp add: ranking_def prefers_def nth_rk_of_pref card_distinct) subsection \Fixing the preference lists\ type_synonym prefs = "nat list list" locale Pref = fixes n fixes P\<^sub>a :: prefs fixes P\<^sub>b :: prefs defines "n \ length P\<^sub>a" assumes length_P\<^sub>b: "length P\<^sub>b = n" assumes P\<^sub>a_set: "a < n \ length(P\<^sub>a!a) = n \ set(P\<^sub>a!a) = {b_set: "b < n \ length(P\<^sub>b!b) = n \ set(P\<^sub>b!b) = { bool" where "wf xs \ length xs = n \ set xs \ { wf A; a < n \ \ A!a < n" by (simp add: subset_eq) corollary wf_le_n1: "\ wf A; a < n \ \ A!a \ n-1" using wf_less_n by fastforce lemma sumA_ub: "wf A \ (\a n*(n-1)" using sum_bounded_above[of "{..The (termination) variant(s)\ text \Basic idea: either some \A!a\ is incremented or size of \M\ is incremented, but this cannot go on forever because in the worst case all \A!a = n-1\ and \M = n\. Because \n*(n-1) + n = n^2\, this leads to the following simple variant:\ definition var0 :: "nat list \ nat set \ nat" where [simp]: "var0 A M = (n^2 - ((\a { a \ M" shows "var0 A (M \ {a}) < var0 A M" proof - have 2: "M \ { { {a n*n" using sumA_ub[OF assms(1)] 0 by (simp add: algebra_simps le_diff_conv2) have "var0 (A[a' := A ! a' + 1]) M = n*n - (1 + (A ! a' + sum ((!) A) ({ = n^2 - (1 + (\a < n^2 - ((\a nat set \ nat" where [simp]: "var A M = (n^2 - n + 1 - ((\a n-1" "\a < n. a \ a' \ A!a \ n-2" shows "(\a (n-1)*(n-1)" proof - have "(\aa \ ({ {a'}. A!a)" by (simp add: assms(1) atLeast0LessThan insert_absorb) also have "\ =(\a \ { \ (\a \ { \ (n-1)*(n-2) + (n-1)" using sum_bounded_above[of "{.. = (n-1)*(n-1)" by (metis Suc_diff_Suc Suc_eq_plus1 add.commute diff_is_0_eq' linorder_not_le mult_Suc_right mult_cancel_left nat_1_add_1) finally show ?thesis . qed definition "match A a = P\<^sub>a ! a ! (A ! a)" lemma match_less_n: "\ wf A; a < n \ \ match A a < n" by (metis P\<^sub>a_set atLeastLessThan_iff match_def nth_mem subset_eq) lemma match_upd_neq: "\ wf A; a < n; a \ a' \ \ match (A[a := b]) a' = match A a'" by (simp add: match_def) definition blocks :: "nat list \ nat \ nat \ bool" where "blocks A a a' = (P\<^sub>a ! a \ match A a' < match A a \ P\<^sub>b ! match A a' \ a < a')" definition stable :: "nat list \ nat set \ bool" where "stable A M = (\(\a\M. \a'\M. a \ a' \ blocks A a a'))" text \The set of Bs that an A would prefer to its current match, i.e. all Bs above its current match \A!a\.\ abbreviation preferred where "preferred A a == nth (P\<^sub>a!a) ` { inj_on (match A) M)" text \If \a'\ is unmatched and final then all other \a\ are matched:\ lemma final_last: assumes M: "M \ { match A ` M" and a: "a < n \ a \ M" and final: "A ! a + 1 = n" shows "insert a M = {a ! a) ` {a_set a map_nth set_map set_upt) hence "inj_on ((!) (P\<^sub>a ! a)) {a ! a)) {a_set a final by (simp add: card_image) have 2: "card ?B \ card M" by(rule surj_card_le[OF subset_eq_atLeast0_lessThan_finite[OF M] pref_match']) have 3: "card M < n" using M a by (metis atLeast0LessThan card_seteq order.refl finite_atLeastLessThan le_neq_implies_less lessThan_iff subset_eq_atLeast0_lessThan_card) have "Suc (card M) = n" using 1 2 3 by simp thus ?thesis using M a by (simp add: card_subset_eq finite_subset) qed lemma more_choices: assumes A: "matching A M" and M: "M \ { { match A ` M" and "a < n" and matched: "match A a \ match A ` M" shows "A ! a + 1 < n" proof (rule ccontr) have match: "match A ` M \ {a_set unfolding matching_def by (smt (verit, best) atLeastLessThan_iff match_def image_subsetI in_mono nth_mem) have "card M < n" using M by (metis card_atLeastLessThan card_seteq diff_zero finite_atLeastLessThan not_less) assume "\ A ! a + 1 < n" hence "A ! a + 1 = n" using A \a < n\ unfolding matching_def by (metis add.commute wf_less_n linorder_neqE_nat not_less_eq plus_1_eq_Suc) hence *: "nth (P\<^sub>a ! a) ` { match A ` M" using pref_match' matched less_Suc_eq match_def by fastforce have "nth (P\<^sub>a!a) ` {a < n\ map_nth P\<^sub>a_set set_map set_upt) hence "match A ` M = {card M < n\ unfolding matching_def by (metis atLeast0LessThan card_image card_lessThan nat_neq_iff) qed corollary more_choices_matched: assumes "matching A M" "M \ { { match A ` M" and "a \ M" shows "A ! a + 1 < n" using more_choices[OF assms(1-4)] \a \ M\ \M \ { atLeastLessThan_iff by blast lemma atmost1_final: assumes M: "M \ {a match A ` M" shows "\\<^sub>\\<^sub>1 a. a < n \ a \ M \ A ! a + 1 = n" apply rule subgoal for x y using final_last[OF M inj, of x] final_last[OF M inj, of y] assms(3) by blast done lemma sumA_UB: assumes "matching A M" "M \ { {a match A ` M" shows "(\a (n-1)^2" proof - have M: "\a\M. A!a + 1 < n" using more_choices_matched[OF assms(1-3)] assms(4) \M \ { atLeastLessThan_iff by blast note Ainj = conj12[OF assms(1)[unfolded matching_def]] show ?thesis proof (cases "\a' M \ A!a' + 1 = n") case True then obtain a' where a': "a' M" "A!a' + 1 = n" using \M \ { \M \ { by blast hence "\a a' \ A!a \ n-2" using Uniq_D[OF atmost1_final[OF assms(2) Ainj(2) assms(4)], of a'] M wf_le_n1[OF Ainj(1)] by (metis Suc_1 Suc_eq_plus1 add_diff_cancel_right' add_le_imp_le_diff diff_diff_left less_eq_Suc_le order_less_le) from sumA_ub2[OF a'(1) _ this] a'(3) show ?thesis unfolding power2_eq_square by linarith next case False hence "\a' M \ A ! a' + 1 < n" by (metis Suc_eq_plus1 Suc_lessI wf_less_n[OF Ainj(1)]) with M have "\aa n*(n-2)" using sum_bounded_above[of "{.. \ (n-1)*(n-1)" by(simp add: algebra_simps) finally show ?thesis unfolding power2_eq_square . qed qed lemma var_ub: assumes "matching A M" "M \ { {a match A ` M" shows "(\a { n^2 + 1 - 2*n" using sumA_UB[OF assms(1-4)] by (simp add: power2_eq_square algebra_simps) have 4: "2*n \ Suc (n^2)" using le_square[of n] unfolding power2_eq_square by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc) show "(\a { {a match A ` M" "a \ M" shows "var A (M \ {a}) < var A M" proof - have 2: "M \ { n^2 + 1 - 2*n" using sumA_UB[OF assms(1-4)] by (simp add: power2_eq_square algebra_simps) have 5: "2*n \ Suc (n^2)" using le_square[of n] unfolding power2_eq_square by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_SucI mult_2 mult_le_mono1 not_less_eq_eq plus_1_eq_Suc) have 6: "(\aa \ M\ finite_subset[OF assms(2)] by(simp) qed lemma var_next: assumes"matching A M" "M \ { {a match A ` M" "a < n" shows "var (A[a := A ! a + 1]) M < var A M" proof - have "var (A[a := A ! a + 1]) M = n*n - n + 1 - (1 + (A ! a + sum ((!) A) ({ = n^2 - n + 1 - (1 + (\a < n^2 - n + 1 - ((\aThe following two predicates express the same property: if \a\ prefers \b\ over \a\'s current match, then \b\ is matched with an \a'\ that \b\ prefers to \a\.\ definition pref_match where "pref_match A M = (\aba!a \ b < match A a \ (\a'\M. b = match A a' \ P\<^sub>b ! b \ a' < a))" definition pref_match' where "pref_match' A M = (\ab \ preferred A a. \a'\M. b = match A a' \ P\<^sub>b ! b \ a' < a)" lemma pref_match'_iff: "wf A \ pref_match' A M = pref_match A M" apply (auto simp add: pref_match'_def pref_match_def imp_ex prefers_def match_def) apply (smt (verit) P\<^sub>a_set atLeast0LessThan order.strict_trans index_first lessThan_iff linorder_neqE_nat nth_index) by (smt (verit, best) P\<^sub>a_set atLeast0LessThan card_atLeastLessThan card_distinct diff_zero in_mono index_nth_id lessThan_iff less_trans nth_mem) definition opti\<^sub>a where "opti\<^sub>a A = (\A'. matching A' { stable A' { (\aa ! a \ match A' a < match A a))" definition pessi\<^sub>b where "pessi\<^sub>b A = (\A'. matching A' { stable A' { (\aa' P\<^sub>b ! match A a \ a < a'))" lemma opti\<^sub>a_pessi\<^sub>b: assumes "opti\<^sub>a A" shows "pessi\<^sub>b A" unfolding pessi\<^sub>b_def proof (safe, goal_cases) case (1 A' a a') have "\ P\<^sub>a!a \ match A a < match A' a" using 1 by (metis atLeast0LessThan blocks_def lessThan_iff prefers_asym stable_def) with 1 \opti\<^sub>a A\ show ?case using P\<^sub>a_set match_less_n opti\<^sub>a_def prefers_def unfolding matching_def by (metis (no_types) atLeast0LessThan inj_on_contraD lessThan_iff less_not_refl linorder_neqE_nat nth_index) qed lemma opti\<^sub>a_inv: assumes A: "wf A" and a: "a < n" and a': "a' < n" and same_match: "match A a' = match A a" and pref: "P\<^sub>b ! match A a' \ a' < a" and "opti\<^sub>a A" shows "opti\<^sub>a (A[a := A ! a + 1])" proof (unfold opti\<^sub>a_def matching_def, rule notI, elim exE conjE) note opti\<^sub>a = \opti\<^sub>a A\[unfolded opti\<^sub>a_def matching_def] let ?A = "A[a := A ! a + 1]" fix A' a'' assume "a'' < n" and A': "length A' = n" "set A' \ {a ! a'' \ match A' a'' < match ?A a''" show False proof cases assume [simp]: "a'' = a" have "A!a < n" using A a by(simp add: subset_eq) with A A' a pref_a'' have "P\<^sub>a ! a \ match A' a < match A a \ match A' a = match A a" apply(auto simp: prefers_def match_def) by (smt (verit) P\<^sub>a_set wf_less_n card_atLeastLessThan card_distinct diff_zero index_nth_id not_less_eq not_less_less_Suc_eq) thus False proof assume "P\<^sub>a ! a \ match A' a < match A a " thus False using opti\<^sub>a A' \a < n\ by(fastforce) next assume "match A' a = match A a" have "a \ a'" using pref a' by(auto simp: prefers_def) hence "blocks A' a' a" using opti\<^sub>a pref A' same_match \match A' a = match A a\ a a' unfolding blocks_def by (metis P\<^sub>a_set atLeast0LessThan match_less_n inj_onD lessThan_iff linorder_neqE_nat nth_index prefers_def) thus False using a a' \a \ a'\ A'(3) by (metis stable_def atLeastLessThan_iff zero_le) qed next assume "a'' \ a" thus False using opti\<^sub>a A' pref_a'' \a'' < n\ by(metis match_def nth_list_update_neq) qed qed lemma pref_match_stable: "\ matching A { \ stable A { M \ { pref_match A M \ opti\<^sub>a A)" lemma invAM_match: "\ invAM A M; a < n \ a \ M; match A a \ match A ` M \ \ invAM A (M \ {a})" by(simp add: pref_match_def) lemma invAM_swap: assumes "invAM A M" assumes a: "a < n \ a \ M" and a': "a' \ M \ match A a' = match A a" and pref: "P\<^sub>b ! match A a' \ a < a'" shows "invAM (A[a' := A!a'+1]) (M - {a'} \ {a})" proof - have A: "wf A" and M : "M \ {a A" by(insert \invAM A M\) (auto) have "M \ { a'" using a' a M by auto have pref_match': "pref_match' A M" using pref_match pref_match'_iff[OF A] by blast let ?A = "A[a' := A!a'+1]" let ?M = "M - {a'} \ {a}" have neq_a': "\x. x \ ?M \ a' \ x" using \a \ a'\ by blast have \set ?A \ { apply(rule set_update_subsetI[OF A[THEN conjunct2]]) using more_choices[OF _ M \M \ {] A inj pref_match' a' subsetD[OF M, of a'] by(fastforce simp: pref_match'_def) hence "wf ?A" using A by(simp) moreover have "inj_on (match ?A) ?M" using a a' inj by(simp add: match_def inj_on_def)(metis Diff_iff insert_iff nth_list_update_neq) moreover have "pref_match' ?A ?M" using a a' pref_match' A pref \a' < n\ apply(simp add: pref_match'_def match_upd_neq neq_a' Ball_def Bex_def image_iff imp_ex nth_list_update less_Suc_eq flip: match_def) by (metis prefers_trans) moreover have "opti\<^sub>a ?A" using opti\<^sub>a_inv[OF A \a' < n\ _ _ _ \opti\<^sub>a A\] a a'[THEN conjunct2] pref by auto ultimately show ?thesis using a a' M pref_match'_iff by auto qed lemma invAM_next: assumes "invAM A M" assumes a: "a < n \ a \ M" and a': "a' \ M \ match A a' = match A a" and pref: "\ P\<^sub>b ! match A a' \ a < a'" shows "invAM (A[a := A!a + 1]) M" proof - have A: "wf A" and M : "M \ {a: "opti\<^sub>a A" and "a' < n" by(insert \invAM A M\ a') (auto) hence pref': "P\<^sub>b ! match A a' \ a' < a" using pref a a' P\<^sub>b_set unfolding prefers_def by (metis match_def match_less_n index_eq_index_conv linorder_less_linear subsetD) have "M \ {x. x\ M \ a \ x" using a by blast have pref_match': "pref_match' A M" using pref_match pref_match'_iff[OF A,of M] by blast hence "\a match A ` M" unfolding pref_match'_def by blast hence "A!a + 1 < n" using more_choices[OF _ M \M \ {] A inj a a' unfolding matching_def by (metis (no_types, lifting) imageI) let ?A = "A[a := A!a+1]" have "wf ?A" using A \A!a + 1 < n\ by(simp add: set_update_subsetI) moreover have "inj_on (match ?A) M" using a inj by(simp add: match_def inj_on_def) (metis nth_list_update_neq) moreover have "pref_match' ?A M" using a pref_match' pref' A a' neq_a by(auto simp: match_upd_neq pref_match'_def Ball_def Bex_def image_iff nth_list_update imp_ex less_Suc_eq simp flip: match_def) moreover have "opti\<^sub>a ?A" using opti\<^sub>a_inv[OF A conjunct1[OF a] \a' < n\ conjunct2[OF a'] pref' opti\<^sub>a] . ultimately show ?thesis using M by (simp add: pref_match'_iff) qed subsection \Algorithm 1\ lemma Gale_Shapley1: "VARS M A a a' [M = {} \ A = replicate n 0] WHILE M \ { a \ M); IF match A a \ match A ` M THEN M := M \ {a} ELSE a' := (SOME a'. a' \ M \ match A a' = match A a); IF P\<^sub>b ! match A a' \ a < a' THEN A[a'] := A!a'+1; M := M - {a'} \ {a} ELSE A[a] := A!a+1 FI FI OD [matching A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def) next case 3 thus ?case using pref_match_stable by auto next case (2 v M A a) hence invAM: "invAM A M" and m: "matching A M" and M: "M \ { {a A" and v: "var A M = v" by auto note Ainj = conj12[OF m[unfolded matching_def]] note pref_match' = pref_match[THEN pref_match'_iff[OF Ainj(1), THEN iffD2]] hence pref_match1: "\a match A ` M" unfolding pref_match'_def by blast define a where "a = (SOME a. a < n \ a \ M)" have a: "a < n \ a \ M" unfolding a_def using M by (metis (no_types, lifting) atLeastLessThan_iff someI_ex subsetI subset_antisym) show ?case (is "?P((SOME a. a < n \ a \ M))") unfolding a_def[symmetric] proof - show "?P a" (is "(?not_matched \ ?THEN) \ (\ ?not_matched \ ?ELSE)") proof (rule; rule) assume ?not_matched show ?THEN proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case using invAM_match[OF invAM a \?not_matched\] . case 2 show ?case using var_match[OF m M pref_match1] var0_match[OF Ainj(1) M(1)] a unfolding v by blast qed next assume matched: "\ ?not_matched" define a' where "a' = (SOME a'. a' \ M \ match A a' = match A a)" have a': "a' \ M \ match A a' = match A a" unfolding a'_def using matched by (smt (verit) image_iff someI_ex) hence "a' < n" "a \ a'" using a M atLeast0LessThan by auto show ?ELSE (is "?P((SOME a'. a' \ M \ match A a' = match A a))") unfolding a'_def[symmetric] proof - show "?P a'" (is "(?pref \ ?THEN) \ (\ ?pref \ ?ELSE)") proof (rule; rule) assume ?pref show ?THEN proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case by(rule invAM_swap[OF invAM a a' \?pref\]) case 2 have "card(M - {a'} \ {a}) = card M" using a a' card.remove subset_eq_atLeast0_lessThan_finite[OF M(1)] by fastforce thus ?case using v var_next[OF m M pref_match1 \a' < n\] var0_next[OF Ainj(1) M \a' < n\] by simp qed next assume "\ ?pref" show ?ELSE proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case using invAM_next[OF invAM a a' \\ ?pref\] . case 2 show ?case using a v var_next[OF m M pref_match1, of a] var0_next[OF Ainj(1) M, of a] by simp qed qed qed qed qed qed text \Proof also works for @{const var0} instead of @{const var}.\ subsection \Algorithm 2: List of unmatched As\ abbreviation invas where "invas as == (set as \ { distinct as)" lemma Gale_Shapley2: "VARS A a a' as [as = [0.. A = replicate n 0] WHILE as \ [] INV { invAM A ({ invas as} VAR {var A ({ match A ` ({ { match A a' = match A a); IF P\<^sub>b ! match A a' \ a < a' THEN A[a'] := A!a'+1; as := a' # tl as ELSE A[a] := A!a+1 FI FI OD [matching A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def) next case 3 thus ?case using pref_match_stable by auto next case (2 v A _ a' as) let ?M = "{ {a A" and "as \ []" and v: "var A ?M = v" and as: "invas as" using 2 by auto note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast from \as \ []\ obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv) have set_as: "?M \ {a} = { a \ ?M" using as unfolding aseq by (simp) show ?case proof (simp only: aseq list.sel, goal_cases) case 1 show ?case (is "(?not_matched \ ?THEN) \ (\ ?not_matched \ ?ELSE)") proof (rule; rule) assume ?not_matched then have nm: "match A a \ match A ` ?M" unfolding aseq . show ?THEN proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case using invAM_match[OF \invAM A ?M\ a nm] as unfolding set_as by (simp add: aseq) case 2 show ?case using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan unfolding set_as v by blast qed next assume matched: "\ ?not_matched" define a' where "a' = (SOME a'. a' \ ?M \ match A a' = match A a)" have a': "a' \ ?M \ match A a' = match A a" unfolding a'_def aseq using matched by (smt (verit) image_iff someI_ex) hence "a' < n" "a \ a'" using a M atLeast0LessThan by auto show ?ELSE unfolding aseq[symmetric] a'_def[symmetric] proof (goal_cases) case 1 show ?case (is "(?pref \ ?THEN) \ (\ ?pref \ ?ELSE)") proof (rule; rule) assume ?pref show ?THEN proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) have *: "{ {a} = {invAM A ?M\ a a' \?pref\] unfolding * using a' as aseq by force case 2 have "card({a' < n\ a atLeast0LessThan by (metis Suc_eq_plus1 lessThan_iff var_def) qed next assume "\ ?pref" show ?ELSE proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case using invAM_next[OF \invAM A ?M\ a a' \\ ?pref\] as by blast case 2 show ?case using a v var_next[OF m M _ pref_match1, of a] by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) qed qed qed qed qed qed abbreviation invAB :: "nat list \ (nat \ nat option) \ nat set \ bool" where "invAB A B M == (ran B = M \ (\b a. B b = Some a \ match A a = b))" lemma invAB_swap: assumes invAB: "invAB A B M" assumes a: "a < n \ a \ M" and a': "a' \ M \ match A a' = match A a" and "inj_on B (dom B)" "B(match A a) = Some a'" shows "invAB (A[a' := A!a'+1]) (B(match A a := Some a)) (M - {a'} \ {a})" proof - have "\b x. b \ match A a \ B b = Some x \ a'\ x" using invAB a' by blast moreover have "a \ a'" using a a' by auto ultimately show ?thesis using assms by(simp add: ran_map_upd_Some match_def) qed subsection \Algorithm 3: Record matching of Bs to As\ lemma Gale_Shapley3: "VARS A B a a' as b [as = [0.. A = replicate n 0 \ B = (\_. None)] WHILE as \ [] INV { invAM A ({ invAB A B ({ invas as} VAR {var A ({b ! match A a' \ a < a' THEN B := B(b := Some a); A[a'] := A!a'+1; as := a' # tl as ELSE A[a] := A!a+1 FI FI OD [matching A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def) next case 3 thus ?case using pref_match_stable by auto next case (2 v A B _ a' as) let ?M = "{ {a A" and "as \ []" and v: "var A ?M = v" and as: "invas as" and invAB: "invAB A B ?M" using 2 by auto note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast from \as \ []\ obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv) have set_as: "?M \ {a} = { a \ ?M" using as unfolding aseq by (simp) show ?case proof (simp only: aseq list.sel, goal_cases) case 1 show ?case (is "(?not_matched \ ?THEN) \ (\ ?not_matched \ ?ELSE)") proof (rule; rule) assume ?not_matched then have nm: "match A a \ match A ` ?M" using invAB unfolding aseq ran_def apply (clarsimp simp: set_eq_iff) using not_None_eq by blast show ?THEN proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases) have invAM': "invAM A ({?not_matched\ set_as by (simp) case 1 show ?case using invAM' as invAB' unfolding set_as aseq by (metis distinct.simps(2) insert_subset list.simps(15)) case 2 show ?case using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan unfolding set_as v by blast qed next assume matched: "\ ?not_matched" then obtain a' where a'eq: "B(match A a) = Some a'" by auto have a': "a' \ ?M \ match A a' = match A a" unfolding aseq using a'eq invAB by (metis ranI aseq) hence "a' < n" "a \ a'" using a M atLeast0LessThan by auto show ?ELSE unfolding aseq[symmetric] a'eq option.sel proof (goal_cases) have inj_dom: "inj_on B (dom B)" by (metis (mono_tags) domD inj_onI invAB) case 1 show ?case (is "(?pref \ ?THEN) \ (\ ?pref \ ?ELSE)") proof (rule; rule) assume ?pref show ?THEN proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) have *: "{ {a} = {b x. b \ match A a \ B b = Some x \ a'\ x" using invAB a' by blast have invAB': "invAB (A[a' := A ! a' + 1]) (B(match A a := Some a)) ({?pref\] invAB' unfolding * using a' as aseq by simp case 2 have "card({a' < n\ a atLeast0LessThan by (metis Suc_eq_plus1 lessThan_iff var_def) qed next assume "\ ?pref" show ?ELSE proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 have "invAB (A[a := A ! a + 1]) B ?M" using invAB a by (metis match_def nth_list_update_neq ranI) thus ?case using invAM_next[OF invAM a a' \\ ?pref\] as by blast case 2 show ?case using a v var_next[OF m M _ pref_match1, of a] by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) qed qed qed qed qed qed (* begin unused: directly implement function B via lists B and M (data refinement); also done in Alg. 4 in a more principled manner *) abbreviation invAB' :: "nat list \ nat list \ bool list \ nat set \ bool" where "invAB' A B M M' == (length B = n \ length M = n \ M' = nth B ` {b. b < n \ M!b} \ (\b B!b < n \ match A (B!b) = b))" lemma Gale_Shapley4': "VARS A B M a a' as b [as = [0.. A = replicate n 0 \ B = replicate n 0 \ M = replicate n False] WHILE as \ [] INV { invAM A ({ invAB' A B M ({ invas as} VAR {var A ({ (M ! b) THEN M[b] := True; B[b] := a; as := tl as ELSE a' := B ! b; IF P\<^sub>b ! match A a' \ a < a' THEN B[b] := a; A[a'] := A!a'+1; as := a' # tl as ELSE A[a] := A!a+1 FI FI OD [wf A \ inj_on (match A) { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case by(auto simp: stable_def opti\<^sub>a_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def) next case 3 thus ?case using pref_match_stable by auto next case (2 v A B M _ a' as) let ?M = "{ {a A" and notall: "as \ []" and v: "var A ?M = v" and as: "invas as" and invAB: "invAB' A B M ?M" using 2 by auto note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast from notall obtain a as' where aseq: "as = a # as'" by (fastforce simp: neq_Nil_conv) have set_as: "?M \ {a} = { a \ ?M" using as unfolding aseq by (simp) show ?case proof (simp only: aseq list.sel, goal_cases) case 1 show ?case (is "(?not_matched \ ?THEN) \ (\ ?not_matched \ ?ELSE)") proof (rule; rule) assume ?not_matched then have nm: "match A a \ match A ` ?M" using invAB set_as unfolding aseq by force show ?THEN proof(simp only:mem_Collect_eq prod.case, rule conjI, goal_cases) have invAM': "invAM A ({?not_matched\ set_as match_less_n[OF A] a by (auto simp add: image_def nth_list_update) case 1 show ?case using invAM' invAB as invAB' unfolding set_as aseq by (metis distinct.simps(2) insert_subset list.simps(15)) case 2 show ?case using var_match[OF m M _ pref_match1, of a] a atLeast0LessThan unfolding set_as v by blast qed next assume matched: "\ ?not_matched" hence "match A a \ match A ` ({ ?M \ match A ?a = match A a" using invAB match_less_n[OF A] matched a by blast hence "?a < n" "a \ ?a" using a by auto show ?ELSE unfolding aseq option.sel proof (goal_cases) case 1 show ?case (is "(?pref \ ?THEN) \ (\ ?pref \ ?ELSE)") proof (rule; rule) assume ?pref show ?THEN proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) have *: "{ {a} = {b match A a \ M!b \ ?a \ B!b" using invAB a' by metis have invAB': "invAB' (A[?a := A ! ?a + 1]) (B[match A a := a]) M ({a \ ?a\ a' match_less_n[OF A, of a] a apply (simp add: nth_list_update) apply rule apply(auto simp add: image_def)[] apply (clarsimp simp add: match_def) apply (metis (opaque_lifting) nth_list_update_neq) done case 1 show ?case using invAM_swap[OF invAM a a' \?pref\] invAB' unfolding * using a' as aseq by (auto) case 2 have "card({?a < n\ a atLeast0LessThan by (metis Suc_eq_plus1 lessThan_iff var_def) qed next assume "\ ?pref" show ?ELSE proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 have "invAB' (A[a := A ! a + 1]) B M ({a \ ?a\ by (metis match_def nth_list_update_neq) thus ?case using invAM_next[OF invAM a a' \\ ?pref\] as aseq by fastforce case 2 show ?case using a v var_next[OF m M _ pref_match1, of a] aseq by (metis Suc_eq_plus1 atLeast0LessThan lessThan_iff) qed qed qed qed qed qed (* end unused *) subsection \Algorithm 4: remove list of unmatched As\ lemma Gale_Shapley4: "VARS A B ai a a' [ai = 0 \ A = replicate n 0 \ B = (\_. None)] WHILE ai < n INV { invAM A { invAB A B { ai \ n } VAR {z = n - ai} DO a := ai; WHILE B (match A a) \ None INV { invAM A ({ invAB A B ({ (a \ ai \ ai < n) \ z = n-ai } VAR {var A {b ! match A a' \ a < a' THEN B := B(match A a := Some a); A[a'] := A!a'+1; a := a' ELSE A[a] := A!a+1 FI OD; B := B(match A a := Some a); ai := ai+1 OD [matching A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case (* outer invar holds initially *) by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def)[] next case 2 (* outer invar and b ibplies inner invar *) thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff) next case (4 z A B ai a) (* inner invar' and not b ibplies outer invar *) note inv = 4[THEN conjunct1] note invAM = inv[THEN conjunct1] note aai = inv[THEN conjunct2,THEN conjunct2] show ?case proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 have *: "{ match A a \ match A ` ({ match A ` ({ { None" and "a \ ai" and v: "var A ?M = v" and as: "a \ ai \ ai < n" and invAB: "invAB A B ?M" using 3 by auto note invar = 3[THEN conjunct1,THEN conjunct1] note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast from matched obtain a' where a'eq: "B(match A a) = Some a'" by auto have a': "a' \ ?M \ match A a' = match A a" using a'eq invAB by (metis ranI) have a: "a < n \ a \ ?M" using invar by auto have "?M \ {a \ ai\ by simp show ?case unfolding a'eq option.sel proof (goal_cases) case 1 show ?case (is "(?unstab \ ?THEN) \ (\ ?unstab \ ?ELSE)") proof (rule; rule) assume ?unstab have *: "{ {a} = { a)) ({?unstab\] invAB' invar a' unfolding * by (simp) next case 2 show ?case using v var_next[OF m M \?M \ { pref_match1 \a' < n\] card by (metis var_def Suc_eq_plus1 psubset_eq) qed next assume "\ ?unstab" show ?ELSE proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) have *: "\b a'. B b = Some a' \ a \ a'" by (metis invAB ranI a) case 1 show ?case using invAM_next[OF invAM a a' \\ ?unstab\] invar * by (simp add: match_def) next case 2 show ?case using v var_next[OF m M \?M \ { pref_match1, of a] a card by (metis Suc_eq_plus1 var_def) qed qed qed qed definition "\ B M = (\b. if b < n \ M!b then Some(B!b) else None)" lemma \_Some[simp]: "\ B M b = Some a \ b < n \ M!b \ a = B!b" by(auto simp add: \_def) lemma \update1: "\ \ M ! b; b < length B; b < length M; n = length M \ \ ran(\ (B[b := a]) (M[b := True])) = ran(\ B M) \ {a}" by(force simp add: \_def ran_def nth_list_update) lemma \update2: "\ M!b; b < length B; b < length M; length M = n \ \ \ (B[b := a]) M = (\ B M)(b := Some a)" by(force simp add: \_def nth_list_update) abbreviation invAB2 :: "nat list \ nat list \ bool list \ nat set \ bool" where "invAB2 A B M M' == (invAB A (\ B M) M' \ (length B = n \ length M = n))" definition invar1 where [simp]: "invar1 A B M ai = (invAM A { invAB2 A B M { ai \ n)" definition invar2 where [simp]: "invar2 A B M ai a \ (invAM A ({ invAB2 A B M ({ a \ ai \ ai < n)" subsection \Algorithm 5: Data refinement of \B\\ lemma Gale_Shapley5: "VARS A B M ai a a' [ai = 0 \ A = replicate n 0 \ length B = n \ M = replicate n False] WHILE ai < n INV { invar1 A B M ai } VAR { z = n - ai} DO a := ai; WHILE M ! match A a INV { invar2 A B M ai a \ z = n-ai } VAR {var A {b ! match A a' \ a < a' THEN B[match A a] := a; A[a'] := A!a'+1; a := a' ELSE A[a] := A!a+1 FI OD; B[match A a] := a; M[match A a] := True; ai := ai+1 OD [matching A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case (* outer invar holds initially *) by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \_def cong: conj_cong) next case 2 (* outer invar and b ibplies inner invar *) thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff) next case (4 z A B M ai a) (* inner invar' and not b ibplies outer invar *) note inv = 4[THEN conjunct1, unfolded invar2_def] note invAM = inv[THEN conjunct1,THEN conjunct1] note aai = inv[THEN conjunct1, THEN conjunct2, THEN conjunct2] show ?case proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 have *: "{ match A a \ match A ` ({ match A ` ({update1 match_less_n insert_absorb nth_list_update) next case 2 thus ?case using 4 by auto qed next case 5 (* outer invar and not b ibplies post *) thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less) next case (3 z v A B M ai a) (* preservation of inner invar *) let ?M = "{ { ai \ ai < n" and invAB: "invAB2 A B M ?M" using 3 by auto note invar = 3[THEN conjunct1, THEN conjunct1, unfolded invar2_def] note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast let ?a = "B ! match A a" have a: "a < n \ a \ ?M" using invar by auto have a': "?a \ ?M \ match A ?a = match A a" using invAB match_less_n[OF A] a matched by (metis \_Some ranI) have "?M \ { {a} = { B M) (dom (\ B M))" by (metis (mono_tags) domD inj_onI invAB) have invAB': "invAB (A[B ! match A a := A ! ?a + 1]) (\ (B[match A a := a]) M) ({update2) show ?case using invAM_swap[OF invAM a a' unstab] invAB' invar a' unfolding * by (simp add: insert_absorb \update2) case 2 show ?case using v var_next[OF m M \?M \ { pref_match1 \?a < n\] card by (metis var_def Suc_eq_plus1) next case stab: 3 have *: "\b. b < n \ M!b \ a \ B!b" by (metis invAB ranI \_Some a) show ?case using invAM_next[OF invAM a a' stab] invar * by (simp add: match_def) case 4 show ?case using v var_next[OF m M \?M \ { pref_match1, of a] a card by (metis Suc_eq_plus1 var_def) qed qed qed lemma inner_to_outer: assumes inv: "invar2 A B M ai a \ b = match A a" and not_b: "\ M ! b" shows "invar1 A (B[b := a]) (M[b := True]) (ai+1)" proof - note invAM = inv[unfolded invar2_def, THEN conjunct1,THEN conjunct1] have *: "{ match A a \ match A ` ({ match A ` ({update1 insert_absorb nth_list_update) qed lemma inner_pres: assumes R: "\ba1a2 P\<^sub>b ! b \ a1 < a2" and inv: "invar2 A B M ai a" and m: "M ! b" and v: "var A { invar2 A1 (B[b:=a]) M ai a' \ var A1 { (\ r ! a < r ! a' \ invar2 A2 B M ai a \ var A2 { { B M) ?M" and mat: "matching A ?M" and pref_match: "pref_match A ?M" and as: "a \ ai \ ai < n" using inv' by auto note pref_match' = pref_match[THEN pref_match'_iff[OF A, THEN iffD2]] hence pref_match1: "\a match A ` ?M" unfolding pref_match'_def by blast let ?a = "B ! match A a" have a: "a < n \ a \ ?M" using inv by auto have a': "?a \ ?M \ match A ?a = match A a" using invAB match_less_n[OF A] a m inv by (metis \_Some ranI \b = _\) have "?M \ { {a} = {b ! match A a' \ a < a'" using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b R by (simp) have inj_dom: "inj_on (\ B M) (dom (\ B M))" by (metis (mono_tags) domD inj_onI invAB) have invAB': "invAB A1 (\ (B[match A a := a]) M) ({update2 inv') show ?case using invAM_swap[OF invAM a a'] unstab invAB' inv a' unfolding * by (simp add: insert_absorb \update2) next case 2 show ?case using v var_next[OF mat M \?M \ { pref_match1 \?a < n\] card assms(5,9) by (metis Suc_eq_plus1 var_def) next have *: "\b. b < n \ M!b \ a \ B!b" by (metis invAB ranI \_Some a) case 3 hence unstab: "\ P\<^sub>b ! match A a' \ a < a'" using R a a' as P\<^sub>b_set P\<^sub>a_set match_less_n[OF A] n_def length_P\<^sub>b by (simp add: ranking_iff_pref) then show ?case using invAM_next[OF invAM a a'] 3 inv * by (simp add: match_def) next case 4 show ?case using v var_next[OF mat M \?M \ { pref_match1, of a] a card assms(6) by (metis Suc_eq_plus1 var_def) qed qed subsection \Algorithm 6: replace \P\<^sub>b\ by ranking \R\\ lemma Gale_Shapley6: assumes "R = map ranking P\<^sub>b" shows "VARS A B M ai a a' b r [ai = 0 \ A = replicate n 0 \ length B = n \ M = replicate n False] WHILE ai < n INV { invar1 A B M ai } VAR {z = n - ai} DO a := ai; b := match A a; WHILE M ! b INV { invar2 A B M ai a \ b = match A a \ z = n-ai } VAR {var A { stable A { opti\<^sub>a A]" proof (vcg_tc, goal_cases) case 1 thus ?case (* outer invar holds initially *) by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \_def cong: conj_cong) next case 2 (* outer invar and b ibplies inner invar *) thus ?case by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff) next case 3 (* preservation of inner invar *) have R: "\ba1a2 P\<^sub>b ! b \ a1 < a2" by (simp add: P\<^sub>b_set \R = _\ length_P\<^sub>b ranking_iff_pref) show ?case proof (simp only: mem_Collect_eq prod.case, goal_cases) case 1 show ?case using inner_pres[OF R _ _ refl refl refl] 3 by blast qed next case 4 (* inner invar' and not b ibplies outer invar *) show ?case proof (simp only: mem_Collect_eq prod.case, rule conjI, goal_cases) case 1 show ?case using 4 inner_to_outer by blast next case 2 thus ?case using 4 by auto qed next case 5 (* outer invar and not b ibplies post *) thus ?case using pref_match_stable unfolding invAM_def invar1_def by(metis le_neq_implies_less) qed end subsection \Functional implementation\ definition "gs_inner P\<^sub>a R M = while (\(A,B,a,b). M!b) (\(A,B,a,b). let a' = B ! b; r = R ! (P\<^sub>a ! a' ! (A ! a')) in let (A, B, a) = if r ! a < r ! a' then (A[a' := A!a' + 1], B[b := a], a') else (A[a := A!a + 1], B, a) in (A, B, a, P\<^sub>a ! a ! (A ! a)))" definition "gs n P\<^sub>a R = while (\(A,B,M,ai). ai < n) (\(A,B,M,ai). let (A,B,a,b) = gs_inner P\<^sub>a R M (A, B, ai, P\<^sub>a ! ai ! (A ! ai)) in (A, B[b:=a], M[b:=True], ai+1)) (replicate n 0, replicate n 0, replicate n False,0)" context Pref begin lemma gs_inner: assumes "R = map ranking P\<^sub>b" assumes "invar2 A B M ai a" "b = match A a" shows "gs_inner P\<^sub>a R M (A, B, a, b) = (A',B',a',b') \ invar1 A' (B'[b' := a']) (M[b' := True]) (ai+1)" unfolding gs_inner_def proof(rule while_rule2[where P = "\(A,B,a,b). invar2 A B M ai a \ b = match A a" and r = "measure (%(A, B, a, b). Pref.var P\<^sub>a A {ba1a2 P\<^sub>b ! b \ a1 < a2" by (simp add: P\<^sub>b_set \R = _\ length_P\<^sub>b ranking_iff_pref) show ?case proof(rule, goal_cases) case 1 show ?case using inv apply(simp only: s prod.case Let_def split: if_split) using inner_pres[OF R _ _ refl refl refl refl refl, of A B M ai a b] unfolding invar2_def match_def by presburger case 2 show ?case using inv apply(simp only: s prod.case Let_def in_measure split: if_split) using inner_pres[OF R _ _ refl refl refl refl refl, of A B M ai a b] unfolding invar2_def match_def by presburger qed next case 3 show ?case proof (rule, goal_cases) case 1 show ?case by(rule inner_to_outer[OF 3[unfolded 1 prod.case]]) qed next case 4 show ?case by simp qed lemma gs: assumes "R = map ranking P\<^sub>b" shows "gs n P\<^sub>a R = (A,BMai) \ matching A { stable A { opti\<^sub>a A" unfolding gs_def proof(rule while_rule2[where P = "\(A,B,M,ai). invar1 A B M ai" and r = "measure(\(A,B,M,ai). n - ai)"], goal_cases) case 1 show ?case by(auto simp: stable_def pref_match_def P\<^sub>a_set card_distinct match_def index_nth_id prefers_def opti\<^sub>a_def \_def cong: conj_cong) next case (2 s) obtain A B M ai where s: "s = (A, B, M, ai)" using prod_cases4 by blast have 1: "invar2 A B M ai ai" using 2 s by (auto simp: atLeastLessThanSuc_atLeastAtMost simp flip: atLeastLessThan_eq_atLeastAtMost_diff) show ?case using 2 s gs_inner[OF \R = _ \ 1] by (auto simp: match_def simp del: invar1_def split: prod.split) next case 3 thus ?case using pref_match_stable by auto next case 4 show ?case by simp qed end subsection \Executable functional Code\ definition "Gale_Shapley P\<^sub>a P\<^sub>b = (if Pref P\<^sub>a P\<^sub>b then Some (fst (gs (length P\<^sub>a) P\<^sub>a (map ranking P\<^sub>b))) else None)" theorem gs: "\ Pref P\<^sub>a P\<^sub>b; n = length P\<^sub>a \ \ \A. Gale_Shapley P\<^sub>a P\<^sub>b = Some(A) \ Pref.matching P\<^sub>a A { Pref.stable P\<^sub>a P\<^sub>b A { Pref.opti\<^sub>a P\<^sub>a P\<^sub>b A" unfolding Gale_Shapley_def using Pref.gs by (metis fst_conv surj_pair) declare Pref_def [code] text \Two examples from Gusfield and Irving:\ lemma "Gale_Shapley [[3,0,1,2], [1,2,0,3], [1,3,2,0], [2,0,3,1]] [[3,0,2,1], [0,2,1,3], [0,1,2,3], [3,0,2,1]] = Some[0,1,0,1]" by eval lemma "Gale_Shapley [[4,6,0,1,5,7,3,2], [1,2,6,4,3,0,7,5], [7,4,0,3,5,1,2,6], [2,1,6,3,0,5,7,4], [6,1,4,0,2,5,7,3], [0,5,6,4,7,3,1,2], [1,4,6,5,2,3,7,0], [2,7,3,4,6,1,5,0]] [[4,2,6,5,0,1,7,3], [7,5,2,4,6,1,0,3], [0,4,5,1,3,7,6,2], [7,6,2,1,3,0,4,5], [5,3,6,2,7,0,1,4], [1,7,4,2,3,5,6,0], [6,4,1,0,7,5,3,2], [6,3,0,4,1,2,5,7]] = Some [0, 1, 0, 5, 0, 0, 0, 2]" by eval end \ No newline at end of file