We invite users to offer entries for this page. If you are a member of the
ACL2 mailing list, then we would appreciate you broadcasting your entry to
`acl2@lists.cc.utexas.edu`

.
You may also send a suggested FAQ entry to Kaufmann and
Moore at `kaufmann@cs.utexas.edu`

and
`moore@cs.utexas.edu`

.

You may join the mailing list by sending a message to `listproc@lists.cc.utexas.edu`

.
The body of the message should contain the line:

```
subscribe
acl2
```

*name*

where *name* is your name (not your
email address).

We would also be delighted to receive entries that contain both questions and your suggested answers. We feel free to edit the entries appropriately but will give credit appropriately too.

The ACL2 User's Manual has many tips, of course; see for example the topics TIPS and TIDBITS as well as ACL2-TUTORIAL.

**[GO!]**Why isn't this rewrite rule being applied?**[GO!]**How can I get a compact view of an unproved goal?**[GO!]**When should I use a macro instead of a (non-recursive) function?**[GO!]**How can I make ACL2 more knowledgeable?

*Elaboration.* I have proved a rewrite rule that is apparently not being
applied in a place where it "should" be applied. Specifically, ACL2 is
producing a goal that it refuses to simplify further even though I expect a
particular rewrite rule to be applied to a particular subterm. How can I
figure out what the problem is?

*Answer.* This is a critical question, and there are many possible
answers as well as approaches to finding an answer. Here are some ways to
proceed.

- Perhaps the rule is disabled. See the
documentation
for
`DISABLEDP`

. - Perhaps the left-hand side of the rule's conclusion does not match. If there are non-recursive function symbols in the rule, they may have been expanded away before the rule had a chance to match. Have you checked whether there was a corresponding warning issued when the rule was originally submitted?
- Was the rule stored as you inteded? See the
documentation
for
`PR`

. - Does the rule have one or more hypotheses that cannot be proved by rewriting? (See also below.)

Some possible approaches to finding the answer:

