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
To achieve this, we try to cast everything in terms of bitset-members. If you want to reason about some bitset-producing function
(bitset-members (foo ...))
instead of directly proving something about:
For example, to reason about bitset-union we prove:
(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
(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:
(defthm equal-bitsets-by-membership (implies (and (natp x) (natp y)) (equal (equal x y) (equal (bitset-members x) (bitset-members y)))))