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.8 Copyright (C) 1989-95 Computational Logic, Inc. (CLI). All rights reserved.  File: acl2-doc-lemacs.info, Node: GUARD-QUICK-REFERENCE, Next: GUARDS-AND-EVALUATION, Prev: GUARD-MISCELLANY, Up: GUARD GUARD-QUICK-REFERENCE brief summary of guard checking and guard verification For a careful introduction to guards, *Note GUARD::. I. GUARD CHECKING DURING EXECUTION *Effect* Guards on definitions are checked at execution time (except for guards on subsidiary calls of recursive or mutually recursive functions). *When does it happen* By default, guards are checked for all forms submitted at the top level. *To disable* :set-guard-checking nil *To (re-)enable* :set-guard-checking t II. GUARD VERIFICATION *Effect* A proof is attempted of the obligations arising from the guards of subsidiary functions in a defun, defthm, or defaxiom event. *When does it happen* Only names of defined functions, defthms, and defaxioms are subject to guard verification. Guard verification may occur when functions are defined (using defun), but it requires an explicit call of verify-guards in order to verify guards for defthms and defaxioms. Constrained functions (*Note ENCAPSULATE::) may not have their guards verified. (verify-guards foo ...) causes guard verification for the defun, defthm, or defaxiom named by foo, if it has not already been successfully done. The default defun-mode (*Note DEFAULT-DEFUN-MODE::) must be :logic, or else this event is ignored. (defun foo ...) causes guard verification of foo if and only if the following conditions are both met. (However, *Note SET-VERIFY-GUARDS-EAGERNESS:: for how to change this behavior.) 1. Foo is processed in :logic mode (either by setting mode :logic globally, or by including :mode :logic in the xargs declaration). 2. The xargs declaration (*Note XARGS::) either specifies :guard or specifies :verify-guards t (or both). (verify-termination foo ...) causes guard verification of foo if foo is a function currently defined in :program mode and the appropriate xargs are supplied, as discussed for the case of defun above. The default defun-mode (*Note DEFAULT-DEFUN-MODE::) must be :logic, or else this event is ignored.  File: acl2-doc-lemacs.info, Node: GUARDS-AND-EVALUATION, Next: GUARDS-FOR-SPECIFICATION, Prev: GUARD-QUICK-REFERENCE, Up: GUARD GUARDS-AND-EVALUATION the relationship between guards and evaluation The guard has no effect on the logical axiom added by the definition of a function. It does, however, have consequences for how calls of that function are evaluated in ACL2. We begin by explaining those consequences, when ACL2 is in its default "mode," i.e., as originally brought up. In subsequent discussion we'll consider other ways that guards can interact with evaluation. For more about guards in general, *Note GUARD::. Also *Note GENERALIZED-BOOLEANS:: for discussion about a subtle issue in the evaluation of certain Common Lisp functions. *Guards and evaluation I: the default* Consider the following very simple definition. (defun foo (x) (cons 1 (cdr x))) First consider how raw Common Lisp behaves when evaluating calls of this function. To evaluate (foo x) for some expression x, first x is evaluated to some value v, and then (cons 1 (cdr x)) is evaluated with x bound to v. For example, if v is (cons 'a 3), then Common Lisp computes (cons 1 3). But if (for example) v is a number, e.g., 7, then there is no way to predict what Common Lisp might do. Some implementations would cause "sensible" errors, others might return nonsense, still others might crash the host machine. The results tend toward the catastrophic if the call of foo in question is in compiled code. Now by default, ACL2 evaluates calls of foo exactly as Common Lisp does, except that it uses guards to check the "legality" of each function call. So for example, since (cdr x) has a guard of (or (consp x) (equal x nil)), the call (foo 7) would cause a "guard violation," as illustrated below. ACL2 !>(foo 7) ACL2 Error in TOP-LEVEL: The guard for the function symbol CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CDR 7). ACL2 !> Thus, the relation between evaluation in ACL2 and evaluation in Common Lisp is that the two produce the very same results, provided there is no guard violation. *Guards and evaluation II:* :set-guard-checking. The ACL2 logic is a logic of total functions. That is, every application of a function defined has a completely specified result. See the documentation for each individual primitive for the specification of what it returns when its guard is violated; for example, *Note CDR::. The presence of guards thus introduces a choice in the sense of evaluation. When you type a form for evaluation do you mean for guards to be checked or not? Put another way, do you mean for the form to be evaluated in Common Lisp (if possible) or in the ACL2 logic? Note: If Common Lisp delivers an answer, it will be the same as in the logic, but it might be erroneous to execute the form in Common Lisp. For example, the ACL2 logic definition of cdr implies that the cdr of an atom is nil; *Note CDR::. So: should (cdr 7) cause a guard violation error or return nil? The top-level ACL2 loop has a variable which controls which sense of execution is provided. By default, "guard checking" is on, by which we mean that guards are checked at runtime, in the sense already described. To turn it off, do :set-guard-checking nil. To turn "guard checking" back on, execute the top-level form :set-guard-checking t. The status of this variable is reflected in the prompt; guard-checking is "on" when the prompt contains an exclamation mark (also *Note DEFAULT-PRINT-PROMPT::). For example, ACL2 !> means guard checking is on and ACL2 > means guard checking is off. The exclamation mark can be thought of as "barring" certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example ACL2 !>(car 'abc) will signal an error, while ACL2 >(car 'abc) will return nil. To return to our previous example: with guard checking off, (foo 7) evaluates to (cons 1 nil). *Guards and evaluation III: guard verification* Consider the defininition of foo given above, but modified so that a reasonable guard of (consp x) is specified, as shown below. (defun foo (x) (declare (xargs :guard (consp x))) (cons 1 (cdr x))) We say "reasonable guard" above because if x is such that (consp x) holds, then the call of cdr in the evaluation of (foo x) will not cause a guard violation. Thus, it "should" be legal to evaluate (foo x), for any such x, simply by evaluating this form in raw Common Lisp. The verify-guards event has been provided for this purpose. Details may be found elsewhere; *Note VERIFY-GUARDS::. Briefly, for any defined function fn, the event (verify-guards fn) attempts to check the condition discussed above, that whenever fn is called on arguments that satisfy its guard, the evaluation of this call will proceed without any guard violation. If this check is successful, then future calls of this sort will be evaluated in raw Common Lisp. Returning to our example above, the (verify-guards foo) will succeed because the guard (consp x) of foo implies the guard generated from the call (cdr x) in the body of the definition, namely, (or (consp x) (equal x nil)) (*Note CDR::). Then the evaluation of (foo (cons 'a 3)) will take place in raw Common Lisp, because (cons 'a 3) satisfies the guard of foo. This ability to dive into raw Common Lisp hinges on the proof that the guards you attach to your own functions are sufficient to insure that the guards encountered in the body are satisfied. This is called "guard verification." Once a function has had its guards verified, then ACL2 can evaluate the function somewhat faster (but see "Guards and evaluation V: efficiency issues" below). Perhaps more importantly, ACL2 can also guarantee that the function will be evaluated correctly by any implementation of Common Lisp (provided the guard of the function is satisfied on the input). That is, if you have verified the guards of a system of functions and you have determined that they work as you wish in your host ACL2 (perhaps by proving it, perhaps by testing), then they will work identically in any Common Lisp. There is a subtlety to our treatment of evaluation of calls of functions whose guards have been verified. If the function's guard is not satisfied by such a call, then no further attempt is made to evaluate any call of that function in raw lisp during the course of evaluation of that call. This is obvious if guard checking is on, because an error is signalled the first time its guard is violated; but in fact it is also true when guard checking is off. *Note GUARD-EXAMPLE:: for an example. *Guards and evaluation IV: functions having :program mode* Strictly speaking, functions in :program mode (*Note DEFUN-MODE::) do not have definitions in the ACL2 logic. So what does it mean to evaluate calls of such functions in ACL2? Our decision is to treat :program functions exactly as we treat :logic functions whose guards have been verified, except that when there is a guard violation we signal an error regardless of whether guard checking is currently on or off. Note that when the guard of a function in :logic mode is violated, there is still a value that the ACL2 logic proves is equal to the given call. But the same cannot be said for a function in :program mode, so we really have no choice but to signal an error when there is a guard violation for such a function. To summarize: as with :logic functions, when a guard has been satisfied on a call of a function with :program mode, no subsidiary guard checking will be done. Consider the same example foo as above, but where foo is submitted in :program mode. Then even with guard checking off, top-level calls of foo will signal a guard violation when the arguments do not satisfy the guard of foo, e.g., (foo 7). Notice that by treating functions in :program mode like functions whose guards have been verified, we are using raw lisp to compute their values when their guards are met. We do not check guards any further once raw lisp is invoked. This can lead to hard lisp errors if the guards are not appropriate, as illustrated below. ACL2 >:program ACL2 p>(defun foo (x) (declare (xargs :guard t)) (cons 1 (cdr x))) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02) FOO ACL2 p>(foo 3) Error: 3 is not of type LIST. Fast links are on: do (use-fast-links nil) for debugging Error signalled by CDR. Broken at COND. Type :H for Help. ACL2>> *Note DEFUN-MODE-CAVEAT::. *Guards and evaluation V: efficiency issues* We have seen that by verifying the guards for a :logic function, we arrange that raw lisp is used for evaluation of calls of such functions when the arguments satisfy its guard. This has several apparent advantages over the checking of guards as we go. First, the savings is magnified as your system of functions gets deeper: the guard is checked upon the top-level entry to your system and then raw Common Lisp does all the computing. Second, if the raw Common Lisp is compiled, enormous speed-ups are possible. Third, if your Common Lisp or its compiler does such optimizations as tail-recursion removal, raw Common Lisp may be able to compute your functions on input much "bigger" than ACL2 can. The first of these advantages is quite important if you have complicated guards. However, the other two advantages are probably not very important, as we now explain. When a function is defined in :logic mode, its defun is executed in raw Common Lisp. (We might call this the "primary" raw lisp definition of the function.) However, a corresponding "logic definition" is also executed. The "logic definition" is a defun in raw lisp that checks guards at runtime and escapes to the primary raw lisp definition if the guard holds of the arguments and the function has already had its guards verified. Otherwise the logic definition executes the body of the function by calling the logic definitions of each subroutine. Now it is true that compilation generally speeds up execution enormously. However, the :comp command (*Note COMP::) compiles both of the raw lisp definitions associated with a :logic function. Also, we have attempted to arrange that for every tail recursion removal done on the actual defun, a corresonding tail recursion removal is done on the "logic definition." We believe that in most cases, the logic definition executes almost as fast as the primary raw lisp definition, at least if the evaluation of the guards is fast. So, the main advantage of guard verification is probably that it lets you know that the function may be executed safely in raw lisp, returning the value predicted by the ACL2 logic, whenever its arguments satisfy its guard. We envision the development of systems of applicative lisp functions that have been developed and reasoned about using ACL2 but which are intended for evaluation in raw Common Lisp (perhaps with only a small "core" of ACL2 loaded), so this advantage of guard verification is important. Nevertheless, guard verification might be important for optimal efficiency when the functions make use of type declarations. For example, at this writing, the GCL implementation of Common Lisp can often take great advantage of declare forms that assign small integer types to formal parameters. To continue the discussion of guards, *Note GUARDS-FOR-SPECIFICATION:: to read about the use of guards as a specification device.  File: acl2-doc-lemacs.info, Node: GUARDS-FOR-SPECIFICATION, Prev: GUARDS-AND-EVALUATION, Up: GUARD GUARDS-FOR-SPECIFICATION guards as a specification device A use of guard verification that has nothing to do with efficiency is as a way to gain confidence in specifications. This use has the feel of "types" in many traditional programming languages, though guards allow much greater expressiveness than most systems of types (and unfortunately, as a result they are not syntactically checkable). For more discussion of guards in general, *Note GUARD::. Suppose you have written a collection of function definitions that are intended to specify the behavior of some system. Perhaps certain functions are only intended to be called on certain sorts of inputs, so you attach guards to those functions in order to "enforce" that requirement. And then, you verify the guards for all those functions. Then what have you gained, other than somewhat increased efficiency of execution (as explained above), which quite possibly isn't your main concern? You have gained the confidence that when evaluating any call of a (specification) function whose arguments satisfy that function's guard, all subsequent function calls during the course of evaluation will have this same property, that the arguments satisfy the guard of the calling function. In logical terms, we can say that the equality of the original call with the returned value is provable from weakened versions of the definitions, where each definitional axiom is replaced by an implication whose antecedent is the requirement that the arguments satisfy the guard and whose consequent is the original axiom. For example, (defun foo (x) (declare (xargs :guard (consp x))) (cons 1 (cdr x))) originally generates the axiom (equal (foo x) (cons 1 (cdr x))) but in fact, when evaluation involves no guard violation then the following weaker axiom suffices in the justification of the evaluation. (implies (consp x) (equal (foo x) (cons 1 (cdr x)))) If you are following links to read this documentation as a hypertext style document, then please *Note GUARD-MISCELLANY::. This concludes our discussion of guards with miscellaneous remarks, and also contains pointers to related topics.  File: acl2-doc-lemacs.info, Node: HIDE, Next: HINTS, Prev: GUARD, Up: MISCELLANEOUS HIDE hide a term from the rewriter Hide is actually the identity function: (hide x) = x for all x. However, terms of the form (hide x) are ignored by the ACL2 rewriter, except when explicit :expand hints are given for such terms (*Note HINTS::). They are also ignored by the induction heuristics. *Note EVISCERATE-HIDE-TERMS:: for how to affect the printing of such terms.  File: acl2-doc-lemacs.info, Node: HINTS, Next: I-AM-HERE, Prev: HIDE, Up: MISCELLANEOUS HINTS advice to the theorem proving process Examples: The following :hints value is nonsensical. Nevertheless, it illustrates all of the available hint keywords: :hints (("Goal" :do-not-induct t :do-not '(generalize fertilize) :expand ((assoc x a) (member y z)) :restrict ((<-trans ((x x) (y (foo x))))) :hands-off (length binary-append) :in-theory (set-difference-theories (current-theory :here) '(assoc)) :induct (and (nth n a) (nth n b)) :use ((:instance assoc-of-append (x a) (y b) (z c)) (:functional-instance (:instance p-f (x a) (y b)) (p consp) (f assoc))) :bdd (:vars (c a0 b0 a1 b1) :prove nil :bdd-constructors (cons)) :cases ((true-listp a) (consp a)) :by ((:instance rev-rev (x (cdr z)))))) A very common hint is the :use hint, which in general takes as its value a list of "lemma instances" (*Note LEMMA-INSTANCE::) but which allows a single lemma name as a special case: :hints (("[1]Subgoal *1/1.2'" :use lemma23)) Background: Hints are allowed in all events that use the theorem prover. During defun events there are two different uses of the theorem prover: one to prove termination and another to verify the guards. To pass a hint to the theorem prover during termination proofs, use the :hints keyword in the defun's xargs declaration. To pass a hint to the theorem prover during the guard verification of defun, use the :guard-hints keyword in the defun's xargs declaration. The verify-guards event and the defthm event also use the theorem prover. To pass hints to them, use the :hints keyword argument to the event. General Form of :hints: ((goal-spec :key1 val1 ... :keyn valn) ... (goal-spec :key1 val1 ... :keyn valn)) where goal-spec is as described in the documentation for goal-spec and the keys and their respective values are shown below with their interpretations. :DO-NOT-INDUCT Value is t, name or nil, indicating whether induction is permitted under the specified goal. If value is t, then the attempt to apply induction to the indicated goal or any subgoal under the indicated goal will immediately cause the theorem prover to report failure. Thus, the indicated goal must be proved entirely by simplification, destructor elimination, and the other "waterfall" processes. Induction to prove the indicated goal (or any subgoal) is not permitted. See however the :induct hint below. If value is a symbol other than t or nil, the theorem prover will give a "bye" to any subgoal that would otherwise be attacked with induction. This will cause the theorem prover to fail eventually but will collect the necessary subgoals. If value is nil, this hint means induction is permitted. Since that is the default, there is no reason to use the value nil. :DO-NOT Value is a term having at most the single free variable world, which when evaluated (with world bound to the current ACL2 logical world) produces a list of symbols that is a subset of the list (preprocess ;propositional logic, simple rules simplify ;as above plus rewriting, linear arithmetic eliminate-destructors fertilize ;use of equalities generalize eliminate-irrelevance). The hint indicates that the "processes" named should not be used at or below the goal in question. Thus, to prevent generalization and fertilization, say, include the hint :do-not '(generalize fertilize) If value is a single symbol, as in :do-not generalize, it is taken to be '(value). :EXPAND Value is a true list of terms, each of which is of one of the forms (let ((v1 t1)...) b) or (fn t1 ... tn), where fn is a defined function symbol with formals v1, ..., vn, and body b. Such a term is said to be "expandable:" it can be replaced by the result of substituting the ti's for the vi's in b. The terms listed in the :expand hint are expanded when they are encountered by the simplifier while working on the specified goal or any of its subgoals. We permit value to be a single such term instead of a singleton list. *Note*: Also allowed are "terms" of the form (:free (var1 var2 ... varn) pattern) where the indicated variables are distinct and pattern is a term. Such "terms" indicate that we consider the indicated variables to be instantiatable, in the following sense: whenever the simplifier encounters a term that can be obtained from pattern by instantiating the variables (var1 var2 ... varn), then it expands that term. :HANDS-OFF Value is a true list of function symbols or lambda expressions, indicating that under the specified goal applications of these functions are not to be rewritten. value may also be a single function symbol or lambda expression instead of a list. :IN-THEORY Value is a "theory expression," i.e., a term having at most the single free variable world which when evaluated (with world bound to the current ACL2 logical world (*Note WORLD::)) will produce a theory to use as the current theory for the goal specified. *Note THEORIES::. :INDUCT Value is either t or a term containing at least one recursively defined function symbol; if t, this hint indicates that the system should proceed to apply its induction heuristic to the specified goal produced (without trying simplification, etc.); if value is a term other than t, then not only should the system apply induction immediately, but it should analyze value rather than the goal to generate its induction scheme. Merging and the other induction heuristics are applied. Thus, if value contains several mergeable inductions, the "best" will be created and chosen. E.g., the :induct hint (and (nth i a) (nth j a)) suggests simultaneous induction on i, j, and a. If both an :induct and a :do-not-induct hint are supplied for a given goal then the indicated induction is applied to the goal and the :do-not-induct hint is inherited by all subgoals generated. :USE Value is a lemma-instance or a true list of lemma-instances, indicating that the propositions denoted by the instances be added as hypotheses to the specified goal. *Note LEMMA-INSTANCE::. Note that :use makes the given instances available as ordinary hypotheses of the formula to be proved. The :instance form of a lemma-instance permits you to instantiate the free variables of previously proved theorems any way you wish; but it is up to you to provide the appropriate instantiations because once the instances are added as hypotheses their variables are no longer instantiable. These new hypotheses participate fully in all subsequent rewriting, etc. If the goal in question is in fact an instance of a previously proved theorem, you may wish to use :by below. :BDD This hint indicates that ordered binary decision diagrams (BDDs) with rewriting are to be used to prove or simplify the goal. *Note BDD:: for an introduction to the ACL2 BDD algorithm. Value is a list of even length, such that every other element, starting with the first, is one of the keywords :vars, :bdd-constructors, :prove, or literal. Each keyword that is supplied should be followed by a value of the appropriate form, as shown below; for others, a default is used. Although :vars must always be supplied, we expect that most users will be content with the defaults used for the other values. :vars -- A list of ACL2 variables, which are to be treated as Boolean variables. The prover must be able to check, using trivial reasoning (*Note TYPE-SET::), that each of these variables is Boolean in the context of the current goal. Note that the prover will use very simple heuristics to order any variables that do not occur in :vars (so that they are "greater than" the variables that do occur in :vars), and these heuristics are often far from optimal. In addition, any variables not listed may fail to be assumed Boolean by the prover, which is likely to seriously impede the effectiveness of ACL2's BDD algorithm. Thus, users are encouraged *not* to rely on the default order, but to supply a list of variables instead. Finally, it is allowed to use a value of t for vars. This means the same as a nil value, except that the BDD algorithm is directed to fail unless it can guarantee that all variables in the input term are known to be Boolean (in a sense discussed elsewhere; *Note BDD-ALGORITHM::). :literal -- An indication of which part of the current goal should receive BDD processing. Possible values are: :all treat entire goal as a single literal (the default) :conc process the conclusion n process the hypothesis with index n (1, 2, ...) :bdd-constructors -- When supplied, this value should be a list of function symbols in the current ACL2 world; it is (cons) by default, unless :bdd-constructors has a value in the acl2-defaults-table by default, in which case that value is the default. We expect that most users will be content with the default. *Note BDD-ALGORITHM:: for information about how this value is used. :prove -- When supplied, this value should be t or nil; it is t by default. When the goal is not proved and this value is t, the entire proof will abort. Use the value nil if you are happy to the proof to go on with the simplified term. :CASES Value is a non-empty list of terms. For each term in the list, a new goal is created from the current goal by assuming that term; and also, in essence, one additional new goal is created by assuming all the terms in the list false. We say "in essence" because if the disjunction of the terms supplied is a tautology, then that final goal will be a tautology and hence will in fact never actually be created. :BY Value is a lemma-instance, nil, or a new event name. If the value is a lemma-instance (*Note LEMMA-INSTANCE::), then it indicates that the goal (when viewed as a clause) is subsumed by the proposition denoted by the instance (when viewed as a clause). To view a formula as a clause, union together the negations of the hypotheses and add the conclusion. For example, (IMPLIES (AND (h1 t1) (h2 t2)) (c t1)) may be viewed as the clause {~(h1 t1) ~(h2 t2) (c t1)}. Clause c1 is "subsumed" by clause c2 iff some instance of c2 is a subset of c1. For example, the clause above is subsumed by {~(h1 x) (c x)}, which when viewed as a formula is (implies (h1 x) (c x)). If the value is nil or a new name, the prover does not even attempt to prove the goal to which this hint is attached. Instead the goal is given a "bye", i.e., it is skipped and the proof attempt continues as though the goal had been proved. If the prover terminates without error then it reports that the proof would have succeeded had the indicated goals been proved and it prints an appropriate defthm form to define each of the :by names. The "name" nil means "make up a name." The system does not attempt to check the uniqueness of the :by names (supplied or made up), since by the time those goals are proved the namespace will be cluttered still further. Therefore, the final list of "appropriate" defthm forms may be impossible to admit without some renaming by the user. If you must invent new names, remember to substitute the new ones for the old ones in the :by hints themselves. :RESTRICT (Warning: This is a sophisticated hint, intended for advanced users. This hint was suggested by Bishop Brock.) Value is an association list. Its members are of the form (x subst1 subst2 ...), where: x is either (1) a rune whose car is :rewrite or (2) an event name corresponding to one or more such runes; and (subst1 subst2 ...) is a non-empty list of substitutions, i.e., of association lists pairing variables with terms. First consider the case that x is a :rewrite rune. First recall that without this hint, the rewrite rule named x is used by matching its left-hand side (call it lhs) against the term currently being considered by the rewriter, that is, by attempting to find a substitution s such that the instantiation of lhs using s is equal to that term. If however the :restrict hint contains (x subst1 subst2 ...), then this behavior will be modified by restricting s so that it must extend subst1; and if there is no such s, then s is restricted so that it must extend subst2; and so on, until the list of substitutions is exhausted. If no such s is found, then the rewrite rule named x is not applied to that term. Finally, if x is an event name corresponding to one or more :rewrite runes (that is, x is the "base symbol" of such runes; *Note RUNE::), say runes r1, ... rn, then the meaning is the same except that (x subst1 subst2 ...) is replaced by (ri subst1 subst2 ...) for each i. Once this replacement is complete, the hint may not contain two members whose car is the same rune. Note that the substitutions in :restrict hints refer to the variables actually appearing in the goals, not to the variables appearing in the :rewrite rule being restricted. Here is an example, supplied by Bishop Brock. Suppose that the database includes the following rewrite rule, which is probably kept disabled. (We ignore the question of how to prove this rule.) cancel-<-*$free: (implies (and (rationalp x) (rationalp y) (rationalp z)) (equal (< y z) (if (< x 0) (> (* x y) (* x z)) (if (> x 0) (< (* x y) (* x z)) (hide (< y z)))))) Then ACL2 can prove the following theorem (unless other rules get in the way), essentially by multiplying both sides by x. (thm (implies (and (rationalp x) (< 1 x)) (< (/ x) 1)) :hints (("Goal" :in-theory (enable cancel-<-*$free) :restrict ((cancel-<-*$free ((x x) (y (/ x)) (z 1))))))) The :restrict hint above says that the variables x, y, and z in the rewrite rule cancel-<-*$free above should be instantiated respectively by x, (/ x), and 1. Thus (< y z) becomes (< (/ x) 1), and this inequality is replaced by the corresponding instance of the right-hand-side of cancel-<-*$free. Since the current conjecture assumes (< 1 x), that instance of the right-hand side simplifies to (< (* x (/ x)) (* x 1)) which in turn simplifies to (< 1 x), a hypothesis in the present theorem.  File: acl2-doc-lemacs.info, Node: I-AM-HERE, Next: IMMEDIATE-FORCE-MODEP, Prev: HINTS, Up: MISCELLANEOUS I-AM-HERE a convenient marker for use with rebuild Example Input File for Rebuild: (defun fn1 (x y) ...) (defthm lemma1 ...) (defthm lemma2 ...) (i-am-here) The following lemma won't go through. I started typing the hint but realized I need to prove a lemma first. See the failed proof attempt in foo.bar. I'm going to quit for the night now and resume tomorrow from home. (defthm lemma3 ... :hints (("Goal" :use (:instance ??? ... By putting an (i-am-here) form at the "frontier" of an evolving file of commands, you can use rebuild to load the file up to the (i-am-here). I-am-here simply returns an ld error triple and any form that "causes an error" will do the same job. Note that the text of the file after the (i-am-here) need not be machine readable.  File: acl2-doc-lemacs.info, Node: IMMEDIATE-FORCE-MODEP, Next: IN-PACKAGE, Prev: I-AM-HERE, Up: MISCELLANEOUS IMMEDIATE-FORCE-MODEP when executable counterpart is enabled, forced hypotheses are attacked immediately This function symbol is defined simply to provide a rune which can be enabled and disabled. Enabling (:executable-counterpart immediate-force-modep) causes ACL2 to attack forced hypotheses immediately instead of delaying them to the next forcing round. Example Hints :in-theory (disable (:executable-counterpart immediate-force-modep)) ; delay forced hyps to forcing round :in-theory (enable (:executable-counterpart immediate-force-modep)) ; split on forced hyps immediately *Note FORCE:: for background information. When a forced hypothesis cannot be established a record is made of that fact and the proof continues. When the proof succeeds a "forcing round" is undertaken in which the system attempts to prove each of the forced hypotheses explicitly. However, if the rune (:executable-counterpart immediate-force-modep) is enabled at the time the hypothesis is forced, then ACL2 does not delay the attempt to prove that hypothesis but undertakes the attempt more or less immediately.  File: acl2-doc-lemacs.info, Node: IN-PACKAGE, Next: INVISIBLE-FNS-ALIST, Prev: IMMEDIATE-FORCE-MODEP, Up: MISCELLANEOUS IN-PACKAGE select current package Example: (in-package "MY-PKG") General Form: (in-package str) where str is a string that names an existing ACL2 package, i.e., one of the initial packages such as "KEYWORD" or "ACL2" or a package introduced with defpkg. For a complete list of the known packages created with defpkg, evaluate (strip-cars (known-package-alist state)). *Note DEFPKG::. In-package forms can only be typed at the top-level of the ACL2 loop and as the first form in a file being loaded or compiled.  File: acl2-doc-lemacs.info, Node: INVISIBLE-FNS-ALIST, Next: KEYWORD-COMMANDS, Prev: IN-PACKAGE, Up: MISCELLANEOUS INVISIBLE-FNS-ALIST functions that are invisible to the loop-stopper algorithm Examples: ACL2 !>(invisible-fns-alist (w state)) ((binary-+ unary--) (binary-* unary-/) (unary-- unary--) (unary-/ unary-/)) Among other things, the setting above has the effect of making unary-- "invisible" for the purposes of applying permutative :rewrite rules to binary-+ trees. *Note SET-INVISIBLE-FNS-ALIST::. The notion of "invisible functions" has to do with the control mechanism on permutative :rewrite rules. *Note LOOP-STOPPER:: for a detailed discussion of the control mechanism. *Note SET-INVISIBLE-FNS-ALIST:: for a discussion of how to set the invisible functions alist.  File: acl2-doc-lemacs.info, Node: KEYWORD-COMMANDS, Next: LD-ERROR-ACTION, Prev: INVISIBLE-FNS-ALIST, Up: MISCELLANEOUS KEYWORD-COMMANDS how keyword commands are processed Examples: user type-in form evaluated :pc 5 (ACL2::PC '5) :pcs app rev (ACL2::PCS 'app 'rev) :length (1 2 3) (ACL2::LENGTH '(1 2 3)) When a keyword, :key, is read as a command, ACL2 determines whether the symbol with the same name in the "ACL2" package, acl2::key, is a function or simple macro of n arguments. If so, ACL2 reads n more objects, obj1, ..., objn, and then acts as though it had read the following form (for a given key): (ACL2::key 'obj1 ... 'objn) Thus, by using the keyword command hack you avoid typing the parentheses, the "ACL2" package name, and the quotation marks. Note the generality of this hack. Almost any function or macro in the "ACL2" package can be so invoked, not just "commands." Indeed, there is no such thing as a distinguished class of commands. The one caveat is that the keyword hack can be used to invoke a macro only if that macro has a simple argument list -- one containing no lambda keywords (such as &rest), since they complicate or render impossible the task of deciding how many objects to read. Users may take advantage of the keyword command hack by defining functions and macros in the "ACL2" package.  File: acl2-doc-lemacs.info, Node: LD-ERROR-ACTION, Next: LD-ERROR-TRIPLES, Prev: KEYWORD-COMMANDS, Up: MISCELLANEOUS LD-ERROR-ACTION determines ld's response to an error Ld-error-action is an ld special (*Note LD::). The accessor is (ld-error-action state) and the updater is (set-ld-error-action val state). Ld-error-action must be :continue, :return, or :error. The initial value of ld-error-action is :continue, which means that the top-level ACL2 command loop will not exit when an error is caused by user-typein. But the default value for ld-error-action on calls of ld is :return. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-error-action is one of them. If, while ld-error-triples is t, a form evaluates to three results, the first of which is non-nil and the third of which is state, an error is said to have occurred. If an error occurs, ld's action depends on ld-error-action. If it is :continue, ld just continues processing the forms in standard-oi. If it is :return, ld stops and returns as though it had emptied the channel. If it is :error, ld stops and returns, signalling an error to its caller.  File: acl2-doc-lemacs.info, Node: LD-ERROR-TRIPLES, Next: LD-EVISC-TUPLE, Prev: LD-ERROR-ACTION, Up: MISCELLANEOUS LD-ERROR-TRIPLES determines whether a form caused an error during ld Ld-error-triples is an ld special (*Note LD::). The accessor is (ld-error-triples state) and the updater is (set-ld-error-triples val state). Ld-error-triples must be either t or nil. The initial value of ld-error-triples is t. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-error-triples is one of them. If this variable has the value t then when a form evaluates to 3 values, the first of which is non-nil and the third of which is state, an error is deemed to have occurred. When an error occurs in evaluating a form, ld rolls back the ACL2 world to the configuration it had at the conclusion of the last error-free form. Then ld takes the action determined by ld-error-action.  File: acl2-doc-lemacs.info, Node: LD-EVISC-TUPLE, Next: LD-KEYWORD-ALIASES, Prev: LD-ERROR-TRIPLES, Up: MISCELLANEOUS LD-EVISC-TUPLE determines whether ld suppresses details when printing Ld-evisc-tuple is an ld special (*Note LD::). The accessor is (ld-evisc-tuple state) and the updater is (set-ld-evisc-tuple val state). Ld-evisc-tuple must be either nil or a list of the form (alist nil nil print-level print-length hiding-cars) where alist is an alist that pairs objects to strings, print-level and print-length are either nil or non-negative integers, and hiding-cars is a list of symbols. The initial value of ld-evisc-tuple is nil. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-evisc-tuple is one of them. Ld may print the forms it is evaluating and/or the results of evaluation. If the value of ld-evisc-tuple is a list as shown above, then ld "eviscerates" the objects it prints before printing them. To "eviscerate" an object we replace certain substructures within it by strings which are printed in their stead. Print-level and print-length, above, are used as described in CLTL (pp 372) to replace those substructures deeper than print-level by "#" and those longer than print-length by "...". Alist is used to replace any substructure occuring as a key in alist by the corresponding string. Finally, any consp x that starts with one of the symbols in hiding-cars is printed as .  File: acl2-doc-lemacs.info, Node: LD-KEYWORD-ALIASES, Next: LD-POST-EVAL-PRINT, Prev: LD-EVISC-TUPLE, Up: MISCELLANEOUS LD-KEYWORD-ALIASES allows the abbreviation of some keyword commands Example: (set-ld-keyword-aliases '((:q 0 q-fn) (:e 0 exit-acl2-macro)) state) Ld-keyword-aliases is an ld special (*Note LD::). The accessor is (ld-keyword-aliases state) and the updater is (set-ld-keyword-aliases val state). Ld-keyword-aliases must be an alist, each element of which is of the form (:keyword n fn), where :keyword is a keyword, n is a nonnegative integer, and fn is a function symbol of arity n, a macro symbol, or a lambda expression of arity n. When keyword is typed as an ld command, n more forms are read, x1, ..., xn, and the form (fn 'x1 ... 'xn) is then evaluated. The initial value of ld-keyword-aliases is nil. In the example above, :q has been redefined to have the effect of executing (q-fn), so for example if you define (defmacro q-fn () '(er soft 'q "You un-bound :q and now we have a soft error.")) then :q will cause an error, and if you define (defmacro exit-acl2-macro () '(exit-ld state)) then :e will cause the effect (it so happens) that :q normally has. If you prefer :e to :q for exiting the ACL2 loop, you might even want to put such definitions of q-fn and exit-acl2-macro together with the set-ld-keyword-aliases form above in your "acl2-customization.lisp" file; *Note ACL2-CUSTOMIZATION::. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-keyword-aliases is one of them. Ld-keyword-aliases affects how keyword commands are parsed. Generally speaking, ld's command interpreter reads ":fn x1 ... xn" as "(fn 'x1 ... 'xn)" when :fn is a keyword and fn is the name of an n-ary function. But this parse is overridden, as described above, for the keywords bound in ld-keyword-aliases.  File: acl2-doc-lemacs.info, Node: LD-POST-EVAL-PRINT, Next: LD-PRE-EVAL-FILTER, Prev: LD-KEYWORD-ALIASES, Up: MISCELLANEOUS LD-POST-EVAL-PRINT determines whether and how ld prints the result of evaluation Ld-post-eval-print is an ld special (*Note LD::). The accessor is (ld-post-eval-print state) and the updater is (set-ld-post-eval-print val state). Ld-post-eval-print must be either t, nil, or :command-conventions. The initial value of ld-post-eval-print is :command-conventions. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-post-eval-print is one of them. If this global variable is t, ld prints the result. In the case of a form that produces multiple values, ld prints the list containing them all (which, logically speaking, is what the form returned). If ld-post-eval-print is nil, ld does not print the values. This is most useful when ld is used to load a previously processed file. Finally, if ld-post-eval-print is :command-conventions then ld prints the result but treats "error triples" specially. An "error triple" is a result, (mv erp val state), that consists of three values, the third of which is state. Many ACL2 functions use such triples to signal errors. The convention is that if erp (the first value) is nil, then the function is returning val (the second value) as its conventional single result and possibly side-effecting state (as with some output). If erp is t, then an error has been caused, val is irrelevant and the error message has been printed in the returned state. Example ACL2 functions that follow this convention include defun and in-package. If such "error producing" functions are evaluated while ld-post-eval-print is set to t, then you would see them producing lists of length 3. This is disconcerting to users accustomed to Common Lisp (where these functions produce single results but sometimes cause errors or side-effect state). When ld-post-eval-print is :command-conventions and a form produces an error triple (mv erp val state) as its value, ld prints nothing if erp is non-nil and otherwise ld prints just val. Because it is a misrepresentation to suggest that just one result was returned, ld prints the value of the global variable 'triple-print-prefix before printing val. 'triple-print-prefix is initially " ", which means that when non-erroneous error triples are being abbreviated to val, val appears one space off the left margin instead of on the margin. In addition, when ld-post-eval-print is :command-conventions and the value component of an error triple is the keyword :invisible then ld prints nothing. This is the way certain commands (e.g., :pc) appear to return no value. By printing nothing when an error has been signalled, ld makes it appear that the error (whose message has already appeared in state) has "thrown" the computation back to load without returning a value. By printing just val otherwise, we suppress the fact that state has possibly been changed.  File: acl2-doc-lemacs.info, Node: LD-PRE-EVAL-FILTER, Next: LD-PRE-EVAL-PRINT, Prev: LD-POST-EVAL-PRINT, Up: MISCELLANEOUS LD-PRE-EVAL-FILTER determines which forms ld evaluates Ld-pre-eval-filter is an ld special (*Note LD::). The accessor is (ld-pre-eval-filter state) and the updater is (set-ld-pre-eval-filter val state). Ld-pre-eval-filter must be either :all, :query, or a new name that could be defined (e.g., by defun or defconst). The initial value of ld-pre-eval-filter is :all. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-pre-eval-filter is one of them. If the filter is :all, then every form read is evaluated. If the filter is :query, then after a form is read it is printed to standard-co and the user is asked if the form is to be evaluated or skipped. If the filter is a new name, then all forms are evaluated until that name is introduced, at which time ld terminates normally. The :all filter is, of course, the normal one. :Query is useful if you want to replay selected the commands in some file. The new name filter is used if you wish to replay all the commands in a file up through the introduction of the given one.  File: acl2-doc-lemacs.info, Node: LD-PRE-EVAL-PRINT, Next: LD-PROMPT, Prev: LD-PRE-EVAL-FILTER, Up: MISCELLANEOUS LD-PRE-EVAL-PRINT determines whether ld prints the forms to be eval'd Ld-pre-eval-print is an ld special (*Note LD::). The accessor is (ld-pre-eval-print state) and the updater is (set-ld-pre-eval-print val state). Ld-pre-eval-print must be either t, nil, or :never. The initial value of ld-pre-eval-print is nil. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-pre-eval-print is one of them. If this global variable is t, then before evaluating the form just read from standard-oi, ld prints the form to standard-co. If the variable is nil, no such printing occurs. The t option is useful if you are reading from a file of commands and wish to assemble a complete script of the session in standard-co. The value :never of ld-pre-eval-print is rarely used. During the evaluation of encapsulate and of certify-book forms, subsidiary events are normally printed, even if ld-pre-eval-print is nil. Thus for example, when the user submits an encapsulate form, all subsidiary events are generally printed even in the default situation where ld-pre-eval-print is nil. But occasionally one may want to suppress such printing. In that case, ld-pre-eval-print should be set to :never.  File: acl2-doc-lemacs.info, Node: LD-PROMPT, Next: LD-QUERY-CONTROL-ALIST, Prev: LD-PRE-EVAL-PRINT, Up: MISCELLANEOUS LD-PROMPT determines the prompt printed by ld Ld-prompt is an ld special (*Note LD::). The accessor is (ld-prompt state) and the updater is (set-ld-prompt val state). Ld-prompt must be either nil, t, or a function symbol that, when given an open output character channel and state, prints the desired prompt to the channel and returns two values: the number of characters printed and the state. The initial value of ld-prompt is t. The general-purpose ACL2 read-eval-print loop, ld, reads forms from standard-oi, evaluates them and prints the result to standard-co. However, there are various flags that control ld's behavior and ld-prompt is one of them. Ld-prompt determines whether ld prints a prompt before reading the next form from standard-oi. If ld-prompt is nil, ld prints no prompt. If ld-prompt is t, the default prompt printer is used, which displays information that includes the current package, default defun-mode, guard checking status (on or off), and ld-skip-proofsp; *Note DEFAULT-PRINT-PROMPT::. If ld-prompt is neither nil nor t, then it should be a function name, fn, such that (fn channel state) will print the desired prompt to channel in state and return (mv col state), where col is the number of characters output (on the last line output). You may define your own prompt printing function. If you supply an inappropriate prompt function, i.e., one that causes an error or does not return the correct number and type of results, the following odd prompt will be printed instead: Bad Prompt See :DOC ld-prompt> which will lead you to this message. You should either call ld appropriately next time or assign an appropriate value to ld-prompt.