This is acl2-doc-emacs.info, produced by makeinfo version 4.5 from
acl2-doc-emacs.texinfo.
This is documentation for ACL2 Version 3.1
Copyright (C) 2006 University of Texas at Austin
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
Written by: Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.
INFO-DIR-SECTION Math
START-INFO-DIR-ENTRY
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
END-INFO-DIR-ENTRY
File: acl2-doc-emacs.info, Node: PROOF-CHECKER-COMMANDS, Next: RETRIEVE, Prev: MACRO-COMMAND, Up: PROOF-CHECKER
PROOF-CHECKER-COMMANDS list of commands for the proof-checker
This documentation section contains documentation for individual
commands that can be given inside the interactive proof-checker loop
that is entered using verify.
* Menu:
* ACL2-PC||=:: (atomic macro)
attempt an equality (or equivalence) substitution
* ACL2-PC||ACL2-WRAP:: (macro)
same as (lisp x)
* ACL2-PC||ADD-ABBREVIATION:: (primitive)
add an abbreviation
* ACL2-PC||BASH:: (atomic macro)
call the ACL2 theorem prover's simplifier
* ACL2-PC||BDD:: (atomic macro)
prove the current goal using bdds
* ACL2-PC||BK:: (atomic macro)
move backward one argument in the enclosing term
* ACL2-PC||BOOKMARK:: (macro)
insert matching ``bookends'' comments
* ACL2-PC||CASESPLIT:: (primitive)
split into two cases
* ACL2-PC||CG:: (macro)
change to another goal.
* ACL2-PC||CHANGE-GOAL:: (primitive)
change to another goal.
* ACL2-PC||CLAIM:: (atomic macro)
add a new hypothesis
* ACL2-PC||COMM:: (macro)
display instructions from the current interactive session
* ACL2-PC||COMMANDS:: (macro)
display instructions from the current interactive session
* ACL2-PC||COMMENT:: (primitive)
insert a comment
* ACL2-PC||CONTRADICT:: (macro)
same as contrapose
* ACL2-PC||CONTRAPOSE:: (primitive)
switch a hypothesis with the conclusion, negating both
* ACL2-PC||DEMOTE:: (primitive)
move top-level hypotheses to the conclusion
* ACL2-PC||DIVE:: (primitive)
move to the indicated subterm
* ACL2-PC||DO-ALL:: (macro)
run the given instructions
* ACL2-PC||DO-ALL-NO-PROMPT:: (macro)
run the given instructions, halting once there is a ``failure''
* ACL2-PC||DO-STRICT:: (macro)
run the given instructions, halting once there is a ``failure''
* ACL2-PC||DROP:: (primitive)
drop top-level hypotheses
* ACL2-PC||DV:: (atomic macro)
move to the indicated subterm
* ACL2-PC||ELIM:: (atomic macro)
call the ACL2 theorem prover's elimination process
* ACL2-PC||EQUIV:: (primitive)
attempt an equality (or congruence-based) substitution
* ACL2-PC||EX:: (macro)
exit after possibly saving the state
* ACL2-PC||EXIT:: (meta)
exit the interactive proof-checker
* ACL2-PC||EXPAND:: (primitive)
expand the current function call without simplification
* ACL2-PC||FAIL:: (macro)
cause a failure
* ACL2-PC||FORWARDCHAIN:: (atomic macro)
forward chain from an implication in the hyps
* ACL2-PC||FREE:: (atomic macro)
create a ``free variable''
* ACL2-PC||GENERALIZE:: (primitive)
perform a generalization
* ACL2-PC||GOALS:: (macro)
list the names of goals on the stack
* ACL2-PC||HELP:: (macro)
proof-checker help facility
* ACL2-PC||HELP!:: (macro)
proof-checker help facility
* ACL2-PC||HELP-LONG:: (macro)
same as help!
* ACL2-PC||HYPS:: (macro)
print the hypotheses
* ACL2-PC||ILLEGAL:: (macro)
illegal instruction
* ACL2-PC||IN-THEORY:: (primitive)
set the current proof-checker theory
* ACL2-PC||INDUCT:: (atomic macro)
generate subgoals using induction
* ACL2-PC||LEMMAS-USED:: (macro)
print the runes (definitions, lemmas, ...) used
* ACL2-PC||LISP:: (meta)
evaluate the given form in Lisp
* ACL2-PC||MORE:: (macro)
proof-checker help facility
* ACL2-PC||MORE!:: (macro)
proof-checker help facility
* ACL2-PC||NEGATE:: (macro)
run the given instructions, and ``succeed'' if and only if they ``fail''
* ACL2-PC||NIL:: (macro)
used for interpreting control-d
* ACL2-PC||NOISE:: (meta)
run instructions with output
* ACL2-PC||NX:: (atomic macro)
move forward one argument in the enclosing term
* ACL2-PC||ORELSE:: (macro)
run the first instruction; if (and only if) it ``fails'', run the
second
* ACL2-PC||P:: (macro)
prettyprint the current term
* ACL2-PC||P-TOP:: (macro)
prettyprint the conclusion, highlighting the current term
* ACL2-PC||PP:: (macro)
prettyprint the current term
* ACL2-PC||PRINT:: (macro)
print the result of evaluating the given form
* ACL2-PC||PRINT-ALL-CONCS:: (macro)
print all the conclusions of (as yet unproved) goals
* ACL2-PC||PRINT-ALL-GOALS:: (macro)
print all the (as yet unproved) goals
* ACL2-PC||PRINT-MAIN:: (macro)
print the original goal
* ACL2-PC||PRO:: (atomic macro)
repeatedly apply promote
* ACL2-PC||PROMOTE:: (primitive)
move antecedents of conclusion's implies term to top-level
hypotheses
* ACL2-PC||PROTECT:: (macro)
run the given instructions, reverting to existing state upon
failure
* ACL2-PC||PROVE:: (primitive)
call the ACL2 theorem prover to prove the current goal
* ACL2-PC||PSO:: (macro)
print the most recent proof attempt from inside the proof-checker
* ACL2-PC||PSO!:: (macro)
print the most recent proof attempt from inside the proof-checker
* ACL2-PC||PUT:: (macro)
substitute for a ``free variable''
* ACL2-PC||QUIET:: (meta)
run instructions without output
* ACL2-PC||R:: (macro)
same as rewrite
* ACL2-PC||REDUCE:: (atomic macro)
call the ACL2 theorem prover's simplifier
* ACL2-PC||REDUCE-BY-INDUCTION:: (macro)
call the ACL2 prover without induction, after going into
induction
* ACL2-PC||REMOVE-ABBREVIATIONS:: (primitive)
remove one or more abbreviations
* ACL2-PC||REPEAT:: (macro)
repeat the given instruction until it ``fails''
* ACL2-PC||REPEAT-REC:: (macro)
auxiliary to repeat
* ACL2-PC||REPLAY:: (macro)
replay one or more instructions
* ACL2-PC||RESTORE:: (meta)
remove the effect of an UNDO command
* ACL2-PC||RETAIN:: (atomic macro)
drop all *but* the indicated top-level hypotheses
* ACL2-PC||RETRIEVE:: (macro)
re-enter the proof-checker
* ACL2-PC||REWRITE:: (primitive)
apply a rewrite rule
* ACL2-PC||RUN-INSTR-ON-GOAL:: (macro)
auxiliary to THEN
* ACL2-PC||RUN-INSTR-ON-NEW-GOALS:: (macro)
auxiliary to then
* ACL2-PC||RUNES:: (macro)
print the runes (definitions, lemmas, ...) used
* ACL2-PC||S:: (primitive)
simplify the current subterm
* ACL2-PC||S-PROP:: (atomic macro)
simplify propositionally
* ACL2-PC||SAVE:: (macro)
save the proof-checker state (state-stack)
* ACL2-PC||SEQUENCE:: (meta)
run the given list of instructions according to a multitude of
options
* ACL2-PC||SHOW-ABBREVIATIONS:: (macro)
display the current abbreviations
* ACL2-PC||SHOW-REWRITES:: (macro)
display the applicable rewrite rules
* ACL2-PC||SKIP:: (macro)
``succeed'' without doing anything
* ACL2-PC||SL:: (atomic macro)
simplify with lemmas
* ACL2-PC||SPLIT:: (atomic macro)
split the current goal into cases
* ACL2-PC||SR:: (macro)
same as SHOW-REWRITES
* ACL2-PC||SUCCEED:: (macro)
run the given instructions, and ``succeed''
* ACL2-PC||TH:: (macro)
print the top-level hypotheses and the current subterm
* ACL2-PC||THEN:: (macro)
apply one instruction to current goal and another to new subgoals
* ACL2-PC||TOP:: (atomic macro)
move to the top of the goal
* ACL2-PC||TYPE-ALIST:: (macro)
display the type-alist from the current context
* ACL2-PC||UNDO:: (meta)
undo some instructions
* ACL2-PC||UNSAVE:: (macro)
remove a proof-checker state
* ACL2-PC||UP:: (primitive)
move to the parent (or some ancestor) of the current subterm
* ACL2-PC||USE:: (atomic macro)
use a lemma instance
* ACL2-PC||WRAP:: (atomic macro)
execute the indicated instructions and combine all the new goals
* ACL2-PC||WRAP-INDUCT:: (atomic macro)
same as induct, but create a single goal
* ACL2-PC||WRAP1:: (primitive)
combine goals into a single goal
* ACL2-PC||X:: (atomic macro)
expand and (maybe) simplify function call at the current subterm
* ACL2-PC||X-DUMB:: (atomic macro)
expand function call at the current subterm, without simplifying
File: acl2-doc-emacs.info, Node: ACL2-PC||=, Next: ACL2-PC||ACL2-WRAP, Prev: PROOF-CHECKER-COMMANDS, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||= (atomic macro)
attempt an equality (or equivalence) substitution
Examples:
= -- replace the current subterm by a term equated to it in
one of the hypotheses (if such a term exists)
(= x) -- replace the current subterm by x, assuming that the prover
can show that they are equal
(= (+ x y) z)
-- replace the term (+ x y) by the term z inside the current
subterm, assuming that the prover can prove
(equal (+ x y) z) from the current top-level hypotheses
or that this term or (equal z (+ x y)) is among the
current top-level hypotheses or the current governors
(= & z)
-- exactly the same as above, if (+ x y) is the current
subterm
(= (+ x y) z :hints :none)
-- same as (= (+ x y) z), except that a new subgoal is
created with the current goal's hypotheses and governors
as its top-level hypotheses and (equal (+ x y) z) as its
conclusion
(= (+ x y) z 0)
-- exactly the same as immediately above
(= (p x)
(p y)
:equiv iff
:otf-flg t
:hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
-- same as (= (+ x y) z), except that the prover uses
the indicated values for otf-flg and hints, and only
propositional (iff) equivalence is used (however, it
must be that only propositional equivalence matters at
the current subterm)
General Form:
(= &optional x y &rest keyword-args)
If terms x and y are supplied, then replace x by y inside the current
subterm if they are "known" to be "equal". Here "known" means the
following: the prover is called as in the prove command (using
keyword-args) to prove (equal x y), except that a keyword argument
:equiv is allowed, in which case (equiv x y) is proved instead, where
equiv is that argument. (See below for how governors are handled.)
Actually, keyword-args is either a single non-keyword or is a list of
the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of the
keywords :equiv, :otf-flg, :hints. Here :equiv defaults to equal if
the argument is not supplied or is nil, and otherwise should be the
name of an ACL2 equivalence relation. :Otf-flg and :hints give
directives to the prover, as explained above and in the documentation
for the prove command; however, no prover call is made if :hints is a
non-nil atom or if keyword-args is a single non-keyword (more on this
below).
_Remarks on defaults_
(1) If there is only one argument, say a, then x defaults to the
current subterm, in the sense that x is taken to be the current subterm
and y is taken to be a.
(2) If there are at least two arguments, then x may be the symbol &,
which then represents the current subterm. Thus, (= a) is equivalent
to (= & a). (Obscure point: actually, & can be in any package, except
the keyword package.)
(3) If there are no arguments, then we look for a top-level hypothesis
or a governor of the form (equal c u) or (equal u c), where c is the
current subterm. In that case we replace the current subterm by u.
As with the prove command, we allow goals to be given "bye"s in the
proof, which may be generated by a :hints keyword argument in
keyword-args. These result in the creation of new subgoals.
A proof is attempted unless the :hints argument is a non-nil atom other
than :none, or unless there is one element of keyword-args and it is
not a keyword. In that case, if there are any hypotheses in the
current goal, then what is attempted is a proof of the implication
whose antecedent is the conjunction of the current hypotheses and
governors and whose conclusion is the appropriate equal term.
*Notes:* (1) It is allowed to use abbreviations in the hints. (2) The
keyword :none has the special role as a value of :hints that is shown
clearly in an example above. (3) If there are governors, then the new
subgoal has as additional hypotheses the current governors.
File: acl2-doc-emacs.info, Node: ACL2-PC||ACL2-WRAP, Next: ACL2-PC||ADD-ABBREVIATION, Prev: ACL2-PC||=, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||ACL2-WRAP (macro)
same as (lisp x)
Example:
(acl2-wrap (pe :here))
General Form:
(acl2-wrap form)
Same as (lisp form). This is provided for interface tools that want to
be able to execute the same form in raw Lisp, in the proof-checker, or
in the ACL2 top-level loop (lp).
File: acl2-doc-emacs.info, Node: ACL2-PC||ADD-ABBREVIATION, Next: ACL2-PC||BASH, Prev: ACL2-PC||ACL2-WRAP, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||ADD-ABBREVIATION (primitive)
add an abbreviation
Example: (add-abbreviation v (* x y)) causes future occurrences of (*
x y) to be printed as (? v), until (unless) a corresponding invocation
of remove-abbreviations occurs. In this case we say that v
"abbreviates" (* x y).
General Form:
(add-abbreviation var &optional raw-term)
Let var be an abbreviation for raw-term, if raw-term is supplied, else
for the current subterm. Note that var must be a variable that does
not already abbreviate some term.
A way to think of abbreviations is as follows. Imagine that whenever
an abbreviation is added, say v abbreviates expr, an entry associating
v to expr is made in an association list, which we will call
"*abbreviations-alist*". Then simply imagine that ? is a function
defined by something like:
(defun ? (v)
(let ((pair (assoc v *abbreviations-alist*)))
(if pair (cdr pair)
(error ...))))
Of course the implementation isn't exactly like that, since the
"constant" *abbreviations-alist* actually changes each time an
add-abbreviation instruction is successfully invoked. Nevertheless, if
one imagines an appropriate redefinition of the "constant"
*abbreviations-alist* each time an add-abbreviation is invoked, then
one will have a clear model of the meaning of such an instruction.
The effect of abbreviations on output is that before printing a term,
each subterm that is abbreviated by a variable v is first replaced by
(? v).
The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is expected
as an argument, i.e., accepts the syntax (? v) whenever v abbreviates a
term. For example, the second argument of add-abbreviation may itself
use abbreviations that have been defined by previous add-abbreviation
instructions.
See also remove-abbreviations and show-abbreviations.
File: acl2-doc-emacs.info, Node: ACL2-PC||BASH, Next: ACL2-PC||BDD, Prev: ACL2-PC||ADD-ABBREVIATION, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||BASH (atomic macro)
call the ACL2 theorem prover's simplifier
Examples:
bash -- attempt to prove the current goal by simplification alone
(bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal by simplification alone,
with the indicated hints
General Form:
(bash &rest hints)
Call the theorem prover's simplifier, creating a subgoal for each
resulting goal.
Notice that unlike prove, the arguments to bash are spread out, and are
all hints.
Bash is similar to reduce in that neither of these allows induction.
But bash only allows simplification, while reduce allows processes
eliminate-destructors, fertilize, generalize, and eliminate-irrelevance.
*Note:* All forcing rounds will be skipped (unless there are more than
15 subgoals generated in the first forcing round, an injustice that
should be rectified by the next release).
File: acl2-doc-emacs.info, Node: ACL2-PC||BDD, Next: ACL2-PC||BK, Prev: ACL2-PC||BASH, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||BDD (atomic macro)
prove the current goal using bdds
Examples:
bdd
(bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)
The general form is as shown in the latter example above, but with any
keyword-value pairs omitted and with values as described for the :bdd
hint; see *note HINTS::.
This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal. Note that if :prove is t (the default),
then the proof will succeed entirely using bdds or else it will fail
immediately. See *Note BDD::.
File: acl2-doc-emacs.info, Node: ACL2-PC||BK, Next: ACL2-PC||BOOKMARK, Prev: ACL2-PC||BDD, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||BK (atomic macro)
move backward one argument in the enclosing term
Example and General Form:
bk
For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is (* (- y) z), then after executing bk, the current subterm
will be x.
Move to the previous argument of the enclosing term.
This is the same as up followed by (dive n-1), where n is the position
of the current subterm in its parent term in the conclusion. Thus in
particular, the nx command fails if one is already at the top of the
conclusion.
See also up, dive, top, and bk.
File: acl2-doc-emacs.info, Node: ACL2-PC||BOOKMARK, Next: ACL2-PC||CASESPLIT, Prev: ACL2-PC||BK, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||BOOKMARK (macro)
insert matching ``bookends'' comments
Example:
(bookmark final-goal)
General Form:
(bookmark name &rest instruction-list)
Run the instructions in instruction-list (as though this were a call of
do-all; see the documentation for do-all), but first insert a begin
bookend with the given name and then, when the instructions have been
completed, insert an end bookend with that same name. See the
documentation of comm for an explanation of bookends and how they can
affect the display of instructions.
File: acl2-doc-emacs.info, Node: ACL2-PC||CASESPLIT, Next: ACL2-PC||CG, Prev: ACL2-PC||BOOKMARK, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CASESPLIT (primitive)
split into two cases
Example:
(casesplit (< x y)) -- assuming that we are at the top of the
conclusion, add (< x y) as a new top-level
hypothesis in the current goal, and create a
subgoal identical to the current goal except
that it has (not (< x y)) as a new top-level
hypothesis
General Form:
(casesplit expr &optional use-hyps-flag do-not-flatten-flag)
When the current subterm is the entire conclusion, this instruction
adds expr as a new top-level hypothesis, and create a subgoal identical
to the existing current goal except that it has the negation of expr as
a new top-level hypothesis. See also claim. The optional arguments
control the use of governors and the "flattening" of new hypotheses, as
we now explain.
The argument use-hyps-flag is only of interest when there are
governors. (To read about governors, see the documentation for the
command hyps). In that case, if use-hyps-flag is not supplied or is
nil, then the description above is correct; but otherwise, it is not
expr but rather it is (implies govs expr) that is added as a new
top-level hypothesis (and whose negation is added as a top-level
hypothesis for the new goal), where govs is the conjunction of the
governors.
If do-not-flatten-flag is supplied and not nil, then that is all there
is to this command. Otherwise (thus this is the default), when the
claimed term (first argument) is a conjunction (and) of terms and the
claim instruction succeeds, then each (nested) conjunct of the claimed
term is added as a separate new top-level hypothesis. Consider the
following example, assuming there are no governors.
(casesplit (and (and (< x y) (integerp a)) (equal r s)) t)
Three new top-level hypotheses are added to the current goal, namely (<
x y), (integerp a), and (equal r s). In that case, only one hypothesis
is added to create the new goal, namely the negation of (and (< x y)
(integerp a) (equal r s)). If the negation of this term had been
claimed, then it would be the other way around: the current goal would
get a single new hypothesis while the new goal would be created by
adding three hypotheses.
*Note:* It is allowed to use abbreviations in the hints.
File: acl2-doc-emacs.info, Node: ACL2-PC||CG, Next: ACL2-PC||CHANGE-GOAL, Prev: ACL2-PC||CASESPLIT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CG (macro)
change to another goal.
Examples:
(cg (main . 1)) -- change to the goal (main . 1)
cg -- change to the next-to-top goal
General Form:
(CG &OPTIONAL goal-name)
Same as (change-goal goal-name t), i.e. change to the indicated and
move the current goal to the end of the goal stack.
File: acl2-doc-emacs.info, Node: ACL2-PC||CHANGE-GOAL, Next: ACL2-PC||CLAIM, Prev: ACL2-PC||CG, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CHANGE-GOAL (primitive)
change to another goal.
Examples:
(change-goal (main . 1)) -- change to the goal (main . 1)
change-goal -- change to the next-to-top goal
General Form:
(change-goal &optional goal-name end-flg)
Change to the goal with the name goal-name, i.e. make it the current
goal. However, if goal-name is nil or is not supplied, then it
defaults to the next-to-top goal, i.e., the second goal in the stack of
goals. If end-flg is supplied and not nil, then move the current goal
to the end of the goal stack; else merely swap it with the next-to-top
goal. Also see documentation for cg.
File: acl2-doc-emacs.info, Node: ACL2-PC||CLAIM, Next: ACL2-PC||COMM, Prev: ACL2-PC||CHANGE-GOAL, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CLAIM (atomic macro)
add a new hypothesis
Examples:
(claim (< x y)) -- attempt to prove (< x y) from the current
top-level hypotheses and if successful, then
add (< x y) as a new top-level hypothesis in
the current goal
(claim (< x y)
:otf-flg t
:hints (("Goal" :induct t)))
-- as above, but call the prover using the
indicated values for the otf-flg and hints
(claim (< x y) 0) -- as above, except instead of attempting to
prove (< x y), create a new subgoal with the
same top-level hypotheses as the current goal
that has (< x y) as its conclusion
(claim (< x y) :hints :none)
-- same as immediately above
General Form:
(claim expr &rest rest-args)
This command creates a new subgoal with the same top-level hypotheses
as the current goal but with a conclusion of expr. If rest-args is a
non-empty list headed by a non-keyword, then there will be no proof
attempted for the new subgoal. With that possible exception, rest-args
should consist of keyword arguments. The keyword argument
:do-not-flatten controls the "flattening" of new hypotheses, just as
with the casesplit command (as described in its documentation). The
remaining rest-args are used with a call the prove command on the new
subgoal, except that if :hints is a non-nil atom, then the prover is
not called -- rather, this is the same as the situation described
above, where rest-args is a non-empty list headed by a non-keyword.
*Notes:* (1) Unlike the casesplit command, the claim command is
completely insensitive to governors. (2) It is allowed to use
abbreviations in the hints. (3) The keyword :none has the special role
as a value of :hints that is shown clearly in an example above.
File: acl2-doc-emacs.info, Node: ACL2-PC||COMM, Next: ACL2-PC||COMMANDS, Prev: ACL2-PC||CLAIM, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||COMM (macro)
display instructions from the current interactive session
Examples:
comm
(comm 10)
General Form:
(comm &optional n)
Prints out instructions in reverse order. This is actually the same as
(commands n t) -- or, (commands nil t) if n is not supplied. As
explained in the documentation for commands, the final argument of t
causes suppression of instructions occurring between so-called
"matching bookends," which we now explain.
A "begin bookend" is an instruction of the form
(COMMENT :BEGIN x . y).
Similarly, an "end bookend" is an instruction of the form
(COMMENT :END x' . y').
The "name" of the first bookend is x and the "name" of the second
bookend is x'. When such a pair of instructions occurs in the current
state-stack, we call them "matching bookends" provided that they have
the same name (i.e. x equals x') and if no other begin or end bookend
with name x occurs between them. The idea now is that comm hides
matching bookends together with the instructions they enclose. Here is
a more precise explanation of this "hiding"; probably there is no value
in reading on!
A comm instruction hides bookends in the following manner. (So does a
comment instruction when its second optional argument is supplied and
non-nil.) First, if the first argument n is supplied and not nil, then
we consider only the last n instructions from the state-stack;
otherwise, we consider them all. Now the resulting list of
instructions is replaced by the result of applying the following
process to each pair of matching bookends: the pair is removed,
together with everything in between the begin and end bookend of the
pair, and all this is replaced by the "instruction"
("***HIDING***" :COMMENT :BEGIN name ...)
where (comment begin name ...) is the begin bookend of the pair.
Finally, after applying this process to each pair of matching bookends,
each begin bookend of the form (comment begin name ...) that remains
is replaced by
("***UNFINISHED***" :COMMENT :BEGIN name ...) .
File: acl2-doc-emacs.info, Node: ACL2-PC||COMMANDS, Next: ACL2-PC||COMMENT, Prev: ACL2-PC||COMM, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||COMMANDS (macro)
display instructions from the current interactive session
Examples:
commands
(commands 10 t)
General Forms:
commands or (commands nil)
Print out all the instructions (in the current state-stack) in
reverse order, i.e. from the most recent instruction to the starting
instruction.
(commands n) [n a positive integer]
Print out the most recent n instructions (in the current
state-stack), in reverse order.
(commands x abbreviate-flag)
Same as above, but if abbreviate-flag is non-NIL, then do not
display commands between ``matching bookends''. See documentation
for comm for an explanation of matching bookends.
*Note*: If there are more than n instructions in the state-stack, then
(commands n) is the same as commands (and also, (commands n abb) is the
same as (commands nil abb)).
File: acl2-doc-emacs.info, Node: ACL2-PC||COMMENT, Next: ACL2-PC||CONTRADICT, Prev: ACL2-PC||COMMANDS, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||COMMENT (primitive)
insert a comment
Example:
(comment now begin difficult final goal)
General Form:
(comment &rest x)
This instruction makes no change in the state except to insert the
comment instruction.
Some comments can be used to improve the display of commands; see
documentation for comm.
File: acl2-doc-emacs.info, Node: ACL2-PC||CONTRADICT, Next: ACL2-PC||CONTRAPOSE, Prev: ACL2-PC||COMMENT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CONTRADICT (macro)
same as contrapose
see documentation for contrapose
File: acl2-doc-emacs.info, Node: ACL2-PC||CONTRAPOSE, Next: ACL2-PC||DEMOTE, Prev: ACL2-PC||CONTRADICT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||CONTRAPOSE (primitive)
switch a hypothesis with the conclusion, negating both
Example:
(contrapose 3)
General Form:
(contrapose &optional n)
The (optional) argument n should be a positive integer that does not
exceed the number of hypotheses. Negate the current conclusion and
make it the nth hypothesis, while negating the current nth hypothesis
and making it the current conclusion. If no argument is supplied then
the effect is the same as for (contrapose 1).
*Note:* By "negate" we mean an operation that replaces nil by t, x by
nil for any other explicit value x, (not x) by x, and any other x by
(not x).
File: acl2-doc-emacs.info, Node: ACL2-PC||DEMOTE, Next: ACL2-PC||DIVE, Prev: ACL2-PC||CONTRAPOSE, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DEMOTE (primitive)
move top-level hypotheses to the conclusion
Examples:
demote -- demote all top-level hypotheses
(demote 3 5) -- demote hypotheses 3 and 5
For example, if the top-level hypotheses are x and y and the conclusion
is z, then after execution of demote, the conclusion will be (implies
(and x y) z) and there will be no (top-level) hypotheses.
General Form:
(demote &rest hyps-indices)
Eliminate the indicated (top-level) hypotheses, but replace the
conclusion conc with (implies hyps conc) where hyps is the conjunction
of the hypotheses that were eliminated. If no arguments are supplied,
then all hypotheses are demoted, i.e. demote is the same as (demote 1 2
... n) where n is the number of top-level hypotheses.
*Note*: You must be at the top of the conclusion in order to use this
command. Otherwise, first invoke top. Also, demote fails if there are
no top-level hypotheses or if indices are supplied that are out of
range.
File: acl2-doc-emacs.info, Node: ACL2-PC||DIVE, Next: ACL2-PC||DO-ALL, Prev: ACL2-PC||DEMOTE, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DIVE (primitive)
move to the indicated subterm
Examples:
(DIVE 1) -- assign the new current subterm to be the first
argument of the existing current subterm
(DIVE 1 2) -- assign the new current subterm to be the result of
first taking the 1st argument of the existing
current subterm, and then the 2nd argument of that
For example, if the current subterm is
(* (+ a b) c),
then after (dive 1) it is
(+ a b).
If after that, then (dive 2) is invoked, the new current subterm will be
b.
Instead of (dive 1) followed by (dive 2), the same current subterm
could be obtained by instead submitting the single instruction (dive 1
2).
General Form:
(dive &rest naturals-list)
If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.
*Note:* Dive is related to the command pp, in that the diving is done
according to raw (translated, internal form) syntax. Use the command
dv if you want to dive according to the syntax displayed by the command
p. Note that (dv n) can be abbreviated by simply n.
File: acl2-doc-emacs.info, Node: ACL2-PC||DO-ALL, Next: ACL2-PC||DO-ALL-NO-PROMPT, Prev: ACL2-PC||DIVE, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DO-ALL (macro)
run the given instructions
Example:
(do-all induct p prove)
General Form:
(do-all &rest instruction-list)
Run the indicated instructions until there is a hard "failure". The
instruction "succeeds" if and only if each instruction in
instruction-list does. (See the documentation for sequence for an
explanation of "success" and "failure.") As each instruction is
executed, the system will print the usual prompt followed by that
instruction, unless the global state variable
print-prompt-and-instr-flg is nil.
*Note:* If do-all "fails", then the failure is hard if and only if the
last instruction it runs has a hard "failure".
Obscure point: For the record, (do-all ins_1 ins_2 ... ins_k) is the
same as (sequence (ins_1 ins_2 ... ins_k)).
File: acl2-doc-emacs.info, Node: ACL2-PC||DO-ALL-NO-PROMPT, Next: ACL2-PC||DO-STRICT, Prev: ACL2-PC||DO-ALL, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DO-ALL-NO-PROMPT (macro)
run the given instructions, halting once there is a ``failure''
Example:
(do-all-no-prompt induct p prove)
General Form:
(do-all-no-prompt &rest instruction-list)
Do-all-no-prompt is the same as do-all, except that the prompt and
instruction are not printed each time, regardless of the value of
print-prompt-and-instr-flg. Also, restoring is disabled. See the
documentation for do-all.
File: acl2-doc-emacs.info, Node: ACL2-PC||DO-STRICT, Next: ACL2-PC||DROP, Prev: ACL2-PC||DO-ALL-NO-PROMPT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DO-STRICT (macro)
run the given instructions, halting once there is a ``failure''
Example:
(do-strict induct p prove)
General Form:
(do-strict &rest instruction-list)
Run the indicated instructions until there is a (hard or soft)
"failure". In fact do-strict is identical in effect to do-all, except
that do-all only halts once there is a hard "failure". See the
documentation for do-all.
File: acl2-doc-emacs.info, Node: ACL2-PC||DROP, Next: ACL2-PC||DV, Prev: ACL2-PC||DO-STRICT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DROP (primitive)
drop top-level hypotheses
Examples:
(drop 2 3) -- drop the second and third hypotheses
drop -- drop all top-level hypotheses
General Forms:
(drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.
drop -- Drop all the top-level hypotheses.
*Note:* If there are no top-level hypotheses, then the instruction
drop will fail. If any of the indices is out of range, i.e. is not an
integer between one and the number of top-level hypotheses (inclusive),
then (drop n1 n2 ...) will fail.
File: acl2-doc-emacs.info, Node: ACL2-PC||DV, Next: ACL2-PC||ELIM, Prev: ACL2-PC||DROP, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||DV (atomic macro)
move to the indicated subterm
Examples:
(dv 1) -- assign the new current subterm to be the first argument
of the existing current subterm
(dv 1 2) -- assign the new current subterm to be the result of
first taking the 1st argument of the existing
current subterm, and then the 2nd argument of that
For example, if the current subterm is
(* (+ a b) c),
then after (dv 1) it is
(+ a b).
If after that, then (dv 2) is invoked, the new current subterm will be
b.
Instead of (dv 1) followed by (dv 2), the same current subterm could be
obtained by instead submitting the single instruction (dv 1 2).
General Form:
(dv &rest naturals-list)
If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers,
let the new current subterm be the result of selecting the n_1-st
argument of the current subterm, and then the n_2-th subterm of that,
..., finally the n_k-th subterm.
*Note:* (dv n) may be abbreviated by simply n, so we could have typed
1 instead of (dv 1) in the first example above.
*Note:* See also dive, which is related to the command pp, in that the
diving is done according to raw (translated, internal form) syntax.
Use the command dv if you want to dive according to the syntax
displayed by the command p.
File: acl2-doc-emacs.info, Node: ACL2-PC||ELIM, Next: ACL2-PC||EQUIV, Prev: ACL2-PC||DV, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||ELIM (atomic macro)
call the ACL2 theorem prover's elimination process
Example and General Form:
elim
Upon running the elim command, the system will create a subgoal will be
created for each goal that would have been pushed for proof by
induction in an ordinary proof, where *only* elimination is used; not
even simplification is used!
File: acl2-doc-emacs.info, Node: ACL2-PC||EQUIV, Next: ACL2-PC||EX, Prev: ACL2-PC||ELIM, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||EQUIV (primitive)
attempt an equality (or congruence-based) substitution
Examples:
(equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
current subterm, if their equality is among the
top-level hypotheses or the governors
(equiv x t iff) -- replace x by t everywhere inside the current
subterm, where only propositional equivalence
needs to be maintained at each occurrence of x
General form:
(equiv old new &optional relation)
Substitute new for old everywhere inside the current subterm, provided
that either (relation old new) or (relation new old) is among the
top-level hypotheses or the governors (possibly by way of backchaining
and/or refinement; see below). If relation is nil or is not supplied,
then it defaults to equal. See also the command =, which is much more
flexible. Note that this command fails if no substitution is actually
made.
*Note:* No substitution takes place inside explicit values. So for
example, the instruction (equiv 3 x) will cause 3 to be replaced by x
if the current subterm is, say, (* 3 y), but not if the current subterm
is (* 4 y) even though 4 = (1+ 3).
The following remarks are quite technical and mostly describe a certain
weak form of "backchaining" that has been implemented for equiv in
order to support the = command. In fact neither the term (relation old
new) nor the term (relation new old) needs to be *explicitly* among the
current "assumptions", i.e., the top-level hypothesis or the governors.
Rather, there need only be such an assumption that "tells us" (r old
new) or (r new old), for *some* equivalence relation r that *refines*
relation. Here, "tells us" means that either one of the indicated
terms is among those assumptions, or else there is an assumption that
is an implication whose conclusion is one of the indicated terms and
whose hypotheses (gathered up by appropriately flattening the first
argument of the implies term) are all among the current assumptions.
File: acl2-doc-emacs.info, Node: ACL2-PC||EX, Next: ACL2-PC||EXIT, Prev: ACL2-PC||EQUIV, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||EX (macro)
exit after possibly saving the state
Example and General Form:
ex
Same as exit, except that first the instruction save is executed.
If save queries the user and is answered negatively, then the exit is
aborted.
File: acl2-doc-emacs.info, Node: ACL2-PC||EXIT, Next: ACL2-PC||EXPAND, Prev: ACL2-PC||EX, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||EXIT (meta)
exit the interactive proof-checker
Examples:
exit -- exit the interactive proof-checker
(exit append-associativity) -- exit and create a defthm
event named append-associativity
General Forms:
exit -- Exit without storing an event.
(exit event-name &optional rule-classes do-it-flg)
Exit, and store an event.
The command exit returns you to the ACL2 loop. At a later time,
(verify) may be executed to get back into the same proof-checker state,
as long as there hasn't been an intervening use of the proof-checker
(otherwise see save).
When given one or more arguments as shown above, exit still returns you
to the ACL2 loop, but first, if the interactive proof is complete, then
it attempts create a defthm event with the specified event-name and
rule-classes (which defaults to (:rewrite) if not supplied). The event
will be printed to the terminal, and then normally the user will be
queried whether an event should really be created. However, if the
final optional argument do-it-flg is supplied and not nil, then an
event will be made without a query.
For example, the form
(exit top-pop-elim (:elim :rewrite) t)
causes a defthm event named top-pop-elim to be created with
rule-classes (:elim :rewrite), without a query to the user (because of
the argument t).
*Note:* it is permitted for event-name to be nil. In that case, the
name of the event will be the name supplied during the original call of
verify. (See the documentation for verify and commands.) Also in that
case, if rule-classes is not supplied then it defaults to the
rule-classes supplied in the original call of verify.
Comments on "success" and "failure". An exit instruction will always
"fail", so for example, if it appears as an argument of a do-strict
instruction then none of the later (instruction) arguments will be
executed. Moreover, the "failure" will be "hard" if an event is
successfully created or if the instruction is simply exit; otherwise it
will be "soft". See the documentation for sequence for an explanation
of hard and soft "failures". An obscure but potentially important fact
is that if the "failure" is hard, then the error signal is a special
signal that the top-level interactive loop can interpret as a request
to exit. Thus for example, a sequencing command that turns an error
triple (mv erp val state) into (mv t val state) would never cause an
exit from the interactive loop.
If the proof is not complete, then (exit event-name ...) will not cause
an exit from the interactive loop. However, in that case it will print
out the original user-supplied goal (the one that was supplied with the
call to verify) and the current list of instructions.
File: acl2-doc-emacs.info, Node: ACL2-PC||EXPAND, Next: ACL2-PC||FAIL, Prev: ACL2-PC||EXIT, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||EXPAND (primitive)
expand the current function call without simplification
Examples:
expand -- expand and do not simplify.
For example, if the current subterm is (append a b), then after (expand
t) the current subterm will be the term:
(if (true-listp x)
(if x
(cons (car x) (append (cdr x) y))
y)
(apply 'binary-append (list x y)))
regardless of the top-level hypotheses and the governors.
General Form:
(expand &optional do-not-expand-lambda-flg)
Expand the function call at the current subterm, and do not simplify.
The options have the following meanings:
do-not-expand-lambda-flg: default is nil; otherwise, the result
should be a lambda expression
See also x, which allows simplification.
File: acl2-doc-emacs.info, Node: ACL2-PC||FAIL, Next: ACL2-PC||FORWARDCHAIN, Prev: ACL2-PC||EXPAND, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||FAIL (macro)
cause a failure
Examples:
fail
(fail t)
General Form:
(fail &optional hard)
This is probably only of interest to writers of macro commands. The
only function of fail is to fail to "succeed".
The full story is that fail and (fail nil) simply return (mv nil nil
state), while (fail hard) returns (mv hard nil state) if hard is not
nil. See also do-strict, do-all, and sequence.
File: acl2-doc-emacs.info, Node: ACL2-PC||FORWARDCHAIN, Next: ACL2-PC||FREE, Prev: ACL2-PC||FAIL, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||FORWARDCHAIN (atomic macro)
forward chain from an implication in the hyps
Example:
(forwardchain 2) ; Second hypothesis should be of the form
; (IMPLIES hyp concl), and the result is to replace
; that hypothesis with concl.
General Forms:
(forwardchain hypothesis-number)
(forwardchain hypothesis-number hints)
(forwardchain hypothesis-number hints quiet-flg)
This command replaces the hypothesis corresponding to given index,
which should be of the form (IMPLIES hyp concl), with its consequent
concl. In fact, the given hypothesis is dropped, and the replacement
hypothesis will appear as the final hypothesis after this command is
executed.
The prover must be able to prove the indicated hypothesis from the
other hypotheses, or else the command will fail. The :hints argument
is used in this prover call, and should have the usual syntax of hints
to the prover.
Output is suppressed if quiet-flg is supplied and not nil.
File: acl2-doc-emacs.info, Node: ACL2-PC||FREE, Next: ACL2-PC||GENERALIZE, Prev: ACL2-PC||FORWARDCHAIN, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||FREE (atomic macro)
create a ``free variable''
Example:
(free x)
General Form:
(free var)
Mark var as a "free variable". Free variables are only of interest for
the put command; see its documentation for an explanation.
File: acl2-doc-emacs.info, Node: ACL2-PC||GENERALIZE, Next: ACL2-PC||GOALS, Prev: ACL2-PC||FREE, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||GENERALIZE (primitive)
perform a generalization
Example:
(generalize
((and (true-listp x) (true-listp y)) 0)
((append x y) w))
General Form:
(generalize &rest substitution)
Generalize using the indicated substitution, which should be a
non-empty list. Each element of that list should be a two-element list
of the form (term variable), where term may use abbreviations. The
effect of the instruction is to replace each such term in the current
goal by the corresponding variable. This replacement is carried out by
a parallel substitution, outside-in in each hypothesis and in the
conclusion. More generally, actually, the "variable" (second)
component of each pair may be nil or a number, which causes the system
to generate a new name of the form _ or _n, with n a natural number;
more on this below. However, when a variable is supplied, it must not
occur in any goal of the current proof-checker state.
When the "variable" above is nil, the system will treat it as the
variable |_| if that variable does not occur in any goal of the current
proof-checker state. Otherwise it treats it as |_0|, or |_1|, or |_2|,
and so on, until one of these is not among the variables of the current
proof-checker state. If the "variable" is a non-negative integer n,
then the system treats it as |_n| unless that variable already occurs
among the current goals, in which case it increments n just as above
until it obtains a new variable.
*Note:* The same variable may not occur as the variable component of
two different arguments (though nil may occur arbitrarily many times,
as may a positive integer).
File: acl2-doc-emacs.info, Node: ACL2-PC||GOALS, Next: ACL2-PC||HELP, Prev: ACL2-PC||GENERALIZE, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||GOALS (macro)
list the names of goals on the stack
Example and General Form:
goals
Goals lists the names of all goals that remain to be proved. They are
listed in the order in which they appear on the stack of remaining
goals, which is relevant for example to the effect of a change-goal
instruction.
File: acl2-doc-emacs.info, Node: ACL2-PC||HELP, Next: ACL2-PC||HELP!, Prev: ACL2-PC||GOALS, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||HELP (macro)
proof-checker help facility
Examples:
(help rewrite) -- partial documentation on the rewrite command; the
rest is available using more or more!
(help! rewrite) -- full documentation on the rewrite command
help, help! -- this documentation (in part, or in totality,
respectively)
General Forms:
(help &optional command)
(help! &optional command)
more
more!
The proof checker supports the same kind of documentation as does ACL2
proper. The main difference is that you need to type
(help command)
in a list rather than :doc command. So, to get all the documentation
on command, type (help! command) inside the interactive loop, but to
get only a one-line description of the command together with some
examples, type (help command). In the latter case, you can get the
rest of the help by typing more!; or type more if you don't necessarily
want all the rest of the help at once. (Then keep typing more if you
want to keep getting more of the help for that command.)
To summarize: as with ACL2, you can type either of the following:
more, more!
-- to obtain more (or, all the rest of) the documentation last
requested by help (or, outside the proof-checker's loop, :doc)
It has been arranged that the use of (help command) will tell you just
about everything you could want to know about command, almost always by
way of examples. For more details about a command, use help!, more, or
more!.
We use the word "command" to refer to the name itself, e.g. rewrite.
We use the word "instruction" to refer to an input to the interactive
system, e.g. (rewrite foo) or (help split). Of course, we allow
commands with no arguments as instructions in many cases, e.g. rewrite.
In such cases, command is treated identically to (command).
File: acl2-doc-emacs.info, Node: ACL2-PC||HELP!, Next: ACL2-PC||HELP-LONG, Prev: ACL2-PC||HELP, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||HELP! (macro)
proof-checker help facility
Same as help, except that the entire help message is printed without
any need to invoke more! or more.
Invoke help for documentation about the proof-checker help facility.
File: acl2-doc-emacs.info, Node: ACL2-PC||HELP-LONG, Next: ACL2-PC||HYPS, Prev: ACL2-PC||HELP!, Up: PROOF-CHECKER-COMMANDS
ACL2-PC||HELP-LONG (macro)
same as help!
See the documentation for help!.
Help-long has been included in addition to help! for historical
reasons. (Such a command is included in Pc-Nqthm).