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
functions, say

**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 **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 **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 `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 `type-prescription` lemma to make
ACL2's typing algorithm aware of it.

**Q**. How do I tell **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 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
**A**. See xargs, specifically

**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 *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 `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

**Q**. How do I say that I **do not want a rewrite rule** generated
from a theorem? **A**. The command

(defthmnameformula: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

(defthmnameformula)

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 *name*)]. It could happen that
*formula* generates more than one rewrite rule, e.g., this happens if the
conclusion is an *name**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

(defthmnameformula: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
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

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

(defthmnameformula:hints (("Goal" :induct (f x1 ... xn))))

where *formula*. You
usually have to define

**Q**. ACL2 doesn't know **simple arithmetic** that can simplify the
term **A**. You should load an arithmetic book whenever
you're dealing with an arithmetic problem. The simplest arithmetic book is
typically loaded with the event

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

(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
`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 `bind-free` form to compute the appropriate instantiation.

**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 `rule-classes`

**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 `hints`

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

**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 **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 `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-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** **mode
to** **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?**
**mode?** **A**. See program and see logic.
You can enter these modes temporarily for a particular `defun` by using

**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
*dir**dir*

**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 `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 **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 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.