Some fairness theorems about `irv`

We prove that `irv` satisfies the following fairness
criteria.

**Majority Criterion:**If a candidate is preferred by an absolute majority of voters, then that candidate must win.**Theorem:**irv-satisfies-the-majority-criterion (defthm irv-satisfies-the-majority-criterion (implies (and (< (majority (number-of-voters xs)) (acl2::duplicity e (make-nth-choice-list 0 xs))) (irv-ballot-p xs)) (equal (irv xs) e)))

**Condorcet Loser Criteria:**A simple definition from Wikipedia is as follows:...if a candidate would lose a head-to-head competition against every other candidate, then that candidate must not win the overall election.

Note that a given election may or may not have a Condorcet Loser.

**Theorem:**irv-satisfies-the-condorcet-loser-criterion (defthm irv-satisfies-the-condorcet-loser-criterion (implies (and (all-head-to-head-competition-loser-p l cids xs) (acl2::set-equiv (cons l cids) (candidate-ids xs)) (no-duplicatesp-equal (cons l cids)) (nat-listp cids) (<= 1 (len cids)) (irv-ballot-p xs)) (not (equal (irv xs) l))))

**Majority Loser Criterion:**If a majority of voters prefers every other candidate over a given candidate, then that candidate must not win. Or said differently: if a candidate has a majority of last-place votes, then he must not win.**Theorem:**irv-satisfies-the-majority-loser-criterion (defthm irv-satisfies-the-majority-loser-criterion (implies (and (< (majority (number-of-voters xs)) (acl2::duplicity l (make-nth-choice-list (last-place xs) xs))) (< 1 (number-of-candidates xs)) (irv-ballot-p xs)) (not (equal (irv xs) l))))

**Independence of Clones Criterion:**If a set of clones contains at least two non-winning candidates, then deleting one of the clones must not change the winner.This property depends on the definition of

pick-candidate , the tie-breaker, in our formalization. Since the tie-breaker is a constrained function, we can't prove it about`irv`in the general case. Here's an illustration:(irv '((1 3) (2))) ;; 2 is the winner. ;; 3 is a clone of 1 --- both are non-winning candidates. (clone-p 3 1 '((1 3) (2))) ;; Suppose the tie-breaker picked the candidate with the smallest ;; ID. ;; Now, eliminating one clone changes the winner from 2 to 3. (irv (eliminate-candidate 1 '((1 3) (2))))

However, we do prove that this property holds when the winner is elected in the first step, i.e., if he has a majority of first-place votes.

**Theorem:**irv-satisfies-the-independence-of-clones-criterion-majority-winner (defthm irv-satisfies-the-independence-of-clones-criterion-majority-winner (implies (and (natp (first-choice-of-majority-p (candidate-ids xs) xs)) (equal w (irv xs)) (clone-p clone c xs) (not (equal w c)) (not (equal w clone)) (irv-ballot-p xs)) (equal (irv (eliminate-candidate clone xs)) w)))

- Eliminate-candidates
- Remove
cids fromxs - Sum-nats
- Eliminate-other-candidates
- Remove all candidates from
xs , except for those incids - Clone-p
- Is
clone a clone ofc inxs ? - Last-place
- Index of the last-place vote in
xs - All-head-to-head-competition-loser-p
- Check if
l will lose in a head-to-head competition against every candidate incids - Non-maj-ind-hint
- Find-condorcet-loser
- Returns a condorcet loser in
xs , if any - Last-place-elim-ind-hint