Theory PAPP_Impossibility

(*
  File:     PAPP_Impossibility.thy
  Author:   Manuel Eberl, University of Innsbruck 
*)
section ‹Lifting the Impossibility Result to Larger Settings›
theory PAPP_Impossibility
  imports PAPP_Impossibility_Base_Case Anonymous_PAPP_Lowering
begin

text ‹
  In this section, we now prove the main results of this work by combining the base case
  with the lifting arguments formalized earlier.

  First, we prove the following very simple technical lemma: a set that is infinite or finite with
  cardinality at least 2 contains two different elements ‹x› and ‹y›.
›

lemma obtain_2_elements:
  assumes "infinite X ∨ card X ≥ 2"
  obtains x y where "x ∈ X" "y ∈ X" "x ≠ y"
proof -
  from assms have "X ≠ {}"
    by auto
  then obtain x where "x ∈ X"
    by blast
  with assms have "infinite X ∨ card (X - {x}) > 0"
    by (subst card_Diff_subset) auto
  hence "X - {x} ≠ {}"
    by (metis card_gt_0_iff finite.emptyI infinite_remove)
  then obtain y where "y ∈ X - {x}"
    by blast
  with ‹x ∈ X› show ?thesis
    using that[of x y] by blast
qed

text ‹
  We now have all the ingredients to formalise the first main impossibility result: There is
  no P-APP rule that satisfies Anonymity, Cardinality-Strategyproofness, and Weak Representation
  if ‹k ≥ 3› and ‹m ≥ k + 1› and ‹n› is a multiple of ‹2k›.

  The proof simply uses the lowering lemmas we proved earlier to first reduce the committee size
  to 3, then reduce the voters to 6, and finally restrict the parties to 4. At that point,
  the base case we proved with SAT solving earlier kicks in.

  This corresponds to Theorem~1 in the paper.
›
theorem papp_impossibility1:
  assumes "k ≥ 3" and "card parties ≥ k + 1" and "finite parties"
  shows   "¬card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
  using assms
proof (induction k arbitrary: parties r rule: less_induct)
  case (less k parties r)
  show ?case
  proof (cases "k = 3")
    assume [simp]: "k = 3"
    text ‹
      If the committee size is 3, we first use our voter-division lemma to
      go from a P-APP rule for $6l$ voters to one with just 6 voters. Next, we choose 4 arbitrary
      parties and use our party-restriction lemma to obtain a P-APP rule for just 4 parties.

      But this is exactly our base case, which we already know to be infeasible. 
    ›
    show ?thesis
    proof
      assume "card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
      then interpret card_stratproof_weak_rep_anon_papp "l * 6" parties 3 r
        by (simp add: mult_ac)
      interpret divide_voters_card_stratproof_weak_rep_anon_papp l 6 parties 3 r ..

      have "card parties ≥ 4"
        using less.prems by auto
      then obtain parties' where parties': "parties' ⊆ parties" "card parties' = 4"
        by (metis obtain_subset_with_card_n)
      have "∃r. card_stratproof_weak_rep_anon_papp 6 parties' 3 r"
      proof (rule card_stratproof_weak_rep_anon_papp_restrict_parties)
        show "card_stratproof_weak_rep_anon_papp 6 parties 3 (r ∘ lift_profile)"
          by (rule lowered.card_stratproof_weak_rep_anon_papp_axioms)
      qed (use parties' in auto)
      thus False
        using papp_impossibility_base_case[OF parties'(2)] by blast
    qed
  next
    assume "k ≠ 3"
    text ‹
      If the committee size is greater than 3, we use our other lowering lemma to reduce the
      committee size by 1 (while also reducing the number of voters by $2l$ and the number of
      parties by 1).
    ›
    with less.prems have "k > 3"
      by simp

    obtain x y where xy: "x ∈ parties" "y ∈ parties" "x ≠ y"
      using obtain_2_elements[of parties] less.prems by auto
    define parties' where "parties' = parties - {y}"
    have [simp]: "card parties' = card parties - 1"
      unfolding parties'_def using xy by (subst card_Diff_subset) auto

    show ?thesis
    proof
      assume "card_stratproof_weak_rep_anon_papp (2 * k * l) parties k r"
      then interpret card_stratproof_weak_rep_anon_papp
        "2 * l * (k - 1 + 1)" "insert y parties'" "k - 1 + 1" r
        using ‹k > 3› xy by (simp add: parties'_def insert_absorb mult_ac)
      interpret decrease_committee_card_stratproof_weak_rep_anon_papp "2 * l" "k - 1" y parties' r x
        by unfold_locales (use ‹k > 3› xy in ‹auto simp: parties'_def›)
      have "¬card_stratproof_weak_rep_anon_papp (2 * (k - 1) * l) parties' (k - 1) lowered"
        by (rule less.IH) (use ‹k > 3› xy less.prems in auto)
      with lowered.card_stratproof_weak_rep_anon_papp_axioms show False
        by (simp add: mult_ac)
    qed
  qed
qed

text ‹
  If Weak Representation is replaced with Weak Proportional Representation, we can strengthen
  the impossibility result by relaxing the conditions on the number of parties to ‹m ≥ 4›.

  This works because with Weak Proportional Representation, we can reduce the size of the committee
  without changing the number of parties. We use this to again bring $k$ down to $3$ without
  changing $m$, at which point we can simply apply our previous impossibility result for
  Weak Representation.

  This corresponds to Theorem~2 in the paper.
›
corollary papp_impossibility2:
  assumes "k ≥ 3" and "card parties ≥ 4" and "finite parties"
  shows   "¬card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
  using assms
proof (induction k arbitrary: parties r rule: less_induct)
  case (less k parties r)
  show ?case
  proof (cases "k = 3")
    assume [simp]: "k = 3"
    text ‹
      For committee size 3, we simply employ our previous impossibility result:
    ›
    show ?thesis
    proof
      assume "card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
      then interpret card_stratproof_weak_prop_rep_anon_papp "l * 6" parties 3 r
        by (simp add: mult_ac)
      have "card_stratproof_weak_rep_anon_papp (l * 6) parties 3 r" ..
      moreover have "¬card_stratproof_weak_rep_anon_papp (l * 6) parties 3 r"
        using papp_impossibility1[of 3 parties l r] less.prems by (simp add: mult_ac)
      ultimately show False
        by contradiction
    qed
  next
    assume "k ≠ 3"
    text ‹
      If the committee size is greater than 3, we use our other lowering lemma to reduce the
      committee size by 1 (while also reducing the number of voters by $2l$).
    ›

    with less.prems have "k > 3"
      by simp

    have "parties ≠ {}"
      using less.prems by auto
    then obtain x where x: "x ∈ parties"
      by blast

    show ?thesis
    proof
      assume "card_stratproof_weak_prop_rep_anon_papp (2 * k * l) parties k r"
      then interpret card_stratproof_weak_prop_rep_anon_papp
        "2 * l * (k - 1 + 1)" parties "k - 1 + 1" r
        using ‹k > 3› by (simp add:  mult_ac)
      interpret decrease_committee_card_stratproof_weak_prop_rep_anon_papp "2 * l" "k - 1" parties r x
        by unfold_locales (use ‹k > 3› x in auto)
      have "¬card_stratproof_weak_prop_rep_anon_papp (2 * (k - 1) * l) parties (k - 1) lowered"
        by (rule less.IH) (use ‹k > 3› less.prems in auto)
      with lowered.card_stratproof_weak_prop_rep_anon_papp_axioms show False
        by (simp add: mult_ac)
    qed
  qed
qed

end