Some hints for using the ACL2 prover

We present here some tips for using ACL2 effectively. Though this
collection is somewhat *ad hoc*, we try to provide some organization,
albeit somewhat artificial: for example, the sections overlap, and no
particular order is intended. This material has been adapted by Bill Young
from a very similar list for Nqthm that appeared in the conclusion of:
``Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem,'' by Matt Kaufmann and Paolo Pecchiari, CLI
Technical Report 100, June, 1995. We also draw from a similar list in Chapter
13 of ``A Computational Logic Handbook'' by R.S. Boyer and J
S. Moore (Academic Press, 1988). We'll refer to this as ``ACLH'' below.

These tips are organized roughly as follows.

A. ACL2 Basics

B. Strategies for creating events

C. Dealing with failed proofs

D. Performance tips

E. Miscellaneous tips and knowledge

F. Some things you DON'T need to know

*ACL2 BASICS*

**A1. The ACL2 logic.**

This is a logic of total functions. For example, if `fix` or
some variant (e.g., `nfix` or `ifix`) in case one of the formals
is to be returned as the value.

ACL2's notion of ordinals is important on occasion in supplying ``measure hints'' for the acceptance of recursive definitions. Be sure that your measure is really an ordinal. Consider the following example, which ACL2 fails to admit (as explained below).

(defun cnt (name a i x) (declare (xargs :measure (+ 1 i))) (cond ((zp (+ 1 i)) 0) ((equal x (aref1 name a i)) (1+ (cnt name a (1- i) x))) (t (cnt name a (1- i) x))))

One might think that `nfix` to

(declare (xargs :measure (nfix (+ 1 i))))

in order to guarantee that the measure will always be an ordinal (in fact, a positive integer).

For more about admissibility of recursive definitions, see defun, in particular the discussion of termination.

**A2. Simplification.**

The ACL2 simplifier is basically a rewriter, with some ``linear
arithmetic'' thrown in. One needs to understand the notion of conditional
rewriting. See rewrite.

**A3. Parsing of rewrite rules.**

ACL2 parses rewrite rules roughly as explained in ACLH,
*except* that it never creates ``unusual'' rule classes. In ACL2, if you
want a `linear` rule, for example, you must specify `linear` in the `rule-classes`. See rule-classes, and also
see rewrite and see linear.

**A4. Linear arithmetic.**

On this subject, it should suffice to know that the prover can handle truths
about `+` and `-`, and that linear rules (see above) are
somehow ``thrown in the pot'' when the prover is doing such reasoning.
Perhaps it's also useful to know that linear rules can have hypotheses,
and that conditional rewriting is used to relieve those hypotheses.

**A5. Events.**

Over time, the expert ACL2 user will know some subtleties of its events. For example, `in-theory` events and hints are
important, and they distinguish between a function's definition and its executable-counterpart.

*B. STRATEGIES FOR CREATING EVENTS*

In this section, we concentrate on the use of definitions and rewrite rules. There are quite a few kinds of rules allowed in ACL2 besides rewrite rules, though most beginning users probably won't usually need to be aware of them. See rule-classes for details. In particular, there is support for congruence rewriting. Also see rune (``RUle NamE'') for a description of the various kinds of rules in the system.

**B1. Use high-level strategy.**

Decompose theorems into ``manageable'' lemmas (admittedly, experience helps
here) that yield the main result ``easily.'' It's important to be able to
outline non-trivial proofs by hand (or in your head). In particular, avoid
submitting goals to the prover when there's no reason to believe that the goal
will be proved and there's no ``sense'' of how an induction argument would
apply. It is often a good idea to avoid induction in complicated theorems
unless you have a reason to believe that it is appropriate.

**B2. Write elegant definitions.**

Try to write definitions in a reasonably modular style, especially recursive
ones. Think of ACL2 as a programming language whose procedures are
definitions and lemmas, hence we are really suggesting that one follow good
programming style (in order to avoid duplication of ``code,'' for
example).

When possible, complex functions are best written as compositions of simpler functions. The theorem prover generally performs better on primitive recursive functions than on more complicated recursions (such as those using accumulating parameters).

Avoid large non-recursive definitions which tend to lead to large case explosions. If such definitions are necessary, try to prove all relevant facts about the definitions and then disable them.

Whenever possible, avoid mutual recursion if you care to prove anything about your functions. The induction heuristics provide essentially no help with reasoning about mutually defined functions. Mutually recursive functions can usually be combined into a single function with a ``flag'' argument. (However, see mutual-recursion-proof-example for a small example of proof involving mutually recursive functions.)

**B3. Look for analogies.**

Sometimes you can easily edit sequences of lemmas into sequences of lemmas
about analogous functions.

**B4. Write useful rewrite rules.**

As explained in A3 above, every rewrite rule is a directive to the
theorem prover, usually to replace one term by another. The directive
generated is determined by the syntax of the `defthm` submitted. Never
submit a rewrite rule unless you have considered its interpretation as
a proof directive.

