FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS

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 make-event.

Q. How do I define mutually recursive functions? A. See mutual-recursion. However, you should realize that when two functions, say f and g, are mutually recursive, properties of f generally 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 automatically at 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 :measure.

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 defun are x and y and your measure is (m x y). Suppose the recursive calls of your function are protected by tests that insure that x and y are naturals. Then you might assume x and 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 x and 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 :well-founded-relation.

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 :rule-classes :well-founded-relation.

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 defun? 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 2 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 defun or 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)

Q. How do I say that I want a formula to be stored as a rewrite rule? A. The command

(defthm name formula)

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

Q. How do I rearrange the shape of a formula before generating a rule from it? A. See rule-classes and read about the :corollary modifier.

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 Readme or README files 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 an :induct hint:

(defthm name
        formula
        :hints (("Goal" :induct (f x1 ... xn))))

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 typically loaded with the event (include-book "arithmetic/top-with-meta" :dir :system). If you're using floor and 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, and see community-books.

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

(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 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, specifically :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 :rewrite or :linear rule class. See rule-classes. Alternatively, undo and prove the problematic rule again and use 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 :cases.

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 again with :rule-classes nil.

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 :hints ((... :in-theory (disable (:executable-counterpart f)) ...c[)).

Q. How can I make ACL2 use a rule in a proof? A. See hints, specifically :use.

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, set-ld-redefinition-action); also 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 :program mode? :Logic 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 books referenced by :dir :system on my machine? A. If your ACL2 is installed on the directory dir/acl2-sources and you follow the standard installation instructions, then the books are typically the files under the directory dir/acl2-sources/books/.

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 and, or, not, implies, iff, and 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 inequality (<, <=, >=, and >). 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 replacing 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 :do-not '(eliminate-destructors).

Q. How can I prevent cross-fertilization? A. See hints, specifically :do-not '(fertilize).

Q. How can I prevent generalization? A. See hints, specifically :do-not '(generalize).

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 A or :q, or :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.