		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