• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
      • Fairness-criteria
      • Candidate-with-least-nth-place-votes
      • Eliminate-candidate
      • First-choice-of-majority-p
      • Candidate-ids
      • Irv
      • Create-nth-choice-count-alist
        • Create-count-alist
          • Count-alistp
        • Make-nth-choice-list
      • Irv-alt
      • Irv-ballot-p
      • Majority
      • Number-of-candidates
      • List-elements-equal
      • Number-of-voters
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Create-nth-choice-count-alist

Create-count-alist

Given a choice list, maps each candidate ID to the number of votes they obtained

Signature

(create-count-alist cids choice-lst) → count-alst

Arguments

cids — All the candidates in the election, sorted.
    Guard (nat-listp cids).

choice-lst — Guard (nat-listp choice-lst).

Returns

count-alst — Type (alistp count-alst).

Definitions and Theorems

Function: create-count-alist

(defun create-count-alist (cids choice-lst)
  (declare (xargs :guard (and (nat-listp cids)
                              (nat-listp choice-lst))))
  (let ((__function__ 'create-count-alist))
    (declare (ignorable __function__))
    (if (endp cids)
        nil
      (b* ((cid (car cids))
           (count (acl2::duplicity cid choice-lst)))
        (cons (cons cid count)
              (create-count-alist (cdr cids)
                                  choice-lst))))))

Theorem: alistp-of-create-count-alist

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

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

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

Theorem: create-count-alist-of-cids=nil

(defthm create-count-alist-of-cids=nil
  (equal (create-count-alist nil x) nil))

Theorem: consp-of-create-count-alist

(defthm consp-of-create-count-alist
  (equal (consp (create-count-alist cids choice-lst))
         (consp cids)))

Theorem: consp-of-strip-cars-of-create-count-alist

(defthm consp-of-strip-cars-of-create-count-alist
  (implies (consp x)
           (consp (strip-cars (create-count-alist x y)))))

Theorem: consp-of-strip-cdrs-of-create-count-alist

(defthm consp-of-strip-cdrs-of-create-count-alist
  (implies (consp x)
           (consp (strip-cdrs (create-count-alist x y)))))

Theorem: strip-cars-of-create-count-alist-x-y-=-x

(defthm strip-cars-of-create-count-alist-x-y-=-x
  (implies (nat-listp x)
           (equal (strip-cars (create-count-alist x y))
                  x)))

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

(defthm strip-cars-of-create-count-alist-is-sorted-if-cids-is-sorted
  (implies (acl2::<-ordered-p cids)
           (acl2::<-ordered-p
                (strip-cars (create-count-alist cids choice-lst)))))

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

(defthm strip-cars-of-create-count-alist-equal-under-set-equiv
  (acl2::set-equiv (strip-cars (create-count-alist cids choice-lst))
                   cids))

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

(defthm no-duplicatesp-equal-of-strip-cars-of-create-count-alist
  (implies (no-duplicatesp-equal cids)
           (no-duplicatesp-equal
                (strip-cars (create-count-alist cids lst)))))

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

(defthm member-of-strip-cars-of-create-count-alist
  (b* ((count-alst (create-count-alist cids xs)))
    (implies (member-equal id cids)
             (member-equal id (strip-cars count-alst)))))

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

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

Theorem: upper-bound-of-duplicity

(defthm upper-bound-of-duplicity
  (<= (acl2::duplicity e x) (len x))
  :rule-classes (:linear :rewrite))

Theorem: len-of-create-count-alist

(defthm len-of-create-count-alist
  (equal (len (create-count-alist x y))
         (len x)))

Theorem: duplicity-is-a-member-of-strip-cdrs-count-alist

(defthm duplicity-is-a-member-of-strip-cdrs-count-alist
  (implies (member-equal e x)
           (member-equal (acl2::duplicity e y)
                         (strip-cdrs (create-count-alist x y)))))

Theorem: duplicity-e-y-is-the-val-of-e-in-count-alist

(defthm duplicity-e-y-is-the-val-of-e-in-count-alist
  (implies (member-equal e x)
           (equal (cdr (assoc-equal e (create-count-alist x y)))
                  (acl2::duplicity e y))))

Theorem: nat-listp-strip-cdrs-count-alist-of-choice-lst

(defthm nat-listp-strip-cdrs-count-alist-of-choice-lst
  (nat-listp (strip-cdrs (create-count-alist x y))))

Subtopics

Count-alistp

Recognizer for a count alist (see create-count-alist)