# In

`(in a x)` determines if a is a member of the set X.

The logical definition of in makes no mention of the set
order, except implicitly by the use of the set primitives like head and tail.

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:

;; 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))))

There are other ways we could optimize in. Since the set is ordered,
we could try to use the set order << 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.

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

(in 1 '(2 3 4 .... 100000))

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

(in 100001 '(1 2 3 4 ... 100000))

we would incur the extra cost of 100,000 calls to <<.

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

- it is not clear which would be faster in all cases,
- 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
- 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
- the current method is arguably no less efficient than an unordered
implementation.

Future note. In principle membership in an ordered list might be done in
O(log_2 n). We are considering using a *galloping* membership check
in the future to obtain something along these lines.

### Definitions and Theorems

**Function: **in

(defun in (a x)
(declare (xargs :guard (setp x)))
(mbe :logic (and (not (empty 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))))))))

**Theorem: **in-type

(defthm in-type
(or (equal (in a x) t)
(equal (in a x) nil))
:rule-classes :type-prescription)

**Theorem: **not-in-self

(defthm not-in-self (not (in x x)))

**Theorem: **in-sfix-cancel

(defthm in-sfix-cancel
(equal (in a (sfix x)) (in a x)))

**Theorem: **never-in-empty

(defthm never-in-empty
(implies (empty x) (not (in a x))))

**Theorem: **in-set

(defthm in-set
(implies (in a x) (setp x)))

**Theorem: **in-tail

(defthm in-tail
(implies (in a (tail x)) (in a x)))

**Theorem: **in-tail-or-head

(defthm in-tail-or-head
(implies (and (in a x) (not (in a (tail x))))
(equal (head x) a)))

**Theorem: **in-head

(defthm in-head
(equal (in (head x) x) (not (empty x))))