Theory Anon_Unan_Stratproof_Impossibility
theory Anon_Unan_Stratproof_Impossibility
imports SWF_Impossibility_Automation
begin
subsection ‹For 5 alternatives and 2 agents›
text ‹
We prove the impossibility for $m = 5$ and $n = 2$ via the SAT encoding using a fixed
list of 198 profiles. For symmetry breaking, we assume that the profile
$(abcde, acbed)$ is mapped to the ranking $abcde$. This assumption will be justified later on
by picking the values of $a, b, c, d, e$ accordingly.
›
external_file "sat_data/kemeny_profiles_5_2.xz"
external_file "sat_data/kemeny_5_2.grat.xz"
locale anonymous_unanimous_kemenysp_swf_explicit_5_2 =
anonymous_unanimous_kemenysp_swf_explicit agents alts swf 2 "[a,b,c,d,e]"
for agents :: "'agent set" and alts :: "'alt set" and swf and a b c d e +
assumes symmetry_breaking: "aswf' {# [a,b,c,d,e], [a,c,b,e,d] #} = [a,b,c,d,e]"
begin
local_setup ‹fn lthy =>
let
val params = {
name = "kemeny_5_2",
locale_thm = @{thm "anonymous_unanimous_kemenysp_swf_explicit_axioms"},
profile_file = SOME \<^path>‹sat_data/kemeny_profiles_5_2.xz›,
sp_file = NONE,
grat_file = \<^path>‹sat_data/kemeny_5_2.grat.xz›,
extra_clauses = @{thms symmetry_breaking}
}
val thm =
Goal.prove_future lthy [] [] \<^prop>‹False›
(fn {context, ...} =>
HEADGOAL (resolve_tac context [Anon_Unan_Stratproof_Impossibility.derive_false context params]))
in
Local_Theory.note ((\<^binding>‹contradiction›, []), [thm]) lthy |> snd
end
›
end
text ‹
We now get rid of the symmetry-breaking assumption by choosing an appropriate permutation of
the five alternatives.
›
locale anonymous_unanimous_kemenysp_swf_5_2 = anonymous_unanimous_kemenysp_swf agents alts swf
for agents :: "'agent set" and alts :: "'alt set" and swf +
assumes card_agents: "card agents = 2"
assumes card_alts: "card alts = 5"
begin
sublocale anonymous_unanimous_swf agents alts swf ..
sublocale anonymous_kemeny_strategyproof_swf agents alts swf ..
lemma symmetry_breaking_aux1:
assumes distinct: "distinct [a,b,c,d,e]" and alts_eq: "alts = {a,b,c,d,e}"
defines "R ≡ {# [a,b,c,d,e], [a,c,b,e,d] #}"
assumes R: "aswf' R = [a,c,b,d,e]"
shows "aswf' {# [a,b,c,e,d], [a,c,b,d,e] #} ∈ {[a,b,c,e,d], [a,c,b,d,e]}"
proof -
have alts_eq': "alts = set [a,b,c,d,e]"
by (simp add: alts_eq)
have [simp]: "a ≠ b" "a ≠ c" "a ≠ d" "a ≠ e" "b ≠ a" "b ≠ c" "b ≠ d" "b ≠ e"
"c ≠ a" "c ≠ b" "c ≠ d" "c ≠ e" "d ≠ a" "d ≠ b" "d ≠ c" "d ≠ e"
"e ≠ a" "e ≠ b" "e ≠ c" "e ≠ d"
using distinct by (simp_all add: eq_commute)
interpret anonymous_unanimous_kemenysp_swf_explicit agents alts swf 2 "[a,b,c,d,e]"
by standard (simp_all add: alts_eq card_agents)
have R_wf: "is_apref_profile' R"
unfolding is_apref_profile'_def by (auto simp: card_agents permutations_of_set_def alts_eq R_def)
define R2 where "R2 = {# [a,c,b,d,e], [a,c,b,e,d] #}"
define R3 where "R3 = {# [a,b,c,d,e], [a,c,b,d,e] #}"
define R4 where "R4 = {# [a,b,c,e,d], [a,c,b,d,e] #}"
note R_defs = R_def R2_def R3_def R4_def
have wf: "is_apref_profile' R" "is_apref_profile' R2" "is_apref_profile' R3" "is_apref_profile' R4"
by (simp_all add: is_apref_profile'_iff R_defs add_mset_commute)
have R2: "aswf' R2 = [a,c,b,d,e]"
proof -
have "aswf' R2 = [a,c,b,d,e] ∨ aswf' R2 = [a,c,b,e,d]"
using aswf'_in_allowed_results[OF wf(2)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R2 ≠ [a,c,b,e,d] ∨ aswf' R ≠ [a,c,b,d,e]"
by (intro kemeny_strategyproof_aswf'_strong wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons)
ultimately show ?thesis using R
by blast
qed
have R3: "aswf' R3 = [a,c,b,d,e]"
proof -
have "aswf' R3 = [a,b,c,d,e] ∨ aswf' R3 = [a,c,b,d,e]"
using aswf'_in_allowed_results[OF wf(3)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R3 ≠ [a,b,c,d,e] ∨ aswf' R ≠ [a,c,b,d,e]"
by (intro kemeny_strategyproof_aswf'_strong wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons)
ultimately show ?thesis using R
by blast
qed
show ?thesis
proof -
have "aswf' R4 ∈ {[a,b,c,d,e], [a,c,b,e,d], [a,b,c,e,d], [a,c,b,d,e]}"
using aswf'_in_allowed_results[OF wf(4)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R4 ≠ [a,b,c,d,e] ∨ aswf' R3 ≠ [a,c,b,d,e]"
by (intro kemeny_strategyproof_aswf'_strong wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons)
moreover have "aswf' R4 ≠ [a,c,b,e,d] ∨ aswf' R2 ≠ [a,c,b,d,e]"
by (intro kemeny_strategyproof_aswf'_strong wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons)
ultimately show ?thesis using R2 R3 unfolding R4_def
by blast
qed
qed
lemma symmetry_breaking_aux2:
obtains abcde where
"distinct abcde" "alts = set abcde" "length abcde = 5"
"case abcde of [a,b,c,d,e] ⇒ aswf' {# [a,b,c,d,e], [a,c,b,e,d] #} = [a,b,c,d,e]"
proof -
obtain abcde where abcde: "distinct abcde" "set abcde = alts"
using finite_distinct_list by blast
have "length abcde = 5"
using card_alts abcde distinct_card by metis
obtain a b c d e where abcde_expand: "abcde = [a,b,c,d,e]"
using ‹length abcde = 5› by (force simp: eval_nat_numeral length_Suc_conv)
have [simp]: "a ≠ b" "a ≠ c" "a ≠ d" "a ≠ e" "b ≠ a" "b ≠ c" "b ≠ d" "b ≠ e"
"c ≠ a" "c ≠ b" "c ≠ d" "c ≠ e" "d ≠ a" "d ≠ b" "d ≠ c" "d ≠ e"
"e ≠ a" "e ≠ b" "e ≠ c" "e ≠ d"
using abcde(1) unfolding abcde_expand by (simp_all add: eq_commute)
have alts_eq: "alts = {a,b,c,d,e}"
unfolding abcde(2) [symmetric] abcde_expand by simp
interpret anonymous_unanimous_kemenysp_swf_explicit agents alts swf 2 "[a,b,c,d,e]"
by standard (simp_all add: alts_eq card_agents)
define R where "R = {# [a,b,c,d,e], [a,c,b,e,d] #}"
have R_wf: "is_apref_profile' R"
unfolding R_def is_apref_profile'_def
by (auto simp: card_agents abcde_expand simp flip: abcde(2) intro!: linorder_of_ranking)
have "aswf' R ∈ {[a,b,c,d,e], [a,c,b,e,d]} ∨ aswf' R ∈ {[a,b,c,e,d], [a,c,b,d,e]}"
using aswf'_in_allowed_results[OF R_wf] unfolding R_def
by (simp add: eval_allowed_results del: Set.filter_eq)
thus ?thesis
proof
assume *: "aswf' R ∈ {[a,b,c,d,e], [a,c,b,e,d]}"
show ?thesis
by (rule that[of "aswf' R"])
(use * in ‹unfold R_def, auto simp add: alts_eq insert_commute add_mset_commute›)
next
assume "aswf' R ∈ {[a,b,c,e,d], [a,c,b,d,e]}"
hence "aswf' R = [a,b,c,e,d] ∨ aswf' R = [a,c,b,d,e]"
by blast
thus ?thesis
proof
assume *: "aswf' R = [a,c,b,d,e]"
have **: "aswf' {#[a,b,c,e,d], [a,c,b,d,e]#} ∈ {[a,b,c,e,d], [a,c,b,d,e]}"
by (rule symmetry_breaking_aux1[of a b c d e])
(use * in ‹simp_all add: R_def add_mset_commute alts_eq›)
show ?thesis
by (rule that[of "aswf' {#[a,b,c,e,d], [a,c,b,d,e]#}"])
(use ** in ‹auto simp: alts_eq add_mset_commute insert_commute›)
next
assume *: "aswf' R = [a,b,c,e,d]"
have **: "aswf' {#[a,c,b,d,e], [a,b,c,e,d]#} ∈ {[a,c,b,d,e], [a,b,c,e,d]}"
by (rule symmetry_breaking_aux1[of a c b e d])
(use * in ‹simp_all add: R_def add_mset_commute alts_eq insert_commute›)
show ?thesis
by (rule that[of "aswf' {#[a,b,c,e,d], [a,c,b,d,e]#}"])
(use ** in ‹auto simp: alts_eq add_mset_commute insert_commute›)
qed
qed
qed
lemma contradiction: False
proof -
obtain abcde where abcde:
"distinct abcde" "alts = set abcde" "length abcde = 5"
"case abcde of [a,b,c,d,e] ⇒ aswf' {# [a,b,c,d,e], [a,c,b,e,d] #} = [a,b,c,d,e]"
using symmetry_breaking_aux2 .
from ‹length abcde = 5› obtain a b c d e where abcde_expand: "abcde = [a,b,c,d,e]"
by (auto simp: length_Suc_conv eval_nat_numeral)
interpret anonymous_unanimous_kemenysp_swf_explicit_5_2 agents alts swf a b c d e
proof
show "aswf' {#[a, b, c, d, e], [a, c, b, e, d]#} = [a, b, c, d, e]"
using abcde unfolding abcde_expand by simp
qed (use abcde(1) in ‹simp_all add: card_agents abcde abcde_expand eq_commute›)
show ?thesis
by (fact contradiction)
qed
end
text ‹
Finally, we employ the usual construction of padding with dummy alternatives and cloning voters
to extend the impossibility to any setting with $m\geq 5$ and $n$ even.
›
theorem (in anonymous_unanimous_kemenysp_swf) impossibility:
assumes "even (card agents)" and "card alts ≥ 5"
shows False
proof -
have "card agents > 0"
using assms(1) finite_agents nonempty_agents by fastforce
with assms(1) have "card agents ≥ 2"
by presburger
obtain agents' where agents': "agents' ⊆ agents" "card agents' = 2"
using ‹card agents ≥ 2› by (meson obtain_subset_with_card_n)
have [simp]: "agents' ≠ {}"
using agents' by auto
obtain alts' where alts': "alts' ⊆ alts" "card alts' = 5"
using ‹card alts ≥ 5› by (meson obtain_subset_with_card_n)
obtain dummy_alts where alts_list': "mset dummy_alts = mset_set (alts - alts')"
using ex_mset by blast
obtain unclone where "cloning agents' agents unclone"
using cloning_exists[of agents' agents] agents' ‹even (card agents)› finite_agents by auto
interpret cloning agents' agents unclone by fact
interpret split: swf_split_agents agents alts swf agents' unclone ..
interpret new1: anonymous_swf agents' alts split.swf_low
by (rule split.anonymous_clone) unfold_locales
interpret new1: unanimous_swf agents' alts split.swf_low
by (rule split.unanimous_clone) unfold_locales
interpret new1: kemeny_strategyproof_swf agents' alts split.swf_low
by (rule split.kemeny_strategyproof_clone) unfold_locales
interpret restrict: unanimous_swf_restrict_alts agents' alts split.swf_low dummy_alts alts'
proof
show "finite alts'"
using alts'(1) finite_subset by blast
show "mset_set alts = mset dummy_alts + mset_set alts'"
by (simp add: ‹finite alts'› alts'(1) alts_list' mset_set_Diff)
show "alts' ≠ {}"
using alts'(2) by fastforce
qed
interpret new2: anonymous_swf agents' alts' restrict.swf_low
by (rule restrict.anonymous_restrict) unfold_locales
interpret new2: unanimous_swf agents' alts' restrict.swf_low ..
interpret new2: kemeny_strategyproof_swf agents' alts' restrict.swf_low
by (rule restrict.kemeny_strategyproof_restrict) unfold_locales
interpret new2: anonymous_unanimous_kemenysp_swf_5_2 agents' alts' restrict.swf_low
by standard fact+
show False
by (fact new2.contradiction)
qed
subsection ‹For 4 alternatives and 4 agents›
text ‹
We now similarly show the impossibility for $m = n = 4$. The main difference now is that the
number of profiles involved is much larger, namely 9900, so the approach of simply generating
all strategyproofness clauses that arise between these profiles is no longer feasible.
Instead we work with an explicit list of the required 254269 strategyproofness clauses that was
extracted from an unsatisfiable core found with MUSer2.
The symmetry-breaking assumption we use this time is that the profile where two agents report
$abcd$ and the other two report $badc$ is mapped to $abcd$.
›
external_file "sat_data/kemeny_sp_4_4.xz"
external_file "sat_data/kemeny_4_4.grat.xz"
locale anonymous_unanimous_kemenysp_swf_explicit_4_4 =
anonymous_unanimous_kemenysp_swf_explicit agents alts swf 4 "[a,b,c,d]"
for agents :: "'agent set" and alts :: "'alt set" and swf and a b c d +
assumes symmetry_breaking: "aswf' {# [a,b,c,d], [a,b,c,d], [b,a,d,c], [b,a,d,c] #} = [a,b,c,d]"
begin
local_setup ‹fn lthy =>
let
val params = {
name = "kemeny_4_4",
locale_thm = @{thm "anonymous_unanimous_kemenysp_swf_explicit_axioms"},
profile_file = NONE,
sp_file = SOME \<^path>‹sat_data/kemeny_sp_4_4.xz›,
grat_file = \<^path>‹sat_data/kemeny_4_4.grat.xz›,
extra_clauses = @{thms symmetry_breaking}
}
val thm =
Goal.prove_future lthy [] [] \<^prop>‹False›
(fn {context, ...} =>
HEADGOAL (resolve_tac context [Anon_Unan_Stratproof_Impossibility.derive_false context params]))
in
Local_Theory.note ((\<^binding>‹contradiction›, []), [thm]) lthy |> snd
end
›
end
text ‹
We again get rid of the symmetry-breaking assumption. The argument is almost exactly the same
one as before, except that we remove the alternative $a$ and all agents get cloned.
Consequently, the arguments involving strategyproofness have to use the stronger notion of
strategyproofness considering simultaneous deviations by clones.
›
locale anonymous_unanimous_kemenysp_swf_4_4 = anonymous_unanimous_kemenysp_swf agents alts swf
for agents :: "'agent set" and alts :: "'alt set" and swf +
assumes card_agents: "card agents = 4"
assumes card_alts: "card alts = 4"
begin
sublocale anonymous_unanimous_swf agents alts swf ..
sublocale anonymous_kemeny_strategyproof_swf agents alts swf ..
lemma symmetry_breaking_aux1:
assumes distinct: "distinct [a,b,c,d]" and alts_eq: "alts = {a,b,c,d}"
defines "R ≡ repeat_mset 2 {# [a,b,c,d], [b,a,d,c] #}"
assumes R: "aswf' R = [b,a,c,d]"
shows "aswf' (repeat_mset 2 {# [a,b,d,c], [b,a,c,d] #}) ∈ {[a,b,d,c], [b,a,c,d]}"
proof -
have alts_eq': "alts = set [a,b,c,d]"
by (simp add: alts_eq)
have [simp]: "a ≠ b" "a ≠ c" "a ≠ d" "b ≠ a" "b ≠ c" "b ≠ d"
"c ≠ a" "c ≠ b" "c ≠ d" "d ≠ a" "d ≠ b" "d ≠ c"
using distinct by (simp_all add: eq_commute)
interpret anonymous_unanimous_kemenysp_swf_explicit agents alts swf 4 "[a,b,c,d]"
by standard (simp_all add: alts_eq card_agents)
have R_wf: "is_apref_profile' R"
unfolding is_apref_profile'_def by (auto simp: card_agents permutations_of_set_def alts_eq R_def)
define R2 where "R2 = repeat_mset 2 {# [b,a,c,d], [b,a,d,c] #}"
define R3 where "R3 = repeat_mset 2 {# [a,b,c,d], [b,a,c,d] #}"
define R4 where "R4 = repeat_mset 2 {# [a,b,d,c], [b,a,c,d] #}"
note R_defs = R_def R2_def R3_def R4_def
have wf: "is_apref_profile' R" "is_apref_profile' R2" "is_apref_profile' R3" "is_apref_profile' R4"
by (simp_all add: is_apref_profile'_iff R_defs add_mset_commute)
have R2: "aswf' R2 = [b,a,c,d]"
proof -
have "aswf' R2 = [b,a,c,d] ∨ aswf' R2 = [b,a,d,c]"
using aswf'_in_allowed_results[OF wf(2)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R2 ≠ [b,a,d,c] ∨ aswf' R ≠ [b,a,c,d]"
by (intro kemeny_strategyproof_aswf'_clones[where A = "[b,a,c,d]" and n = 2] wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons eval_nat_numeral)
ultimately show ?thesis using R
by blast
qed
have R3: "aswf' R3 = [b,a,c,d]"
proof -
have "aswf' R3 = [a,b,c,d] ∨ aswf' R3 = [b,a,c,d]"
using aswf'_in_allowed_results[OF wf(3)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R3 ≠ [a,b,c,d] ∨ aswf' R ≠ [b,a,c,d]"
by (intro kemeny_strategyproof_aswf'_clones[where A = "[b,a,c,d]" and n = 2] wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons eval_nat_numeral)
ultimately show ?thesis using R
by blast
qed
show ?thesis
proof -
have "aswf' R4 ∈ {[a,b,c,d], [b,a,d,c], [a,b,d,c], [b,a,c,d]}"
using aswf'_in_allowed_results[OF wf(4)] unfolding R_defs
by (simp add: eval_allowed_results del: Set.filter_eq)
moreover have "aswf' R3 ≠ [b,a,c,d] ∨ aswf' R4 ≠ [a,b,c,d]"
by (intro kemeny_strategyproof_aswf'_clones[where A = "[a,b,c,d]" and n = 2] wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons eval_nat_numeral)
moreover have " aswf' R2 ≠ [b,a,c,d] ∨ aswf' R4 ≠ [b,a,d,c]"
by (intro kemeny_strategyproof_aswf'_clones[where A = "[b,a,d,c]" and n = 2] wf)
(simp_all add: R_defs insert_commute swap_dist_code' inversion_number_Cons eval_nat_numeral)
ultimately show ?thesis using R2 R3 unfolding R4_def
by blast
qed
qed
lemma symmetry_breaking_aux2:
obtains abcd where
"distinct abcd" "alts = set abcd" "length abcd =4"
"case abcd of [a,b,c,d] ⇒ aswf' (repeat_mset 2 {# [a,b,c,d], [b,a,d,c] #}) = [a,b,c,d]"
proof -
obtain abcd where abcd: "distinct abcd" "set abcd = alts"
using finite_distinct_list by blast
have "length abcd = 4"
using card_alts abcd distinct_card by metis
obtain a b c d where abcd_expand: "abcd = [a,b,c,d]"
using ‹length abcd = 4› by (force simp: eval_nat_numeral length_Suc_conv)
have [simp]: "a ≠ b" "a ≠ c" "a ≠ d""b ≠ a" "b ≠ c" "b ≠ d"
"c ≠ a" "c ≠ b" "c ≠ d" "d ≠ a" "d ≠ b" "d ≠ c"
using abcd(1) unfolding abcd_expand by (simp_all add: eq_commute)
have alts_eq: "alts = {a,b,c,d}"
unfolding abcd(2) [symmetric] abcd_expand by simp
interpret anonymous_unanimous_kemenysp_swf_explicit agents alts swf 4 "[a,b,c,d]"
by standard (simp_all add: alts_eq card_agents)
define R where "R = repeat_mset 2 {# [a,b,c,d], [b,a,d,c] #}"
have R_wf: "is_apref_profile' R"
unfolding R_def is_apref_profile'_def
by (auto simp: card_agents abcd_expand simp flip: abcd(2) intro!: linorder_of_ranking)
have "aswf' R ∈ {[a,b,c,d], [b,a,d,c]} ∨ aswf' R ∈ {[a,b,d,c], [b,a,c,d]}"
using aswf'_in_allowed_results[OF R_wf] unfolding R_def
by (simp add: eval_allowed_results del: Set.filter_eq)
thus ?thesis
proof
assume *: "aswf' R ∈ {[a,b,c,d], [b,a,d,c]}"
show ?thesis
by (rule that[of "aswf' R"])
(use * in ‹unfold R_def, auto simp add: alts_eq insert_commute add_mset_commute eval_nat_numeral›)
next
assume "aswf' R ∈ {[a,b,d,c], [b,a,c,d]}"
hence "aswf' R = [a,b,d,c] ∨ aswf' R = [b,a,c,d]"
by blast
thus ?thesis
proof
assume *: "aswf' R = [b,a,c,d]"
have **: "aswf' (repeat_mset 2 {#[a,b,d,c], [b,a,c,d]#}) ∈ {[a,b,d,c], [b,a,c,d]}"
by (rule symmetry_breaking_aux1[of a b c d])
(use * in ‹simp_all add: R_def add_mset_commute alts_eq›)
show ?thesis
by (rule that[of "aswf' (repeat_mset 2 {#[a,b,d,c], [b,a,c,d]#})"])
(use ** in ‹auto simp: alts_eq add_mset_commute insert_commute add.commute›)
next
assume *: "aswf' R = [a,b,d,c]"
have **: "aswf' (repeat_mset 2 {#[b,a,c,d], [a,b,d,c]#}) ∈ {[b,a,c,d], [a,b,d,c]}"
by (rule symmetry_breaking_aux1[of b a d c])
(use * in ‹simp_all add: R_def add_mset_commute alts_eq insert_commute›)
show ?thesis
by (rule that[of "aswf' (repeat_mset 2 {#[a,b,d,c], [b,a,c,d]#})"])
(use ** in ‹auto simp: alts_eq add_mset_commute insert_commute add.commute›)
qed
qed
qed
lemma contradiction: False
proof -
obtain abcd where abcd:
"distinct abcd" "alts = set abcd" "length abcd = 4"
"case abcd of [a,b,c,d] ⇒ aswf' (repeat_mset 2 {# [a,b,c,d], [b,a,d,c] #}) = [a,b,c,d]"
using symmetry_breaking_aux2 .
from ‹length abcd = 4› obtain a b c d where abcd_expand: "abcd = [a,b,c,d]"
by (auto simp: length_Suc_conv eval_nat_numeral)
interpret anonymous_unanimous_kemenysp_swf_explicit_4_4 agents alts swf a b c d
proof
show "aswf' {#[a, b, c, d], [a, b, c, d], [b, a, d, c], [b, a, d, c]#} = [a, b, c, d]"
using abcd unfolding abcd_expand by (simp add: eval_nat_numeral add_mset_commute)
qed (use abcd(1) in ‹simp_all add: card_agents abcd abcd_expand eq_commute›)
show ?thesis
by (fact contradiction)
qed
end
text ‹
The final result: extending the impossibility to $m\geq 2$ and $n$ a multiple of 4.
›
theorem (in anonymous_unanimous_kemenysp_swf) impossibility':
assumes "4 dvd card agents" and "card alts ≥ 4"
shows False
proof -
have "card agents ≥ 4"
using assms(1) nonempty_agents finite_agents by (meson card_0_eq dvd_imp_le not_gr0)
obtain agents' where agents': "agents' ⊆ agents" "card agents' = 4"
using ‹card agents ≥ 4› by (meson obtain_subset_with_card_n)
have [simp]: "agents' ≠ {}"
using agents' by auto
obtain alts' where alts': "alts' ⊆ alts" "card alts' = 4"
using ‹card alts ≥ 4› by (meson obtain_subset_with_card_n)
obtain dummy_alts where alts_list': "mset dummy_alts = mset_set (alts - alts')"
using ex_mset by blast
obtain unclone where "cloning agents' agents unclone"
using cloning_exists[of agents' agents] agents' ‹4 dvd card agents› finite_agents by auto
interpret cloning agents' agents unclone by fact
interpret split: swf_split_agents agents alts swf agents' unclone ..
interpret new1: anonymous_swf agents' alts split.swf_low
by (rule split.anonymous_clone) unfold_locales
interpret new1: unanimous_swf agents' alts split.swf_low
by (rule split.unanimous_clone) unfold_locales
interpret new1: kemeny_strategyproof_swf agents' alts split.swf_low
by (rule split.kemeny_strategyproof_clone) unfold_locales
interpret restrict: unanimous_swf_restrict_alts agents' alts split.swf_low dummy_alts alts'
proof
show "finite alts'"
using alts'(1) finite_subset by blast
show "mset_set alts = mset dummy_alts + mset_set alts'"
by (simp add: ‹finite alts'› alts'(1) alts_list' mset_set_Diff)
show "alts' ≠ {}"
using alts'(2) by fastforce
qed
interpret new2: anonymous_swf agents' alts' restrict.swf_low
by (rule restrict.anonymous_restrict) unfold_locales
interpret new2: unanimous_swf agents' alts' restrict.swf_low ..
interpret new2: kemeny_strategyproof_swf agents' alts' restrict.swf_low
by (rule restrict.kemeny_strategyproof_restrict) unfold_locales
interpret new2: anonymous_unanimous_kemenysp_swf_4_4 agents' alts' restrict.swf_low
by standard fact+
show False
by (fact new2.contradiction)
qed
text ‹
The following collects thw two impossibility results in one theorem.
›
theorem anonymous_unanimous_kemenysp_impossibility:
assumes "(card alts = 4 ∧ 4 dvd card agents) ∨ (card alts ≥ 5 ∧ even (card agents))"
assumes "anonymous_swf agents alts swf"
assumes "unanimous_swf agents alts swf"
assumes "kemeny_strategyproof_swf agents alts swf"
shows False
proof -
interpret anonymous_swf agents alts swf by fact
interpret unanimous_swf agents alts swf by fact
interpret kemeny_strategyproof_swf agents alts swf by fact
interpret anonymous_unanimous_kemenysp_swf agents alts swf ..
show False using assms(1) impossibility impossibility' by linarith
qed
end