		Search-engine friendly clone of the ACL2 documentation.

Duplicity

(duplicity a x) counts how many times the element a occurs within the list x.

This function is much nicer to reason about than ACL2's built-in count function because it is much more limited:

count can operate on either strings or lists; duplicity only works on lists.
count can consider only some particular sub-range of its input; duplicity always considers the whole list.

Reasoning about duplicity is useful when trying to show two lists are permutations of one another (sometimes called multiset- or bag-equivalence). A classic exercise for new ACL2 users is to prove that a permutation function is symmetric. Hint: a duplicity-based argument may compare quite favorably to induction on the definition of permutation.

This function can also be useful when trying to establish no-duplicatesp, e.g., see no-duplicatesp-equal-same-by-duplicity.

Definitions and Theorems

Function: duplicity-exec

(defun duplicity-exec (a x n)
  (declare (xargs :guard (natp n)))
  (if (atom x)
      n
    (duplicity-exec a (cdr x)
                    (if (equal (car x) a) (+ 1 n) n))))

Function: duplicity

(defun duplicity (a x)
  (declare (xargs :guard t))
  (mbe :logic (cond ((atom x) 0)
                    ((equal (car x) a)
                     (+ 1 (duplicity a (cdr x))))
                    (t (duplicity a (cdr x))))
       :exec (duplicity-exec a x 0)))

Theorem: duplicity-exec-removal

(defthm duplicity-exec-removal
  (implies (natp n)
           (equal (duplicity-exec a x n)
                  (+ (duplicity a x) n))))

Theorem: duplicity-when-not-consp

(defthm duplicity-when-not-consp
  (implies (not (consp x))
           (equal (duplicity a x) 0)))

Theorem: duplicity-of-cons

(defthm duplicity-of-cons
  (equal (duplicity a (cons b x))
         (if (equal a b)
             (+ 1 (duplicity a x))
           (duplicity a x))))

Theorem: duplicity-of-list-fix

(defthm duplicity-of-list-fix
  (equal (duplicity a (list-fix x))
         (duplicity a x)))

Theorem: list-equiv-implies-equal-duplicity-2

(defthm list-equiv-implies-equal-duplicity-2
  (implies (list-equiv x x-equiv)
           (equal (duplicity a x)
                  (duplicity a x-equiv)))
  :rule-classes (:congruence))

Theorem: duplicity-of-append

(defthm duplicity-of-append
  (equal (duplicity a (append x y))
         (+ (duplicity a x) (duplicity a y))))

Theorem: duplicity-of-rev

(defthm duplicity-of-rev
  (equal (duplicity a (rev x))
         (duplicity a x)))

Theorem: duplicity-of-revappend

(defthm duplicity-of-revappend
  (equal (duplicity a (revappend x y))
         (+ (duplicity a x) (duplicity a y))))

Theorem: duplicity-of-reverse

(defthm duplicity-of-reverse
  (equal (duplicity a (reverse x))
         (duplicity a x)))

Theorem: duplicity-when-non-member-equal

(defthm duplicity-when-non-member-equal
  (implies (not (member-equal a x))
           (equal (duplicity a x) 0)))

Theorem: duplicity-when-member-equal

(defthm duplicity-when-member-equal
  (implies (member-equal a x)
           (< 0 (duplicity a x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: duplicity-zero-to-member-equal

(defthm duplicity-zero-to-member-equal
  (iff (equal 0 (duplicity a x))
       (not (member-equal a x))))

Theorem: no-duplicatesp-equal-when-high-duplicity

(defthm no-duplicatesp-equal-when-high-duplicity
  (implies (> (duplicity a x) 1)
           (not (no-duplicatesp-equal x))))

Theorem: duplicity-of-flatten-of-rev

(defthm duplicity-of-flatten-of-rev
  (equal (duplicity a (flatten (rev x)))
         (duplicity a (flatten x))))

Subtopics

Duplicity-badguy: (duplicity-badguy x) finds an element that occurs multiple times in the list x, if one exists.
No-duplicatesp-equal-same-by-duplicity: Proof strategy: show that a list satisfies no-duplicatesp-equal because it has no element whose duplicity is over 1.