**B4a. Rewrite rules should simplify.**

Try to write rewrite rules whose right-hand sides are in some sense
``simpler than'' (or at worst, are variants of) the left-hand sides. This
will help to avoid infinite loops in the rewriter.

**B4b. Avoid needlessly expensive rules.**

Consider a rule whose conclusion's left-hand side (or, the entire conclusion)
is a term such as

**B4c. The ``Knuth-Bendix problem''.**

Be aware that left sides of rewrite rules should match the ``normalized
forms'', where ``normalization'' (rewriting) is inside out. Be sure to avoid
the use of nonrecursive function symbols on left sides of rewrite
rules, except when those function symbols are disabled, because they
tend to be expanded away before the rewriter would encounter an instance of
the left side of the rule. Also assure that subexpressions on the left hand
side of a rewrite rule are in simplified form; see community-books
example

**B4d. Avoid proving useless rules.**

Sometimes it's tempting to prove a rewrite rule even before you see how
it might find application. If the rule seems clean and important, and not
unduly expensive, that's probably fine, especially if it's not too hard to
prove. But unless it's either part of the high-level strategy or, on the
other hand, intended to get the prover past a particular unproved goal, it may
simply waste your time to prove the rule, and then clutter the database of
rules if you are successful.

**B4e. State rules as strongly as possible, usually.**

It's usually a good idea to state a rule in the strongest way possible, both
by eliminating unnecessary hypotheses and by generalizing subexpressions to
variables.

Advanced users may choose to violate this policy on occasion, for example in order to avoid slowing down the prover by excessive attempted application of the rule. However, it's a good rule of thumb to make the strongest rule possible, not only because it will then apply more often, but also because the rule will often be easier to prove (see also B6 below). New users are sometimes tempted to put in extra hypotheses that have a ``type restriction'' appearance, without realizing that the way ACL2 handles (total) functions generally lets it handle trivial cases easily.

**B4f. Avoid circularity.**

A stack overflow in a proof attempt almost always results from circular
rewriting. Use `brr` to investigate the stack; see break-lemma.
Because of the complex heuristics, it is not always easy to define just when a
rewrite will cause circularity. See the very good discussion of this
topic in ACLH.

See break-lemma for a trick involving use of the forms

**B4g. Remember restrictions on permutative rules.**

Any rule that permutes the variables in its left hand side could cause
circularity. For example, the following axiom is automatically supplied by
the system:

(defaxiom commutativity-of-+ (equal (+ x y) (+ y x))).

This would obviously lead to dangerous circular rewriting if such ``permutative'' rules were not governed by a further restriction. The restriction is that such rules will not produce a term that is ``lexicographically larger than'' the original term (see loop-stopper). However, this sometimes prevents intended rewrites. See Chapter 13 of ACLH for a discussion of this problem.

**B5. Conditional vs. unconditional rewrite rules.**

It's generally preferable to form unconditional rewrite rules unless
there is a danger of case explosion. That is, rather than pairs of rules such
as

(implies p (equal term1 term2))

and

(implies (not p) (equal term1 term3))

consider:

(equal term1 (if p term2 term3))

However, sometimes this strategy can lead to case explosions: `if`
terms introduce cases in ACL2. Use your judgment. (On the subject of
`if`: `cond`, `case`, `and`, and `or` are macros
that abbreviate `if` forms, and propositional functions such as `implies` quickly expand into `if` terms.)

**B6. Create elegant theorems.**

Try to formulate lemmas that are as simple and general as possible. For
example, sometimes properties about several functions can be ``factored'' into
lemmas about one function at a time. Sometimes the elimination of unnecessary
hypotheses makes the theorem easier to prove, as does generalizing first by
hand.

**B7. Use** `defaxiom`s **temporarily to explore
possibilities.**

