TIPS

Major Section:  ACL2-TUTORIAL

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 A and B are less than or equal to each other, then we need to know something more in order to conclude that they are equal (e.g., that they are numbers). This kind of twist is important in writing definitions; for example, if you expect a function to return a number, you may want to apply the function 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))))

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

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 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 (consp x) that matches many terms encountered by the prover. If in addition the rule has complicated hypotheses, this rule could slow down the prover greatly. Consider switching the conclusion and a complicated hypothesis (negating each) in that case.

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 rule are in simplified form.

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 brr t and (cw-gstack) for inspecting loops in the rewriter.

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))).

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))

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

(equal term1
       (if p term2 term3))

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 defaxioms temporarily to explore possibilities.
When there is a difficult goal that seems to follow immediately (by a :use hint or by rewriting) from some other lemmas, you can create those lemmas as 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 the file "doc/README" in the ACL2 distribution for information on books that come with the system.

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 :induct hints.

C4. Use the ``Proof Checker'' 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 :expand hints. Consider giving :expand hints. These are especially useful when a proof by induction is failing. It's almost always helpful to open up a recursively defined function that is supplying the induction scheme, but sometimes ACL2 is too timid to do so; or perhaps the function in question is disabled.

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 :use hints. Also, disable recursively defined functions for which you can prove what seem to be all the relevant properties. The prover can spend significant time ``behind the scenes'' trying to open up recursively defined functions, where the only visible effect is slowness.

D2. Turn off the ``break rewrite'' facility. Remember to execute :brr nil after you've finished with the ``break rewrite'' utility (see break-rewrite), in order to bring the prover back up to full speed.

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 x) first. If the context has several terms around that are known to be consps, then x may be bound to the wrong one of them. For much more information on free variables, see free-variables.

E4. Obtaining information Use :pl foo to inspect rewrite rules whose left hand sides are applications of the function foo. Another approach to seeing which rewrite rules apply is to enter the proof-checker with verify, and use the show-rewrites or sr command.

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 :rewrite rules. Should you use them? This is a complex question that we are not ready to answer with any generality. Our general advice is to avoid relying on such rules as long as you doubt their utility. More specifically: be careful not to use conditional type prescription rules, as these have been known to bring ACL2 to its knees, unless you are conscious that you are doing so and have reason to believe that they are working well.

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 :expand hints for those calls that you want opened up, which aren't. See also C8 above.

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.