- Use the BREAK-REWRITE utility (see documentation).
- Use the PROOF-CHECKER (see documentation;
example may appear later in this FAQ, and
there is an example in
*Computer-AIded Reasoning: An Approach.* - Attempt to formulate the problematic rewrite rule with as few hypotheses as possible, and without free variables (i.e., variables occuring in the rule that do not occur in the left-hand side of the conclusion).
- Consider applying FORCE to the hypotheses so you can watch the prover's
attempt to prove them. See the
documentation
for
`FORCE`

.

Click here for a fairly advanced investigation of a subtle kind of rewriting failure that can occur.

**[Return to Table of Contents.]**

*Elaboration.* I'm looking at a goal that the prover couldn't prove, and
it's quite complicated: lots of function calls have already opened up. How can
I look at the unproved goal without getting swamped by details?

*Answer.* One way is to use the proof-checker as follows. Here, we
imagine a big subterm, <big_subterm>, which you would prefer to be
printed as a single symbol, say $my-state$.

ACL2 !>(verify <unproved_goal>) ->: (generalize ((<big_subterm> $my-state$))) ->: p ; print the resulting goal

Multiple terms can be generalized simultaneously, and an alternate "abbreviation" mechanism is available as well. See the documentation for acl2-pc::generalize (or acl2-pc::add-abbreviation). Note that in Emacs Info, the proof-checker commands are listed using "||" in place of "::", e.g., acl2-pc||generalize.

**[Return to Table of Contents.]**

*Answer.*
This question has many facets. The main difference, of course, is that macros
are immediately expanded (evaluated) when forms are read in, while functions
are called/expanded at run/proof time. Using a macro can result in faster
execution at run time by avoiding the overhead of a function call and giving
the compiler more opportunities for optimization. For many applications though,
the run-time differences between macros and functions are nominal, so we will
focus on the facets arising during proofs.

We will use defabbrev in our examples below instead of defmacro for presentation purposes. The interested reader is referred to the documentation of defabbrev. It is worth noting that using defabbrev is equivalent in proofs to direct replacement. For instance with the following abbreviation:

(defabbrev f (x) (g x))the body of the following theorem:

(defthm f-simplification (equal (f y) y))is "expanded" to: (i.e. it is stored in ACL2 as:)

(equal (g y) y)and is thus a rewrite rule which is only applied to terms of the form (g ..) even though the theorem does not mention the function g directly. In contrast, if we had instead defined f as a function, then the body of the theorem would have been stored in ACL2 as (equal (f y) y), i.e., as a rewrite rule only applied to terms of the form (f ..). In the case where f is a function, ACL2 expands the definition of f during the proof of the theorem, while in the defabbrev case, f is expanded as ACL2 initially reads and processes the theorem.

In order to help gauge the tradeoffs in using defabbrev (macros) vs. defun (functions), it is important to realize that the ACL2 user has no control over the expansion of macros while the user can control when and if ACL2 expands the definition of a function. We demonstrate this with the following forms:

ACL2 !> (defun fun (x) (car x)) ACL2 !> (thm (equal (fun (cons x y)) x)) ... Q.E.D. ;; we now turn off the definition of (fun x) ACL2 !> (in-theory (disable fun)) ;; the following theorem fails because ACL2 cannot expand (fun x) ACL2 !> (thm (equal (fun (cons x y)) x)) ... ******** FAILED ******** ACL2 !> (defabbrev abr (x) (car x)) ;; there is no way to turn off the expansion of (abr x). ACL2 !> (thm (equal (abr (cons x y)) x)) ... Q.E.D.

Furthermore, functions play a role in the application of various classes of rules derived from theorems. We will focus on :rewrite rules, but most of these points apply to other rule classes as well. To see the differences, consider the following forms:

ACL2 !> (defun foo (x) (car x)) ACL2 !> (defun bar (x) (foo x)) ACL2 !> (defthm bar-reduce (implies (consp x) (equal (bar x) (car x)))) ... Q.E.D. ACL2 !> (in-theory (disable foo)) ACL2 !> (defthm bar-try (equal (bar (cons x y)) x)) ... ******** FAILED ******** ACL2 !> (in-theory (disable bar)) ACL2 !> (defthm bar-try (equal (bar (cons x y)) x)) ... Q.E.D.

In the above example, the rewrite rule created by the theorem bar-reduce will only rewrite (bar x) to (car x) when the hypothesis (consp x) is satisfied. The reason the first attempt to prove bar-try fails is because ACL2 decides to first open up the definition of (bar x) to (foo x). But the definition of foo is disabled and so ACL2 is left with trying to prove (equal (foo (cons x y)) x). But, ACL2 cannot use the theorem bar-reduce because it can only rewrite terms (bar x), not (foo x), and thus ACL2 fails since it has no other rules it can apply to (foo x). The second time we attempt bar-try, we have disabled the definition of (bar x) and so ACL2 does not rewrite it to (foo x). This time, though, ACL2 succeeds in applying the rule bar-reduce and thus succeeds in proving bar-try. If foo and bar had been defined as macros, then bar-try would succeed immediately since it would be reduced to (equal (car (cons x y)) x). Thus, the use of macros allows a greater normalization of the terms in theorems and the rewrite rules they generate.

The previous example demonstrated a pitfall in the use of functions. We now consider an example where it is useful to disable a function in order to avoid the introduction of the body of the function. Consider the following forms. (NOTE -- the following example was inspired by a similar example given by Matt Wilding.)

ACL2 !> (defabbrev f (x) (if (> x 0) (1+ x) x)) ACL2 !> (defthm f^10-is-increasing (>= (f (f (f (f (f (f (f (f (f (f x)))))))))) x)) ... Q.E.D. Time: 119.37 seconds ACL2 !> (defun g (x) (if (> x 0) (1+ x) x)) ACL2 !> (defthm g-is-increasing (implies (>= x y) (>= (g x) y))) ... Q.E.D. ACL2 !> (thm (>= (g (g (g (g (g (g (g (g (g (g x)))))))))) x)) ... Q.E.D. Time: 1.06 seconds ;; OR even better ACL2 !> (in-theory (disable g)) ACL2 !> (defthm g^10-is-increasing (>= (g (g (g (g (g (g (g (g (g (g x)))))))))) x)) ... Q.E.D. Time: 0.02 seconds

The proof for the theorem f^10-is-increasing took considerably longer than g^10-is-increasing because in the first case, the term (f (f .. )) was expanded by ACL2 into a very large (if ..) expression. ACL2 then normalizes this expression in order to determine the cases it needs to verify. In the case of (g (g ..)) we were able to control ACL2 by disabling (g ..) and proving a simple theorem which ACL2 could use to prove g^10-is-increasing. While this example may seem contrived, the ability to efficiently direct ACL2 by proving sufficient theorems about complex non-recursive functions and then hiding their definition is crucial in tackling larger proof efforts in ACL2. Another benefit to using functions and selectively opening their definitions is that the proof output from ACL2 can be far easier to read and further diagnose as to where ACL2 failed.

As the above examples hopefully demonstrate, it is important for the user of ACL2 to be aware of the nature of the operators used to build the terms in theorems. It is important to know which ones are macros, which ones are disabled functions, and which ones are enabled functions. It is also important that the user is aware of the nature of the built-in ACL2 operators. For instance, the user may prove the following theorem:

(defthm gh-rewrites-to-f (= (g (h x)) (f x)))and expect it to be a useful rewrite rule applied to terms of the form (g (h ..)). But, even though (= x y) is defined to be (equal x y), since = is a function, the rewrite rule will only rewrite terms of the form (= (g (h ..)) (f ..)) to T.

In summary, the basic criterion for whether to use a macro or a function is the tradeoff between the normalization offered by macros to the control offered by functions. Generally, if a function has conditional expressions (e.g. if, cond, case, etc.) or if it is the composition of several other functions, then it is probably best to leave it as a function and to enable the function carefully during proofs. Otherwise, it is often better to use a macro in order to free yourself from having to consider the effects of enabling and disabling a function and the contexts in which rewrite rules will be applied.

**[Return to Table of Contents.]**

*Elaboration.* ACL2 seems to do a poor job of proving even basic facts
about arithmetic (for example). Is there any way to tell it to be "smarter"?

*Answer.* Yes. ACL2 comes with a substantial body of already-proved
facts, in the `books/`

subdirectory of the distribution. File
`README.html`

from that directory describes the collections of ACL2 *books* (i.e.,
collections of definitions and proved theorems) that are provided with ACL2.
Instructions also appear there for *certifying* the books, i.e., making
them available for use on your file system. These books have been contributed
by several ACL2 users; if you have some that you may be interested in
contributing, then by all means let us know.

For example, when you bring up the following proof attempt with fail.

(thm (implies (not (equal (fix z) 0)) (equal (* x (+ y (/ z))) (/ (+ (* x y z) x) z))))A useful book for arithmetic proofs is file

`top-with-meta.lisp`

in
the `arithmetic/`

subdirectory of the `books/`

directory. And in fact, the proof attempt shown above succeeds after the
execution of the following event form, where
`/acl2-sources/`

is the directory of the ACL2
distribution on the local file system:
`(include-book "`

*dir*`/acl2-sources/books/arithmetic/top-with-meta")`

```
```

**[Return to Table of Contents.]**

```
```