Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.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-emacs.info, Node: ACL2-PC||X, Next: ACL2-PC||X-DUMB, Prev: ACL2-PC||USE, Up: PROOF-CHECKER ACL2-PC||X (atomic macro) expand and (maybe) simplify function call at the current subterm Examples: x -- expand and simplify. For example, if the current subterm is (append a b), then after x the current subterm will probably be (cons (car a) (append (cdr a) b)) if (consp a) and (true-listp a) are among the top-level hypotheses and governors. If there are no top-level hypotheses and governors, then after x the current subterm will probably be: (if (true-listp x) (if x (cons (car x) (append (cdr x) y)) y) (apply 'binary-append (list x y))). General Form: (X &key rewrite normalize backchain-limit in-theory hands-off expand) Expand the function call at the current subterm, and simplify using the same conventions as with the s command (see documentation for s). Unlike s, it is permitted to set both :rewrite and :normalize to nil, which will result in no simplification; see x-dumb. *Note* (obscure): On rare occasions the current address may be affected by the use of x. For example, suppose we have the definition (defun g (x) (if (consp x) x 3)) and then we enter the proof-checker with (verify (if (integerp x) (equal (g x) 3) t)) . Then after invoking the instruction (dive 2 1), so that the current subterm is (g x), followed by the instruction x, we would expect the conclusion to be (if (integerp x) (equal 3 3) t). However, the system actually replaces (equal 3 3) with t (because we use the ACL2 term-forming primitives), and hence the conclusion is actually (if (integerp x) (equal 3 3) t). Therefore, the current address is put at (2) rather than (2 1). In such cases, a warning "NOTE" will be printed to the terminal. The other primitive commands to which the above "truncation" note applies are equiv, rewrite, and s.  File: acl2-doc-emacs.info, Node: ACL2-PC||X-DUMB, Next: DEFINE-PC-HELP, Prev: ACL2-PC||X, Up: PROOF-CHECKER ACL2-PC||X-DUMB (atomic macro) expand function call at the current subterm, without simplifying Example: x-dumb: expand without simplification. General Form: (x-dumb &optional new-goals-flg keep-all-guards-flg) Same as (expand t new-goals-flg keep-all-guards-flg). See documentation for expand. See also x, which allows simplification.  File: acl2-doc-emacs.info, Node: DEFINE-PC-HELP, Next: INSTRUCTIONS, Prev: ACL2-PC||X-DUMB, Up: PROOF-CHECKER DEFINE-PC-HELP define a macro command whose purpose is to print something Example: (define-pc-help pp () (if (goals t) (fms0 "~|~q0~|" (list (cons #0 (fetch-term (conc t) (current-addr t))))) (print-all-goals-proved-message state))) General Form: (define-pc-help name args &rest body) This defines a macro command named name, as explained further below. The body should (after removing optional declarations) have multiplicity 1 and state-out t, i.e. it should return a single value of state. Typically, it will just print something. What (define-pc-help name args &rest body) really does is to create a call of define-pc-macro that defines name to take arguments args, to have the declarations indicated by all but the last form in body, and to have a body that (via pprogn) first executes the form in the last element of body and then returns a call to the command skip (which will return (mv nil t state)).  File: acl2-doc-emacs.info, Node: INSTRUCTIONS, Next: MACRO-COMMAND, Prev: DEFINE-PC-HELP, Up: PROOF-CHECKER INSTRUCTIONS instructions to the proof checker Example: :instructions (induct prove promote (dive 1) x (dive 2) = top (drop 2) prove) See *Note DEFTHM:: for the role of :instructions in place of :hints. As illustrated by the example above, the value associated with :instructions is a list of proof-checker commands. At the moment the best way to understand the idea of the interactive proof-checker (see *Note PROOF-CHECKER:: and see *Note VERIFY::) is probably to read the first 11 pages of CLI Technical Report 19, which describes the corresponding facility for Nqthm. When inside the interactive loop (i.e., after executing verify), use help to get a list of legal instructions and (help instr) to get help for the instruction instr.  File: acl2-doc-emacs.info, Node: MACRO-COMMAND, Next: RETRIEVE, Prev: INSTRUCTIONS, Up: PROOF-CHECKER MACRO-COMMAND compound command for the proof-checker The proof-checker (see *Note PROOF-CHECKER::) allows the user to supply interactive commands. Compound commands, called macro commands, may be defined; these expand into zero or more other commands. Some of these are "atomic" macro commands; these are viewed as a single command step when completed successfully. More documentation will be written on the proof-checker. For now, we simply point out that there are lots of examples of the use of define-pc-macro and define-pc-atomic-macro in the ACL2 source file "proof-checker-b.lisp". The former is used to create macro commands, which can be submitted to the interactive loop (see *Note VERIFY::) and will "expand" into zero or more commands. The latter is similar, except that the undoing mechanism (see *Note ACL2-PC::UNDO::) understands atomic macro commands to represent single interactive commands. Also see *Note ACL2-PC::COMM::and see *Note ACL2-PC::COMMANDS:: for a discussion of the display of interactive commands. Also see *Note TOGGLE-PC-MACRO:: for how to change a macro command to an atomic macro command, and vice versa.  File: acl2-doc-emacs.info, Node: RETRIEVE, Next: TOGGLE-PC-MACRO, Prev: MACRO-COMMAND, Up: PROOF-CHECKER RETRIEVE re-enter a (specified) proof-checker state Examples: (retrieve associativity-of-permutationp) retrieve General Form: (retrieve &optional name) See *Note ACL2-PC::RETRIEVE::, or use (help retrieve) inside the interactive proof-checker loop. Also see *Note UNSAVE::.  File: acl2-doc-emacs.info, Node: TOGGLE-PC-MACRO, Next: UNSAVE, Prev: RETRIEVE, Up: PROOF-CHECKER TOGGLE-PC-MACRO change an ordinary macro command to an atomic macro, or vice-versa Example: (toggle-pc-macro pro) Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command) General Form: (toggle-pc-macro name &optional new-tp) If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type, or else there is no change.  File: acl2-doc-emacs.info, Node: UNSAVE, Next: VERIFY, Prev: TOGGLE-PC-MACRO, Up: PROOF-CHECKER UNSAVE remove a proof-checker state Example: (unsave assoc-of-append) General Form: (unsave name) Eliminates the association of a proof-checker state with name. See *Note UNSAVE:: or see *Note ACL2-PC::UNSAVE::. Also see *Note ACL2-PC::SAVE:: and see *Note RETRIEVE::.  File: acl2-doc-emacs.info, Node: VERIFY, Prev: UNSAVE, Up: PROOF-CHECKER VERIFY enter the interactive proof checker For proof-checker command summaries, see *Note PROOF-CHECKER::. Examples: (VERIFY (implies (and (true-listp x) (true-listp y)) (equal (append (append x y) z) (append x (append y z))))) -- Attempt to prove the given term interactively. (VERIFY (p x) :event-name p-always-holds :rule-classes (:rewrite :generalize) :instructions ((rewrite p-always-holds-lemma) change-goal)) -- Attempt to prove (p x), where the intention is to call the resulting DEFTHM event by the name p-always-holds, with rule-classes as indicated. The two indicated instructions will be run immediately to start the proof. (VERIFY) -- Re-enter the proof-checker in the state at which is was last left. General Form: (VERIFY &OPTIONAL raw-term &KEY event-name rule-classes instructions) Verify is the function used for entering the proof-checker's interactive loop.  File: acl2-doc-emacs.info, Node: PROOF-TREE, Next: RELEASE-NOTES, Prev: PROOF-CHECKER, Up: Top PROOF-TREE proof tree displays A view of ACL2 proofs may be obtained by way of "proof tree displays." Environments such as emacs may be customized to provide window-based versions of proof tree displays. (See for example documentation of the emacs function start-proof-tree, co-written with Michael K. Smith, that the implementors are happy to make available.) Proof tree displays may be turned on with the command :start-proof-tree and may be turned off with the command :start-proof-tree; see *Note START-PROOF-TREE:: and see *Note STOP-PROOF-TREE::. * Menu: * CHECKPOINT-FORCED-GOALS:: Cause forcing goals to be checkpointed in proof trees * PROOF-TREE-DETAILS:: proof tree details not covered elsewhere * PROOF-TREE-EXAMPLES:: proof tree example * START-PROOF-TREE:: start displaying proof trees during proofs * STOP-PROOF-TREE:: stop displaying proof trees during proofs Here is an example of a proof tree display, with comments. Lines marked with "c" are considered "checkpoints," i.e., goals whose scrutiny may be of particular value. ( DEFTHM PLUS-TREE-DEL ...) ;currently proving PLUS-TREE-DEL 1 Goal preprocess ;"Goal" creates 1 subgoal by preprocessing 2 | Goal' simp ;"Goal'" creates 2 subgoals by simplification c 0 | | Subgoal 2 PUSH *1 ;"Subgoal 2" pushes "*1" for INDUCT ++++++++++++++++++++++++++++++ ;first pass thru waterfall completed c 6 *1 INDUCT ;Proof by induction of "*1" has | <5 more subgoals> ; created 6 top-level subgoals. At ; this point, one of those 6 has been ; proved, and 5 remain to be proved. ; We are currently working on the ; first of those 5 remaining goals. See *Note PROOF-TREE-EXAMPLES:: for many examples that contain proof tree displays. But first, we summarize the kinds of lines that may appear in a proof tree display. The simplest form of a proof tree display is a header showing the current event, followed by list of lines, each having one of the following forms. n ... Says that the indicated goal created n subgoals using the indicated process. Here "..." refers to possible additional information. c n ... As above, but calls attention to the fact that this goal is a "checkpoint" in the sense that it may be of particular interest. Some displays may overwrite "c" with ">" to indicate the current checkpoint being shown in the proof transcript. | ... | | Indicates that the goal just above this line, which is pointed to by the rightmost vertical bar ("|"), has k subgoals, none of which have yet been processed. | ... | | As above, except that some subgoals have already been processed. ++++++++++++++++++++++++++++++ Separates successive passes through the "waterfall". Thus, this "fencepost" mark indicates the start of a new proof by induction or of a new forcing round. See *Note PROOF-TREE-EXAMPLES:: for detailed examples. To learn how to turn off proof tree displays or to turn them back on again, see *Note STOP-PROOF-TREE:: and see *Note START-PROOF-TREE::, respectively. See *Note CHECKPOINT-FORCED-GOALS:: to learn how to mark goals as checkpoints that force the creation of goals in forcing rounds. Finally, see *Note PROOF-TREE-DETAILS:: for some points not covered elsewhere.  File: acl2-doc-emacs.info, Node: CHECKPOINT-FORCED-GOALS, Next: PROOF-TREE-DETAILS, Prev: PROOF-TREE, Up: PROOF-TREE CHECKPOINT-FORCED-GOALS Cause forcing goals to be checkpointed in proof trees Example forms: (checkpoint-forced-goals t) (checkpoint-forced-goals nil) Also see *Note PROOF-TREE::. By default, goals are not marked as checkpoints by a proof tree display (as described in the documentation for proof-tree) merely because they force some hypotheses, thus possibly contributing to a forcing round. However, some users may want such behavior, which will occur once the command (checkpoint-forced-goals) t) has been executed. To return to the default behavior, use the command (checkpoint-forced-goals nil).  File: acl2-doc-emacs.info, Node: PROOF-TREE-DETAILS, Next: PROOF-TREE-EXAMPLES, Prev: CHECKPOINT-FORCED-GOALS, Up: PROOF-TREE PROOF-TREE-DETAILS proof tree details not covered elsewhere See *Note PROOF-TREE:: for an introduction to proof trees, and for a list of related topics. Here we present some details not covered elsewhere. 1. When proof tree display is enabled (because the command :stop-proof-tree has not been executed, or has been superseded by a later :start-proof-tree command), then time summaries will include the time for proof tree display. This time includes the time spent computing with proof trees, such as the pruning process described briefly above. Even when proof trees are not displayed, such as when their display is turned off in the middle of a proof, this time will be printed if it is not 0. 2. When a goal is given a :bye in a proof (see *Note HINTS::), it is treated for the purpose of proof tree display just as though it had been proved. 3. Several state global variables affect proof tree display. (@ proof-tree-indent) is initially the string "| ": it is the string that is laid down the appropriate number of times to effect indentation. (@ proof-tree-buffer-width) is initially the value of (fmt-soft-right-margin state), and is used to prevent printing of the annotation "(forced ...)" in any greater column than this value. However, (assign proof-tree-buffer-width nil) to avoid any such suppression. Finally, (@ checkpoint-processors) is a list of processors from the constant list *preprocess-clause-ledge*, together with :induct. You may remove elements of (@ checkpoint-processors) to limit which processes are considered checkpoints. 4. When :otf-flg is not set to t in a proof, and the prover then decides to revert to the original goal and prove it by induction, the proof tree display will reflect this fact as shown here: c 0 | | Subgoal 2 PUSH (reverting) 5. Proof-tree display is turned off during calls of certify-book. 6. The usual failure message is printed as part of the prooftree display when a proof has failed.  File: acl2-doc-emacs.info, Node: PROOF-TREE-EXAMPLES, Next: START-PROOF-TREE, Prev: PROOF-TREE-DETAILS, Up: PROOF-TREE PROOF-TREE-EXAMPLES proof tree example See *Note PROOF-TREE:: for an introduction to proof trees, and for a list of related topics. Here we present a detailed example followed by a shorter example that illustrates proof by induction. Consider the guard proof for the definition of a function cancel_equal_plus; the body of this definition is of no importance here. The first proof tree display is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <18 subgoals> This is to be read as follows. At this stage of the proof we have encountered the top-level goal, named "Goal", which generated 18 subgoals using the "preprocess" process. We have not yet begun to work on those subgoals. The corresponding message from the ordinary prover output is: By case analysis we reduce the conjecture to the following 18 conjectures. Note that the field just before the name of the goal ("Goal"), which here contains the number 18, indicates the number of cases (children) created by the goal using the indicated process. This number will remain unchanged as long as this goal is displayed. The next proof tree display is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp | | <1 subgoal> | <17 more subgoals> which indicates that at this point, the prover has used the simplification ("simp") process on Subgoal 18 to create one subgoal ("<1 subgoal>"). The vertical bar ("|") below "Subgoal 18", accompanied by the line below it, signifies that there are 17 siblings of Subgoal 18 that remain to be processed. The next proof tree displayed is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp c 2 | | Subgoal 18' ELIM | | | <2 subgoals> | <17 more subgoals> Let us focus on the fourth line of this display: c 2 | | Subgoal 18' ELIM The "c" field marks this goal as a "checkpoint", i.e., a goal worthy of careful scrutiny. In fact, any goal that creates children by a process other than "preprocess" or "simp" is marked as a checkpoint. In this case, the destructor-elimination ("ELIM") process has been used to create subgoals of this goal. The indentation shows that this goal, Subgoal 18', is a child of Subgoal 18. The number "2" indicates that 2 subgoals have been created (by ELIM). Note that this information is consistent with the line just below it, which says "<2 subgoals>". Finally, the last line of this proof tree display, | <17 more subgoals> is connected by vertical bars ("|") up to the string "Subgoal 18", which suggests that there are 17 immediate subgoals of Goal remaining to process after Subgoal 18. Note that this line is indented one level from the second line, which is the line for the goal named "Goal". The display is intended to suggest that the subgoals of Goal that remain to be proved consist of Subgoal 18 together with 17 more subgoals. The next proof tree display differs from the previous one only in that now, Subgoal 18' has only one more subgoal to be processed. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp c 2 | | Subgoal 18' ELIM | | | <1 more subgoal> | <17 more subgoals> Note that the word "more" in "<1 more subgoal>" tells us that there was originally more than one subgoal of Subgoal 18. In fact that information already follows from the line above, which (as previously explained) says that Subgoal 18' originally created 2 subgoals. The next proof tree display occurs when the prover completes the proof of that "1 more subgoal" referred to above. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <17 more subgoals> Then, Subgoal 17 is processed and creates one subgoal, by simplification: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 17 simp | | <1 subgoal> | <16 more subgoals> ... and so on. Later in the proof one might find the following successive proof tree displays. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <9 more subgoals> ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED) | <8 more subgoals> These displays tell us that Subgoal 9 simplified to t (note that the "0" shows clearly that no subgoals were created), but that some rule's hypotheses were forced. Although this goal is not checkpointed (i.e., no "c" appears on the left margin), one can cause such goals to be checkpointed; see *Note CHECKPOINT-FORCED-GOALS::. In fact, the proof tree displayed at the end of the "main proof" (the 0-th forcing round) is as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED) 0 | Subgoal 8 simp (FORCED) 0 | Subgoal 7 simp (FORCED) 0 | Subgoal 6 simp (FORCED) 0 | Subgoal 4 simp (FORCED) 0 | Subgoal 3 simp (FORCED) This is followed by the following proof tree display at the start of the forcing round. 18 Goal preprocess 0 | Subgoal 9 simp (FORCED [1]Subgoal 4) 0 | Subgoal 8 simp (FORCED [1]Subgoal 6) 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) 0 | Subgoal 6 simp (FORCED [1]Subgoal 3) 0 | Subgoal 4 simp (FORCED [1]Subgoal 5) 0 | Subgoal 3 simp (FORCED [1]Subgoal 2) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND 2 | [1]Subgoal 6 preprocess | | <2 subgoals> | <5 more subgoals> This display shows which goals to "blame" for the existence of each goal in the forcing round. For example, Subgoal 9 is to blame for the creation of [1]Subgoal 4. Actually, there is no real goal named "[1]Goal". However, the line 6 [1]Goal FORCING-ROUND appears in the proof tree display to suggest a "parent" of the six top-level goals in that forcing round. As usual, the numeric field before the goal name contains the original number of children of that (virtual, in this case) goal -- in this case, 6. In our example proof, Subgoal 6 eventually gets proved, without doing any further forcing. At that point, the proof tree display looks as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED [1]Subgoal 4) 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) 0 | Subgoal 6 simp (FORCED [1]Subgoal 3) 0 | Subgoal 4 simp (FORCED [1]Subgoal 5) 0 | Subgoal 3 simp (FORCED [1]Subgoal 2) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND | <5 more subgoals> Notice that the line for Subgoal 8, 0 | Subgoal 8 simp (FORCED [1]Subgoal 6) no longer appears. That is because the goal [1]Subgoal 6 has been proved, along with all its children; and hence, the proof of Subgoal 8 no longer depends on any further reasoning. The final two proof tree displays in our example are as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND 2 | [1]Subgoal 1 preprocess 1 | | [1]Subgoal 1.1 preprocess 1 | | | [1]Subgoal 1.1' simp c 3 | | | | [1]Subgoal 1.1" ELIM | | | | | <1 more subgoal> ( DEFUN CANCEL_EQUAL_PLUS ...) <> The explanation for the empty proof tree is simple: once [1]Subgoal 1.1.1 was proved, nothing further remained to be proved. In fact, the much sought-after "Q.E.D." appeared shortly after the final proof tree was displayed. Let us conclude with a final, brief example that illustrates proof by induction. Partway through the proof one might come across the following proof tree display. ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 | | <1 more subgoal> This display says that in the attempt to prove a theorem called plus-tree-del, preprocessing created the only child Goal' from Goal, and Goal' simplified to two subgoals. Subgoal 2 is immediately pushed for proof by induction, under the name "*1". In fact if Subgoal 1 simplifies to t, then we see the following successive proof tree displays after the one shown above. ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 ++++++++++++++++++++++++++++++ c 6 *1 INDUCT | <5 more subgoals> The separator "+++++..." says that we are beginning another trip through the waterfall. In fact this trip is for a proof by induction (as opposed to a forcing round), as indicated by the word "INDUCT". Apparently *1.6 was proved immediately, because it was not even displayed; a goal is only displayed when there is some work left to do either on it or on some goal that it brought (perhaps indirectly) into existence. Once a proof by induction is completed, the "PUSH" line that refers to that proof is eliminated ("pruned"). So for example, when the present proof by induction is completed, the line c 0 | | Subgoal 2 PUSH *1 is eliminated, which in fact causes the lines above it to be eliminated (since they no longer refer to unproved children). Hence, at that point one might expect to see: ( DEFTHM PLUS-TREE-DEL ...) <> However, if the proof by induction of *1 necessitates further proofs by induction or a forcing round, then this "pruning" will not yet be done.  File: acl2-doc-emacs.info, Node: START-PROOF-TREE, Next: STOP-PROOF-TREE, Prev: PROOF-TREE-EXAMPLES, Up: PROOF-TREE START-PROOF-TREE start displaying proof trees during proofs Also see *Note PROOF-TREE:: and see *Note STOP-PROOF-TREE::. Note that :start-proof-tree works by removing 'proof-tree from the inhibit-output-lst; see *Note SET-INHIBIT-OUTPUT-LST::. Proof tree displays are explained in the documentation for proof-tree. :start-proof-tree causes proof tree display to be turned on, once it has been turned off by :stop-proof-tree. Do not attempt to invoke start-proof-tree during an interrupt in the middle of a proof.  File: acl2-doc-emacs.info, Node: STOP-PROOF-TREE, Prev: START-PROOF-TREE, Up: PROOF-TREE STOP-PROOF-TREE stop displaying proof trees during proofs Also see *Note PROOF-TREE:: and see *Note START-PROOF-TREE::. Note that :stop-proof-tree works by adding 'proof-tree to the inhibit-output-lst; see *Note SET-INHIBIT-OUTPUT-LST::. Proof tree displays are explained in the documentation for proof-tree. :Stop-proof-tree causes proof tree display to be turned off. It is permissible to submit the form (stop-proof-tree) during a break. Thus, you can actually turn off proof tree display in the middle of a proof by interrupting ACL2 and submitting the form (stop-proof-tree) in raw Lisp.  File: acl2-doc-emacs.info, Node: RELEASE-NOTES, Next: RULE-CLASSES, Prev: PROOF-TREE, Up: Top RELEASE-NOTES pointers to what has changed * Menu: * NOTE1:: Acl2 Version 1.1 Notes * NOTE2:: Acl2 Version 1.2 Notes * NOTE3:: Acl2 Version 1.3 Notes * NOTE4:: Acl2 Version 1.4 Notes * NOTE5:: Acl2 Version 1.5 Notes * NOTE6:: Acl2 Version 1.6 Notes * NOTE7:: ACL2 Version 1.7 (released October 1994) Notes * NOTE8:: ACL2 Version 1.8 (May, 1995) Notes * NOTE8-UPDATE:: ACL2 Version 1.8 (Summer, 1995) Notes This section of the online documentation contains notes on the changes that distinguish successive released versions of ACL2. The current version of ACL2 is the value of the constant *acl2-version*.  File: acl2-doc-emacs.info, Node: NOTE1, Next: NOTE2, Prev: RELEASE-NOTES, Up: RELEASE-NOTES NOTE1 Acl2 Version 1.1 Notes The new features are extensively documented. The relevant topics are: * Menu: Related topics other than immediate subtopics: * BOOKS:: files of ACL2 event forms * GUARD:: restricting the domain of a function * MORE:: your response to :doc or :more-doc's "(cont'd)" * REDUNDANT-EVENTS:: allowing a name to be introduced "twice" It is especially important to read all of of the documentation for books before trying to use books. However, the new :more keyword command is so handy for reading long documentation strings that we recommend you start with :doc more if reading at the terminal. Some documentation has been written for guards which you might find interesting.  File: acl2-doc-emacs.info, Node: NOTE2, Next: NOTE3, Prev: NOTE1, Up: RELEASE-NOTES NOTE2 Acl2 Version 1.2 Notes Hacker mode has been eliminated and programming mode has been added. Programming mode is unsound but does syntax checking and permits redefinitions of names. See :doc load-mode and :doc g-mode. The arguments to ld have changed. Ld is now much more sophisticated. See *Note LD::. For those occasions on which you wish to look at a large list structure that you are afraid to print, try (walkabout x state), where x is an Acl2 expression that evaluates to the structure in question. I am afraid there is no documentation yet, but it is similar in spirit to the Interlisp structure editor. You are standing on an object and commands move you around in it. E.g., 1 moves you to its first element, 2 to its second, etc.; 0 moves you up to its parent; nx and bk move you to its next sibling and previous sibling; pp prettyprints it; q exits returning nil; = exits returning the thing you're standing on; (= symb) assigns the thing you're standing on to the state global variable symb. Several new hints have been implemented, including :by and :do-not. The old :do-not-generalize has been scrapped in favor of such new hints as :do-not (generalize elim). :By lets you say "this goal is subsumed by" a given lemma instance. The :by hint also lets you say "this goal can't be proved yet but skip it and see how the rest of the proof goes." See *Note HINTS::.  File: acl2-doc-emacs.info, Node: NOTE3, Next: NOTE4, Prev: NOTE2, Up: RELEASE-NOTES NOTE3 Acl2 Version 1.3 Notes Programming mode has been eliminated. Instead, all functions have a "color" which indicates what can be done with the function. For example, :red functions can be executed but have no axioms describing them. Thus, :red functions can be introduced after passing a simple syntactic check and they can be redefined without undoing. But nothing of consequence can be proved about them. At the other extreme are :gold functions which can be executed and which also have passed both the termination and the guard verification proofs. The color of a function can be specified with the new xargs keyword, :color, which, if omitted defaults to the global setting of ld-color. Ld-color replaces load-mode. Setting ld-color to :red causes behavior similar to the old :g-mode. Setting ld-color to :gold causes behavior similar to the old :v-mode. It is possible to prototype your system in :red and then convert :red functions to :blue individually by calling verify-termination on them. They can then be converted to :gold with verify-guards. This allows us to undertake to verify the termination and guards of system functions. See :doc color for an introduction to the use of colors. Type prescription rules have been added. Recall that in Nqthm, some rewrite rules were actually stored as "type-prescriptions." Such rules allow the user to inform Nqthm's primitive type mechanism as to the kinds of shells returned by a function. Earlier versions of Acl2 did not have an analogous kind of rule because Acl2's type mechanism is complicated by guards. Version 1.3 supports type-prescription rules. See *Note TYPE-PRESCRIPTION::. Three more new rule-classes implement congruence-based rewriting. It is possible to identify a binary relation as an equivalence relation (see *Note EQUIVALENCE::), to show that one equivalence relation refines another (see *Note REFINEMENT::) and to show that a given equivalence relation is maintained when rewriting a given function call, e.g., (fn ...xk...), by maintaining another equivalence relation while rewriting the kth argument (see *Note CONGRUENCE::). If r has been shown to be an equivalence relation and then (implies hyps (r (foo x) (bar x))) is proved as a :rewrite rule, then instances of (foo x) will be replaced by corresponding instances of (bar x) provided the instance occurs in a slot where the maintainence of r-equivalence is known to be sufficient and hyps can be established as usual. In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or :elim. In Version 1.3, rule-classes have been elaborated to allow you to specify how the theorem ought to be used as a rule. That is, the new rule-classes allows you to separate the mathematical statement of the formula from its interpretation as a rule. See *Note RULE-CLASSES::. Rules used to be named by symbols, e.g., car and car-cons were the names of rules. Unfortunately, this was ambiguous because there are three rules associated with function symbols: the symbolic definition, the executable counterpart, and the type-prescription; many different rules might be associated with theorems, depending on the rule classes. In Version 1.3 rules are named by "runes" (which is just short hand for "rule names"). Example runes are (:definition car), (:executable-counterpart car), and (:type-prescription car . 1). Every rule added by an event has a different name and you can enable and disable them independently. See *Note RUNE:: and see *Note THEORIES::. The identity function force, of one argument, has been added and given a special interpretation by the functions responsible for establishing hypotheses in backchaining: When the system fails to establish some hypothesis of the form (force term), it simply assumes it is true and goes on, delaying until later the establishment of term. In particular, pushes a new subgoal to prove term in the current context. When that subgoal is attacked, all of the resources of the theorem prover, not just rewriting, are brought to bear. Thus, for example, if you wish to prove the rule (implies (good-statep s) (equal (exec s n) s')) and it is your expectation that every time exec appears its first argument is a good-statep then you might write the rule as (implies (force (good-statep s)) (equal (exec s n) s')). This rule is essentially an unconditional rewrite of (exec s n) to s' that spawns the new goal (good-statep s). See *Note FORCE::. Because you can now specify independently how a theorem is used as a rule, you need not write the force in the actual theorem proved. See *Note RULE-CLASSES::. Version 1.3 supports a facility similar to Nqthm's break-lemma. See *Note BREAK-REWRITE::. You can install "monitors" on runes that will cause interactive breaks under certain conditions. Acl2 also provides "wormholes" which allow you to write functions that cause interaction with the user but which do not require that you have access to state. See *Note WORMHOLE::. The rewriter now automatically backchains to stronger recognizers. There is no user hook to this feature but it may simplify some proofs with which older versions of Acl2 had trouble. For example, if the rewriter is trying to prove (rationalp (foo a b c)) it is now smart enough to try lemmas that match with (integerp (foo a b c)).  File: acl2-doc-emacs.info, Node: NOTE4, Next: NOTE5, Prev: NOTE3, Up: RELEASE-NOTES NOTE4 Acl2 Version 1.4 Notes Once again ld only takes one required argument, as the bind-flg has been deleted. Three commands have been added in the spirit of :pe. :Pe! is similar to :pe but it prints all events with the given name, rather than just the most recent. The command :pf prints the corollary formula corresponding to a name or rune. The command :pl (print lemmas) prints rules whose top function symbol is the given name. See *Note PE!::, see *Note PF::, and see *Note PL::. Book naming conventions have been changed somewhat. The once-required .lisp extension is now prohibited! Directories are supported, including a notion of "connected book directory". See *Note BOOK-NAME::. Also, the second argument of certify-book is now optional, defaulting to 0. Compilation is now supported inside the Acl2 loop. See *Note COMP::and see *Note SET-COMPILE-FNS::. The default color is now part of the Acl2 world; see :doc default-color. Ld-color is no longer an ld special. Instead, colors are events; see the documentation for red, pink, blue, and gold. A table exists for controlling whether Acl2 prints comments when it forces hypotheses of rules; see :doc force-table. Also, it is now possible to turn off the forcing of assumptions by disabling the definition of force; see *Note FORCE::. The event defconstant is no longer supported, but a very similar event, defconst, has been provided in its place. See *Note DEFCONST::. The event for defining congruence relations is now defcong (formerly, defcon). Patterns are now allowed in :expand hints. See the documentation for :expand inside the documentation for hints. We have improved the way we report rules used by the simplifier. All runes of the same type are reported together in the running commentary associated with each goal, so that for example, executable counterparts are listed separately from definitions, and rewrite rules are listed separately from linear rules. The preprocessor now mentions "simple" rules; see *Note SIMPLE::. The mechanism for printing warning messages for new rewrite rules, related to subsumption, now avoids worrying about nonrecursive function symbols when those symbols are disabled. These messages have also been eliminated for the case where the old rule is a :definition rule. Backquote has been modified so that it can usually provide predictable results when used on the left side of a rewrite rule. Time statistics are now printed even when an event fails. The Acl2 trace package has been modified so that it prints using the values of the Lisp globals *print-level* and *print-length* (respectively). Table has been modified so that the :clear option lets you replace the entire table with one that satisfies the val and key guards (if any); see *Note TABLE::. We have relaxed the translation rules for :measure hints to defun, so that the the same rules apply to these terms that apply to terms in defthm events. In particular, in :measure hints mv is treated just like list, and state receives no special handling. The loop-stopper test has been relaxed. The old test required that every new argument be strictly less than the corresponding old argument in a certain term-order. The new test uses a lexicographic order on term lists instead. For example, consider the following rewrite rule. (equal (variable-update var1 val1 (variable-update var2 val2 vs)) (variable-update var2 val2 (variable-update var1 val1 vs))) This rule is permutative. Now imagine that we want to apply this rule to the term (variable-update u y (variable-update u x vs)). Since the actual corresponding to both var1 and var2 is u, which is not strictly less than itself in the term-order, this rule would fail to be applied in this situation when using the old test. However, since the pair (u x) is lexicographically less than the pair (u y) with respect to our term-order, the rule is in fact applied using our new test. Messages about events now contain a space after certain left parentheses, in order to assist emacs users. For example, the event (defthm abc (equal (+ (len x) 0) (len x))) leads to a summary containing the line Form: ( DEFTHM ABC ...) and hence, if you search backwards for "(defthm abc", you won't stop at this message. More tautology checking is done during a proof; in fact, no goal printed to the screen, except for the results of applying :use and :by hints or the top-level goals from an induction proof, are known to Acl2 to be tautologies. The ld-query-control-alist may now be used to suppress printing of queries; see *Note LD-QUERY-CONTROL-ALIST::. Warning messages are printed with short summary strings, for example the string "Use" in the following message. Acl2 Warning [Use] in DEFTHM: It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling FOO. At the end of the event, just before the time is printed, all such summary strings are printed out. The keyword command :u has been introduced as an abbreviation for :ubt :max. Printing of query messages is suppressed by :u. The keyword :cheat is no longer supported by any event form. Some irrelevant formals are detected; see *Note IRRELEVANT-FORMALS::. A bug in the application of metafunctions was fixed: now if the output of a metafunction is equal to its input, the application of the metafunction is deemed unsuccessful and the next metafunction is tried. An example has been added to the documentation for equivalence to suggest how to make use of equivalence relations in rewriting. The following Common Lisp functions have been added to Acl2: alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase, string-downcase, string-upcase, and digit-charp-p. A documentation section called proof-checker has been added for the interactive facility, whose documentation has been slightly improved. See in particular the documentation for proof-checker, verify, and macro-command. A number of events that had been inadvertently disallowed in books are now permitted in books. These are: defcong, defcor, defequiv, defrefinement, defstub, and verify-termination.  File: acl2-doc-emacs.info, Node: NOTE5, Next: NOTE6, Prev: NOTE4, Up: RELEASE-NOTES NOTE5 Acl2 Version 1.5 Notes Acl2 now allows "complex rationals," which are complex numbers whose real parts are rationals and whose imaginary parts are non-zero rationals. See *Note COMPLEX::. A new way of handling forced hypotheses has been implemented. Rather than cause a case split at the time the force occurs, we complete the main proof and then embark on one or more "forcing rounds" in which we try to prove the forced hypotheses. See *Note FORCING-ROUND::. To allow us to compare the new handling of force with the old, Version 1.5 implements both and uses a flag in state to determine which method should be used. Do (assign old-style-forcing t) if you want force to be handled as it was in Version 1.4. However, we expect to eliminate the old-style forcing eventually because we think the new style is more effective. To see the difference between the two approaches to forcing, try proving the associativity of append under both settings of old-style-forcing. To get the new behavior invoke: (thm (implies (and (true-listp a) (true-listp b)) (equal (append (append a b) c) (append a (append b c))))) Then (assign old-style-forcing t) and invoke the thm command above again. A new :cases hints allows proof by cases. See *Note HINTS::. Include-book and encapsulate now restore the acl2-defaults-table when they complete. See *Note INCLUDE-BOOK:: and see *Note ENCAPSULATE::. The guards on many Acl2 primitives defined in axioms.lisp have been weakened to permit them to be used in accordance with lisp custom and tradition. It is possible to attach heuristic filters to :rewrite rules to limit their applicability. See *Note SYNTAXP::. A tutorial has been added; see *Note ACL2-TUTORIAL::. Events now print the Summary paragraph listing runes used, time, etc., whether they succeed or fail. The format of the "failure banner" has been changed but still has multiple asterisks in it. Thm also prints a Summary, whether it succeeds or fails; but thm is not an event. A new event form skip-proofs has been added; see *Note SKIP-PROOFS::. A user-specific customization facility has been added in the form of a book that is automatically included, if it exists on the current directory. See *Note ACL2-CUSTOMIZATION::. A facility for conditional metalemmas has been implemented; see *Note META::. The acceptable values for ld-skip-proofsp have changed. In the old version (Version 1.4), a value of t meant that proofs and local events are to be skipped. In Version 1.5, a value of t means proofs (but not local events) are to be skipped. A value of 'include-book means proofs and local events are to be skipped. There are two other, more obscure, acceptable values. See *Note LD-SKIP-PROOFSP::. In order to turn off the forcing of assumptions, one should now disable the :executable-counterpart of force (rather than the :definition of force, as in the previous release); see *Note FORCE::. The macros enable-forcing and disable-forcing make it convenient to enable or disable forcing. See *Note ENABLE-FORCING:: and see *Note DISABLE-FORCING::. The new commands :pr and :pr! print the rules created by an event or command. See *Note PR:: and see *Note PR!::. The new history commands :puff and :puff* will replace a compound command such as an encapsulate or include-book by the sequence of events in it. That is, they "puff up" or "lift" the subevents of a command to the command level, eliminating the formerly superior command and lengthening the history. This is useful if you want to "partially undo" an encapsulate or book or other compound command so you can experiment. See *Note PUFF:: and see *Note PUFF*::. Theory expressions now are allowed to use the free variable world and prohibited from using the free variable state. See *Note THEORIES::, although it is essentially the same as before except it mentions world instead of state. See *Note WORLD:: for a discussion of the Acl2 logical world. Allowing in-theory events to be state-sensitive violated an important invariant about how books behaved. Table keys and values now are allowed to use the free variable world and prohibited from using the free variable state. See the note above about theory expressions for some explanation. The macro for minus, -, used to expand (- x 3) to (+ x -3) and now expands it to (+ -3 x) instead. The old macro, if used in the left-hand sides of rewrite rules, produced inapplicable rules because the constant occurs in the second argument of the +, but potential target terms generally had the constant in the first argument position because of the effect of commutativity-of-+. A new class of rule, :linear-alias rules, allows one to implement the nqthm package and similar hacks in which a disabled function is to be known equivalent to an arithmetic function. See *Note LINEAR-ALIAS::. A new class of rule, :built-in-clause rules, allows one to extend the set of clauses proved silently by defun during measure and guard processing. See *Note BUILT-IN-CLAUSES::. The new command pcb! is like pcb but sketches the command and then prints its subsidiary events in full. See *Note PCB!::. :Rewrite class rules may now specify the :loop-stopper field. See *Note RULE-CLASSES:: and see *Note LOOP-STOPPER::. The rules for how loop-stoppers control permutative rewrite rules have been changed. One effect of this change is that now when the built-in commutativity rules for + are used, the terms a and (- a) are permuted into adjacency. For example, (+ a b (- a)) is now normalized by the commutativity rules to (+ a (- a) b); in Version 1.4, b was considered syntactically smaller than (- a) and so (+ a b (- a)) is considered to be in normal form. Now it is possible to arrange for unary functions be be considered "invisible" when they are used in certain contexts. By default, unary-- is considered invisible when its application appears in the argument list of binary-+. See *Note LOOP-STOPPER:: and see *Note SET-INVISIBLE-FNS-ALIST::. Extensive documentation has been provided on the topic of Acl2's "term ordering." See *Note TERM-ORDER::. Calls of ld now default ld-error-action to :return rather than to the current setting. The command descriptor :x has been introduced and is synonymous with :max, the most recently executed command. History commands such as :pbt print a :x beside the most recent command, simply to indicate that it *is* the most recent one. The command descriptor :x-23 is synonymous with (:x -23). More generally, every symbol in the keyword package whose first character is #\x and whose remaining characters parse as a negative integer is appropriately understood. This allows :pbt :x-10 where :pbt (:max -10) or :pbt (:here -10) were previously used. The old forms are still legal. The order of the arguments to defcong has been changed. The simplifier now reports the use of unspecified built-in type information about the primitives with the phrase "primitive type reasoning." This phrase may sometimes occur in situations where "propositional calculus" was formerly credited with the proof. The function pairlis has been replaced in the code by a new function pairlis$, because Common Lisp does not adequately specify its pairlis function. Some new Common Lisp functions have been added, including logtest, logcount, integer-length, make-list, remove-duplicates, string, and concatenate. The source file /slocal/src/acl2/axioms.lisp is the ultimate reference regarding Common Lisp functions in Acl2. The functions defuns and theory-invariant have been documented. See *Note DEFUNS:: and see *Note THEORY-INVARIANT::. A few symbols have been added to the list *acl2-exports*. A new key has been implemented for the acl2-defaults-table, :irrelevant-formals-ok. See *Note SET-IRRELEVANT-FORMALS-OK::. The connected book directory, cbd, must be nonempty and begin and end with a slash. It is set (and displayed) automatically upon your first entry to lp. You may change the setting with set-cbd. See *Note CBD::. :oops will undo the last :ubt. See *Note OOPS::. Documentation has been written about the ordinals. See *Note E0-ORDINALP:: and see *Note E0-ORD-<::. The color events -- (red), (pink), (blue), and (gold) -- may no longer be enclosed inside calls of local, for soundness reasons. In fact, neither may any event that sets the acl2-defaults-table. See *Note EMBEDDED-EVENT-FORM::. See *Note LD-KEYWORD-ALIASES:: for an example of how to change the exit keyword from :q to something else. The attempt to install a monitor on :rewrite rules stored as simple abbreviations now causes an error because the application of abbreviations is not tracked. A new message is sometimes printed by the theorem prover, indicating that a given simplification is "specious" because the subgoals it produces include the input goal. In Version 1.4 this was detected but not reported, causing behavior some users found bizarre. See *Note SPECIOUS-SIMPLIFICATION::. :Definition rules are no longer always required to specify the :clique and :controller-alist fields; those fields can be defaulted to system-determined values in many common instances. See *Note DEFINITION::. A warning is printed if a macro form with keyword arguments is given duplicate keyword values. Execute (thm t :doc nil :doc "ignored") and read the warning printed. A new restriction has been placed on encapsulate. Non-local recursive definitions inside the encapsulate may not use, in their tests and recursive calls, the constrained functions introduced by the encapsulate. See *Note SUBVERSIVE-INDUCTIONS::. The events defequiv, defcong, defrefinement, and defevaluator have been reimplemented so that they are just macros that expand into appropriate defthm or encapsulate events; they are no longer primitive events. See the documentation of each affected event. The defcor event, which was a shorthand for a defthm that established a corollary of a named, previously proved event, has been eliminated because its implementation relied on a technique we have decided to ban from our code. If you want the effect of a defcor in Version 1.5 you must submit the corresponding defthm with a :by hint naming the previously proved event. Error reporting has been improved for inappropriate in-theory hints and events, and for syntax errors in rule classes, and for non-existent filename arguments to ld. Technical Note: We now maintain the Third Invariant on type-alists, as described in the Essay on the Invariants on Type-alists, and Canonicality. This change will affect some proofs, for example, by causing a to rewrite more quickly to c when (equiv a b) and (equiv b c) are both known and c is the canonical representative of the three.