• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Prime-field-constraint-systems
    • Proof-checker-array
    • Soft
    • Rp-rewriter
    • Farray
    • 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
      • Irv-alt
      • Irv-ballot-p
      • Majority
      • Number-of-candidates
      • List-elements-equal
      • Number-of-voters
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Bigmem
    • Regex
    • ACL2-programming-language
    • Java
    • C
    • Jfkr
    • X86isa
    • Equational
    • Cryptography
    • Where-do-i-place-my-book
    • Json
    • Built-ins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Instant-runoff-voting

Eliminate-candidate

Eliminate candidate id from every voter's preference list in xs

Signature

(eliminate-candidate id xs) → *

Arguments

id — Candidate ID.
    Guard (natp id).

xs — Guard (irv-ballot-p xs).

Definitions and Theorems

Function: eliminate-candidate

(defun eliminate-candidate (id xs)
       (declare (xargs :guard (and (natp id) (irv-ballot-p xs))))
       (let ((__function__ 'eliminate-candidate))
            (declare (ignorable __function__))
            (if (endp xs)
                nil
                (b* ((one (car xs))
                     (rest (cdr xs))
                     (new-one (remove-equal id one))
                     (new-rest (eliminate-candidate id rest)))
                    (if (endp new-one)
                        new-rest (cons new-one new-rest))))))

Theorem: nat-listp-after-remove-equal

(defthm nat-listp-after-remove-equal
        (implies (nat-listp x)
                 (nat-listp (remove-equal val x))))

Theorem: irv-ballot-p-of-eliminate-candidate

(defthm irv-ballot-p-of-eliminate-candidate
        (implies (irv-ballot-p xs)
                 (b* ((new-xs (eliminate-candidate id xs)))
                     (irv-ballot-p new-xs))))

Theorem: eliminate-candidate-returns-a-subset-of-candidates

(defthm eliminate-candidate-returns-a-subset-of-candidates
        (subsetp-equal (candidate-ids (eliminate-candidate id xs))
                       (candidate-ids xs)))

Theorem: eliminate-candidate-removes-no-candidate-when-cid-not-in-candidates

(defthm
 eliminate-candidate-removes-no-candidate-when-cid-not-in-candidates
 (implies (and (irv-ballot-p xs)
               (not (member-equal id (candidate-ids xs))))
          (equal (eliminate-candidate id xs) xs)))

Theorem: eliminate-candidate-does-remove-a-candidate

(defthm
 eliminate-candidate-does-remove-a-candidate
 (implies
   (and (irv-ballot-p xs) (natp id))
   (equal (member-equal id
                        (candidate-ids (eliminate-candidate id xs)))
          nil)))

Theorem: eliminate-candidate-removes-only-the-requested-candidate

(defthm
 eliminate-candidate-removes-only-the-requested-candidate
 (implies
     (not (equal c1 c2))
     (iff (member-equal c2
                        (candidate-ids (eliminate-candidate c1 xs)))
          (member-equal c2 (candidate-ids xs)))))

Theorem: eliminate-candidate-reduces-the-number-of-candidates

(defthm
     eliminate-candidate-reduces-the-number-of-candidates
     (implies (and (irv-ballot-p xs)
                   (member-equal id (candidate-ids xs)))
              (< (number-of-candidates (eliminate-candidate id xs))
                 (number-of-candidates xs)))
     :rule-classes :linear)

Theorem: if-eliminate-candidate-reduced-the-number-of-candidates-then-id-was-a-candidate

(defthm
 if-eliminate-candidate-reduced-the-number-of-candidates-then-id-was-a-candidate
 (implies (and (irv-ballot-p xs)
               (< (number-of-candidates (eliminate-candidate id xs))
                  (number-of-candidates xs)))
          (member-equal id (candidate-ids xs))))

Theorem: remove-equal-and-append

(defthm remove-equal-and-append
        (equal (remove-equal id (append x y))
               (append (remove-equal id x)
                       (remove-equal id y))))

Theorem: remove-equal-of-<-insert-same-element

(defthm remove-equal-of-<-insert-same-element
        (equal (remove-equal e (acl2::<-insert e lst))
               (remove-equal e lst)))

Theorem: remove-equal-of-<-insert-different-element

(defthm remove-equal-of-<-insert-different-element
        (implies (and (not (equal e1 e2))
                      (acl2::<-ordered-p lst))
                 (equal (remove-equal e1 (acl2::<-insert e2 lst))
                        (acl2::<-insert e2 (remove-equal e1 lst)))))

Theorem: remove-equal-and-<-insertsort-commute

(defthm remove-equal-and-<-insertsort-commute
        (equal (acl2::<-insertsort (remove-equal id x))
               (remove-equal id (acl2::<-insertsort x))))

Theorem: candidate-ids-of-eliminate-candidate-is-remove-equal-of-candidate-ids

(defthm
 candidate-ids-of-eliminate-candidate-is-remove-equal-of-candidate-ids
 (equal (candidate-ids (eliminate-candidate id xs))
        (remove-equal id (candidate-ids xs))))

Theorem: eliminate-candidate-reduces-the-number-of-candidates-by-one

(defthm
  eliminate-candidate-reduces-the-number-of-candidates-by-one
  (implies (and (irv-ballot-p xs)
                (member-equal id (candidate-ids xs)))
           (equal (number-of-candidates (eliminate-candidate id xs))
                  (+ -1 (number-of-candidates xs)))))

Theorem: consp-of-eliminate-candidate

(defthm consp-of-eliminate-candidate
        (implies (and (irv-ballot-p xs)
                      (< 1 (number-of-candidates xs)))
                 (consp (eliminate-candidate id xs)))
        :rule-classes (:rewrite :type-prescription))

Theorem: number-of-voters-after-eliminate-candidate

(defthm number-of-voters-after-eliminate-candidate
        (implies (irv-ballot-p xs)
                 (<= (number-of-voters (eliminate-candidate id xs))
                     (number-of-voters xs)))
        :rule-classes (:rewrite :linear))