		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.