membership

(in-package "SET")

(include-book "primitives")

(include-book "computed-hints")

(set-verify-guards-eagerness 2)

(defsection in
  :parents (std/osets)
  :short "@(call in) determines if @('a') is a member of the set @('X')."
  :long "<p>The logical definition of @('in') makes no mention of the set
order, except implicitly by the use of the set @(see primitives) like @(see
head) and @(see tail).</p>

<p>The :exec version just inlines the set primitives and does one level of loop
unrolling.  On CCL, it seems to run about 2.6x faster on the following
loop:</p>

@({
 ;; 4.703 sec logic, 1.811 sec exec
 (let ((big-set (loop for i from 1 to 100000 collect i)))
   (gc$)
   (time (loop for i fixnum from 1 to 30000 do (set::in i big-set))))
})

<p>There are other ways we could optimize @('in').  Since the set is ordered,
we could try to use the set order @(see <<) to stop early when we ran into an
element that is larger than the one we are looking for.  For instance, when
looking for 1 in the set '(2 3 4), we know that since @('1 << 2') that @('1')
cannot be a member of this set.</p>

<p>The simplest way to do this is to use @('<<') at every element.  But set
order comparisons can be very expensive, especially when sets contain large
cons structures.  So while it is easy to contrive situations where exploiting
the order would be advantageous, like</p>

@({
 (in 1 '(2 3 4 .... 100000))
})

<p>where we could return instantly, there are also times where it would be
slower.  For instance, on</p>

@({
 (in 100001 '(1 2 3 4 ... 100000))
})

<p>we would incur the extra cost of 100,000 calls to @('<<').</p>

<p>For this reason, we do not currently implement any short-circuiting.  The
reasoning is:</p>

<ul>

<li>it is not clear which would be faster in all cases,</li>

<li>it is not clear what the typical usage behavior of @('in') is, so even if
we wanted to benchmark alternate implementations, it may be hard to come up
with the right benchmarking suite</li>

<li>both solutions are O(n) anyway, and @('in') isn't a function that should
probably be used in any kind of loop so its performance shouldn't be especially
critical to anything</li>

<li>the current method is arguably no less efficient than an unordered
implementation.</li>

</ul>

<p>Future note.  In principle membership in an ordered list might be done in
@('O(log_2 n)').  We are considering using a <i>galloping</i> membership check
in the future to obtain something along these lines.</p>"
  (defun in
    (a x)
    (declare (xargs :guard (setp x) :verify-guards nil))
    (mbe :logic (and (not (emptyp x))
        (or (equal a (head x))
          (in a (tail x))))
      :exec (and x
        (or (equal a (car x))
          (and (cdr x)
            (or (equal a (cadr x))
              (in a (cddr x))))))))
  (verify-guards in
    :hints (("Goal" :in-theory (enable (:ruleset primitive-rules)))))
  (defthm in-type
    (or (equal (in a x) t)
      (equal (in a x) nil))
    :rule-classes :type-prescription)
  (encapsulate nil
    (local (defthm head-not-whole
        (implies (not (emptyp x))
          (not (equal (head x) x)))
        :hints (("Goal" :in-theory (enable (:ruleset primitive-rules))))))
    (local (defthm lemma
        (implies (> (acl2-count x) (acl2-count y))
          (not (in x y)))))
    (defthm not-in-self (not (in x x))))
  (defthm in-sfix-cancel
    (equal (in a (sfix x))
      (in a x)))
  (defthm never-in-empty
    (implies (emptyp x)
      (not (in a x))))
  (defthm in-set
    (implies (in a x) (setp x)))
  (defthm in-tail
    (implies (in a (tail x))
      (in a x)))
  (defthm in-tail-or-head
    (implies (and (in a x)
        (not (in a (tail x))))
      (equal (head x) a)))
  (defthm in-head
    (equal (in (head x) x)
      (not (emptyp x)))))

(defsection head-unique
  :extension head
  (local (defthm lemma
      (implies (and (not (emptyp x))
          (not (equal a (head x)))
          (not (<< a (head (tail x))))
          (<< a (head x)))
        (not (in a x)))
      :hints (("Goal" :in-theory (enable (:ruleset order-rules))
         :cases ((emptyp (tail x)))))))
  (defthm head-minimal
    (implies (<< a (head x))
      (not (in a x)))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules)))))
  (defthm head-minimal-2
    (implies (in a x)
      (not (<< a (head x)))))
  (add-to-ruleset order-rules
    '(head-minimal head-minimal-2))
  (local (defthm lemma2
      (implies (emptyp (tail x))
        (not (in (head x) (tail x))))))
  (local (defthm lemma3
      (implies (not (emptyp (tail x)))
        (not (in (head x) (tail x))))
      :hints (("Goal" :in-theory (enable (:ruleset order-rules))))))
  (defthm head-unique
    (not (in (head x) (tail x)))
    :hints (("Goal" :use ((:instance lemma2) (:instance lemma3))))))

