Bitops-compatibility
Notes about using Bitops with other arithmetic libraries.
Bitops can work well with many other arithmetic libraries. Here we
briefly sketch some tips about using various libraries with Bitops.
ihs/
Bitops started as an extension to the ihs library. Because of this
heritage, the relationship between ihs/ and bitops/ is somewhat
complex. Some parts of ihs can still be used with Bitops, others are best
avoided.
IHS Definition Books
The ihs/basic-definitions book is included directly in Bitops. You may
often want to non-locally include this book (to get definitions such as
loghead and logtail), then locally include Bitops books such as
ihsext-basics (to get the lemmas).
The basic-definitions book wasn't always part of ihs. We created it by
extracting "the good parts" of the richer ihs/logops-definitions book.
We typically do not load the additional definitions and macros that
remain in ihs/logops-definitions, or the @logops book which defines
various four-valued operations. But if you have some particular reason to want
these definitions, it would probably be fine to load them alongside Bitops.
IHS Lemma Books
The ihs/quotient-remainder-lemmas book has lemmas about integer
division operations like floor, mod, truncate, rem,
etc. This book generally works well with Bitops and may be a fine choice.
Other options include arithmetic-3 and arithmetic-5; see below.
The ihs/math-lemmas book is an extremely minimal math library. You
should probably use a library like arithmetic/top instead; see below.
The ihs/logops-lemmas book is a key book for bit-vector reasoning in
ihs. But you should generally not use it when you are using Bitops,
because the Bitops book ihsext-basics supersedes it—it imports the
good rules and then introduces improved replacements for many of the
ihsext-basics rules.
The ihs-lemmas book is a wrapper that includes the other -lemmas
books; it probably is best to just load quotient-remainder-lemmas instead,
since you generally wouldn't want to use the other books with Bitops.
arithmetic/
This is a very lightweight library that loads quickly and generally works
well with Bitops. It provides modest support for reasoning about how basic
operations like <, +, -, *, / and expt relate to
one another over integers and rationals.
1. The book arithmetic/top is generally a good starting point.
It can effectively deal with simple terms like (+ 1 -1 a) and apply other
obvious reductions. This is a good book to use when your use of arithmetic is
mostly incidental, e.g., you have a function that recurs by calling (- n
1) or similar.
2. The book arithmetic/top-with-meta is only slightly stronger;
it adds some ACL2::meta rules that can more effectively cancel out
summands and factors that can arise in various equalities and inequalities.
It's a fine choice that is about on par with arithmetic/top, but which is
superior in some cases.
arithmetic-3/
1. The basic arithmetic-3/bind-free/top book is essentially
similar to the arithmetic library, but features a much more sophisticated
use of meta rules for reducing sums and products, and recognizing when
arithmetic expressions return integers. It also features a much stronger
integration with ACL2::non-linear-arithmetic reasoning, which may be
especially useful when working with * and /.
This book is also very compatible with Bitops and may be a good choice for
cases where arithmetic/top-with-meta is not doing a good enough job with
respect to the basic arithmetic operations. Just about the only issue is that
it has some special support for (expt 2 ...) which overlaps a bit with
Bitops rules about ash. But this is really pretty unlikely to cause you
any problems.
If your proofs involving large terms (e.g., you are doing proofs about
machine models), you might want to start with arithmetic/top-with-meta
instead of arithmetic-3, but only because arithmetic-3's more
powerful rules are perhaps somewhat slower—it has a lot of ACL2::type-prescription rules, for instance, and these can sometimes get
slow.
2. The arithmetic-3/floor-mod/floor-mod book extends
bind-free/top with rules about floor and mod. It also gets
rid of rem, truncate, round, and ceiling by
rewriting them into floor and mod terms.
Bitops has very little support for working with floor and mod, so
all of this is generally compatible with Bitops except for powers of 2.
In Bitops, we generally prefer to deal with (loghead n x) and (logtail
n x) instead of (mod x (expt 2 n)) and (floor x (expt 2 n)). We
also generally prefer (ash 1 n) over (expt 2 n), but this is more
minor.
At any rate, if you are dealing with something like (floor x 3), or
more generally with floor or mod by arbitrary moduli, then writing
your goals in terms of floor and mod and using the floor-mod
book may be a fine choice. But if you are dealing with powers of 2, it is
probably generally best to avoid floor and mod, and phrase your goal
using the bit-vector operations instead.
3. The arithmetic-3/extra/top-ext book extends the
floor-mod book with additional lemmas about both the basic operators and
about floor and mod.
This is a bit heavier weight. It adds build dependencies on
arithmetic-2 and a (small) portion of the rtl library, and may
generally be a bit slower since, e.g., some of the rules it adds introduce
additional case splits. But while you may not want to try this book when
dealing with very large terms, it is generally a good book to try when you need
to prove a hard lemma involving lots of arithmetic.
arithmetic-5/
The arithmetic-5/top book is a popular, quite heavy-weight book that
is somewhat compatible with Bitops.
We usually prefer not to use arithmetic-5. The library can sometimes
be quite slow; many rules case split and there are, for instance, a great
number of ACL2::type-prescription rules that can become very expensive
in some cases. For instance, an extreme case was lemma-4-1-30 from
rtl/rel9/seed.lisp—we were able to speed this proof up from 651
seconds to 1 second by mostly just disabling these type-prescription rules; see
SVN revision 2160 for details.
On the other hand, arithmetic-5 is a very sophisticated library that
can deal with hard arithmetic problems, and now and again it can be useful to
use it instead of other libraries.
Combining arithmetic-5 with Bitops may sometimes be tricky.
As with arithmetic-3/floor-mod, you will want to watch out for powers
of 2. In Bitops we generally prefer to work with bit-vector functions like
loghead, logtail, ash, etc., instead of writing terms
involving floor and mod terms by (expt 2 n).
But unlike arithmetic-3, arithmetic-5 has many rules about
bit-vector functions such as logand, logior, etc., and these
rules may sometimes work against you. For instance, rules like these are likely
not what you want:
Theorem: (logand 1 x)
(defthm acl2::|(logand 1 x)|
(implies (integerp x)
(equal (logand 1 x)
(if (evenp x) 0 1))))
And generally arithmetic-5 likes to reason about (integerp (* 1/2
x)) instead of (logcar x), which is messy because it introduces rational
arithmetic into your problem.
It's possible to overcome and work around these problems, but you may want
to be looking out for these sorts of issues and making sure that you aren't
being pulled toward competing normal forms.
