(* File: PAPP_Impossibility_Base_Case.thy Author: Manuel Eberl, University of Innsbruck *) section ‹The Base Case of the Impossibility› theory PAPP_Impossibility_Base_Case imports Anonymous_PAPP SAT_Replay begin text ‹ In this section, we will prove the base case of our P-APP impossibility result, namely that there exists no anonymous P-APP rule ‹f› for 6 voters, 4 parties, and committee size 3 that satisfies Weak Representation and Cardinality Strategyproofness. The proof works by looking at some (comparatively small) set of preference profiles and the set of all 20 possible output committees. Each proposition $f(A) = C$ (where ‹A› is a profile from our set and ‹C› is one of the 20 possible output committees) is considered as a Boolean variable. All the conditions arising on these variables based on the fact that ‹f› is a function and the additional properties (Representation, Strategyproofness) are encoded as SAT clauses. This SAT problem is then proven unsatisfiable by an external SAT solver and the resulting proof re-imported into Isabelle/HOL. › subsection ‹Auxiliary Material› text ‹ We define the set of committees of the given size ‹k› for a given set of parties ‹P›. › definition committees :: "nat ⇒ 'a set ⇒ 'a multiset set" where "committees k P = {W. set_mset W ⊆ P ∧ size W = k}" text ‹ We now prove a recurrence for this set so that we can more easily compute the set of all possible committees: › lemma committees_0 [simp]: "committees 0 P = {{#}}" by (auto simp: committees_def) lemma committees_Suc: "committees (Suc n) P = (⋃x∈P. ⋃W∈committees n P. {{#x#} + W})" proof safe fix C assume C: "C ∈ committees (Suc n) P" hence "size C = Suc n" by (auto simp: committees_def) hence "C ≠ {#}" by auto then obtain x where x: "x ∈# C" by auto define C' where "C' = C - {#x#}" have "C = {#x#} + C'" "x ∈ P" "C' ∈ committees n P" using C x by (auto simp: committees_def C'_def size_Diff_singleton dest: in_diffD) thus "C ∈ (⋃x∈P. ⋃W∈committees n P. {{#x#} + W})" by blast qed (auto simp: committees_def) text ‹ The following function takes a list $[a_1, \ldots, a_n]$ and computes the list of all pairs of the form $(a_i, a_j)$ with $i < j$: › fun pairs :: "'a list ⇒ ('a × 'a) list" where "pairs [] = []" | "pairs (x # xs) = map (λy. (x, y)) xs @ pairs xs" lemma distinct_conv_pairs: "distinct xs ⟷ list_all (λ(x,y). x ≠ y) (pairs xs)" by (induction xs) (auto simp: list_all_iff) lemma list_ex_unfold: "list_ex P (x # y # xs) ⟷ P x ∨ list_ex P (y # xs)" "list_ex P [x] ⟷ P x" by simp_all lemma list_all_unfold: "list_all P (x # y # xs) ⟷ P x ∧ list_all P (y # xs)" "list_all P [x] ⟷ P x" by simp_all subsection ‹Setup for the Base Case› text ‹ We define a locale for an anonymous P-APP rule for 6 voters, 4 parties, and committee size 3 that satisfies weak representation and cardinality strategyproofness. Our goal is to prove the theorem \<^term>‹False› inside this locale. › locale papp_impossibility_base_case = card_stratproof_weak_rep_anon_papp 6 parties 3 r for parties :: "'a set" and r + assumes card_parties: "card parties = 4" begin text ‹ A slightly more convenient version of Weak Representation: › lemma weak_representation': assumes "is_pref_profile A" "A' ≡ A" "∀z∈Z. count A {z} ≥ 2" "¬Z ⊆ set_mset W" shows "r A' ≠ W" using weak_representation[OF assms(1)] assms(2-4) by auto text ‹ The following lemma (Lemma~2 in the appendix of the paper) is a strengthening of Weak Representation and Strategyproofness in our concrete setting: Let ‹A› be a preference profile containing approval lists ‹X› and let ‹Z› be a set of parties such that each element of ‹Z› is uniquely approved by at least two voters in ‹A›. Due to Weak Representation, at least ‹|X ∩ Z|› members of the committee are then approved by ‹X›. What the lemma now says is that if there exists another voter with approval list ‹Y ⊆ X› and $Y \nsubseteq Z$, then there is an additional committee member that is approved by ‹X›. This lemma will be used both in our symmetry-breaking argument and as a means to add more clauses to the SAT instance. Since these clauses are logical consequences of Strategyproofness and Weak Representation, they are technically redundant -- but their presence allows us to use consider a smaller set of profiles and still get a contradiction. Without using the lemma, we would need to feed more profiles to the SAT solver to obtain the same information. › lemma lemma2: assumes A: "is_pref_profile A" assumes "X ∈# A" and "Y ∈# A - {#X#}" and "Y ⊆ X" and "¬Y ⊆ Z" assumes Z: "∀z∈Z. count A {z} ≥ 2" shows "size (filter_mset (λx. x ∈ X) (r A)) > card (X ∩ Z)" proof (rule ccontr) text ‹ For the sake of contradiction, suppose the number of elements approved by ‹X› were no larger than ‹|X ∩ Z|›. › assume "¬size (filter_mset (λx. x ∈ X) (r A)) > card (X ∩ Z)" hence le: "size (filter_mset (λx. x ∈ X) (r A)) ≤ card (X ∩ Z)" by linarith interpret anon_papp_profile 6 parties 3 A by fact have "Z ⊆ parties" using assms(1,6) by (meson is_committee_def order.trans rule_wf weak_representation') have [simp]: "finite Z" by (rule finite_subset[OF _ finite_parties]) fact text ‹ Due to Weak Representation, each member of ‹X ∩ Z› must be chosen at least once. But due to the above, it cannot be chosen more than once. So it has to be chosen exactly once. › have X_approved_A_eq: "filter_mset (λx. x ∈ X) (r A) = mset_set (X ∩ Z)" proof - have "mset_set Z ⊆# r A" using Z weak_representation[OF A] by (subst mset_set_subset_iff) auto hence "size (filter_mset (λx. x ∈ X) (mset_set Z)) ≤ size (filter_mset (λx. x ∈ X) (r A))" by (intro size_mset_mono multiset_filter_mono) also have "filter_mset (λx. x ∈ X) (mset_set Z) = mset_set {x∈Z. x ∈ X}" by simp also have "{x∈Z. x ∈ X} = X ∩ Z" by auto also have "size (mset_set (X ∩ Z)) = card (X ∩ Z)" by simp finally have "size (filter_mset (λx. x ∈ X) (r A)) = card (X ∩ Z)" using le by linarith moreover have "mset_set (X ∩ Z) ⊆# filter_mset (λx. x ∈ X) (r A)" using Z weak_representation[OF A] by (subst mset_set_subset_iff) auto ultimately show "filter_mset (λx. x ∈ X) (r A) = mset_set (X ∩ Z)" by (intro mset_subset_size_ge_imp_eq [symmetric]) auto qed have count_eq_1: "count (r A) x = 1" if "x ∈ X ∩ Z" for x using that X_approved_A_eq by (metis ‹finite Z› count_filter_mset count_mset_set' diff_is_0_eq diff_zero finite_subset inf_le2 not_one_le_zero) text ‹ Let ‹x› be some element of ‹Y› that is not in ‹Z›. › obtain x where x: "x ∈ Y - Z" using ‹¬Y ⊆ Z› by blast with assms have x': "x ∈ X - Z" by auto have [simp]: "x ∈ parties" using A_subset assms(2) x' by blast text ‹ Let ‹A'› be the preference profile obtained by having voter ‹X› lying and pretending she only approves ‹x›. › define A' where "A' = A - {#X#} + {#{x}#}" have A': "is_pref_profile A'" using is_pref_profile_replace[OF A ‹X ∈# A›, of "{x}"] by (auto simp: A'_def) text ‹ We now show that even with this manipulated profile, the committee members approved by ‹X› are exactly the same as before: › have X_approved_A'_eq: "filter_mset (λx. x ∈ X) (r A') = mset_set (X ∩ Z)" proof - text ‹ Every element of ‹Z› must still be in the result committee due to Weak Representation. › have "mset_set Z ⊆# r A'" proof (subst mset_set_subset_iff) show "Z ⊆ set_mset (r A')" proof fix z assume z: "z ∈ Z" from x' z have [simp]: "x ≠ z" by auto have [simp]: "X ≠ {z}" using x' by auto show "z ∈# r A'" using Z weak_representation[OF A', of z] z x x' by (auto simp: A'_def) qed qed auto text ‹ Thus the parties in ‹X ∩ Z› must be in the committee (and they are approved by ‹X›). › have "mset_set (X ∩ Z) ⊆# filter_mset (λx. x ∈ X) (r A')" proof - have "filter_mset (λx. x ∈ X) (mset_set Z) ⊆# filter_mset (λx. x ∈ X) (r A')" using ‹mset_set Z ⊆# r A'› by (intro multiset_filter_mono) auto also have "filter_mset (λx. x ∈ X) (mset_set Z) = mset_set (X ∩ Z)" by auto finally show "mset_set (X ∩ Z) ⊆# filter_mset (λx. x ∈ X) (r A')" . qed text ‹ Due to Strategyproofness, no additional committee members can be approved by ‹X›, so indeed only ‹X ∩ Z› is approved by ‹X›, and they each occur only once. › moreover have "¬card_manipulable A X {x}" using not_manipulable by blast hence "size (mset_set (X ∩ Z)) ≥ size (filter_mset (λx. x ∈ X) (r A'))" using assms by (simp add: card_manipulable_def A'_def strong_committee_preference_iff not_less X_approved_A_eq) ultimately show "filter_mset (λx. x ∈ X) (r A') = mset_set (X ∩ Z)" by (metis mset_subset_size_ge_imp_eq) qed text ‹ Next, we show that the set of committee members approved by ‹Y› in the committee returned for the manipulated profile is exactly ‹Y ∩ Z› (and again, each party only occurs once). › have Y_approved_A'_eq: "filter_mset (λx. x ∈ Y) (r A') = mset_set (Y ∩ Z)" proof - have "filter_mset (λx. x ∈ Y) (filter_mset (λx. x ∈ X) (r A')) = filter_mset (λx. x ∈ Y) (mset_set (X ∩ Z))" by (simp only: X_approved_A'_eq) also have "filter_mset (λx. x ∈ Y) (filter_mset (λx. x ∈ X) (r A')) = filter_mset (λx. x ∈ Y ∧ x ∈ X) (r A')" by (simp add: filter_filter_mset conj_commute) also have "(λx. x ∈ Y ∧ x ∈ X) = (λx. x ∈ Y)" using assms by auto also have "filter_mset (λx. x ∈ Y) (mset_set (X ∩ Z)) = mset_set (Y ∩ Z)" using assms by auto finally show ?thesis . qed text ‹ Next, define the profile ‹A''› obtained from ‹A'› by also having ‹Y› pretend to approve only ‹x›. › define A'' where "A'' = A' - {#Y#} + {#{x}#}" have "Y ∈# A'" using assms by (auto simp: A'_def) hence A'': "is_pref_profile A''" using is_pref_profile_replace[OF A', of Y "{x}"] by (auto simp: A''_def) text ‹ Again, the elements of ‹Z› must be chosen due to Weak Representation. › have "Z ⊆ set_mset (r A'')" proof fix z assume z: "z ∈ Z" from x' z have [simp]: "x ≠ z" by auto have [simp]: "X ≠ {z}" "Y ≠ {z}" using x x' by auto show "z ∈# r A''" using Z weak_representation[OF A'', of z] z x x' by (auto simp: A''_def A'_def) qed text ‹ But now additionally, ‹x› must be chosen, since both ‹X› and ‹Y› uniquely approve it. › moreover have "x ∈# r A''" using x x' ‹Y ∈# A - {#X#}› by (intro weak_representation A'') (auto simp: A''_def A'_def) ultimately have "insert x (Y ∩ Z) ⊆ set_mset (r A'') ∩ Y" using x by blast text ‹ Now we have a contradiction due to Strategyproofness, since ‹Y› can force the additional member ‹x› into the committee by lying. › hence "mset_set (insert x (Y ∩ Z)) ⊆# filter_mset (λw. w ∈ Y) (r A'')" by (subst mset_set_subset_iff) auto hence "size (mset_set (insert x (Y ∩ Z))) ≤ size (filter_mset (λw. w ∈ Y) (r A''))" by (rule size_mset_mono) hence "size (filter_mset (λx. x ∈ Y) (r A'')) > size (filter_mset (λx. x ∈ Y) (r A'))" using x by (simp add: Y_approved_A'_eq) hence "card_manipulable A' Y {x}" using A' x ‹Y ∈# A'› unfolding card_manipulable_def strong_committee_preference_iff A''_def by auto thus False using not_manipulable by blast qed text ‹ The following are merely reformulation of the above lemma for technical reasons. › lemma lemma2': assumes "is_pref_profile A" assumes "∀z∈Z. count A {z} ≥ 2" assumes "X ∈# A ∧ (∃Y. Y ∈# A - {#X#} ∧ Y ⊆ X ∧ ¬Y ⊆ Z)" shows "¬filter_mset (λx. x ∈ X) (r A) ⊆# mset_set (X ∩ Z)" proof assume subset: "filter_mset (λx. x ∈ X) (r A) ⊆# mset_set (X ∩ Z)" from assms(3) obtain Y where Y: "X ∈# A" "Y ∈# A - {#X#}" "Y ⊆ X" "¬Y ⊆ Z" by blast have "card (X ∩ Z) < size {#x ∈# r A. x ∈ X#}" by (rule lemma2[where Y = Y]) (use Y assms(1,2) in auto) with size_mset_mono[OF subset] show False by simp qed lemma lemma2'': assumes "is_pref_profile A" assumes "A' ≡ A" assumes "∀z∈Z. count A {z} ≥ 2" assumes "X ∈# A ∧ (∃Y∈set_mset (A - {#X#}). Y ⊆ X ∧ ¬Y ⊆ Z)" assumes "filter_mset (λx. x ∈ X) W ⊆# mset_set (X ∩ Z)" shows "r A' ≠ W" using lemma2'[of A Z X] assms by auto subsection ‹Symmetry Breaking› text ‹ In the following, we formalize the symmetry-breaking argument that shows that we can reorder the four alternatives $C_1$ to $C_4$ in such a way that the preference profile \[ \{C_1\}\ \ \{C_2\}\ \ \{C_1, C_2\}\ \ \{C_3\}\ \ \{C_3\}\ \ \{C_3, C_4\} \] is mapped to one of the committees $[C_1, C_1, C_3]$ or $[C_1, C_2, C_3]$. We start with a simple technical lemma that states that if we have a multiset $A$ of size 3 consisting of the elements $x$ and $y$ and $x$ occurs at least as often as $y$, then $A = [x, x, y]$. › lemma papp_multiset_3_aux: assumes "size A = 3" "x ∈# A" "y ∈# A" "set_mset A ⊆ {x, y}" "x ≠ y" "count A x ≥ count A y" shows "A = {#x, x, y#}" proof - have "count A x > 0" using assms by force have "size A = (∑z∈set_mset A. count A z)" by (rule size_multiset_overloaded_eq) also have "set_mset A = {x, y}" using assms by auto also have "(∑z∈…. count A z) = count A x + count A y" using assms by auto finally have "count A x + count A y = 3" by (simp add: assms(1)) moreover from assms have "count A x > 0" "count A y > 0" by auto ultimately have *: "count A x = 2 ∧ count A y = 1" using ‹count A x ≥ count A y› by linarith show ?thesis proof (rule multiset_eqI) fix z show "count A z = count {#x, x, y#} z" proof (cases "z ∈ {x, y}") case False with assms have "z ∉ set_mset A" by auto hence "count A z = 0" by (simp add: Multiset.not_in_iff) thus ?thesis using False by auto qed (use * in auto) qed qed text ‹ The following is the main symmetry-breaking result. It shows that we can find parties $C_1$ to $C_4$ with the desired property. This is a somewhat ad-hoc argument; in the appendix of the paper this is done more systematically in Lemma~3. › lemma symmetry_break_aux: obtains C1 C2 C3 C4 where "parties = {C1, C2, C3, C4}" "distinct [C1, C2, C3, C4]" "r ({#{C1}, {C2}, {C1, C2}, {C3}, {C4}, {C3, C4}#}) ∈ {{#C1, C1, C3#}, {#C1, C2, C3#}}" proof - note I = that have "∃xs. set xs = parties ∧ distinct xs" using finite_distinct_list[of parties] by blast then obtain xs where xs: "set xs = parties" "distinct xs" by blast from xs have "length xs = 4" using card_parties distinct_card[of xs] by auto then obtain C1 C2 C3 C4 where xs_eq: "xs = [C1, C2, C3, C4]" by (auto simp: eval_nat_numeral length_Suc_conv) have parties_eq: "parties = {C1, C2, C3, C4}" by (subst xs(1) [symmetric], subst xs_eq) auto have [simp]: "C1 ≠ C2" "C1 ≠ C3" "C1 ≠ C4" "C2 ≠ C1" "C2 ≠ C3" "C2 ≠ C4" "C3 ≠ C1" "C3 ≠ C2" "C3 ≠ C4" "C4 ≠ C1" "C4 ≠ C2" "C4 ≠ C3" using ‹distinct xs› unfolding xs_eq by auto define A where "A = {#{C1}, {C2}, {C1, C2}, {C3}, {C4}, {C3, C4}#}" define m where "m = Max (count (r A) ` parties)" have A: "is_pref_profile A" unfolding A_def is_pref_profile_iff by (simp add: parties_eq) hence "is_committee (r A)" by (rule rule_wf) hence rA: "size (r A) = 3" "set_mset (r A) ⊆ parties" unfolding is_committee_def by auto define X where "X = set_mset (r A)" have "X ≠ {}" "X ⊆ parties" using rA by (auto simp: X_def) have "m > 0" proof - obtain x where "x ∈ X" using ‹X ≠ {}› by blast with ‹X ⊆ parties› have "C1 ∈ X ∨ C2 ∈ X ∨ C3 ∈ X ∨ C4 ∈ X" unfolding parties_eq by blast thus ?thesis unfolding m_def X_def by (subst Max_gr_iff) (auto simp: parties_eq) qed have "m ≤ 3" proof - have "m ≤ size (r A)" unfolding m_def by (subst Max_le_iff) (auto simp: count_le_size) also have "… = 3" by fact finally show ?thesis . qed have "m ∈ (count (r A) ` parties)" unfolding m_def by (intro Max_in) auto then obtain C1' where C1': "count (r A) C1' = m" "C1' ∈ parties" by blast have "C1' ∈# r A" using ‹m > 0› C1'(1) by auto have "∃C2'∈parties-{C1'}. {C1', C2'} ∈# A" using C1' unfolding A_def parties_eq by (elim insertE; simp add: insert_Diff_if insert_commute) then obtain C2' where C2': "C2' ∈ parties - {C1'}" "{C1', C2'} ∈# A" by blast have [simp]: "C1' ≠ C2'" "C2' ≠ C1'" using C2' by auto have disj: "C1' = C1 ∧ C2' = C2 ∨ C1' = C2 ∧ C2' = C1 ∨ C1' = C3 ∧ C2' = C4 ∨ C1' = C4 ∧ C2' = C3" using C1'(2) C2' unfolding A_def parties_eq by (elim insertE; force simp: insert_commute) obtain C3' where C3': "C3' ∈ parties-{C1', C2'}" using C1'(2) C2' unfolding parties_eq by (fastforce simp: insert_Diff_if) obtain C4' where C4': "C4' ∈ parties-{C1', C2', C3'}" using C1'(2) C2' C3' unfolding parties_eq by (fastforce simp: insert_Diff_if) have A_eq: "A = {#{C1'}, {C2'}, {C1', C2'}, {C3'}, {C4'}, {C3', C4'}#}" using disj C3' C4' by (elim disjE) (auto simp: A_def parties_eq insert_commute) have distinct: "C1' ≠ C2'" "C1' ≠ C3'" "C1' ≠ C4'" "C2' ≠ C1'" "C2' ≠ C3'" "C2' ≠ C4'" "C3' ≠ C1'" "C3' ≠ C2'" "C3' ≠ C4'" "C4' ≠ C1'" "C4' ≠ C2'" "C4' ≠ C3'" using C1' C2' C3' C4' by blast+ have parties_eq': "parties = {C1', C2', C3', C4'}" using C1'(2) C2'(1) C3' C4' distinct unfolding parties_eq by (elim insertE) auto have "¬{#x ∈# r A. x ∈ {C3', C4'}#} ⊆# mset_set ({C3', C4'} ∩ {})" by (rule lemma2'[OF A]) (auto simp: A_eq) hence C34': "C3' ∈# r A ∨ C4' ∈# r A" by auto then consider "C3' ∈# r A" "C4' ∈# r A" | "C3' ∈# r A" "C4' ∉# r A" | "C3' ∉# r A" "C4' ∈# r A" by blast thus ?thesis proof cases assume *: "C3' ∈# r A" "C4' ∈# r A" have "r A = {#C3', C4', C1'#}" by (rule sym, rule mset_subset_size_ge_imp_eq) (use * ‹C1' ∈# r A› distinct in ‹auto simp: ‹size (r A) = 3› Multiset.insert_subset_eq_iff in_diff_multiset_absorb2›) thus ?thesis using distinct by (intro that[of C3' C4' C1' C2']) (auto simp: parties_eq' A_eq add_mset_commute insert_commute) next assume *: "C3' ∈# r A" "C4' ∉# r A" show ?thesis proof (cases "C2' ∈# r A") case True have "r A = {#C1', C2', C3'#}" by (rule sym, rule mset_subset_size_ge_imp_eq) (use * ‹C1' ∈# r A› distinct True in ‹auto simp: ‹size (r A) = 3› Multiset.insert_subset_eq_iff in_diff_multiset_absorb2›) thus ?thesis using distinct by (intro that[of C1' C2' C3' C4']) (auto simp: parties_eq' A_eq add_mset_commute insert_commute) next case False have "r A = {#C1', C1', C3'#}" proof (rule papp_multiset_3_aux) show "set_mset (r A) ⊆ {C1', C3'}" using ‹set_mset (r A) ⊆ _› * False unfolding parties_eq' by auto next have "count (r A) C3' ≤ m" unfolding m_def by (subst Max_ge_iff) (auto simp: parties_eq') also have "m = count (r A) C1'" by (simp add: C1') finally show "count (r A) C3' ≤ count (r A) C1'" . qed (use C1' * False ‹C1' ∈# r A› distinct in ‹auto simp: ‹size (r A) = 3››) thus ?thesis using distinct by (intro that[of C1' C2' C3' C4']) (auto simp: parties_eq' insert_commute add_mset_commute A_eq) qed next assume *: "C3' ∉# r A" "C4' ∈# r A" show ?thesis proof (cases "C2' ∈# r A") case True have "r A = {#C1', C2', C4'#}" by (rule sym, rule mset_subset_size_ge_imp_eq) (use * ‹C1' ∈# r A› distinct True in ‹auto simp: ‹size (r A) = 3› Multiset.insert_subset_eq_iff in_diff_multiset_absorb2›) thus ?thesis using distinct by (intro that[of C1' C2' C4' C3']) (auto simp: parties_eq' A_eq add_mset_commute insert_commute) next case False have "r A = {#C1', C1', C4'#}" proof (rule papp_multiset_3_aux) show "set_mset (r A) ⊆ {C1', C4'}" using ‹set_mset (r A) ⊆ _› * False unfolding parties_eq' by auto next have "count (r A) C4' ≤ m" unfolding m_def by (subst Max_ge_iff) (auto simp: parties_eq') also have "m = count (r A) C1'" by (simp add: C1') finally show "count (r A) C4' ≤ count (r A) C1'" . qed (use C1' * False ‹C1' ∈# r A› distinct in ‹auto simp: ‹size (r A) = 3››) thus ?thesis using distinct by (intro that[of C1' C2' C4' C3']) (auto simp: parties_eq' insert_commute add_mset_commute A_eq) qed qed qed text ‹ We now use the choice operator to get our hands on such values $C_1$ to $C_4$. › definition C1234 where "C1234 = (SOME xs. set xs = parties ∧ distinct xs ∧ (case xs of [C1, C2, C3, C4] ⇒ r ({#{C1}, {C2}, {C1, C2}, {C3}, {C4}, {C3, C4}#}) ∈ {{#C1, C1, C3#}, {#C1, C2, C3#}}))" definition C1 where "C1 = C1234 ! 0" definition C2 where "C2 = C1234 ! 1" definition C3 where "C3 = C1234 ! 2" definition C4 where "C4 = C1234 ! 3" lemma distinct: "distinct [C1, C2, C3, C4]" and parties_eq: "parties = {C1, C2, C3, C4}" and symmetry_break: "r ({#{C1}, {C2}, {C1, C2}, {C3}, {C4}, {C3, C4}#}) ∈ {{#C1, C1, C3#}, {#C1, C2, C3#}}" proof - have C1234: "set C1234 = parties ∧ distinct C1234 ∧ (case C1234 of [C1', C2', C3', C4'] ⇒ r ({#{C1'}, {C2'}, {C1', C2'}, {C3'}, {C4'}, {C3', C4'}#}) ∈ {{#C1', C1', C3'#}, {#C1', C2', C3'#}})" unfolding C1234_def proof (rule someI_ex) obtain C1' C2' C3' C4' where *: "parties = {C1', C2', C3', C4'}" "distinct [C1', C2', C3', C4']" "r ({#{C1'}, {C2'}, {C1', C2'}, {C3'}, {C4'}, {C3', C4'}#}) ∈ {{#C1', C1', C3'#}, {#C1', C2', C3'#}}" using symmetry_break_aux by blast show "∃xs. set xs = parties ∧ distinct xs ∧ (case xs of [C1', C2', C3', C4'] ⇒ r ({#{C1'}, {C2'}, {C1', C2'}, {C3'}, {C4'}, {C3', C4'}#}) ∈ {{#C1', C1', C3'#}, {#C1', C2', C3'#}})" by (intro exI[of _ "[C1', C2', C3', C4']"]) (use * in auto) qed have "length C1234 = 4" using C1234 card_parties distinct_card[of C1234] by simp then obtain C1' C2' C3' C4' where C1234_eq: "C1234 = [C1', C2', C3', C4']" by (auto simp: eval_nat_numeral length_Suc_conv) show "distinct [C1, C2, C3, C4]" "parties = {C1, C2, C3, C4}" "r ({#{C1}, {C2}, {C1, C2}, {C3}, {C4}, {C3, C4}#}) ∈ {{#C1, C1, C3#}, {#C1, C2, C3#}}" using C1234 by (simp_all add: C1234_eq C1_def C2_def C3_def C4_def) qed lemma distinct' [simp]: "C1 ≠ C2" "C1 ≠ C3" "C1 ≠ C4" "C2 ≠ C1" "C2 ≠ C3" "C2 ≠ C4" "C3 ≠ C1" "C3 ≠ C2" "C3 ≠ C4" "C4 ≠ C1" "C4 ≠ C2" "C4 ≠ C3" using distinct by auto lemma in_parties [simp]: "C1 ∈ parties" "C2 ∈ parties" "C3 ∈ parties" "C4 ∈ parties" by (subst (2) parties_eq; simp; fail)+ subsection ‹The Set of Possible Committees› text ‹ Next, we compute the set of the 20 possible committees. › abbreviation COM where "COM ≡ committees 3 parties" definition COM' where "COM' = [{#C1, C1, C1#}, {#C1, C1, C2#}, {#C1, C1, C3#}, {#C1, C1, C4#}, {#C1, C2, C2#}, {#C1, C2, C3#}, {#C1, C2, C4#}, {#C1, C3, C3#}, {#C1, C3, C4#}, {#C1, C4, C4#}, {#C2, C2, C2#}, {#C2, C2, C3#}, {#C2, C2, C4#}, {#C2, C3, C3#}, {#C2, C3, C4#}, {#C2, C4, C4#}, {#C3, C3, C3#}, {#C3, C3, C4#}, {#C3, C4, C4#}, {#C4, C4, C4#}]" lemma distinct_COM': "distinct COM'" by (simp add: COM'_def add_mset_neq) lemma COM_eq: "COM = set COM'" by (subst parties_eq) (simp_all add: COM'_def numeral_3_eq_3 committees_Suc add_ac insert_commute add_mset_commute) lemma r_in_COM: assumes "is_pref_profile A" shows "r A ∈ COM" using rule_wf[OF assms] unfolding committees_def is_committee_def by auto lemma r_in_COM': assumes "is_pref_profile A" "A' ≡ A" shows "list_ex (λW. r A' = W) COM'" using r_in_COM[OF assms(1)] assms(2) by (auto simp: list_ex_iff COM_eq) lemma r_right_unique: "list_all (λ(W1,W2). r A ≠ W1 ∨ r A ≠ W2) (pairs COM')" proof - have "list_all (λ(W1,W2). W1 ≠ W2) (pairs COM')" using distinct_COM' unfolding distinct_conv_pairs by blast thus ?thesis unfolding list_all_iff by blast qed end subsection ‹Generating Clauses and Replaying the SAT Proof› text ‹ We now employ some custom-written ML code to generate all the SAT clauses arising from the given profiles (read from an external file) as Isabelle/HOL theorems. From these, we then derive \<^term>‹False› by replaying an externally found SAT proof (also written from an external file). The proof was found with the glucose SAT solver, which outputs proofs in the DRUP format (a subset of the more powerful DRAT format). We then used the ∗‹DRAT-trim› tool by Wetzler et al.~\cite{wetzler_drat_trim} to make the proof smaller. This was done repeatedly until the proof size did not decrease any longer. Then, the proof was converted into the ∗‹GRAT› format introduced by Lammich~\cite{lammich_grat}, which is easier to check (or in our case replay) than the less explicit DRAT (or DRUP) format. › external_file "sat_data/profiles" external_file "sat_data/papp_impossibility.grat.xz" context papp_impossibility_base_case begin ML_file ‹papp_impossibility.ML› text ‹ This invocation proves a theorem called ∗‹contradiction› whose statement is \<^term>‹False›. Note that the DIMACS version of the SAT file that is being generated can be viewed by clicking on ``See theory exports'' in the messages output by the invocation below. On a 2021 desktop PC with 12 cores, proving all the clauses takes 8.4\,s (multithreaded; CPU time 55\,s). Replaying the proof takes 30\,s (singlethreaded). › local_setup ‹fn lthy => let val thm = PAPP_Impossibility.derive_false lthy (\<^master_dir> + \<^path>‹sat_data/profiles›) (\<^master_dir> + \<^path>‹sat_data/papp_impossibility.grat.xz›) in Local_Theory.note ((\<^binding>‹contradiction›, []), [thm]) lthy |> snd end › end text ‹ With this, we can now prove the impossibility result: › lemma papp_impossibility_base_case: assumes "card parties = 4" shows "¬card_stratproof_weak_rep_anon_papp 6 parties 3 r" proof assume "card_stratproof_weak_rep_anon_papp 6 parties 3 r" then interpret card_stratproof_weak_rep_anon_papp 6 parties 3 r . interpret papp_impossibility_base_case parties r by unfold_locales fact+ show False by (rule contradiction) qed end