(defsection in-insert
  :extension insert
  (defthm insert-identity
    (implies (in a x)
      (equal (insert a x) x))
    :hints (("Goal" :in-theory (enable head-tail-same
         (:ruleset order-rules)))))
  (defthm in-insert
    (equal (in a (insert b x))
      (or (in a x) (equal a b)))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules))
       :induct (insert b x)))))

(defsection weak-insert-induction
  :parents (insert)
  :short "Inducting over insert without exposing the set order."
  :long "<p>When we want to insert an element into an ordered set, the set
order obviously has to be involved so that we can decide where to put the new
element.  Accordingly, the set order plays a role in the induction scheme that
we get from @(see insert)'s definition.  This makes insert somewhat different
than other set operations (membership, union, cardinality, etc.) that just use
a simple @(see tail)-based induction, where the set order is already hidden by
@('tail').</p>

<p>When we are proving theorems about sets, we generally want to avoid thinking
about the set order, but we sometimes need to induct over @('insert').  So,
here we introduce a new induction scheme that allows us to induct over insert
but hides the set order.  We disable the ordinary induction scheme that insert
uses, and set up an induction hint so that @('weak-insert-induction') will
automatically be used instead.</p>"
  (defthm weak-insert-induction-helper-1
    (implies (and (not (in a x))
        (not (equal (head (insert a x)) a)))
      (equal (head (insert a x))
        (head x)))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules)))))
  (defthm weak-insert-induction-helper-2
    (implies (and (not (in a x))
        (not (equal (head (insert a x)) a)))
      (equal (tail (insert a x))
        (insert a (tail x))))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules)))))
  (defthm weak-insert-induction-helper-3
    (implies (and (not (in a x))
        (equal (head (insert a x)) a))
      (equal (tail (insert a x))
        (sfix x)))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules)))))
  (defun weak-insert-induction
    (a x)
    (declare (xargs :guard (setp x)))
    (cond ((emptyp x) nil)
      ((in a x) nil)
      ((equal (head (insert a x)) a) nil)
      (t (list (weak-insert-induction a (tail x))))))
  (in-theory (disable (:induction insert)))
  (defthm use-weak-insert-induction
    t
    :rule-classes ((:induction :pattern (insert a x)
       :scheme (weak-insert-induction a x)))))

