• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Remove-duplicates

Hons-remove-duplicates

(hons-remove-duplicates l) removes duplicate elements from a list, and is implemented using fast-alists.

This operation is similar to the built-in ACL2 function remove-duplicates-equal, but it has different performance characteristics and the answer it produces is in an oddly different order.

ACL2's remove-duplicates function preserves the order of non-duplicated elements but has a rather inefficient O(n^2) implementation: it walks down the list, checking for each element whether there are any more occurrences of the element in the tail of the list.

In contrast, hons-remove-duplicates is a tail-recursive function that uses a fast alist to record the elements that have been seen so far. This is effectively O(n) if we assume that hashing is constant time. Note, however. that this approach requires us to hons the elements in the list, which may be quite expensive if the list contains large structures.

Another reasonably efficient way to remove duplicate elements from a list include sorting the elements, e.g., via set::mergesort.

In the special case of removing duplicates from lists of natural numbers, nat-list-remove-duplicates may be offer superior performance.

Even though hons-remove-duplicates has a reasonably nice logical definition that is merely in terms of remove-duplicates-equal and rev, we leave it disabled by default and go ahead and prove various theorems about it. These theorems are perhaps best regarded as a back-up plan. In general, you may often be able to avoid reasoning about hons-remove-duplicates via the following, strong set-equiv rule:

Theorem: hons-remove-duplicates-under-set-equiv

(defthm hons-remove-duplicates-under-set-equiv
        (set-equiv (hons-remove-duplicates x)
                   (remove-duplicates-equal x)))

Definitions and Theorems

Function: hons-remove-duplicates1

(defun
 hons-remove-duplicates1 (l tab)
 (declare (xargs :guard t))
 (cond
   ((atom l)
    (progn$ (fast-alist-free tab) nil))
   ((hons-get (car l) tab)
    (hons-remove-duplicates1 (cdr l) tab))
   (t (cons (car l)
            (hons-remove-duplicates1 (cdr l)
                                     (hons-acons (car l) t tab))))))

Function: hons-remove-duplicates

(defun hons-remove-duplicates (l)
       (declare (xargs :guard t))
       (mbe :logic (rev (remove-duplicates-equal (rev l)))
            :exec (hons-remove-duplicates1 l (len l))))

Theorem: hons-remove-duplicates-when-atom

(defthm hons-remove-duplicates-when-atom
        (implies (atom x)
                 (equal (hons-remove-duplicates x) nil)))

Theorem: hons-remove-duplicates-of-list-fix

(defthm hons-remove-duplicates-of-list-fix
        (equal (hons-remove-duplicates (list-fix x))
               (hons-remove-duplicates x)))

Theorem: list-equiv-implies-equal-hons-remove-duplicates-1

(defthm list-equiv-implies-equal-hons-remove-duplicates-1
        (implies (list-equiv x x-equiv)
                 (equal (hons-remove-duplicates x)
                        (hons-remove-duplicates x-equiv)))
        :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-hons-remove-duplicates-1

(defthm set-equiv-implies-set-equiv-hons-remove-duplicates-1
        (implies (set-equiv x x-equiv)
                 (set-equiv (hons-remove-duplicates x)
                            (hons-remove-duplicates x-equiv)))
        :rule-classes (:congruence))

Theorem: hons-remove-duplicates-under-set-equiv

(defthm hons-remove-duplicates-under-set-equiv
        (set-equiv (hons-remove-duplicates x)
                   (remove-duplicates-equal x)))

Theorem: no-duplicatesp-equal-of-hons-remove-duplicates

(defthm no-duplicatesp-equal-of-hons-remove-duplicates
        (no-duplicatesp-equal (hons-remove-duplicates x)))

Theorem: duplicity-in-of-hons-remove-duplicates

(defthm duplicity-in-of-hons-remove-duplicates
        (equal (duplicity a (hons-remove-duplicates x))
               (if (member a x) 1 0)))

Theorem: hons-remove-duplicates1-of-nil

(defthm hons-remove-duplicates1-of-nil
        (equal (hons-remove-duplicates1 x nil)
               (hons-remove-duplicates x)))

Theorem: acl2-count-of-hons-remove-duplicates

(defthm acl2-count-of-hons-remove-duplicates
        (<= (acl2-count (hons-remove-duplicates x))
            (acl2-count x))
        :rule-classes ((:rewrite) (:linear)))