# Theory Anonymous_PAPP

(*
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"

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'"
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