(defsection subset
  :parents (std/osets)
  :short "@(call subset) determines if @('X') is a subset of @('Y')."
  :long "<p>We use a logically simple definition, but using MBE we exploit the
set order to implement a tail-recursive, linear subset check.</p>

<p>The :exec version of fast-subset just inlines the set primitives and tweaks
the way the order check is done.  It is about 3x faster than the :logic version
of fast-subset on the following loop:</p>

@({
 ;; 3.83 sec logic, 1.24 seconds exec
 (let ((x (loop for i from 1 to 1000 collect i)))
   (gc$)
   (time$ (loop for i fixnum from 1 to 100000 do (set::subset x x))))
})

<p>In the future we may investigate developing a faster subset check based on
galloping.</p>"
  (defun fast-subset
    (x y)
    (declare (xargs :guard (and (setp x) (setp y))
        :guard-hints (("Goal" :in-theory (enable (:ruleset primitive-rules) <<)))))
    (mbe :logic (cond ((emptyp x) t)
        ((emptyp y) nil)
        ((<< (head x) (head y)) nil)
        ((equal (head x) (head y)) (fast-subset (tail x) (tail y)))
        (t (fast-subset x (tail y))))
      :exec (cond ((null x) t)
        ((null y) nil)
        ((fast-lexorder (car x) (car y)) (and (equal (car x) (car y))
            (fast-subset (cdr x) (cdr y))))
        (t (fast-subset x (cdr y))))))
  (defun-inline subset
    (x y)
    (declare (xargs :guard (and (setp x) (setp y))
        :verify-guards nil))
    (mbe :logic (if (emptyp x)
        t
        (and (in (head x) y)
          (subset (tail x) y)))
      :exec (fast-subset x y)))
  (defthm subset-type
    (or (equal (subset x y) t)
      (equal (subset x y) nil))
    :rule-classes :type-prescription)
  (encapsulate nil
    (local (defthmd lemma
        (implies (not (in (head y) x))
          (equal (subset x y)
            (subset x (tail y))))))
    (local (defthm case-1
        (implies (and (not (emptyp x))
            (not (emptyp y))
            (not (<< (head x) (head y)))
            (not (equal (head x) (head y)))
            (implies (and (setp x) (setp (tail y)))
              (equal (fast-subset x (tail y))
                (subset x (tail y)))))
          (implies (and (setp x) (setp y))
            (equal (fast-subset x y)
              (subset x y))))
        :hints (("Goal" :in-theory (enable (:ruleset order-rules))
           :use (:instance lemma)))))
    (local (defthm case-2
        (implies (and (not (emptyp x))
            (not (emptyp y))
            (not (<< (head x) (head y)))
            (equal (head x) (head y))
            (implies (and (setp (tail x))
                (setp (tail y)))
              (equal (fast-subset (tail x) (tail y))
                (subset (tail x) (tail y)))))
          (implies (and (setp x) (setp y))
            (equal (fast-subset x y)
              (subset x y))))
        :hints (("Goal" :in-theory (enable (:ruleset order-rules))
           :use (:instance lemma (x (tail x)))))))
    (local (defthm fast-subset-equivalence
        (implies (and (setp x) (setp y))
          (equal (fast-subset x y)
            (subset x y)))
        :hints (("Goal" :in-theory (enable (:ruleset order-rules))
           :induct (fast-subset x y)))))
    (verify-guards subset$inline)))

