		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Create-nth-choice-count-alist

Create a count-alistp for nth-preference candidates

Signature
(create-nth-choice-count-alist n cids xs) → count-alst
Arguments: n — Guard (natp n).; cids — All the candidates in the election, sorted.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).
Returns: count-alst — Type (alistp count-alst).

Definitions and Theorems

Function: create-nth-choice-count-alist

(defun create-nth-choice-count-alist (n cids xs)
  (declare (xargs :guard (and (natp n)
                              (nat-listp cids)
                              (irv-ballot-p xs))))
  (let ((__function__ 'create-nth-choice-count-alist))
    (declare (ignorable __function__))
    (b* ((choice-lst (make-nth-choice-list n xs))
         (count-alst (create-count-alist cids choice-lst)))
      count-alst)))

Theorem: alistp-of-create-nth-choice-count-alist

(defthm alistp-of-create-nth-choice-count-alist
  (b* ((count-alst (create-nth-choice-count-alist n cids xs)))
    (alistp count-alst))
  :rule-classes :rewrite)

Theorem: count-alistp-of-create-nth-choice-count-alist

(defthm count-alistp-of-create-nth-choice-count-alist
  (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
    (implies (nat-listp cids)
             (count-alistp count-alst))))

Theorem: strip-cars-of-create-nth-choice-count-alist-is-sorted-if-cids-is-sorted

(defthm
 strip-cars-of-create-nth-choice-count-alist-is-sorted-if-cids-is-sorted
 (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
   (implies (acl2::<-ordered-p cids)
            (acl2::<-ordered-p (strip-cars count-alst)))))

Theorem: consp-of-create-nth-choice-count-alist

(defthm consp-of-create-nth-choice-count-alist
  (equal (consp (create-nth-choice-count-alist n cids xs))
         (consp cids)))

Theorem: strip-cars-of-create-nth-choice-count-alist-equal-under-set-equiv

(defthm
  strip-cars-of-create-nth-choice-count-alist-equal-under-set-equiv
  (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
    (acl2::set-equiv (strip-cars count-alst)
                     cids)))

Theorem: no-duplicatesp-equal-of-strip-cars-of-create-nth-choice-count-alist

(defthm
 no-duplicatesp-equal-of-strip-cars-of-create-nth-choice-count-alist
 (implies
      (no-duplicatesp-equal cids)
      (no-duplicatesp-equal
           (strip-cars (create-nth-choice-count-alist n cids xs)))))

Theorem: member-of-strip-cars-of-create-nth-choice-count-alist

(defthm member-of-strip-cars-of-create-nth-choice-count-alist
 (implies
      (member-equal id cids)
      (member-equal
           id
           (strip-cars (create-nth-choice-count-alist n cids xs)))))

Theorem: member-of-strip-cdrs-of-create-nth-choice-count-alist

(defthm member-of-strip-cdrs-of-create-nth-choice-count-alist
  (b* ((count-alst (create-nth-choice-count-alist n cids xs)))
    (implies (member-equal id cids)
             (member-equal (cdr (assoc-equal id count-alst))
                           (strip-cdrs count-alst)))))

Theorem: len-of-create-nth-choice-count-alist-0th-choice

(defthm len-of-create-nth-choice-count-alist-0th-choice
  (equal (len (create-nth-choice-count-alist 0 cids xs))
         (len cids)))

Subtopics

Create-count-alist: Given a choice list, maps each candidate ID to the number of votes they obtained
Make-nth-choice-list: Returns a list of the nth-preference candidates of all the voters