		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

First-choice-of-majority-p

Returns the candidate, if any, who is the first choice of more than half of the voters

Signature
(first-choice-of-majority-p cids xs) → first-choice-of-majority
Arguments: cids — Sorted candidate IDs.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).
Returns: first-choice-of-majority — Type (acl2::maybe-natp first-choice-of-majority), given the guard.

This function encodes step (1) of the IRV algorithm: if a candidate among cids is the first choice of more than half of the voters, then it wins --- this function returns the ID of that candidate. If no such candidate exists, this function returns nil.

Definitions and Theorems

Theorem: member-equal-of-car-of-rassoc-equal

(defthm member-equal-of-car-of-rassoc-equal
        (implies (car (rassoc-equal val alst))
                 (member-equal (car (rassoc-equal val alst))
                               (strip-cars alst))))

Theorem: natp-of-car-of-rassoc-equal-of-nat-listp-strip-cars

(defthm natp-of-car-of-rassoc-equal-of-nat-listp-strip-cars
        (implies (and (member-equal val (strip-cdrs alst))
                      (nat-listp (strip-cars alst)))
                 (natp (car (rassoc-equal val alst))))
        :rule-classes (:rewrite :type-prescription))

Theorem: consp-of-rassoc-equal-of-max-nats-of-strip-cdrs

(defthm consp-of-rassoc-equal-of-max-nats-of-strip-cdrs
        (implies (and (consp alst)
                      (nat-listp (strip-cdrs alst)))
                 (consp (rassoc-equal (max-nats (strip-cdrs alst))
                                      alst))))

Theorem: natp-of-car-of-rassoc-equal-of-max-nats-of-strip-cdrs

(defthm
     natp-of-car-of-rassoc-equal-of-max-nats-of-strip-cdrs
     (implies (and (consp alst)
                   (nat-listp (strip-cars alst))
                   (nat-listp (strip-cdrs alst)))
              (natp (car (rassoc-equal (max-nats (strip-cdrs alst))
                                       alst))))
     :rule-classes (:rewrite :type-prescription))

Function: first-choice-of-majority-p

(defun
 first-choice-of-majority-p (cids xs)
 (declare (xargs :guard (and (nat-listp cids)
                             (irv-ballot-p xs))))
 (let
     ((__function__ 'first-choice-of-majority-p))
     (declare (ignorable __function__))
     (if (or (endp xs) (endp cids))
         nil
         (b* ((n (number-of-voters xs))
              (majority (majority n))
              (count-alst (create-nth-choice-count-alist 0 cids xs))
              (max-votes (max-nats (strip-cdrs count-alst))))
             (if (< majority max-votes)
                 (car (rassoc-equal max-votes count-alst))
                 nil)))))

Theorem: maybe-natp-of-first-choice-of-majority-p

(defthm
 maybe-natp-of-first-choice-of-majority-p
 (implies
  (and (nat-listp cids) (irv-ballot-p xs))
  (b*
   ((first-choice-of-majority (first-choice-of-majority-p cids xs)))
   (acl2::maybe-natp first-choice-of-majority)))
 :rule-classes :rewrite)

Theorem: rassoc-equal-returns-a-member-of-keys

(defthm rassoc-equal-returns-a-member-of-keys
        (implies (member-equal val (strip-cdrs alst))
                 (member-equal (car (rassoc-equal val alst))
                               (strip-cars alst))))

Theorem: rassoc-equal-returns-nil-when-value-not-found-in-alist

(defthm rassoc-equal-returns-nil-when-value-not-found-in-alist
        (implies (not (member-equal val (strip-cdrs alst)))
                 (equal (rassoc-equal val alst) nil)))

Theorem: majority-winner-is-a-member-of-cids

(defthm majority-winner-is-a-member-of-cids
        (implies (and (natp (first-choice-of-majority-p cids xs))
                      (irv-ballot-p xs))
                 (member-equal (first-choice-of-majority-p cids xs)
                               cids)))

Subtopics

Max-nats: Pick the maximum number in a list of natural numbers