(defsection all-by-membership
  :parents (std/osets)
  :short "A way to quantify over sets."
  :long "<p>@('all-by-membership') is a generic theorem that can be used to
prove that a property holds of a set by showing that a related property holds
of the set elements.</p>

<p>The most important role of @('all-by-membership') is to allow for
pick-a-point proofs of @(see subset).  That is, it allows us to show that
@('(subset X Y)') holds by showing that every element of X satisfies @('(in a
Y)').</p>

<p>More generally, we could show that a set satisfies a predicate like
@('integer-setp') because each of its elements satisfies @('integerp').</p>


<h3>Pick-a-Point Proofs in ACL2</h3>

<p>We begin by explaining how pick-a-point proofs of subset can be carried out.
In traditional mathematics, @(see subset) is defined using quantification over
members, e.g., as follows:</p>

@({
  (equal (subset X Y)
         (forall a (implies (in a X) (in a Y))))
})

<p>This definition is very useful for <b>pick-a-point</b> proofs that some set
@('X') is a subset of @('Y').  Such a proof begins by picking an arbitrary
point @('a') that is a member of @('X').  Then, if we can show that @('a') must
be a member of @('Y'), we have established @('(subset X Y)').</p>

<p>These kinds of arguments are extremely useful, and we would like to be able
to carry them out in ACL2 about osets.  But since ACL2 does not have explicit
quantifiers, we cannot even write a theorem like this:</p>

@({
 (implies (forall a (implies (in a X) (in a Y)))
          (subset X Y))
})

<p>But consider the contrapositive of this theorem:</p>

@({
 (implies (not (subset X Y))
          (exists a (and (in a X) (not (in a Y)))))
})

<p>We <i>can</i> prove something like this, by writing an explicit function to
search for an element of @('X') that is not an element of @('Y').  That is, we
can prove:</p>

@({
 (implies (not (subset X Y))
          (let ((a (find-witness X Y)))
            (and (in a X)
                 (not (in a Y)))))
})

<p>Once we prove the above, we still need to be able to "reduce" a proof of
@('(subset X Y)') to a proof of @('(implies (in a X) (in a Y))').  While we
can't do this with a direct rewrite rule, we can sort of fake it using
functional instantiation.  As groundwork:</p>

<ul>

<li>Using @(see encapsulate), we introduce functions @('sub') and @('super')
with the constraint that @({
 (implies (in a (sub))
          (in a (super)))
})</li>

<li>Using this constraint, we prove the generic theorem:
@({
 (subset (sub) (super))
})</li>

</ul>

<p>Then, when we want to prove @('(subset X Y)') for some particular @('X') and
@('Y'), we can functionally instantiate the generic theorem with</p>

@({
   sub   <-- (lambda () X)
   super <-- (lambda () Y)
})

<p>And this allows us to prove @('(subset X Y)') as long as we can relieve the
constraint, i.e., @('(implies (in a X) (in a Y))').</p>


<h3>Generalizing Pick-a-Point Proofs</h3>

<p>In earlier versions of the osets library, we used an explicit argument to
reduce subset proofs to pick-a-point style membership arguments.  But we later
generalized the approach to arbitrary predicates instead.</p>

<p>First, notice that if you let the predicate @('(P a)') be defined as @('(in
a Y)'), then @('(subset X Y)') is just</p>

@({
 (forall a (implies (in a X) (P a)))
})

<p>Our generalization basically lets you reduce a proof of @('(P-setp X)') to a
proof of @('(implies (in a X) (P a))'), for an arbitrary predicate @('P').
This can be used to prove subset by just chooisng @('P') as described above,
but it can also be used for many other ideas by just changing the meaning of
@('P').  For instance, if @('P') is @(see integerp), then we can show that
@('X') is an @('integer-setp') or similar.</p>

<p>The mechanism is just an adaptation of that described in the previous
section.</p>

<ul>

<li>We begin by introducing a completely arbitrary @('predicate').</li>

<li>Based on @('predicate'), we introduce a new function, @('all'), which
checks to see if every member in a set satisfies @('predicate').</li>

<li>We set up an encapsulate which allows us to assume that some hypotheses are
true and that any member of some set satisfies @('predicate').</li>

</ul>

<p>Finally, we prove @('all-by-membership'), which shows that under these
assumptions, the set satisfies @('all').  This theorem can be functionally
instantiated to reduce a proof of @('(all X)') to a proof of</p>

@({
  (implies (in a X) (P a))
})"
  (encapsulate (((predicate *) => *))
    (local (defun predicate (x) x)))
  (defun all
    (set-for-all-reduction)
    (declare (xargs :guard (setp set-for-all-reduction)))
    (if (emptyp set-for-all-reduction)
      t
      (and (predicate (head set-for-all-reduction))
        (all (tail set-for-all-reduction)))))
  (encapsulate (((all-hyps) => *) ((all-set) => *))
    (local (defun all-hyps nil nil))
    (local (defun all-set nil nil))
    (defthmd membership-constraint
      (implies (all-hyps)
        (implies (in arbitrary-element (all-set))
          (predicate arbitrary-element)))))
  (local (defun find-not
      (x)
      (declare (xargs :guard (setp x)))
      (cond ((emptyp x) nil)
        ((not (predicate (head x))) (head x))
        (t (find-not (tail x))))))
  (local (defthm lemma-find-not-is-a-witness
      (implies (not (all x))
        (and (in (find-not x) x)
          (not (predicate (find-not x)))))))
  (defthmd all-by-membership
    (implies (all-hyps) (all (all-set)))
    :hints (("Goal" :use (:instance membership-constraint
         (arbitrary-element (find-not (all-set))))))))

