The classic books/arithmetic library is fast and lightweight.
It provides only modest support for reasoning about how basic operations like
<, +, -, *, /, and expt relate to one
another over integers, rationals, and (for ACL2(r) users) the reals.
The original arithmetic library dates back to the early days of ACL2.
Many people contributed to its development, especially Bishop Brock, John
Cowles, Matt Kaufmann, Art Flatau, and Ruben Gamboa. The natp-posp book
was contributed more recently by Panagiotis Manolios and Daron Vroon. The
documentation was added by Jared Davis.
When should you use arithmetic? Later arithmetic libraries like
arithmetic-3 and arithmetic-5 are more comprehensive. They support
reasoning about many operations that arithmetic does not, e.g., floor and mod.
Later libraries typically also feature more sophisticated rules that can
automatically solve much harder goals that involve only the basic operators.
So, if you are facing hard arithmetic problems, or if your problems involve
operators that arithmetic does not support, you should definitely consider
using other libraries.
On the other hand, if you have simpler arithmetic needs, the ordinary
arithmetic library may be a fine choice. It is lightweight and fast, and
typically does not cause rewriting loops. It can also sometimes be easier to
understand what arithmetic is doing than other libraries, i.e., it is less
likely to lead you to strange subgoals that you don't understand.
Loading the Library
To avoid getting locked into any particular arithmetic library, good
practice is to always only locally include arithmetic books. So, to
load the most complete version of the arithmetic library, you should
(local (include-book "arithmetic/top-with-meta" :dir :system))
In certain cases, more sophisticated users may wish to load only some
portion of the library. A reasonable, slightly lighter-weight alternative
(local (include-book "arithmetic/top" :dir :system))
ACL2 books on arithmetic
Copyright (C) 1997 Computational Logic, Inc.
License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
- Rules for reducing inequalities between products, canceling like
factors, and comparing products against 0.
- Trivial normalization and cancellation rules for products.
- Basic rules for moving reciprocals across inequalities, comparing
reciprocals, and canceling reciprocals by multiplying across an inequality.
- Lemmas for reasoning about when the basic arithmetic operators
produce natural and positive integer results.
- Basic rules for normalizing and simplifying exponents.
- Rules about numerator and denominator in the
- Rules for resolving inequalities between exponents.
- Trivial normalization and cancellation rules for sums.
- Basic cancellation rules for numerator and denominator terms.
- Rules about when expt produces integers, positive numbers, etc.
- Basic normalization to move negative terms to the other side of an
- Rules for normalizing products with negative factors, and reciprocals
- Identity macro — does nothing, you can safely ignore this.