Theory PAPP_Impossibility_Base_Case
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