When there is a difficult goal that seems to follow immediately (by a
`defaxiom` events (or, the application of `skip-proofs` to `defthm` events) and then double-check that the
difficult goal really does follow from them. Then you can go back and try to
turn each `defaxiom` into a `defthm`. When you do that, it's
often useful to disable any additional rewrite rules that you
prove in the process, so that the ``difficult goal'' will still be proved from
its lemmas when the process is complete.

Better yet, rather than disabling rewrite rules, use the `local` mechanism offered by `encapsulate` to make temporary rules
completely `local` to the problem at hand. See encapsulate and
see local.

**B9. Use books.**

Consider using previously certified books, especially for arithmetic reasoning. This cuts down the duplication of effort and starts
your specification and proof effort from a richer foundation. See community-books.

*C. DEALING WITH FAILED PROOFS*

**C1. Look in proof output for goals that can't be further
simplified.**

Use the ``proof-tree'' utility to explore the proof space. However,
you don't need to use that tool to use the ``checkpoint'' strategy. The idea
is to think of ACL2 as a ``simplifier'' that either proves the theorem or
generates some goal to consider. That goal is the first ``checkpoint,'' i.e.,
the first goal that does not further simplify. Exception: it's also important
to look at the induction scheme in a proof by induction, and if induction
seems appropriate, then look at the first checkpoint *after* the
induction has begun.

Consider whether the goal on which you focus is even a theorem. Sometimes you can execute it for particular values to find a counterexample.

When looking at checkpoints, remember that you are looking for any reason at all to believe the goal is a theorem. So for example, sometimes there may be a contradiction in the hypotheses.

Don't be afraid to skip the first checkpoint if it doesn't seem very helpful. Also, be willing to look a few lines up or down from the checkpoint if you are stuck, bearing in mind however that this practice can be more distracting than helpful.

**C2. Use the ``break rewrite'' facility.**

`Brr` and related utilities let you inspect the ``rewrite stack.''
These can be valuable tools in large proof efforts. See break-lemma
for an introduction to these tools, and see break-rewrite for more
complete information.

The break facility is especially helpful in showing you why a particular rewrite rule is not being applied.

**C3. Use induction hints when necessary.** Of course, if you can define
your functions so that they suggest the correct inductions to ACL2, so much
the better! But for complicated inductions, induction hints are
crucial. See hints for a description of

**C4. Use the interactive ``Proof-Builder'' to explore.**

The `verify` command supplied by ACL2 allows one to explore problem
areas ``by hand.'' However, even if you succeed in proving a conjecture with
`verify`, it is useful to prove it without using it, an activity that
will often require the discovery of rewrite rules that will be useful
in later proofs as well.

**C5. Don't have too much patience.**

Interrupt the prover fairly quickly when simplification isn't succeeding.

**C6. Simplify rewrite rules.**

When it looks difficult to relieve the hypotheses of an existing rewrite rule that ``should'' apply in a given setting, ask yourself if you
can eliminate a hypothesis from the existing rewrite rule. If so, it
may be easier to prove the new version from the old version (and some
additional lemmas), rather than to start from scratch.

**C7. Deal with base cases first.**

Try getting past the base case(s) first in a difficult proof by induction.
Usually they're easier than the inductive step(s), and rules developed in
proving them can be useful in the inductive step(s) too. Moreover, it's
pretty common that mistakes in the statement of a theorem show up in the base
case(s) of its proof by induction.

**C8. Use** **hints.** Consider giving

*D. PERFORMANCE TIPS*

**D1. Disable rules.**

There are a number of instances when it is crucial to disable rules,
including (often) those named explicitly in

**D2. Turn off the ``break rewrite'' facility.** Remember to execute

*E. MISCELLANEOUS TIPS AND KNOWLEDGE*

**E1. Order of application of rewrite rules.**

Keep in mind that the most recent rewrite rules in the history
are tried first.

**E2. Relieving hypotheses is not full-blown theorem proving.**

Relieving hypotheses on rewrite rules is done by rewriting and linear arithmetic alone, not by case splitting or by other prover processes
``below'' simplification.

**E3. ``Free variables'' in rewrite rules.**

The set of ``free
variables'' of a rewrite rule is defined to contain those variables
occurring in the rule that do not occur in the left-hand side of the rule.
It's often a good idea to avoid rules containing free variables because they
are ``weak,'' in the sense that hypotheses containing such variables can
generally only be proved when they are ``obviously'' present in the current
context. This weakness suggests that it's important to put the most
``interesting'' (specific) hypotheses about free variables first, so that the
right instances are considered. For example, suppose you put a very general
hypothesis such as `consp`s, then

**E4. Obtaining information**

Use `pl` `verify`, and use the

**E5. Consider esoteric rules with care.**

If you care to see rule-classes and peruse the list of subtopics (which
will be listed right there in most versions of this documentation),
you'll see that ACL2 supports a wide variety of rules in addition to

*F. SOME THINGS YOU DON'T NEED TO KNOW*

Most generally: you shouldn't usually need to be able to predict too much about ACL2's behavior. You should mainly just need to be able to react to it.

**F1. Induction heuristics.**

Although it is often important to read the part of the prover's
output that gives the induction scheme chosen by the prover, it is
not necessary to understand how the prover made that choice.
(Granted, advanced users may occasionally gain minor insight from such
knowledge. But it's truly minor in many cases.) What *is* important is
to be able to tell it an appropriate induction when it doesn't pick the right
one (after noticing that it doesn't). See C3 above.

**F2. Heuristics for expanding calls of recursively defined
functions.**

As with the previous topic, the important thing isn't to understand these
heuristics but, rather, to deal with cases where they don't seem to be
working. That amounts to supplying

**F3. The ``waterfall''.**

As discussed many times already, a good strategy for using ACL2 is to look for
checkpoints (goals stable under simplification) when a proof fails, perhaps
using the proof-tree facility. Thus, it is reasonable to ignore almost
all the prover output, and to avoid pondering the meaning of the other
``processes'' that ACL2 uses besides simplification (such as elimination,
cross-fertilization, generalization, and elimination of irrelevance). For
example, you don't need to worry about prover output that mentions ``type
reasoning'' or ``abbreviations,'' for example.