# Reasoning

How to reason about bitsets.

Note: for now this discussion is only about plain bitsets. In the future, we intend this discussion to apply equally well to
sbitsets.

A general goal of the bitsets library is to let you take advantage of
efficient operations like logand and logior without having to do any
arithmetic reasoning. Instead, ideally, you should be able to carry out all of
your reasoning on the level of sets.

#### Basic Approach

To achieve this, we try to cast everything in terms of bitset-members. If you want to reason about some bitset-producing function
foo, then you should typically try to write your theorems about:

(bitset-members (foo ...))

instead of directly proving something about:

(foo ...)

For example, to reason about bitset-union we prove:

**Theorem: **bitset-members-of-bitset-union

(defthm bitset-members-of-bitset-union
(equal (bitset-members (bitset-union x y))
(union (bitset-members x)
(bitset-members y))))

In most cases, this theorem is sufficient for reasoning about the behavior
of bitset-union.

#### Equivalence Proofs

The bitset-members approach is good most of the time, but in some cases
you may wish to show that two bitset-producing functions literally create the
same bitset. That is, instead of showing:

(bitset-members (foo ...)) = (bitset-members (bar ...))

it is perhaps better to prove:

(foo ...) = (bar ...)

It should be automatic to prove this stronger form (after first proving the
weaker form) by using the theorem:

**Theorem: **equal-bitsets-by-membership

(defthm equal-bitsets-by-membership
(implies (and (natp x) (natp y))
(equal (equal x y)
(equal (bitset-members x)
(bitset-members y)))))