(defsection pick-a-point-subset-strategy
  :parents (std/osets)
  :short "Automatic pick-a-point proofs of @(see subset)."
  :long "<p>The rewrite rule @('pick-a-point-subset-strategy') tries to
automatically reduce proof goals such as:</p>

@({
 (implies hyps
          (subset X Y))
})

<p>To proofs of:</p>

@({
 (implies (and hyps (in a X))
          (in a Y))
})

<p>The mechanism for doing this is somewhat elaborate: the rewrite rule
replaces the @('(subset X Y)') with @('(subset-trigger X Y)').  This trigger is
recognized by a computed hint, which then suggests proving the theorem via
functional instantiation of @(see all-by-membership).</p>

<p>The pick-a-point method is often a good way to prove subset relations.  On
the other hand, this rule is very heavy-handed, and you may need to disable it
if you do not want to use the pick-a-point method to solve your goal.</p>"
  (defun subset-trigger
    (x y)
    (declare (xargs :guard (and (setp x) (setp y))))
    (subset x y))
  (defthm pick-a-point-subset-strategy
    (implies (and (syntaxp (rewriting-goal-lit mfc state))
        (syntaxp (rewriting-conc-lit `(subset$inline ,SET::X ,SET::Y)
            mfc
            state)))
      (equal (subset x y)
        (subset-trigger x y))))
  (in-theory (disable subset-trigger))
  (automate-instantiation :new-hint-name pick-a-point-subset-hint
    :generic-theorem all-by-membership
    :generic-predicate predicate
    :generic-hyps all-hyps
    :generic-collection all-set
    :generic-collection-predicate all
    :actual-collection-predicate subset
    :actual-trigger subset-trigger
    :predicate-rewrite (((predicate ?x ?y) (in ?x ?y)))
    :tagging-theorem pick-a-point-subset-strategy)
  (defthm pick-a-point-subset-constraint-helper
    (implies (syntaxp (equal set-for-all-reduction
          'set-for-all-reduction))
      (equal (subset set-for-all-reduction rhs)
        (cond ((emptyp set-for-all-reduction) t)
          ((in (head set-for-all-reduction) rhs) (subset (tail set-for-all-reduction)
              rhs))
          (t nil))))))

(defsection subset-theorems
  :extension subset
  (defthm subset-sfix-cancel-x
    (equal (subset (sfix x) y)
      (subset x y)))
  (defthm subset-sfix-cancel-y
    (equal (subset x (sfix y))
      (subset x y)))
  (defthm emptyp-subset
    (implies (emptyp x)
      (subset x y)))
  (defthm emptyp-subset-2
    (implies (emptyp y)
      (equal (subset x y) (emptyp x))))
  (defthm subset-in
    (and (implies (and (subset x y) (in a x))
        (in a y))
      (implies (and (in a x) (subset x y))
        (in a y))))
  (defthm subset-in-2
    (and (implies (and (subset x y)
          (not (in a y)))
        (not (in a x)))
      (implies (and (not (in a y))
          (subset x y))
        (not (in a x)))))
  (encapsulate nil
    (local (defthm l0
        (equal (subset (insert a nil) y)
          (in a y))
        :hints (("Goal" :in-theory (enable (:ruleset primitive-rules))))))
    (defthm subset-insert-x
      (equal (subset (insert a x) y)
        (and (subset x y) (in a y)))
      :hints (("Goal" :induct (insert a x)))))
  (defthm subset-reflexive
    (subset x x))
  (defthm subset-transitive
    (and (implies (and (subset x y)
          (subset y z))
        (subset x z))
      (implies (and (subset y z)
          (subset x y))
        (subset x z))))
  (defthm subset-membership-tail
    (implies (and (subset x y)
        (in a (tail x)))
      (in a (tail y)))
    :hints (("Goal" :in-theory (enable (:ruleset order-rules)))))
  (defthm subset-membership-tail-2
    (implies (and (subset x y)
        (not (in a (tail y))))
      (not (in a (tail x))))
    :hints (("Goal" :in-theory (disable subset-membership-tail)
       :use (:instance subset-membership-tail))))
  (defthm subset-insert
    (subset x (insert a x)))
  (defthm subset-tail
    (subset (tail x) x)
    :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tail x))))))

(defsection double-containment
  :parents (std/osets)
  :short "A strategy for proving sets are equal because they are subsets
of one another."
  :long "<p>Double containment can be a good way to prove that two sets are
equal to one another.</p>

<p>Unfortunately, because this rule targets @('equal') it can get quite
expensive.  You may sometimes wish to disable it to speed up your proofs, as
directed by @(see accumulated-persistence).  In fact, this rule is disabled
when importing @('[books]/std/osets/top.lisp'). To reduce its cost when enabled,
this rule has a backchain limit.</p>

<p>On the other hand, there are cases in which this rule works well, and where
the backchain limit is detrimental.  For this reason, we also provide a version
of the rule that has no backchain limit.  This version can be enabled
as needed.</p>"
  (local (defthmd double-containment-lemma-head
      (implies (and (subset x y)
          (subset y x))
        (equal (head x) (head y)))
      :hints (("Goal" :in-theory (enable (:ruleset order-rules))))))
  (local (defthmd in-tail-expand
      (equal (in a (tail x))
        (and (in a x)
          (not (equal a (head x)))))))
  (local (defthmd double-containment-lemma-in-tail
      (implies (and (subset x y)
          (subset y x))
        (implies (in a (tail x))
          (in a (tail y))))
      :hints (("Goal" :in-theory (enable (:ruleset order-rules))
         :use ((:instance in-tail-expand
            (a a)
            (x x)) (:instance in-tail-expand
             (a a)
             (x y)))))))
  (local (defthmd double-containment-lemma-tail
      (implies (and (subset x y)
          (subset y x))
        (subset (tail x) (tail y)))
      :hints (("Goal" :in-theory (enable double-containment-lemma-in-tail)))))
  (local (defun double-tail-induction
      (x y)
      (declare (xargs :guard (and (setp x) (setp y))))
      (if (or (emptyp x) (emptyp y))
        (list x y)
        (double-tail-induction (tail x)
          (tail y)))))
  (local (defthm double-containment-is-equality-lemma
      (implies (and (not (or (emptyp x) (emptyp y)))
          (implies (and (subset (tail x) (tail y))
              (subset (tail y) (tail x)))
            (equal (equal (tail x) (tail y)) t))
          (setp x)
          (setp y)
          (subset x y)
          (subset y x))
        (equal (equal x y) t))
      :hints (("Goal" :in-theory (enable head-tail-same)
         :use ((:instance double-containment-lemma-tail
            (x x)
            (y y)) (:instance double-containment-lemma-tail
             (x y)
             (y x))
           (:instance double-containment-lemma-head
             (x x)
             (y y)))))))
  (local (defthmd double-containment-is-equality
      (implies (and (setp x)
          (setp y)
          (subset x y)
          (subset y x))
        (equal (equal x y) t))
      :hints (("Goal" :in-theory (enable head-tail-same)
         :induct (double-tail-induction x y)))))
  (defthm double-containment
    (implies (and (setp x) (setp y))
      (equal (equal x y)
        (and (subset x y)
          (subset y x))))
    :rule-classes ((:rewrite :backchain-limit-lst 1))
    :hints (("Goal" :use (:instance double-containment-is-equality))))
  (defthmd double-containment-no-backchain-limit
    (implies (and (setp x) (setp y))
      (equal (equal x y)
        (and (subset x y)
          (subset y x))))
    :hints (("Goal" :by double-containment))))

(in-theory (disable head-minimal head-minimal-2))

(encapsulate nil
  (local (in-theory (enable (:ruleset primitive-rules)
        (:ruleset order-rules))))
  (defthm setp-of-cons
    (equal (setp (cons a x))
      (and (setp x)
        (or (<< a (head x))
          (emptyp x)))))
  (defthm in-to-member
    (implies (setp x)
      (equal (in a x)
        (if (member a x)
          t
          nil))))
  (defthm not-member-when-smaller
    (implies (and (<< a (car x)) (setp x))
      (not (member a x))))
  (defthm subset-to-subsetp
    (implies (and (setp x) (setp y))
      (equal (subset x y) (subsetp x y))))
  (defthm lexorder-<<-equiv
    (implies (not (equal a b))
      (equal (equal (<< a b)
          (lexorder a b))
        t))
    :hints (("Goal" :in-theory (enable <<)))))

(def-ruleset low-level-rules
  '(setp-of-cons in-to-member
    not-member-when-smaller
    subset-to-subsetp
    lexorder-<<-equiv
    (:ruleset primitive-rules)
    (:ruleset order-rules)))

(in-theory (disable (:ruleset low-level-rules)))

(defun fast-measure
  (x y)
  (+ (acl2-count x) (acl2-count y)))