An ACL2 Formalization of an Instant-Runoff Voting Scheme

The function `irv` formalizes the following instant-runoff
voting scheme.

The winner of an IRV election will be chosen as follows:

- If a candidate is the first choice of more than half of the voters, then he/she wins. Otherwise:
- Adjust each ballot by eliminating the candidate with the fewest first-place votes. If there is a tie for the fewest first-place votes, then delete the candidate with the least second-place votes, and so on. If the tie persists all through to the last-place level, then resolve it using a tie-breaker function that picks exactly one candidate out of those involved in the tie.
- Go to the first step.

See fairness-criteria for some fairness theorems about this
voting scheme. We also define a simpler version of IRV --- `irv-alt` --- that may be suitable for proofs of certain kinds of
properties.

- This IRV formalization accepts partial as well as total rankings; i.e., a voter can choose to rank a subset of the candidates in the election.
- The tie-breaker function
pick-candidate is constrained, so you can define your own tie-breaker method for execution. By default, we attach the function`pick-candidate-with-smallest-id`topick-candidate to pick the candidate with the smallest identifier.

- Fairness-criteria
- Some fairness theorems about
`irv` - Candidate-with-least-nth-place-votes
- Returns a candidate to be eliminated in step (2) of the IRV algorithm
- Eliminate-candidate
- Eliminate candidate
id from every voter's preference list inxs - First-choice-of-majority-p
- Returns the candidate, if any, who is the first choice of more than half of the voters
- Candidate-ids
- Get a sorted list of candidate IDs currently in the election
- Irv
- Compute the winner of an IRV election
- Create-nth-choice-count-alist
- Create a count-alistp for
n th-preference candidates - Irv-alt
- An alternative (but equivalent) definition of irv, with the majority step removed
- Irv-ballot-p
- Recognizer for a well-formed IRV ballot
- Majority
- Number-of-candidates
- List-elements-equal
- Returns
t if all elements ofx are equal toe - Number-of-voters