Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: DEFAULT-PRINT-PROMPT, Next: DEFUN-MODE, Prev: DEFAULT-DEFUN-MODE, Up: MISCELLANEOUS DEFAULT-PRINT-PROMPT the default prompt printed by ld Example prompt: ACL2 p!s> The prompt printed by ACL2 displays the current package, followed by a space, followed by zero or more of the three characters as specified below, followed by the character > printed one or more times, reflecting the number of recursive calls of ld. The three characters in the middle are as follows: p ; when (default-defun-mode (w state)) is :program ! ; when guard checking is on s ; when (ld-skip-proofsp state) is t *Note DEFAULT-DEFUN-MODE::, *Note SET-GUARD-CHECKING::, and *Note LD-SKIP-PROOFSP::. Also *Note LD-PROMPT:: to see how to install your own prompt. Here are some examples with ld-skip-proofsp nil. ACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking off Here are some examples with default-defun-mode of :logic. ACL2 > ; guard checking off, ld-skip-proofsp nil ACL2 s> ; guard checking off, ld-skip-proofsp t ACL2 !> ; guard checking on, ld-skip-proofsp nil ACL2 !s> ; guard checking on, ld-skip-proofsp t  File: acl2-doc-lemacs.info, Node: DEFUN-MODE, Next: DEFUN-MODE-CAVEAT, Prev: DEFAULT-PRINT-PROMPT, Up: MISCELLANEOUS DEFUN-MODE determines whether a function definition is a logical act Two "defun-modes" are supported, :program and :logic. Roughly speaking, :program mode allows you to prototype a function for execution without any proof burdens, while :logic mode allows you to add a new definitional axiom to the logic. The system comes up in :logic mode. Execution of functions whose defun-mode is :program may render ACL2 unsound! *Note DEFUN-MODE-CAVEAT::. When you define a function in the ACL2 logic, that function can be run on concrete data. But it is also possible to reason deductively about the function because each definition extends the underlying logic with a definitional axiom. To insure that the logic is sound after the addition of this axiom, certain restrictions have to be met, namely that the recursion terminates. This can be quite challenging. Because ACL2 is a programming language, you often may wish simply to program in ACL2. For example, you may wish to define your system and test it, without any logical burden. Or, you may wish to define "utility" functions -- functions that are executed to help manage the task of building your system but functions whose logical properties are of no immediate concern. Such functions might be used to generate test data or help interpret the results of tests. They might create files or explore the ACL2 data base. The termination arguments for such functions are an unnecessary burden provided no axioms about the functions are ever used in deductions. Thus, ACL2 introduces the idea of the "defun-mode" of a function. The :mode keyword of defun's declare xarg allows you to specify the defun-mode of a given definition. If no :mode keyword is supplied, the default defun-mode is used; *Note DEFAULT-DEFUN-MODE::. There are two defun-modes, each of which is written as a keyword: :program -- logically undefined but executable outside deductive contexts. :logic -- axiomatically defined as per the ACL2 definitional principle. It is possible to change the defun-mode of a function from :program to :logic. We discuss this below. We think of functions having :program mode as "dangerous" functions, while functions having :logic mode are "safe." The only requirement enforced on :program mode functions is the syntactic one: each definition must be well-formed ACL2. Naively speaking, if a :program mode function fails to terminate then no harm is done because no axiom is added (so inconsistency is avoided) and some invocations of the function may simply never return. This simplistic justification of :program mode execution is faulty because it ignores the damage that might be caused by "mis-guarded" functions. *Note DEFUN-MODE-CAVEAT::. We therefore implicitly describe an imagined implementation of defun-modes that is safe and, we think, effective. But please *Note DEFUN-MODE-CAVEAT::. The default defun-mode is :logic. This means that when you defun a function the system will try to prove termination. If you wish to introduce a function of a different defun-mode use the :mode xargs keyword. Below we show fact introduced as a function in :program mode. (defun fact (n) (declare (xargs :mode :program)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n))))) No axiom is added to the logic as a result of this definition. By introducing fact in :program mode we avoid the burden of a termination proof, while still having the option of executing the function. For example, you can type ACL2 !>(fact 3) and get the answer 6. If you type (fact -1) you will get a hard lisp error due to "infinite recursion." However, the ACL2 theorem prover knows no axioms about fact. In particular, if the term (fact 3) arises in a proof, the theorem prover is unable to deduce that it is 6. From the perspective of the theorem prover it is as though fact were an undefined function symbol of arity 1. Thus, modulo certain important issues (*Note DEFUN-MODE-CAVEAT::), the introduction of this function in :program mode does not imperil the soundness of the system -- despite the fact that the termination argument for fact was omitted -- because nothing of interest can be proved about fact. Indeed, we do not allow fact to be used in logical contexts such as conjectures submitted for proof. It is possible to convert a function from :program mode to :logic mode at the cost of proving that it is admissible. This can be done by invoking (verify-termination fact) which is equivalent to submitting the defun of fact, again, but in :logic mode. (defun fact (n) (declare (xargs :mode :logic)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n))))) This particular event will fail because the termination argument requires that n be nonnegative. A repaired defun, for example with = replaced by <=, will succeed, and an axiom about fact will henceforth be available. Technically, verify-termination submits a redefinition of the :program mode function. This is permitted, even when ld-redefinition-action is nil, because the new definition is identical to the old (except for its :mode and, possibly, other non-logical properties). *Note GUARD:: for a discussion of how to restrict the execution of functions. Guards may be "verified" for functions in :logic mode; *Note VERIFY-GUARDS::.  File: acl2-doc-lemacs.info, Node: DEFUN-MODE-CAVEAT, Next: DEFUNS, Prev: DEFUN-MODE, Up: MISCELLANEOUS DEFUN-MODE-CAVEAT functions with defun-mode of :program considered unsound Technically speaking, in the current implementation, the execution of functions having defun-mode :program may damage the ACL2 system in a way that renders it unsound. *Note DEFUN-MODE:: for a discussion of defun-modes. That discussion describes an imagined implementation that is slightly different from this one. This note explains that the current implementation is open to unsoundness. For discussion of a different soundness issue that is also related to function execution, *Note GENERALIZED-BOOLEANS::. The execution of a function having defun-mode :program may violate Common Lisp guards on the subroutines used. (This may be true even for calls of a function on arguments that satisfy its guard, because ACL2 has not verified that its guard is sufficient to protect its subroutines.) When a guard is violated at runtime all bets are off. That is, no guarantees are made either about the answer being "right" or about the continued rationality of the ACL2 system itself. For example, suppose you make the following defun: (defun crash (i) (declare (xargs :mode :program :guard (integerp i))) (car i)) Note that the declared guard does not in fact adequately protect the subroutines in the body of crash; indeed, satisfying the guard to crash will guarantee that the car expression is in violation of its guard. Because this function is admitted in :program-mode, no checks are made concerning the suitability of the guard. Furthermore, in the current ACL2 implementation, crash is executed directly in Common Lisp. Thus if you call crash on an argument satisfying its guard you will cause an erroneous computation to take place. ACL2 !>(crash 7) Error: Caught fatal error [memory may be damaged] ... There is no telling how much damage is done by this errant computation. In some lisps your ACL2 job may actually crash back to the operating system. In other lisps you may be able to recover from the "hard error" and resume ACL2 in a damaged but apparently functional image. THUS, HAVING A FUNCTION WITH DEFUN-MODE :PROGRAM IN YOUR SYSTEM ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE SOUNDNESS OF OUR SYSTEM. Furthermore ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN :PROGRAM MODE, EVEN IF IT IS ULTIMATELY CONVERTED TO :LOGIC MODE (since its execution could have damaged the system in a way that makes it possible to verify its termination and guards unsoundly). Finally, THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN :PROGRAM MODE AND SO ALL BETS ARE OFF FROM BEFORE YOU START! This hopeless state of current affairs will change, we think. We think we have defined our functions "correctly" in the sense that they can be converted, without "essential" modification, to :logic mode. We think it very unlikely that a mis-guarded function in :program mode (whether ours or yours) will cause unsoundness without some sort of hard lisp error accompanying it. We think that ultimately we can make it possible to execute your functions (interpretively) without risk to the system, even when some have :program mode. In that imagined implementation, code using functions having :program mode would run more slowly, but safely. These functions could be introduced into the logic ex post facto, whereupon the code's execution would speed up because Common Lisp would be allowed to execute it directly. We therefore ask that you simply pretend that this is that imagined implementation, introduce functions in :program mode, use them as convenient and perhaps ultimately introduce some of them in :logic mode and prove their properties. If you use the system this way we can develop (or dismiss) this style of formal system development. BUT BE ON THE LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF YOUR FUNCTIONS HAVING :PROGRAM MODE!  File: acl2-doc-lemacs.info, Node: DEFUNS, Next: DISABLE-FORCING, Prev: DEFUN-MODE-CAVEAT, Up: MISCELLANEOUS DEFUNS an alternative to mutual-recursion Example: (DEFUNS (evenlp (x) (if (consp x) (oddlp (cdr x)) t)) (oddlp (x) (if (consp x) (evenlp (cdr x)) nil))) General Form: (DEFUNS defuns-tuple1 ... defuns-tuplen) is equivalent to (MUTUAL-RECURSION (DEFUN . defuns-tuple1) ... (DEFUN . defuns-tuplen)) In fact, defuns is the more primitive of the two and mutual-recursion is just a macro that expands to a call of defun after stripping off the defun at the car of each argument to mutual-recursion. We provide and use mutual-recursion rather than defuns because by leaving the defuns in place, mutual-recursion forms can be processed by the Emacs tags program. *Note MUTUAL-RECURSION::.  File: acl2-doc-lemacs.info, Node: DISABLE-FORCING, Next: DISABLEDP, Prev: DEFUNS, Up: MISCELLANEOUS DISABLE-FORCING to disallow forced case splits General Form: ACL2 !>:disable-forcing ; disallow forced case splits *Note FORCE:: for a discussion of forced case splits. Disable-forcing is a macro that disables the executable counterpart of the function symbol force; *Note FORCE::. When you want to disable forcing in hints, use a form such as: :in-theory (disable (:executable-counterpart force))  File: acl2-doc-lemacs.info, Node: DISABLEDP, Next: E0-ORD-<, Prev: DISABLE-FORCING, Up: MISCELLANEOUS DISABLEDP determine whether a given name or rune is disabled Examples: :disabledp foo ; returns a list of all disabled runes whose base ; symbol is foo (*Note RUNE::) (disabledp 'foo) ; same as above (i.e., :disabledp foo) :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is ; disabled, else nil (disabledp (:rewrite bar . 1)); same as immediately above Also *Note PR::, which gives much more information about the rules associated with a given event. Disabledp takes one argument, an event name or a rune. In the former case it returns the list of disabled runes associated with that name (in the sense that the rune's "base symbol" is that name; *Note RUNE::). In the latter case it returns t if the given rune is disabled, and nil otherwise.  File: acl2-doc-lemacs.info, Node: E0-ORD-<, Next: E0-ORDINALP, Prev: DISABLEDP, Up: MISCELLANEOUS E0-ORD-< the well-founded less-than relation on ordinals up to epsilon-0 If x and y are both e0-ordinalps (*Note E0-ORDINALP::) then (e0-ord-< x y) is true iff x is strictly less than y. e0-ord-< is well-founded on the e0-ordinalps. When x and y are both nonnegative integers, e0-ord-< is just the familiar "less than" relation (<). e0-ord-< plays a key role in the formal underpinnings of the ACL2 logic. In order for a recursive definition to be admissible it must be proved to "terminate." By terminate we mean that the arguments to the function "get smaller" as the function recurses and this sense of size comparison must be such that there is no "infinitely descending" sequence of ever smaller arguments. That is, the relation used to compare successive arguments must be well-founded on the domain being measured. The most basic way ACL2 provides to prove termination requires the user to supply (perhaps implicitly) a mapping of the argument tuples into the ordinals with some "measure" expression in such a way that the measures of the successive argument tuples produced by recursion decrease according to the relation e0-ord-<. The validity of this method rests on the well-foundedness of e0-ord-< on the e0-ordinalps. Without loss of generality, suppose the definition in question introduces the function f, with one formal parameter x (which might be a list of objects). Then we require that there exist a measure expression, (m x), that always produces an e0-ordinalp. Furthermore, consider any recursive call, (f (d x)), in the body of the definition. Let hyps be the conjunction terms (each of which is either the test of an if in the body or else the negation of such a test) describing the path through the body to the recursive call in question. Then it must be a theorem that (IMPLIES hyps (E0-ORD-< (m (d x)) (m x))). When we say e0-ord-< is "well-founded" on the e0-ordinalps we mean that there is no infinite sequence of e0-ordinalps such that each is smaller than its predecessor in the sequence. Thus, the theorems that must be proved about f when it is introduced establish that it cannot recur forever because each time a recursive call is taken (m x) gets smaller. From this, and the syntactic restrictions on definitions, it can be shown (as on page 44 in "A Computational Logic", Boyer and Moore, Academic Press, 1979) that there exists a function satisfying the definition; intuitively, the value assigned to any given x by the alleged function is that computed by a sufficiently large machine. Hence, the logic is consistent if the axiom defining f is added. *Note E0-ORDINALP:: for a discussion of the ordinals and how to compare two ordinals. The definitional principle permits the use of relations other than e0-ord-< but they must first be proved to be well-founded on some domain. *Note WELL-FOUNDED-RELATION::. Roughly put, alternative relations are shown well-founded by providing an order-preserving mapping from their domain into the ordinals. *Note DEFUN:: for details on how to specify which well-founded relation is to be used.  File: acl2-doc-lemacs.info, Node: E0-ORDINALP, Next: EMBEDDED-EVENT-FORM, Prev: E0-ORD-<, Up: MISCELLANEOUS E0-ORDINALP a recognizer for the ordinals up to epsilon-0 Using the nonnegative integers and lists we can represent the ordinals up to epsilon-0. The ACL2 notion of ordinal is the same as that found in nqthm-1992 and both are very similar to the development given in "New Version of the Consistency Proof for Elementary Number Theory" in The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland Publishing Company, Amsterdam, 1969, pp 132-213. The following essay is intended to provide intuition about ordinals. The truth, of course, lies simply in the ACL2 definitions of e0-ordinalp and e0-ord-<. Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e., 0 0 1 | 2 || 3 ||| 4 |||| ... ... Then "omega," here written as w, is the ordinal that might be written as w |||||..., i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of w in the picture above produces w again, which gives rise to a standard definition of w: w is the least ordinal such that adding another stroke at the beginning does not change the ordinal. We denote by w+w or w*2 the "doubly infinite" sequence that we might write as follows. w*2 |||||... |||||... One way to think of w*2 is that it is obtained by replacing each stroke in 2 (||) by w. Thus, one can imagine w*3, w*4, etc., which leads ultimately to the idea of "w*w," the ordinal obtained by replacing each stroke in w by w. This is also written as "omega squared" or w^2, or: 2 w |||||... |||||... |||||... |||||... |||||... ... We can analogously construct w^3 by replacing each stroke in w by w^2 (which, it turns out, is the same as replacing each stroke in w^2 by w). That is, we can construct w^3 as w copies of w^2, 3 2 2 2 2 w w ... w ... w ... w ... ... Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4, etc., ultimately suggesting w^w. We can then stack omegas, i.e., (w^w)^w etc. Consider the "limit" of all of those stacks, which we might display as follows. . . . w w w w w That is epsilon-0. Below we begin listing some ordinals up to epsilon-0; the reader can fill in the gaps at his or her leisure. We show in the left column the conventional notation, using w as "omega," and in the right column the ACL2 object representing the corresponding ordinal. ordinal ACL2 representation 0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ... 2 w '(2 . 0) ... ... 2 w +w*4+3 '(2 1 1 1 1 . 3) ... ... 3 w '(3 . 0) ... ... w w '((1 . 0) . 0) ... ... w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ... 2 w w '((2 . 0) . 0) ... ... w w w '(((1 . 0) . 0) . 0) ... ... Observe that the sequence of e0-ordinalps starts with the nonnegative integers. This is convenient because it means that if a term, such as a measure expression for justifying a recursive function (*Note E0-ORD-<::) must produce an e0-ordinalp it suffices for it to produce a nonnegative integer. The ordinals listed above are listed in ascending order. This is the ordering tested by e0-ord-<. The "epsilon-0 ordinals" of ACL2 are recognized by the recursively defined function e0-ordinalp. The base case of the recursion tells us that nonnegative integers are epsilon-0 ordinals. Otherwise, an epsilon-0 ordinal is a cons pair (o1 . o2), where o1 is a non-0 epsilon-0 ordinal, o2 is an epsilon-0 ordinal, and if o2 is not an integer then its car (which, by the foregoing, must be an epsilon-0 ordinal) is no greater than o1. Thus, if you think of a (non-integer) epsilon-0 ordinal as a list, each element is an non-0 epsilon-0 ordinal, the ordinals are listed in weakly descending order, and the final cdr of the list is an integer. The function e0-ord-< compares two epsilon-0 ordinals, x and y. If both are integers, e0-ord-< is just x:enable-forcing ; allowed forced case splits *Note FORCE:: for a discussion of forced case splits. Enable-forcing is a macro that enables the executable counterpart of the function symbol force; *Note FORCE::. When you want to enable forcing in hints, use a form such as: :in-theory (enable (:executable-counterpart force))  File: acl2-doc-lemacs.info, Node: ENTER-BOOT-STRAP-MODE, Next: ESCAPE-TO-COMMON-LISP, Prev: ENABLE-FORCING, Up: MISCELLANEOUS ENTER-BOOT-STRAP-MODE The first millisecond of the Big Bang ACL2 functions, e.g., if, that show enter-boot-strap-mode as their defining command are in fact primitives. It is impossible for the system to display defining axioms about these symbols. Enter-boot-strap-mode is a Common Lisp function but not an ACL2 function. It magically creates from nil an ACL2 property list world that lets us start the boot-strapping process. That is, once enter-boot-strap-mode has created its world, it is possible to process the defconsts, defuns, and defaxioms, necessary to bring up the rest of the system. Before that world is created, the attempt by ACL2 even to translate a defun form, say, would produce an error because defun is undefined. Several ACL2 functions show enter-boot-strap-mode as their defining command. Among them are if, cons, car, and cdr. These functions are characterized by axioms rather than definitional equations --- axioms that in most cases are built into our code and hence do not have any explicit representation among the rules and formulas in the system.  File: acl2-doc-lemacs.info, Node: ESCAPE-TO-COMMON-LISP, Next: EVISCERATE-HIDE-TERMS, Prev: ENTER-BOOT-STRAP-MODE, Up: MISCELLANEOUS ESCAPE-TO-COMMON-LISP escaping to Common Lisp Example: ACL2 !>:Q There is no Common Lisp escape feature in the lp. This is part of the price of purity. To execute a form in Common Lisp as opposed to ACL2, exit lp with :q, submit the desired forms to the Common Lisp read-eval-print loop, and reenter ACL2 with (lp).  File: acl2-doc-lemacs.info, Node: EVISCERATE-HIDE-TERMS, Next: EXECUTABLE-COUNTERPART, Prev: ESCAPE-TO-COMMON-LISP, Up: MISCELLANEOUS EVISCERATE-HIDE-TERMS to print (hide ...) as Example: (assign eviscerate-hide-terms t) (assign eviscerate-hide-terms nil) Eviscerate-hide-terms is a state global variable whose value is either t or nil. The variable affects how terms are displayed. If t, terms of the form (hide ...) are printed as . Otherwise, they are printed normally.  File: acl2-doc-lemacs.info, Node: EXECUTABLE-COUNTERPART, Next: EXIT-BOOT-STRAP-MODE, Prev: EVISCERATE-HIDE-TERMS, Up: MISCELLANEOUS EXECUTABLE-COUNTERPART a rule for computing the value of a function Examples: (:executable-counterpart length) which may be abbreviated in theories as (length) Every defun introduces at least two rules used by the theorem prover. Suppose fn is the name of a defun'd function. Then (:definition fn) is the rune (*Note RUNE::) naming the rule that allows the simplifier to replace calls of fn by its instantiated body. (:executable-counterpart fn) is the rune for the rule for how to evaluate the function on known constants. When typing theories it is convenient to know that (fn) is a runic designator that denotes (:executable-counterpart fn). *Note THEORIES::. If (:executable-counterpart fn) is enabled, then when applications of fn to known constants are seen by the simplifier they are computed out by executing the Common Lisp code for fn (with the appropriate handling of guards). Suppose fact is defined as the factorial function. If the executable counterpart rune of fact, (:executable-counterpart fact), is enabled when the simplifier encounters (fact 12), then that term will be "immediately" expanded to 479001600. Such one-step expansions are sometimes counterproductive because they prevent the anticipated application of certain lemmas about the subroutines of the expanded function. Such computed expansions can be prevented by disabling the executable counterpart rune of the relevant function. For example, if (:executable-counterpart fact) is disabled, (fact 12) will not be expanded by computation. In this situation, (fact 12) may be rewritten to (* 12 (fact 11)), using the rule named (:definition fact), provided the system's heuristics permit the introduction of the term (fact 11). Note that lemmas about multiplication may then be applicable (while such lemmas would be inapplicable to 479001600). In many proofs it is desirable to disable the executable counterpart runes of certain functions to prevent their expansion by computation. *Note EXECUTABLE-COUNTERPART-THEORY::. Finally: What do we do about functions that are "constrained" rather than defined, such as the following? (*Note ENCAPSULATE::.) (encapsulate ((foo (x) t)) (local (defun foo (x) x))) Does foo have an executable counterpart? Yes: since the vast majority of functions have sensible executable counterparts, it was decided that *all* functions, even such "constrained" ones, have executable counterparts. We essentially "trap" when such calls are inappropriate. Thus, consider for example: (defun bar (x) (if (rationalp x) (+ x 1) (foo x))) If the term (bar '3) is encountered by the ACL2 rewriter during a proof, and if the :executable-counterpart of bar is enabled, then it will be invoked to reduce this term to '4. However, if the term (bar 'a) is encountered during a proof, then since 'a is not a rationalp and since the :executable-counterpart of foo is only a "trap," then this call of the :executable-counterpart of bar will result in a "trap." In that case, the rewriter will return the term (hide (bar 'a)) so that it never has to go through this process again. *Note HIDE::.  File: acl2-doc-lemacs.info, Node: EXIT-BOOT-STRAP-MODE, Next: FAILED-FORCING, Prev: EXECUTABLE-COUNTERPART, Up: MISCELLANEOUS EXIT-BOOT-STRAP-MODE the end of pre-history Exit-boot-strap-mode is the last step in creating the ACL2 world in which the user lives. It has command number 0. Commands before it are part of the system initialization and extend all the way back to :min. Commands after it are those of the user. Exit-boot-strap-mode is a Common Lisp function but not an ACL2 function. It is called when every defconst, defun, etc., in our source code has been processed under ACL2 and the world is all but complete. exit-boot-strap-mode has only one job: to signal the completion of the boot-strapping.  File: acl2-doc-lemacs.info, Node: FAILED-FORCING, Next: FAILURE, Prev: EXIT-BOOT-STRAP-MODE, Up: MISCELLANEOUS FAILED-FORCING how to deal with a proof failure in a forcing round *Note FORCING-ROUND:: for a background discussion of the notion of forcing rounds. When a proof fails during a forcing round it means that the "gist" of the proof succeeded but some "technical detail" failed. The first question you must ask yourself is whether the forced goals are indeed theorems. We discuss the possibilities below. If you believe the forced goals are theorems, you should follow the usual methodology for "fixing" failed ACL2 proofs, e.g., the identification of key lemmas and their timely and proper use as rules. *Note FAILURE:: and *Note PROOF-TREE::. The rules designed for the goals of forcing rounds are often just what is needed to prove the forced hypothesis at the time it is forced. Thus, you may find that when the system has been "taught" how to prove the goals of the forcing round no forcing round is needed. This is intended as a feature to help structure the discovery of the necessary rules. If a hint must be provided to prove a goal in a forcing round, the appropriate "goal specifier" (the string used to identify the goal to which the hint is to be applied) is just the text printed on the line above the formula, e.g., "[1]Subgoal *1/3"". *Note GOAL-SPEC::. If you solve a forcing problem by giving explicit hints for the goals of forcing rounds, you might consider whether you could avoid forcing the assumption in the first place by giving those hints in the appropriate places of the main proof. This is one reason that we print out the origins of each forced assumption. An argument against this style, however, is that an assumption might be forced in hundreds of places in the main goal and proved only once in the forcing round, so that by delaying the proof you actually save time. We now turn to the possibility that some goal in the forcing round is not a theorem. There are two possibilities to consider. The first is that the original theorem has insufficient hypotheses to insure that all the forced hypotheses are in fact always true. The "fix" in this case is to amend the original conjecture so that it has adequate hypotheses. A more difficult situation can arise and that is when the conjecture has sufficient hypotheses but they are not present in the forcing round goal. This can be caused by what we call "premature" forcing. Because ACL2 rewrites from the inside out, it is possible that it will force hypotheses while the context is insufficient to establish them. Consider trying to prove (p x (foo x)). We first rewrite the formula in an empty context, i.e., assuming nothing. Thus, we rewrite (foo x) in an empty context. If rewriting (foo x) forces anything, that forced assumption will have to be proved in an empty context. This will likely be impossible. On the other hand, suppose we did not attack (foo x) until after we had expanded p. We might find that the value of its second argument, (foo x), is relevant only in some cases and in those cases we might be able to establish the hypotheses forced by (foo x). Our premature forcing is thus seen to be a consequence of our "over eager" rewriting. Here, just for concreteness, is an example you can try. In this example, (foo x) rewrites to x but has a forced hypothesis of (rationalp x). P does a case split on that very hypothesis and uses its second argument only when x is known to be rational. Thus, the hypothesis for the (foo x) rewrite is satisfied. On the false branch of its case split, p simplies to (p1 x) which can be proved under the assumption that x is not rational. (defun p1 (x) (not (rationalp x))) (defun p (x y)(if (rationalp x) (equal x y) (p1 x))) (defun foo (x) x) (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x))) (in-theory (disable foo)) The attempt then to do (thm (p x (foo x))) forces the unprovable goal (rationalp x). Since all "formulas" are presented to the theorem prover as single terms with no hypotheses (e.g., since implies is a function), this problem would occur routinely were it not for the fact that the theorem prover expands certain "simple" definitions immediately without doing anything that can cause a hypothesis to be forced. *Note SIMPLE::. This does not solve the problem, since it is possible to hide the propositional structure arbitrarily deeply. For example, one could define p, above, recursively so that the test that x is rational and the subsequent first "real" use of y occurred arbitrarily deeply. Therefore, the problem remains: what do you do if an impossible goal is forced and yet you know that the original conjecture was adequately protected by hypotheses? One alternative is to disable forcing entirely. *Note DISABLE-FORCING::. Another is to disable the rule that caused the force. A third alternative is to prove that the negation of the main goal implies the forced hypothesis. For example, (defthm not-p-implies-rationalp (implies (not (p x (foo x))) (rationalp x)) :rule-classes nil) Observe that we make no rules from this formula. Instead, we merely :use it in the subgoal where we must establish (rationalp x). (thm (p x (foo x)) :hints (("Goal" :use not-p-implies-rationalp))) When we said, above, that (p x (foo x)) is first rewritten in an empty context we were misrepresenting the situation slightly. When we rewrite a literal we know what literal we are rewriting and we implicitly assume it false. This assumption is "dangerous" in that it can lead us to simplify our goal to nil and give up -- we have even seen people make the mistake of assuming the negation of what they wished to prove and then via a very complicated series of transformations convince themselves that the formula is false. Because of this "tail biting" we make very weak use of the negation of our goal. But the use we make of it is sufficient to establish the forced hypothesis above. A fourth alternative is to weaken your desired theorem so as to make explicit the required hypotheses, e.g., to prove (defthm rationalp-implies-main (implies (rationalp x) (p x (foo x))) :rule-classes nil) This of course is unsatisfying because it is not what you originally intended. But all is not lost. You can now prove your main theorem from this one, letting the implies here provide the necessary case split. (thm (p x (foo x)) :hints (("Goal" :use rationalp-implies-main)))  File: acl2-doc-lemacs.info, Node: FAILURE, Next: FIND-RULES-OF-RUNE, Prev: FAILED-FORCING, Up: MISCELLANEOUS FAILURE how to deal with a proof failure When ACL2 gives up it does not mean that the submitted conjecture is invalid, even if the last formula ACL2 printed in its proof attempt is manifestly false. Since ACL2 sometimes generalizes the goal being proved, it is possible it adopted an invalid subgoal as a legitimate (but doomed) strategy for proving a valid goal. Nevertheless, conjectures submitted to ACL2 are often invalid and the proof attempt often leads the careful reader to the realization that a hypothesis has been omitted or that some special case has been forgotten. It is good practice to ask yourself, when you see a proof attempt fail, whether the conjecture submitted is actually a theorem. If you think the conjecture is a theorem, then you must figure out from ACL2's output what you know that ACL2 doesn't about the functions in the conjecture and how to impart that knowledge to ACL2 in the form of rules. Books could be written about this, but they haven't been yet. However, *Note PROOF-TREE:: for a utility that may be very helpful in locating parts of the failed proof that are of particular interest. See also the discussion of how to read Nqthm proofs and how to use Nqthm rules in "A Computational Logic Handbook" by Boyer and Moore (Academic Press, 1988). If the failure occurred during a forcing round, *Note FAILED-FORCING::.  File: acl2-doc-lemacs.info, Node: FIND-RULES-OF-RUNE, Next: FORCE, Prev: FAILURE, Up: MISCELLANEOUS FIND-RULES-OF-RUNE find the rules named rune General Form: (find-rules-of-rune rune wrld) This function finds all the rules in wrld with :rune rune. It returns a list of rules in their internal form (generally as described by the corresponding defrec). Decyphering these rules is difficult since one cannot always look at a rule object and decide what kind of record it is without exploiting many system invariants (e.g., that :rewrite runes only name rewrite-rules). At the moment this function returns nil if the rune in question is a :refinement rune, because there is no object representing :refinement rules. (:refinement rules cause changes in the 'coarsenings properties.) In addition, if the rune is an :equivalence rune, then congruence rules with that rune will be returned -- because :equivalence lemmas generate some congruence rules -- but the fact that a certain function is now known to be an equivalence relation is not represented by any rule object and so no such rule is returned. (The fact that the function is an equivalence relation is encoded entirely in its presence as a 'coarsening of equal.)  File: acl2-doc-lemacs.info, Node: FORCE, Next: FORCING-ROUND, Prev: FIND-RULES-OF-RUNE, Up: MISCELLANEOUS FORCE identity function used to force a case split When a hypothesis of a conditional rule has the form (force hyp) it is logically equivalent to hyp but has a pragmatic effect. In particular, when the rule is considered, the needed instance of the hypothesis, hyp', is assumed and a special case is generated, requiring the system to prove that hyp' is true in the current context. The proofs of all such "forced assumptions" are delayed until the successful completion of the main goal. *Note FORCING-ROUND::. Forcing should only be used on hypotheses that are always expected to be true, such as the guards of functions. All the power of the theorem prover is brought to bear on a forced hypothesis and no backtracking is possible. If the :executable-counterpart of the function force is disabled, then no hypothesis is forced. *Note ENABLE-FORCING:: and *Note DISABLE-FORCING::. It sometimes happens that a conditional rule is not applied because some hypothesis, hyp, could not be relieved, even though the required instance of hyp, hyp', can be shown true in the context. This happens when insufficient resources are brought to bear on hyp' at the time we try to relieve it. A sometimes desirable alternative behavior is for the system to assume hyp', apply the rule, and to generate explicitly a special case to show that hyp' is true in the context. This is called "forcing" hyp. It can be arranged by restating the rule so that the offending hypothesis, hyp, is embedded in a call of force, as in (force hyp). By using the :corollary field of the rule-classes entry, a hypothesis can be forced without changing the statement of the theorem from which the rule is derived. Technically, force is just a function of one argument that returns that argument. It is generally enabled and hence evaporates during simplification. But its presence among the hypotheses of a conditional rule causes case splitting to occur if the hypothesis cannot be conventionally relieved. Since a forced hypothesis must be provable whenever the rule is otherwise applicable, forcing should be used only on hypotheses that are expected always to be true. A common situation is when the hypothesis is in fact a guard (or part of a guard) of some function involved in the pattern that triggers the rule. Intuitively, if that pattern term occurs in the current conjecture, then its guards had better be true, since otherwise nothing is known about the term. A particularly common situation in which some hypotheses should be forced is in "most general" type-prescription lemmas. If a single lemma describes the "expected" type of a function, for all "expected" arguments, then it is probably a good idea to force the hypotheses of the lemma. Thus, every time a term involving the function arises, the term will be given the expected type and its arguments will be required to be of the expected type. In applying this advice it might be wise to avoid forcing those hypotheses that are in fact just type predicates on the arguments, since the routine that applies type-prescription lemmas has fairly thorough knowledge of the types of all terms. Force can have the additional benefit of causing the ACL2 typing mechanism to interact with the ACL2 rewriter to establish the hypotheses of type-prescription rules. To understand this remark, think of the ACL2 type reasoning system as a rather primitive rule-based theorem prover for questions about Common Lisp types, e.g., "does this expression produce a consp?" "does this expression produce some kind of ACL2 number, e.g., an integerp, a rationalp, or a complex-rationalp?" etc. It is driven by type-prescription rules. To relieve the hypotheses of such rules, the type system recursively invokes itself. This can be done for any hypothesis, whether it is "type-like" or not, since any proposition, p, can be phrased as the type-like question "does p produce an object of type nil?" However, as you might expect, the type system is not very good at establishing hypotheses that are not type-like, unless they happen to be assumed explicitly in the context in which the question is posed, e.g., "If p produces a consp then does p produce nil?" If type reasoning alone is insufficient to prove some instance of a hypothesis, then the instance will not be proved by the type system and a type-prescription rule with that hypothesis will be inapplicable in that case. But by embedding such hypotheses in force expressions you can effectively cause the type system to "punt" them to the rest of the theorem prover. Of course, as already noted, this should only be done on hypotheses that are "always true." In particular, if rewriting is required to establish some hypothesis of a type-prescription rule, then the rule will be found inapplicable because the hypothesis will not be established by type reasoning alone. The ACL2 rewriter uses the type reasoning system as a subsystem. It is therefore possible that the type system will force a hypothesis that the rewriter could establish. Before a forced hypothesis is reported out of the rewriter, we try to establish it by rewriting. This makes the following surprising behavior possible: A type-prescription rule fails to apply because some true hypothesis is not being relieved. The user changes the rule so as to *force* the hypothesis. The system then applies the rule but reports no forcing. How can this happen? The type system "punted" the forced hypothesis to the rewriter, which established it. Finally, we should mention that the rewriter is never willing to force when there is an if term present in the goal being simplified. Since and and or terms are merely abbreviations for if terms, they also prevent forcing.  File: acl2-doc-lemacs.info, Node: FORCING-ROUND, Next: GENERALIZED-BOOLEANS, Prev: FORCE, Up: MISCELLANEOUS FORCING-ROUND a section of a proof dealing with forced assumptions If ACL2 "forces" some hypothesis of some rule to be true, it is obliged later to prove the hypothesis. *Note FORCE::. ACL2 delays the consideration of forced hypotheses until the main goal has been proved. It then undertakes a new round of proofs in which the main goal is essentially the conjunction of all hypotheses forced in the preceding proof. Call this round of proofs the "Forcing Round." Additional hypotheses may be forced by the proofs in the Forcing Round. The attempt to prove these hypotheses is delayed until the Forcing Round has been successfully completed. Then a new Forcing Round is undertaken to prove the recently forced hypotheses and this continues until no hypotheses are forced. Thus, there is a succession of Forcing Rounds. The Forcing Rounds are enumerated starting from 1. The Goals and Subgoals of a Forcing Round are printed with the round's number displayed in square brackets. Thus, "[1]Subgoal 1.3" means that the goal in question is Subgoal 1.3 of the 1st forcing round. To supply a hint for use in the proof of that subgoal, you should use the goal specifier "[1]Subgoal 1.3". *Note GOAL-SPEC::. When a round is successfully completed -- and for these purposes you may think of the proof of the main goal as being the 0th forcing round -- the system collects all of the assumptions forced by the just-completed round. Here, an assumption should be thought of as an implication, (implies context hyp), where context describes the context in which hyp was assumed true. Before undertaking the proofs of these assumptions, we try to "clean them up" in an effort to reduce the amount of work required. This is often possible because the forced assumptions are generated by the same rule being applied repeatedly in a given context. For example, suppose the main goal is about some term (pred (xtrans i) i) and that some rule rewriting pred contains a forced hypothesis that the first argument is a good-inputp. Suppose that during the proof of Subgoal 14 of the main goal, (good-inputp (xtrans i)) is forced in a context in which i is an integerp and x is a consp. (Note that x is irrelevant.) Suppose finally that during the proof of Subgoal 28, (good-inputp (xtrans i)) is forced "again," but this time in a context in which i is a rationalp and x is a symbolp. Since the forced hypothesis does not mention x, we deem the contextual information about x to be irrelevant and discard it from both contexts. We are then left with two forced assumptions: (implies (integerp i) (good-inputp (xtrans i))) from Subgoal 14, and (implies (rationalp i) (good-inputp (xtrans i))) from Subgoal 28. Note that if we can prove the assumption required by Subgoal 28 we can easily get that for Subgoal 14, since the context of Subgoal 28 is the more general. Thus, in the next forcing round we will attempt to prove just (implies (rationalp i) (good-inputp (xtrans i))) and "blame" both Subgoal 14 and Subgoal 28 of the previous round for causing us to prove this. By delaying and collecting the forced assumptions until the completion of the "main goal" we gain two advantages. First, the user gets confirmation that the "gist" of the proof is complete and that all that remains are "technical details." Second, by delaying the proofs of the forced assumptions ACL2 can undertake the proof of each assumption only once, no matter how many times it was forced in the main goal. In order to indicate which proof steps of the previous round were responsible for which forced assumptions, we print a sentence explaining the origins of each newly forced goal. For example, [1]Subgoal 1, below, will focus on (GOOD-INPUTP (XTRANS I)), which was forced in Subgoal 14, above, by applying (:REWRITE PRED-CRUNCHER) to (PRED (XTRANS I) I), and Subgoal 28, above, by applying (:REWRITE PRED-CRUNCHER) to (PRED (XTRANS I) I). In this entry, "[1]Subgoal 1" is the name of a goal which will be proved in the next forcing round. On the next line we display the forced hypothesis, call it x, which is (good-inputp (xtrans i)) in this example. This term will be the conclusion of the new subgoal. Since the new subgoal will be printed in its entirety when its proof is undertaken, we do not here exhibit the context in which x was forced. The sentence then lists (possibly a succession of) a goal name from the just-completed round and some step in the proof of that goal that forced x. In the example above we see that Subgoals 14 and 28 of the just-completed proof forced (good-inputp (xtrans i)) by applying (:rewrite pred-cruncher) to the term (pred (xtrans i) i). If one were to inspect the theorem prover's description of the proof steps applied to Subgoals 14 and 28 one would find the word "forced" (or sometimes "forcibly") occurring in the commentary. Whenever you see that word in the output, you know you will get a subsequent forcing round to deal with the hypotheses forced. Similarly, if at the beginning of a forcing round a rune is blamed for causing a force in some subgoal, inspection of the commentary for that subgoal will reveal the word "forced" after the rule name blamed. Most forced hypotheses come from within the prover's simplifier. When the simplifier encounters a hypothesis of the form (force hyp) it first attempts to establish it by rewriting hyp to, say, hyp'. If the truth or falsity of hyp' is known, forcing is not required. Otherwise, the simplifier actually forces hyp'. That is, the x mentioned above is hyp', not hyp, when the forced subgoal was generated by the simplifier. Once the system has printed out the origins of the newly forced goals, it proceeds to the next forcing round, where those goals are individually displayed and attacked. At the beginning of a forcing round, the enabled structure defaults to the global enabled structure. For example, suppose some rune, rune, is globally enabled. Suppose in some event you disable the rune at "Goal" and successfully prove the goal but force "[1]Goal". Then during the proof of "[1]Goal", rune is enabled "again." The right way to think about this is that the rune is "still" enabled. That is, it is enabled globally and each forcing round resumes with the global enabled structure.