Some questions newcomers frequently ask
This FAQ is for people who've read through all the other sections
of the tutorial introduction to the theorem prover (see introduction-to-the-theorem-prover and all the links from it that are not
marked with the little warning sign (``
Q. How do I find something in the ACL2 documentation? A. Try the ``Jump to'' or ``Search'' boxes at the ACL2+Books Manual.
Q. How does the theorem prover work? A. We really don't think you need to know much about the inner workings of the prover to become an effective user. That doesn't mean the system is self-explanatory! It means that stuff you need to learn is not how the theorem prover works but how to interact with it! That is what introduction-to-the-theorem-prover is about. However, if you want the most basic overview of the prover, see architecture-of-the-prover.
Q. How do I define a new function? A. See defun.
Q. How do I define a new predicate? A. See defun.
Q. How do I define a new relation? A. See defun.
Q. How do I define a function or predicate that takes a varying number of arguments? A. You can't. However, see defmacro to learn how to define a macro that takes a varying number of arguments and expands into an arbitrary term that you compute.
Q. How do I define a macro that is sensitive to the state? A. You can't. However, advanced users should consider make-event.
Q. How do I define mutually recursive functions? A.
See mutual-recursion. However, you should realize that when two
Q. How do I declare the type signature of a function?
A. You can't. ACL2 is a syntactically untyped language and all
functions are defined on all objects in the ACL2 universe. We recommend that
the new user get used to this and only then explore the use of ACL2 to express
and enforce a type regime. In ACL2, the guard of a function is akin to
the type signature of a function in typed languages. However, ACL2 guards may
be arbitrary terms, not just type conditions, they only concern the inputs to
the function (not its result), and do not affect the axiom defining the
function — all functions are defined on every combination of objects.
You may, of course, prove theorems that establish that every function called
in a definition or theorem is supplied with input satisfying its guards (which
necessarily involves describe the outputs too). These formulas are called
guard conjectures and the process of proving them is called guard
verification. Since guards are arbitrary ACL2 formulas, the ``type
regimes'' one tends to enforce in ACL2 can be much for flexible and expressive
than those in most programming languages. However, that expressibility also
means guard verification can be challenging (indeed undecidable). On the
other hand, if one limits oneself to simple type-like guards, lemmas can be
proved that make most guard verification fully automatic and one can configure
ACL2 to do guard verification automatically at
Q. How do I tell
Q. I specified a measure that always returns a natural number but
ACL2 is acting like it's not a natural number. A. There are two
likely problems. The most likely one is that your measure isn't really always
a natural! Suppose the formals of your
Q. How do I tell
Q. How do I show that a relation is well-founded?
A. Prove a theorem establishing that there is an order preserving
embedding into the ordinals and store it with
Q. What is an ordinal? What does it mean to be well-founded? A. Ordinals are an extension of the natural numbers used to ensure that a process can't go on forever. Like naturals, they can be added, multiplied, and exponentiated. There is a sense of one ordinal being less than another. Unlike the naturals, each of which is finite, the ordinals include infinite objects. Now imagine ``standing'' on an ordinal and ``stepping'' to a smaller one. Like the naturals, this ``walk down the ordinals'' can't go on forever, even if you start on an infinite ordinal. That is because the ordinals are well-founded. See o-p for more information about ordinals in ACL2 and about well-foundedness. See ordinals for a deeper discussion and a discussion of books that can help configure ACL2 to reason about ordinals.
Q. How can provide hints for the termination proofs in
Q. How do I define a constant (something like a global variable)? A. See defconst. But remember that as an applicative programming language, ACL2 does not have global variables! You can define a symbol to have a fixed value and use the symbol sort of like a global variable in function definitions: you may refer to the value of the symbol in your functions without passing the variable in as formal parameter. But you may not ever change the value of the symbol!
Q. How do I save the value of a top-level computation for future use? A. See assign and see @.
Q. How do I introduce new syntactic form or abbreviation? A. See defmacro.
Q. How can create and modify an array? A. ACL2 is a functional language, so it is impossible to destructively modify an existing object; technically, all ``updates'' to objects must be implemented by ``copy-on-write'' semantics. That said, ACL2 provides support for arrays, provided you use them in a restricted way. They give you constant-time access and change under the use restrictions.
Q. How do I read from or write to a file? How do I do IO? A. To manipulate files, your function must have state as an argument, so you should read about the restrictions that imposes. For input/output facilities, see io.
Q. How do I define a structure that can be destructively
modified? A. ACL2 is an applicative programming language.
You can't modify objects arbitrarily! You basically have to ``copy on
write,'' which means you construct new objects from old ones, making the
changes you want in the new one. If the
Q. How do I write a universal quantifier? An existential quantifier? How can I say ``for all'' or ``there exists''? A You can't literally write quantifiers. But ACL2 has the power of full first order logic with quantification. See quantifiers.
Q. How do I introduce an undefined or uninterpreted function symbol? Can I constrain it to have certain properties? A. See encapsulate.
Q. How can I hide a lemma? I want to prove a lemma temporarily to
use in another proof but I don't want the lemma around thereafter. A.
One way to get a similar effect is to prove the lemma and then disable it with
Q. What is an event? A. An event is a command
that adds information to the ACL2 database (the ``logical world''), like
Q. How do I say that I do not want a rewrite rule generated from a theorem? A. The command
(defthm name formula :rule-classes nil)
will attempt to prove formula and, if successful, give formula the name name, which you may use in hints as a theorem, but it will build no rules from the formula.
Q. How do I say that I want a formula to be stored as a rewrite rule? A. The command
(defthm name formula)
will attempt to prove formula and, if successful, it will give
formula the name name and generate a rewrite rule from it, with
the runic name
Q. How do I say that I want a formula to be stored as a rewrite rule and some other kinds of rules? A. The command
(defthm name formula :rule-classes (:class1 ... classk))
will attempt to prove formula and, if successful, it will give
formula the name name and generate a rule of each :classi
specified. Each :classi should either be a keyword, like
Q. How do I rearrange the shape of a formula before
generating a rule from it? A. See rule-classes and read about
Q. What is a type-prescription? A. ACL2 has an algorithm for determining the type of object returned by a term, where a type is one of the Common Lisp primitive datatypes such as natural, integer, Boolean, cons, true-listp, etc. Rules provided by you can influence this algorithm. See type-prescription.
Q. How do rewrite rules work? A. Re-read the tutorial sections: introduction-to-rewrite-rules-part-1 and introduction-to-rewrite-rules-part-2.
Q. How do I see what's in the database? A. You can't
look at the entire database with user-friendly tools. You can print the
command that introduced a particular name, print the entire sequence of user
commands, print the commands in the region between two commands, print all the
rewrite rules that apply to a given term or function symbol, and many other
options. See history. If you have loaded a book from another user,
you might wish to read the source file. For example, the source file for
Q. How do I undo a command? A. See history, especially see u (``undo'') and see ubt (``undo back through''). Q. What rewrite rules match a given term? A. See pl.
Q. What were those questions to ask when looking at key checkpoints? A. See introduction-to-key-checkpoints.
Q. How do I figure out why a rewrite rule won't fire? A. If you activate rewrite rule monitoring (see brr) and then install a monitor (see monitor) on the rule in question, ACL2 will enter an interactive break whenever the pattern of the rule is matched against a target in a proof. So after installing the monitor, re-try the proof and then interact with the rewriter via break commands (see brr-commands). Like all trace and break packages, you have to know what you're doing to use the break rewrite facility, so read the material in the reference manual. If no interactive break happens after you've installed the monitor on your rule and re-tried the proof, it means no suitable target ever arose. Don't forget to turn off monitoring when you're done as it slows down the system.
Q. Why is a proof taking so long? A. Unexpectedly poor performance on simple problems is usually a sign of cyclic rewriting or combinatoric explosion. See dmr and see accumulated-persistence.
Q. How do I tell ACL2 what induction to do for a particular
formula? A. When issuing the
(defthm name formula :hints (("Goal" :induct (f x1 ... xn))))
Q. ACL2 doesn't know simple arithmetic that can simplify the
Q. ACL2 is not using an arithmetic lemma that I proved. A. Lemmas concluding with arithmetic inequalities, like
(implies (member e x) (< (len (delete e x)) (len x)))
are not good rewrite rules because they rarely match targets because of
intervening arithmetic operators. For example, the above conclusion doesn't
(defthm len-delete (implies (member e x) (< (len (delete e x)) (len x))) :rule-classes :linear)
Q. What is a linear rule? A. See linear.
Q. How do I make ACL2 treat a relation as an equality? A. We assume you mean to treat the relation as an equivalence, i.e., replace one term by another when they are equivalent under your relation. See equivalence, see congruence, and see refinement.
Q. One of my rewrite rules has a hypothesis that doesn't
rewrite to true. What do I do? A. Prove a rewrite rule that
establishes that hypothesis under the relevant assumptions from the context of
the intended target. Alternatively, undo the rule and restate it with a
force around the problematic hypothesis, making ACL2 assume the
hypothesis when the rule is applied and raising the truth of the hypothesis as
an explicit subgoal of the proof. See also case-split. Of course,
you should always state the strongest rewrite rules you can think of,
eliminating hypotheses or shifting them to the right-hand side inside of
Q. How do I make ACL2 ``guess'' the right instantiation of a free
variable? A. You can provide a
Q. How can I make ACL2 do a case split to prove a certain
subgoal? A. See hints, specifically
Q. How can I prevent ACL2 from using a rewrite rule?
A. See hints, specifically
Q. How can I prevent ACL2 from running a definition on constants?
I tried disabling the function but that didn't work. A. If you have a
Q. How can I make ACL2 use a rule in a proof? A. See
Q. How can I make ACL2 expand a function call in a proof?
A. You can give an
Q. ACL2 sometimes aborts the proof attempt before showing me all of the subgoals. How can I make it just keep going instead of aborting early? A. See otf-flg, which stands for Onward Thru the Fog FLaG.
Q. How can I compute when I want a rule to fire? A. See syntaxp.
Q. How can I add pragmatic advice to a lemma after it has been
proved? For example, how can add a forced hypothesis, a backchain limit,
Q. How can I stop ACL2 from rewriting a term? A. If
you need rewriting done but want to prevent some particular terms from being
rewritten, see hints, specifically
Q. Can I compute which subgoals a hint refers to? A. Yes, see computed-hints. This topic is for advanced users but knowing that it is possible might come in handy someday.
Q. I want the rewriter to always use one theory and then switch to another so that it doesn't use my most complicated before until doing the simple things. A. This is possible but is something for the advanced user. It can be done using a form of computed-hints. See using-computed-hints-7.
Q. Is there a way to attach the same hint to every defthm? A. See default-hints.
Q. How can I just tell ACL2 the proof steps? A. See verify and see proof-builder.
Q. How can I write my own simplifier? A. See meta.
Q. How can I add an axiom or just assume some lemma without proof? A. This is very dangerous but is a good strategy for exploring whether or not a certain set of lemmas (and their rules) is sufficient to prove your goal. See defaxiom and see skip-proofs.
Q. How can redefine a user-defined function? A. This is
tricky. What if you've already proved theorems about the old definition and
then wish to change it? There are several options. See ld-redefinition-action (and note specifically the discussion of updater
function for it,
Q. How do I change a function from
Q. How do I change the guards on a function? A. You can't. Undo it and redefine it.
Q. What is program mode? A. See program.
Q. What does the ACL2 prompt mean? A. See introduction-to-a-few-system-considerations or, specifically, see prompt.
Q. What is logic mode? A. See logic.
Q. How do I get into or out of
Q. How do I quit from ACL2? A. This varies depending on the interface you're using. See introduction-to-a-few-system-considerations.
Q. How do I load a file of definitions and theorems created by someone else? A. See include-book.
Q. How do I create my own book of definitions and theorems? A. See books.
Q. Where are the books referenced by :dir :system on my
machine? A. If your ACL2 is installed on the directory
Q. How can I find out what books are available? A. Go
to the ACL2 home page,
Q. How do I produce my own book? A. See books.
Q. What is a decision procedure? What decision procedures
does ACL2 have? A. A decision procedure is an algorithm
that given enough time and space can determine, for all the formulas in a
certain syntactic class of formulas, whether the formula is a theorem or not.
The most well-known decision procedure is for propositional calculus: by
testing a formula under all the combinations Boolean assignments to the
variables, one can decide if a propositional formula is a theorem. The
syntactic class consists of all formulas you can write using just variables,
constants, and compositions of the functions
Q. ACL2 has the change of variable trick (destructor
elimination) that it does to get rid of
Q. How can I prevent destructor elimination? A. See
Q. How can I prevent cross-fertilization? A. See
Q. How can I prevent generalization? A. See hints, specifically
Q. How can I make ACL2 impose a restriction on a new variable introduced by destructor elimination or generalization? A. See generalize.
Q. What rule classes are there? A. See rule-classes.
Q. What is a theory? A. See theories.
Q. How are hints inherited by the children of a subgoal? A. See hints-and-the-waterfall.
Q. How do I use ACL2 under Emacs? A. See emacs.
Q. How do I use ACL2 under Eclipse? A. See ACL2-Sedan.
Q. How do I interrupt the prover? A. The keyboard sequence
for interrupting a running process depends your operating system, host Common
Lisp, and user interface (e.g., Emacs, Eclipse, etc.). But perhaps a few
examples will help you discover what you need to know. If your host Common
Lisp is GCL or Allegro and you are typing directly to the Common Lisp process,
then you can interrupt a computation by typing ``ctrl-c'' (hold down the
Control key and hit the ``c'' key once). But other Lisps may require some
other control sequence. If you are typing to an Emacs process which is
running the GCL or Allegro Common Lisp process in a shell buffer, you should
type ctrl-c ctrl-c — that is, you have to type the previously mentioned
sequence twice in succession. If you are running the ACL2 Sedan, you can use
the Interrupt Session button on the tool bar. The environment you
enter when you interrupt depends on various factors and basically you should
endeavor to get back to the top level ACL2 command loop, perhaps by typing
some kind of Lisp dependent ``abort'' command like
Q. What is the ACL2 loop? A. That is the name given to the interactive environment ACL2 provides, a ``read-eval-print loop'' in which the user submits successive commands by typing ACL2 expressions and keyword commands. See introduction-to-a-few-system-considerations.
Q. What is raw lisp? A. That is our name for the host Common Lisp in which ACL2 is implemented. See introduction-to-a-few-system-considerations. There is an ACL2 mode named raw mode which is different from ``raw lisp.'' See set-raw-mode.
Q. Can I get a tree-like view of a proof? A. See proof-tree for an Emacs utility that displays proof trees and allows you to navigate through a proof from the proof tree. The ACL2 Sedan also supports proof trees and you should see the ACL2s documentation on that topic.
Q. I used the earlier Boyer-Moore theorem prover, Nqthm. How is ACL2 different? A. See nqthm-to-ACL2.
If you are reading this as part of the tutorial introduction to the theorem prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover.