primitives

(in-package "SET")

(include-book "misc/total-order" :dir :system)

(include-book "tools/rulesets" :dir :system)

(include-book "xdoc/top" :dir :system)

(set-verify-guards-eagerness 2)

(defxdoc primitives
  :parents (std/osets)
  :short "Replacements for @('car'), @('cdr'), etc., that respect the
<i>non-set convention</i>."
  :long "<p>Since the osets library uses ordered lists as the underlying
representation of sets, at some point we have to use <b>list
primitives</b> (car, cdr, endp, cons) to operate on sets.  A problem with using
these functions directly is that they do not follow the non-set convention.</p>

<p>The <b>non-set convention</b> is: set operations should treat improper
sets (i.e., non-@('nil') atoms and lists that have duplicated or mis-ordered
elements) as the empty set.  We adopt this convention throughout the library.
It allows most of our rewrite rules to have no @(see setp) hypotheses.</p>

<p>The primitive list functions do not follow the non-set convention.  For
instance:</p>

<ul>
 <li>@('(car '(1 1 1)) = 1'),            but @('(car nil) = nil')</li>
 <li>@('(cdr '(1 1 1)) = (1 1)'),        but @('(cdr nil) = nil')</li>
 <li>@('(cons 1 '(1 1 1)) = (1 1 1 1)'), but @('(cons 1 nil) = (1)')</li>
 <li>@('(endp '(1 1 1)) = nil'),         but @('(endp nil) = t')</li>
</ul>

<p>These behaviors make it harder to reason about set operations that are
written directly in terms of the list primitives.  When we try to do so, we
usually have to do lots of work to consider all the cases about whether the
inputs are ordered, etc.</p>

<p>To solve lots of these problems, we introduce new <b>set primitives</b> that
are mostly like the list primitives, except that they follow the non-set
convention.  These primitives are:</p>

<ul>
 <li>@('(head X)') - the first element of a set, nil for non/empty sets</li>
 <li>@('(tail X)') - all rest of the set, nil for non/empty sets</li>
 <li>@('(insert a X)') - ordered insert of @('a') into @('X')</li>
 <li>@('(emptyp X)') - recognizer for non/empty sets.</li>
</ul>

<p>The general idea is that set operations should be written in terms of these
set primitives instead of the list primitives, and the definitions of the set
primitives should be kept disabled to avoid having to reason about the low
level structure of sets.</p>")

(defsection setp
  :parents (primitives)
  :short "@(call setp) recognizes well-formed ordered sets."
  :long "<p>A proper ordered set is a @(see true-listp) whose elements are
fully ordered under @(see <<).  Note that this implicitly means that sets have
no duplicate elements.</p>

<p>Testing @('setp') is necessarily somewhat slow: we have to check that the
elements are in order.  Its cost is linear in the size of @('n').</p>"
  (defun setp
    (x)
    (declare (xargs :guard t :verify-guards nil))
    (if (atom x)
      (null x)
      (or (null (cdr x))
        (and (consp (cdr x))
          (fast-<< (car x) (cadr x))
          (setp (cdr x))))))
  (verify-guards setp
    :hints (("Goal" :in-theory (enable <<))))
  (defthm setp-type
    (or (equal (setp x) t)
      (equal (setp x) nil))
    :rule-classes :type-prescription)
  (defthmd sets-are-true-lists
    (implies (setp x) (true-listp x)))
  (defthm sets-are-true-lists-compound-recognizer
    (implies (setp x) (true-listp x))
    :rule-classes :compound-recognizer)
  (defthm sets-are-true-lists-cheap
    (implies (setp x) (true-listp x))
    :rule-classes ((:rewrite :backchain-limit-lst (1)))))

(defsection emptyp
  :parents (primitives)
  :short "@(call emptyp) recognizes empty sets."
  :long "<p>This function is like @(see endp) for lists, but it respects the
non-set convention and always returns true for ill-formed sets.</p>"
  (defun-inline emptyp
    (x)
    (declare (xargs :guard (setp x)))
    (mbe :logic (or (null x) (not (setp x)))
      :exec (null x)))
  (defthm emptyp-type
    (or (equal (emptyp x) t)
      (equal (emptyp x) nil))
    :rule-classes :type-prescription)
  (defthm nonempty-means-set
    (implies (not (emptyp x)) (setp x))))

(defthm empty-set-unique
  (implies (and (setp x)
      (setp y)
      (emptyp x)
      (emptyp y))
    (equal (equal x y) t)))

(defsection sfix
  :parents (primitives)
  :short "@(call sfix) is a fixing function for sets."
  :long "<p>We return any proper @(see setp) unchanged, but coerce any
non-@(see setp) into the empty set.</p>

<p>This does for sets what functions like @(see nfix) or @(see rfix) do for
numbers.  It is often useful to use @('sfix') in the base case of a set
operation to ensure that an ordered set is always produced.</p>"
  (defun-inline sfix
    (x)
    (declare (xargs :guard (setp x)))
    (mbe :logic (if (emptyp x)
        nil
        x)
      :exec x))
  (defthm sfix-produces-set
    (setp (sfix x)))
  (defthm sfix-set-identity
    (implies (setp x)
      (equal (sfix x) x)))
  (defthm sfix-when-emptyp
    (implies (emptyp x)
      (equal (sfix x) nil))))

(defthm emptyp-sfix-cancel
  (equal (emptyp (sfix x))
    (emptyp x)))

(xdoc-extend emptyp "@(def emptyp-sfix-cancel)")

(defsection head
  :parents (primitives)
  :short "@(call head) returns the smallest element in a set."
  :long "<p>This is like @(see car), but respects the non-set convention and
always returns @('nil') for ill-formed sets.</p>"
  (defun-inline head
    (x)
    (declare (xargs :guard (and (setp x) (not (emptyp x)))))
    (mbe :logic (car (sfix x))
      :exec (car x)))
  (defthm head-count
    (implies (not (emptyp x))
      (< (acl2-count (head x))
        (acl2-count x)))
    :rule-classes ((:rewrite) (:linear)))
  (defthm head-count-built-in
    (implies (not (emptyp x))
      (o< (acl2-count (head x))
        (acl2-count x)))
    :rule-classes :built-in-clause)
  (defthm head-when-emptyp
    (implies (emptyp x)
      (equal (head x) nil)))
  (defthm head-sfix-cancel
    (equal (head (sfix x)) (head x))))

(defsection tail
  :parents (primitives)
  :short "@(call tail) returns the remainder of a set after removing its @(see
head)."
  :long "<p>This is like @(see cdr), but respects the non-set convention and
always returns @('nil') for ill-formed sets.</p>"
  (defun-inline tail
    (x)
    (declare (xargs :guard (and (setp x) (not (emptyp x)))))
    (mbe :logic (cdr (sfix x))
      :exec (cdr x)))
  (defthm tail-count
    (implies (not (emptyp x))
      (< (acl2-count (tail x))
        (acl2-count x)))
    :rule-classes ((:rewrite) (:linear)))
  (defthm tail-count-built-in
    (implies (not (emptyp x))
      (o< (acl2-count (tail x))
        (acl2-count x)))
    :rule-classes :built-in-clause)
  (defthm tail-produces-set
    (setp (tail x)))
  (defthm tail-when-emptyp
    (implies (emptyp x)
      (equal (tail x) nil)))
  (defthm tail-sfix-cancel
    (equal (tail (sfix x)) (tail x))))

