• 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
      • 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

• 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))