uniquep

(in-package "ACL2")

(defsort :compare< << :prefix <<)

(define no-adjacent-duplicates-p
  (x)
  :parents (uniquep)
  (cond ((atom x) t)
    ((atom (cdr x)) t)
    (t (and (not (equal (car x) (cadr x)))
        (no-adjacent-duplicates-p (cdr x))))))

(define uniquep
  (x)
  :parents (no-duplicatesp)
  :short "Sometimes better than @(see no-duplicatesp): first sorts the list and
then looks for adjacent duplicates."
  :long "<p>@(call uniquep) is provably equal to @('(no-duplicatesp x)'), but
has different performance characteristics.  It operates by sorting its argument
and then scanning for adjacent duplicates.</p>

<p>Note: we leave this function enabled.  You should never write a theorem
about @('uniquep').  Reason about @(see no-duplicatesp) instead.</p>

<p>Since we use a mergesort, the complexity of @('uniquep') is @('O(n log n)').
By comparison, @('no-duplicatesp') is @('O(n^2)').</p>

<p>It is not always better to use @('uniquep') than @('no-duplicatesp'):</p>

<ul>

<li>It uses far more memory than @('no-duplicatesp') because it sorts the
list.</li>

<li>On a list with lots of duplicates, @('no-duplicatesp') may find a duplicate
very quickly and stop early, but @('uniquep') has to sort the whole list before
it looks for any duplicates.</li>

</ul>

<p>However, if your lists are sometimes long with few duplicates, @('uniquep')
is probably a much better function to use.</p>"
  :inline t
  :enabled t
  (mbe :logic (no-duplicatesp x)
    :exec (no-adjacent-duplicates-p (<<-sort x)))
  :prepwork ((local (defthm lemma
       (implies (<<-ordered-p x)
         (equal (no-adjacent-duplicates-p x) (no-duplicatesp x)))
       :hints (("Goal" :in-theory (enable no-duplicatesp
            no-adjacent-duplicates-p
            <<-ordered-p)))))))