(defthmd head-tail-same
  (implies (and (equal (head x) (head y))
      (equal (tail x) (tail y))
      (not (emptyp x))
      (not (emptyp y)))
    (equal (equal x y) t)))

(defsection insert
  :parents (primitives)
  :short "@(call insert) adds the element @('a') to the set @('X')."
  :long "<p>This is the fundamental set constructor.  It is similar to @(see
cons) for lists, but of course performs an ordered insertion.  It respects the
non-set convention and treats any ill-formed input as the empty set.</p>

<p>Efficiency note.  Insert is @('O(n)').  It is very inefficient to call it
repeatedly.  Instead, consider building sets with @(see mergesort) or out of
other sets using @(see union).</p>

<p>The :exec version just inlines the set primitives and does one level of loop
unrolling.  On CCL, it runs about 1.65x faster than the :logic version on the
following loop:</p>

@({
 ;; 1.92 seconds :logic, 1.16 seconds :exec
 (let ((acc nil))
  (gc$)
  (time$ (loop for i fixnum from 1 to 10000 do
               (setq acc (set::insert i acc)))))
})"
  (local (in-theory (disable nonempty-means-set
        empty-set-unique
        head-when-emptyp
        tail-when-emptyp
        sfix-when-emptyp
        default-car
        default-cdr)))
  (defun insert
    (a x)
    (declare (xargs :guard (setp x) :verify-guards nil))
    (mbe :logic (cond ((emptyp x) (list a))
        ((equal (head x) a) x)
        ((<< a (head x)) (cons a x))
        (t (cons (head x)
            (insert a (tail x)))))
      :exec (cond ((null x) (cons a nil))
        ((equal (car x) a) x)
        ((fast-lexorder a (car x)) (cons a x))
        ((null (cdr x)) (cons (car x) (cons a nil)))
        ((equal (cadr x) a) x)
        ((fast-lexorder a (cadr x)) (cons (car x) (cons a (cdr x))))
        (t (cons (car x)
            (cons (cadr x) (insert a (cddr x))))))))
  (verify-guards insert
    :hints (("Goal" :in-theory (e/d (<<)
         (<<-trichotomy <<-implies-lexorder)))))
  (defthm insert-produces-set
    (setp (insert a x)))
  (defthm insert-sfix-cancel
    (equal (insert a (sfix x))
      (insert a x)))
  (defthm insert-never-empty
    (not (emptyp (insert a x))))
  (defthm insert-when-emptyp
    (implies (and (syntaxp (not (equal x ''nil)))
        (emptyp x))
      (equal (insert a x) (insert a nil))))
  (defthm head-of-insert-a-nil
    (equal (head (insert a nil)) a))
  (defthm tail-of-insert-a-nil
    (equal (tail (insert a nil)) nil))
  (defthm head-insert
    (equal (head (insert a x))
      (cond ((emptyp x) a)
        ((<< a (head x)) a)
        (t (head x)))))
  (defthm tail-insert
    (equal (tail (insert a x))
      (cond ((emptyp x) nil)
        ((<< a (head x)) x)
        ((equal a (head x)) (tail x))
        (t (insert a (tail x))))))
  (encapsulate nil
    (local (defthm l0
        (implies (and (not (<< y x)) (not (equal x y)))
          (<< x y))
        :rule-classes ((:rewrite :backchain-limit-lst 0))))
    (local (defthm l1
        (implies (<< x y)
          (not (<< y x)))
        :rule-classes ((:rewrite :backchain-limit-lst 0))))
    (local (in-theory (disable sfix-set-identity
          insert-when-emptyp
          (:definition insert)
          <<-trichotomy
          <<-asymmetric)))
    (local (defthm l2
        (implies (and (<< b (car x)) (setp x))
          (equal (cons b (insert (car x) x))
            (insert b (insert (car x) x))))
        :rule-classes ((:rewrite :backchain-limit-lst 0))
        :hints (("Goal" :expand ((:free (x) (insert b x)))))))
    (local (defthm l3
        (implies (and (<< b (car l))
            (not (equal b a))
            (not (<< a b)))
          (<< b (car (insert a l))))
        :rule-classes ((:rewrite :backchain-limit-lst 0))
        :hints (("goal" :expand (insert a l)))))
    (local (in-theory (disable head-insert tail-insert)))
    (defthm repeated-insert
      (equal (insert a (insert a x))
        (insert a x))
      :hints (("Goal" :induct t
         :expand ((insert a nil) (insert a x)
           (insert (car x) x)
           (:free (k1 k2)
             (insert a (cons k1 k2)))))))
    (defthm insert-insert
      (equal (insert a (insert b x))
        (insert b (insert a x)))
      :rule-classes ((:rewrite :loop-stopper ((a b))))
      :hints (("Goal" :induct t
         :expand ((insert a x) (insert b x)
           (:free (k1) (insert k1 nil))
           (:free (k1 k2 k3)
             (insert k1 (cons k2 k3))))))))
  (defthm insert-head
    (implies (not (emptyp x))
      (equal (insert (head x) x) x)))
  (defthm insert-head-tail
    (implies (not (emptyp x))
      (equal (insert (head x) (tail x))
        x)))
  (defthm insert-induction-case
    (implies (and (not (<< a (head x)))
        (not (equal a (head x)))
        (not (emptyp x)))
      (equal (insert (head x)
          (insert a (tail x)))
        (insert a x)))))

(defthm head-tail-order
  (implies (not (emptyp (tail x)))
    (<< (head x) (head (tail x)))))

(defthm head-tail-order-contrapositive
  (implies (not (<< (head x) (head (tail x))))
    (emptyp (tail x))))

(defthm head-not-head-tail
  (implies (not (emptyp (tail x)))
    (not (equal (head x) (head (tail x))))))

(def-ruleset primitive-rules
  '(setp emptyp
    head
    tail
    sfix
    insert))

(def-ruleset order-rules
  '(<<-irreflexive <<-transitive
    <<-asymmetric
    <<-trichotomy
    <<-implies-lexorder
    (:induction insert)
    insert-induction-case
    head-insert
    tail-insert
    head-tail-order
    head-tail-order-contrapositive))

(in-theory (disable (:ruleset primitive-rules)
    (:ruleset order-rules)))