Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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 (``''). Do not expect to understand our answers if you haven't taken the time to read through the tutorial. In the answers below you will see more links into the hypertext reference manual. While such links were marked ``'' in the tutorial, they are not marked that way here. When you enter the reference manual be prepared to explore and assemble a mini-course on the topic of interest, not a quick fix.
Q. How do I find something in the ACL2 documentation? A. Try going to the Search link on the ACL2 home page.
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
Q. How do I define mutually recursive functions? A.
See mutual-recursion. However, you should realize that when two functions,
g, are mutually recursive, properties of
have to be stated simultaneously with properties of
g, since inductive
proofs about one function require inductive hypotheses about the other.
Furthermore, ACL2 does not know how to do inductions for mutually recursive
functions and must be told. See mutual-recursion-proof-example.
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
defun-time. One may also delay guard verification
until ``the right'' lemmas have been proved. By doing guard verification
one can make functions execute faster by allowing the code to avoid runtime
checks. This is especially valuable to industrial users who have large
models used both in verification and as simulation engines for designed
artifacts. In addition, guard verification can give you the assurance that
you are using your functions within their intended domains and hence is a
form of functional specification and verification. However, all these
advantages aside, it is remarkably easy to drift away from the simplest type
regimes and write a guard that raises deep mathematical problems. New users
should not try to confront these problems until they are comfortable with
the theorem prover and with lemma development. Therefore, we strongly
recommend that you forget about types and guards and get used to reasoning
about total functions. When you do decide to learn about them, be prepared
for a complex story involving specification, execution efficiency,
and proof management. See guard.
Q. How do I tell
defun what measure to use?
A. See xargs, specifically
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
y and your measure
(m x y). Suppose the recursive calls of your function are protected
by tests that insure that
y are naturals. Then you might
y are naturals in the measure. But
ACL2 has to prove
(o-p (m x y)), where
o-p is the
predicate that recognizes ordinals (and naturals are ordinals). Note that the
theorem doesn't have any hypotheses! You might intuitively think that your measure
has to be an ordinal just under the conditions that lead to recursive calls. That's not
what ACL2 enforces. It has to be an ordinal, always. So you must change your
specified measure. For example, consider wrapping
nfix around it or around
its uses of
y to coerce those quantities to naturals. The second most likely
explanation is that your measure returns a natural, always, but ACL2 doesn't know that and it
takes induction to prove. This might happen if
m involves some recursive functions.
In this case, prove
(natp (m x y)) before your
defun. Perhaps you should
consider making the
natp lemma a
type-prescription lemma to make ACL2's
typing algorithm aware of it.
Q. How do I tell
defun what well-founded relation to use?
A. See xargs, specifically
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 insure 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
A. See xargs, specifically
:hints (for the termination proofs) and
:guard-hints (for the guard verification proofs).
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
car of some object is
1 at one moment and
later, then the basic logical axiom
(car x) =
(car x) is violated!
However, if the only reference to the old object, e.g., x, was to pass
it to the code that copied and ``changed'' it, then ACL2 can re-use the old
object to produce the new one and the axioms would not object. Such
syntactic restrictions can make x a modifiable structure but they will
impose a heavy burden on you as a programmer: if pass such an x to a
function and the function modifies it, then you must pass x only to that
function and you must return the modified value and use it henceforth. Such
objects are said to be single threaded. See defstobj.
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 an
(in-theory (disable ...)) event; see in-theory.
Another way is to put the lemma and the theorem that needs it into an
encapsulate and wrap a
local around the lemma.
Q. What is an event? A. An event is a command that adds
information to the ACL2 database (the ``logical world''), like
defthm. See events.
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
(:rewritename)]. It could happen that formula generates more than one rewrite rule, e.g., this happens if the conclusion is an
AND. In this case, each conjunctive branch through the conclusion generates a rule named
. i), for i=1,2,... For more details, see rewrite.
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
:GENERALIZE, naming a rule class (see rule-classes), or else should be a list that starts with a rule class and then lists the relevant modifiers. Be sure to include
:REWRITEamong the rule classes if you want the formula to generate a rewrite rule. It doesn't do that automatically if you explicitly specify
Q. How do I rearrange the shape of a formula before generating a
rule from it? A. See rule-classes and read about the
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
(include-book "arithmetic-5/top" :dir :system) is the file named
arithmetic-5/top.lisp on the
acl2-sources/books/ directory where
ever your ACL2 sources are installed. Often, books are well-documented by
comments by their authors. Some books have
on the same directory.
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 command for the formula, supply
(defthm name formula :hints (("Goal" :induct (f x1 ... xn))))where
fis a function that recurs the way you want the induction to unfold and
x1 ... xnare the relevant variables in formula. You usually have to define
fappropriately for each formula that needs an induct hint, though sometimes you can re-use an earlier
for one of the functions in the formula itself. It doesn't matter what value
(f x1 ... xn)returns. All that matters is how it recurs. The termination analysis for
fjustifies the induction done. See hints, especially the section on
:inducthints; also see induction.
Q. ACL2 doesn't know simple arithmetic that can simplify the term
(+ 1 -1 x). A. You should load an arithmetic book whenever you're dealing
with an arithmetic problem. The simplest arithmetic book is loaded with the
(include-book "arithmetic/top-with-meta" :dir :system). If
mod or non-linear arithmetic like
(* x y)
you should use
(include-book "arithmetic-5/top" :dir :system). See
also the discussion of arithmetic books under the ``Lemma Libraries and
Utilities'' link of the ACL2 home page.
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 match
(< (LEN (DELETE E X)) (+ 1 (LEN X))). You should store such lemmas as
:linearrules by using the command:
(defthm len-delete (implies (member e x) (< (len (delete e x)) (len x))) :rule-classes :linear)See 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
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
IFs; see strong-rewrite-rules.
Q. How do I make ACL2 ``guess'' the right instantiation of a free variable?
A. You can provide a
:restrict hint that names the problematic
lemma and provides an instantiation of the free variable. See hints,
:restrict. You could alternatively give a hint that
:uses the rule and provides the appropriate instantiation in full.
See hints, specifically
:use. Recall that ACL2 guesses free variable
instantiations by matching the problematic hypothesis to the assumptions in
the context of the target. If the appropriate assumption is present but
ACL2 is finding another one, try undoing the problematic rule and proving it
again, specifying the
:match-free :all modifier of the
:linear rule class. See rule-classes. Alternatively, undo and prove the
problematic rule again and use a
bind-free form to compute the
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
:in-theory (disable ...). If the use of the
rule is problematic in only one subgoal and the lemma is needed in other subgoals,
disable the lemma only in the problematic subgoal by specifying the subgoal name (e.g.,
"Subgoal 1/3.2.1") as the goal specifier in the hint. If the rule
isn't needed anywhere in the proof, you could use the specifier
"Goal". If you don't think the rule will ever be needed for a while,
you could globally disable it with the event
(in-theory (disable ...))
(see in-theory) executed before the first problematic proof. If the
rule has never been used or must always be disabled, undo it and prove it
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 function named
f then disabling
f will disable the
definitional axiom about
f. But ACL2 has another kind of rule about
f, telling it how to evaluate
f. The rune of this rule is
(:executable-counterpart f). Try disabling that, as in the
:in-theory (disable (:executable-counterpart f)) ...c[)).
Q. How can I make ACL2 use a rule in a proof?
A. See hints, specifically
Q. How can I make ACL2 expand a function call in a proof?
A. You can give an
:See expand hint.
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, or a
syntaxp test? A. You can't. You can undo the lemma, restate it
appropriately, and prove it again. This produces the cleanest database.
Alternatively, you can prove the restated lemma under a new name -- a
task that should be easy since the old version is in the database and will
presumably make the proof trivial -- and then disable the old name.
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
:hands-off. Alternatively, consider
embedding the problematic term in a
hide. Users sometime develop
special theories (see theory) containing just the rules they want and
then use hints to switch to those theories on the appropriate subgoals.
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-checker.
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,
see redef, see redef!, see redef+, and see redef-.
Q. How do I change a function from
:program mode to
:logic mode? A. See verify-termination.
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
mode? A. See program and see logic. You can enter these modes
temporarily for a particular
defun by using
(declare (xargs :mode :program)) or
(declare (xargs :mode :logic))
after the list of formal parameters to the definition.
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 ``distributed books'' referenced by :dir :system
on my machine? A. If your ACL2 is installed on the directory
/acl2-sources, then the distributed books are the files under the
Q. How can I find out what books are available? A. Go to the
ACL2 home page,
http://www.cs.utexas.edu/u/moore/acl2/ and look at the
link labeled ``Lemma Libraries and Utilities.''
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
if. There are, of course, an exponential number of
different assignments so the algorithm can be slow. ACL2 contains a
propositional decision procedure based on symbolic normalization that can be
faster than trying all the combinations of truthvalues -- but is not
guaranteed to be faster. ACL2 also contains an optional bdd procedure.
ACL2 also contains a decision procedure for rational arithmetic involving
variables, rational constants, addition, multiplication by rational
constants, equality, and the various versions of arithmetic
>). It can be extended with
linear lemmas. ACL2 is complete for equality over
uninterpreted (e.g., undefined and unconstrained) function symbols using an
algorithm based on transitive closure of equivalence classes under
functional substitutivity. Finally, you can make ACL2 use other decision
procedures, even ones implemented outside of ACL2; see clause-processor.
Q. ACL2 has the change of variable trick (destructor elimination)
that it does to get rid of
(CAR X) and
(CDR X) by
(CONS A B). Is there a way to make ACL2 do that for
other terms? A. Yes. See elim.
Q. How can I prevent destructor elimination?
A. See hints, specifically
Q. How can I prevent cross-fertilization?
A. See hints, specifically
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 depenent ``abort'' command like
:abort!. You can usually determine what environment
you're in by paying attention to the prompt.
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 documention 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.