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.
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.
DISABLEDP.
PR.
Some possible approaches to finding the answer:
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
dir/acl2-sources/ is the directory of the ACL2
distribution on the local file system:
[Return to Table of Contents.]
(include-book "dir/acl2-sources/books/arithmetic/top-with-meta")