(* File: Anonymous_PAPP.thy Author: Manuel Eberl, University of Innsbruck *) section ‹Anonymous Party Approval Rules› theory Anonymous_PAPP imports Complex_Main "Randomised_Social_Choice.Order_Predicates" PAPP_Multiset_Extras begin text ‹ In this section we will define (anonymous) P-APP rules and some basic desirable properties of P-APP rules. › subsection ‹Definition of the General Setting› text ‹ The following locale encapsulates an anonymous ∗‹party approval election›; that is: ▪ a number of voters ▪ a set of parties ▪ the size of the desired committee The number of parties and voters is assumed to be finite and non-zero. As a modelling choice, we do not distinguish the voters at all; there is no explicit set of voters. We only care about their number. › locale anon_papp_election = fixes n_voters :: nat and parties :: "'a set" and committee_size :: nat assumes finite_parties [simp, intro]: "finite parties" assumes n_voters_pos: "n_voters > 0" assumes nonempty_parties [simp]: "parties ≠ {}" begin text ‹ The result of a P-APP election is a committee, i.e.\ a multiset of parties with the desired size. › definition is_committee :: "'a multiset ⇒ bool" where "is_committee W ⟷ set_mset W ⊆ parties ∧ size W = committee_size" end text ‹ A ∗‹preference profile› for a P-APP collection consists of one approval list (i.e.\ a set of approved parties) for each voter. Since we are in an anonymous setting, this means that we have a ∗‹multiset› consisting of ‹n› sets of parties (where ‹n› is the number of voters). Moreover, we make the usual assumption that the approval lists must be non-empty. › locale anon_papp_profile = anon_papp_election + fixes A :: "'a set multiset" assumes A_subset: "⋀X. X ∈# A ⟹ X ⊆ parties" assumes A_nonempty: "{} ∉# A" assumes size_A: "size A = n_voters" begin lemma A_nonempty': "A ≠ {#}" using size_A n_voters_pos by auto end context anon_papp_election begin abbreviation is_pref_profile where "is_pref_profile ≡ anon_papp_profile n_voters parties" lemma is_pref_profile_iff: "is_pref_profile A ⟷ set_mset A ⊆ Pow parties - {{}} ∧ size A = n_voters" unfolding anon_papp_profile_def anon_papp_profile_axioms_def using anon_papp_election_axioms by auto lemma not_is_pref_profile_empty [simp]: "¬is_pref_profile {#}" using anon_papp_profile.A_nonempty'[of n_voters] by auto text ‹ The following relation is a key definition: it takes an approval list ‹A› and turns it into a preference relation on committees. A committee is to be at least as good as another if the number of approved parties in it is at least as big. This relation is a reflexive, transitive, and total. › definition committee_preference :: "'a set ⇒ 'a multiset relation" ("Comm") where "W1 ≼[Comm(A)] W2 ⟷ size {# x∈#W1. x ∈ A #} ≤ size {# x∈#W2. x ∈ A #}" lemma not_strict_Comm [simp]: "¬(W1 ≺[Comm(A)] W2) ⟷ W1 ≽[Comm(A)] W2" by (auto simp: committee_preference_def strongly_preferred_def) lemma not_weak_Comm [simp]: "¬(W1 ≼[Comm(A)] W2) ⟷ W1 ≻[Comm(A)] W2" by (auto simp: committee_preference_def strongly_preferred_def) sublocale Comm: preorder "Comm(A)" "λx y. x ≺[Comm(A)] y" by standard (auto simp: committee_preference_def strongly_preferred_def) lemma strong_committee_preference_iff: "W1 ≺[Comm(A)] W2 ⟷ size {# x∈#W1. x ∈ A #} < size {# x∈#W2. x ∈ A #}" by (auto simp: committee_preference_def strongly_preferred_def) text ‹ We also define the Pareto ordering on parties induced by a given preference profile: One party is at least as good (in the Pareto relation) as another if all voters agree that it is at least as good. That is, $y \succeq x$ in the Pareto ordering if all voters who approve $x$ also approve $y$. This relation is also reflexive and transitive. › definition Pareto :: "'a set multiset ⇒ 'a relation" where "x ≼[Pareto(A)] y ⟷ x ∈ parties ∧ y ∈ parties ∧ (∀X∈#A. x ∈ X ⟶ y ∈ X)" sublocale Pareto: preorder_on parties "Pareto A" by standard (auto simp: Pareto_def) text ‹ Pareto losers are parties that are (strictly) Pareto-dominated, i.e.\ there exists some other party that all voters consider to be at least as good and at least one voter considers it to be strictly better. › definition pareto_losers :: "'a set multiset ⇒ 'a set" where "pareto_losers A = {x. ∃y. y ≻[Pareto(A)] x}" end subsection ‹P-APP rules and Desirable Properties› text ‹ The following locale describes a P-APP rule. This is simply a function that maps every preference profile to a committee of the desired size. Note that in our setting, a P-APP rule has a fixed number of voters, a fixed set of parties, and a fixed desired committee size. › locale anon_papp = anon_papp_election + fixes r :: "'a set multiset ⇒ 'a multiset" assumes rule_wf: "is_pref_profile A ⟹ is_committee (r A)" subsection ‹Efficiency› text ‹ Efficiency is a common notion in Social Choice Theory. The idea is that if a party is ``obviously bad'', then it should not be chosen. What ``obviously bad'' means depends on the precise notion of Efficiency that is used. We will talk about two notions: Weak Efficiency and Pareto Efficiency. A P-APP rule is ∗‹weakly efficient› if a party that is approved by no one is never part of the output committee. Note that approval lists must be non-empty, so there is always at least one party that is approved by at least one voter. › locale weakly_efficient_anon_papp = anon_papp + assumes weakly_efficient: "is_pref_profile A ⟹ ∀X∈#A. x ∉ X ⟹ x ∉# r A" text ‹ A P-APP rule is ∗‹Pareto-efficient› if a Pareto-dominated party is never part of the output committee. › locale pareto_optimal_anon_papp = anon_papp + assumes pareto_optimal: "is_pref_profile A ⟹ x ∈ pareto_losers A ⟹ x ∉# r A" begin text ‹ Pareto-efficiency implies weak efficiency: › sublocale weakly_efficient_anon_papp proof fix A x assume A: "is_pref_profile A" and x: "∀X∈#A. x ∉ X" interpret anon_papp_profile n_voters parties committee_size A by fact have "A ≠ {#}" using A_nonempty' . then obtain X where X: "X ∈# A" by auto with A_nonempty have "X ≠ {}" by auto then obtain y where y: "y ∈ X" by auto show "x ∉# r A" proof (cases "x ∈ parties") case False thus ?thesis using rule_wf[OF A] by (auto simp: is_committee_def) next case True have "y ≻[Pareto(A)] x" unfolding Pareto_def using X x y True A_subset[of X] by (auto simp: strongly_preferred_def) hence "x ∈ pareto_losers A" by (auto simp: pareto_losers_def) thus ?thesis using pareto_optimal[OF A] by auto qed qed end subsection ‹Strategyproofness› text ‹ Strategyproofness is another common notion in Social Choice Theory that generally encapsulates the notion that an voter should not be able to manipulate the outcome of an election in their favour by (unilaterally) submitting fake preferences; i.e.\ reporting one's preferences truthfully should always be the optimal choice. A P-APP rule is called ∗‹cardinality-strategyproof› if an voter cannot obtain a better committee (i.e.\ one that contains strictly more of their approved parties) by submitting an approval list that is different from their real approval list. › text ‹ To make the definition simpler, we first define the notion of ∗‹manipulability›: in the context of a particular P-APP rule ‹r›, a preference profile ‹A› is said to be manipulable by the voter ‹i› with the fake preference list ‹Y› if ‹r(A(i := Y))› contains strictly more parties approved by ‹i› than ‹r(A)›. Since we have anonymous profiles and do not talk about particular voters, we replace ‹i› with their approval list ‹X›. Since ‹A› is a multiset, the definition of manipulability becomes $r(A-\{X\}+\{Y\}) \succ_{X} r(A)$. › definition (in anon_papp) card_manipulable where "card_manipulable A X Y ⟷ is_pref_profile A ∧ X ∈# A ∧ Y ≠ {} ∧ Y ⊆ parties ∧ r (A - {#X#} + {#Y#}) ≻[Comm(X)] r A" text ‹ A technical (and fairly obvious) lemma: replacing an voter's approval list with a different approval list again yields a valid preference profile. › lemma (in anon_papp) is_pref_profile_replace: assumes "is_pref_profile A" and "X ∈# A" and "Y ≠ {}" and "Y ⊆ parties" shows "is_pref_profile (A - {#X#} + {#Y#})" proof - interpret anon_papp_profile n_voters parties committee_size A by fact show ?thesis using assms A_subset A_nonempty unfolding is_pref_profile_iff by (auto dest: in_diffD simp: size_Suc_Diff1) qed locale card_stratproof_anon_papp = anon_papp + assumes not_manipulable: "¬card_manipulable A X Y" begin text ‹ The two following alternative versions of non-manipulability are somewhat nicer to use in practice. › lemma not_manipulable': assumes "is_pref_profile A" "is_pref_profile A'" "A + {#Y#} = A' + {#X#}" shows "¬(r A' ≻[Comm(X)] r A)" proof (cases "X = Y") case True thus ?thesis using assms by (simp add: strongly_preferred_def) next case False interpret A: anon_papp_profile n_voters parties committee_size A by fact interpret A': anon_papp_profile n_voters parties committee_size A' by fact from assms(3) False have *: "Y ∈# A'" "X ∈# A" by (metis add_mset_add_single insert_noteq_member)+ have "¬card_manipulable A X Y" by (intro not_manipulable) hence "¬r (A - {#X#} + {#Y#}) ≻[Comm(X)] r A" using assms * A.A_subset A'.A_subset A.A_nonempty A'.A_nonempty by (auto simp: card_manipulable_def) also have "A - {#X#} + {#Y#} = A'" using assms(3) False by (metis add_eq_conv_diff add_mset_add_single) finally show ?thesis . qed lemma not_manipulable'': assumes "is_pref_profile A" "is_pref_profile A'" "A + {#Y#} = A' + {#X#}" shows "r A' ≼[Comm(X)] r A" using not_manipulable'[OF assms] by simp end subsection ‹Representation› text ‹ ∗‹Representation› properties are in a sense the opposite of Efficiency properties: if a sufficiently high voters agree that certain parties are good, then these should, to some extent, be present in the result. For instance, if we have 20 voters and 5 of them approve parties ‹A› and ‹B›, then if the output committee has size 4, we would expect either ‹A› or ‹B› to be in the committee to ensure that these voters' preferences are represented fairly. Weak representation is a particularly weak variant of this that states that if at least one $k$-th of the voters (where $k$ is the size of the output committee) approve only a single party ‹x›, then ‹x› should be in the committee at least once: › locale weak_rep_anon_papp = anon_papp n_voters parties committee_size r for n_voters and parties :: "'alt set" and committee_size :: nat and r + assumes weak_representation: "is_pref_profile A ⟹ committee_size * count A {x} ≥ n_voters ⟹ x ∈# r A" text ‹ The following alternative definition of Weak Representation is a bit closer to the definition given in the paper. › lemma weak_rep_anon_papp_altdef: "weak_rep_anon_papp n_voters parties committee_size r ⟷ anon_papp n_voters parties committee_size r ∧ (committee_size = 0 ∨ (∀A x. anon_papp_profile n_voters parties A ⟶ count A {x} ≥ n_voters / committee_size ⟶ x ∈# r A))" by (cases "committee_size = 0") (auto simp: field_simps weak_rep_anon_papp_def weak_rep_anon_papp_axioms_def anon_papp_def anon_papp_axioms_def anon_papp_election_def simp flip: of_nat_mult) text ‹ ∗‹Justified Representation› is a stronger notion which demands that if there is a subgroup of voters that comprises at least one $k$-th of all voters and for which the intersection of their approval lists is some nonempty set ‹X›, then at least one of the parties approved by at least one voter in that subgroup must be in the result committee. › locale justified_rep_anon_papp = anon_papp n_voters parties committee_size r for n_voters and parties :: "'alt set" and committee_size :: nat and r + assumes justified_representation: "is_pref_profile A ⟹ G ⊆# A ⟹ committee_size * size G ≥ n_voters ⟹ (⋂X∈set_mset G. X) ≠ {} ⟹ ∃X x. X ∈# G ∧ x ∈ X ∧ x ∈# r A" begin text ‹ Any rule that satisfies Justified Representation also satisfies Weak Representation › sublocale weak_rep_anon_papp proof fix A x assume *: "is_pref_profile A" "n_voters ≤ committee_size * count A {x}" define G where "G = replicate_mset (count A {x}) {x}" have [simp]: "size G = count A {x}" by (auto simp: G_def) have **: "set_mset G ⊆ {{x}}" by (auto simp: G_def) have ***: "G ⊆# A" unfolding G_def by (meson count_le_replicate_mset_subset_eq order_refl) have "∃X x. X ∈# G ∧ x ∈ X ∧ x ∈# r A" by (rule justified_representation) (use * ** *** in auto) thus "x ∈# r A" using ** by auto qed end locale card_stratproof_weak_rep_anon_papp = card_stratproof_anon_papp + weak_rep_anon_papp subsection ‹Proportional Representation› text ‹ The notions of Representation we have seen so far are fairly week in that they only demand that certain parties be in the committee at least once if enough voters approve them. Notions of Proportional Representation strengthen this by demanding that if a sufficiently large subgroup of voters approve some parties, then these voters must be represented in the result committe not just once, but to a degree proportional to the size of that subgroup of voters. For Weak Representation, the proportional generalization is fairly simple: if a fraction of at least $\frac{ln}{k}$ of the voters uniquely approve a party ‹x›, then ‹x› must be in the committee at least ‹l› times. › locale weak_prop_rep_anon_papp = anon_papp n_voters parties committee_size r for n_voters and parties :: "'alt set" and committee_size :: nat and r + assumes weak_proportional_representation: "is_pref_profile A ⟹ committee_size * count A {x} ≥ l * n_voters ⟹ count (r A) x ≥ l" begin sublocale weak_rep_anon_papp proof fix A x assume "is_pref_profile A" "n_voters ≤ committee_size * count A {x}" thus "x ∈# r A" using weak_proportional_representation[of A 1] by auto qed end text ‹ Similarly, Justified ∗‹Proportional› Representation demands that if the approval lists of a subgroup of at least $\frac{ln}{k}$ voters have a non-empty intersection, then at least ‹l› parties in the result committee are each approved by at least one of the voters in the subgroup. › locale justified_prop_rep_anon_papp = anon_papp n_voters parties committee_size r for n_voters and parties :: "'alt set" and committee_size :: nat and r + assumes justified_proportional_representation: "is_pref_profile A ⟹ G ⊆# A ⟹ committee_size * size G ≥ l * n_voters ⟹ (⋂X∈set_mset G. X) ≠ {} ⟹ size {# x ∈# r A. x ∈ (⋃X∈set_mset G. X) #} ≥ l" begin sublocale justified_rep_anon_papp proof fix A G assume "is_pref_profile A" "G ⊆# A" "n_voters ≤ committee_size * size G" "(⋂X∈set_mset G. X) ≠ {}" hence "size {#x ∈# r A. ∃X∈#G. x ∈ X#} ≥ 1" using justified_proportional_representation[of A G 1] by auto hence "{#x ∈# r A. ∃X∈#G. x ∈ X#} ≠ {#}" by auto thus "∃X x. X ∈# G ∧ x ∈ X ∧ x ∈# r A" by fastforce qed sublocale weak_prop_rep_anon_papp proof fix A l x assume *: "is_pref_profile A" "l * n_voters ≤ committee_size * count A {x}" define G where "G = replicate_mset (count A {x}) {x}" from * have "size {#x ∈# r A. x ∈ (⋃X∈set_mset G. X)#} ≥ l" by (intro justified_proportional_representation) (auto simp: G_def simp flip: count_le_replicate_mset_subset_eq) also have "size {#x ∈# r A. x ∈ (⋃X∈set_mset G. X)#} ≤ count (r A) x" by (auto simp: G_def) finally show "count (r A) x ≥ l" . qed end locale card_stratproof_weak_prop_rep_anon_papp = card_stratproof_anon_papp + weak_prop_rep_anon_papp end