		Search-engine friendly clone of the ACL2 documentation.

Arithmetic

Arithmetic-1

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.

Introduction

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 typically use:

(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 is:

(local (include-book "arithmetic/top" :dir :system))

Copyright Information

License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.

Subtopics

Inequalities-of-products: Rules for reducing inequalities between products, canceling like factors, and comparing products against 0.
Basic-product-normalization: Trivial normalization and cancellation rules for products.
Inequalities-of-reciprocals: Basic rules for moving reciprocals across inequalities, comparing reciprocals, and canceling reciprocals by multiplying across an inequality.
Arithmetic/natp-posp: Lemmas for reasoning about when the basic arithmetic operators produce natural and positive integer results.
Basic-expt-normalization: Basic rules for normalizing and simplifying exponents.
More-rational-identities: Rules about numerator and denominator in the arithmetic/rationals book.
Inequalities-of-exponents: Rules for resolving inequalities between exponents.
Basic-sum-normalization: Trivial normalization and cancellation rules for sums.
Basic-rational-identities: Basic cancellation rules for numerator and denominator terms.
Basic-expt-type-rules: Rules about when expt produces integers, positive numbers, etc.
Inequalities-of-sums: Basic normalization to move negative terms to the other side of an inequality.
Basic-products-with-negations: Rules for normalizing products with negative factors, and reciprocals of negations.
Fc: Identity macro — does nothing, you can safely ignore this.