Major Section: PROOF-CHECKER
Example:
(define-pc-help pp ()
(if (goals t)
(io? proof-checker nil state
(fms0 "~|~y0~|"
(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) be a form
that returns state as its single value. 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)).
Major Section: PROOF-CHECKER
Example:
(define-pc-macro ib (&optional term)
(value
(if term
`(then (induct ,term) bash)
`(then induct bash))))
The example above captures a common paradigm: one attempts to prove
the current goal by inducting and then simplifying the resulting
goals. (see proof-checker-commands for documentation of the
command then, which is itself a pc-macro command, and commands
induct and bash.) Rather than issuing (then induct bash), or
worse yet issuing induct and then issuing bash for each resulting
goals, the above definition of ib would let you issue ib and get the
same effect.
General Form: (define-pc-macro cmd args doc-string dcl ... dcl body)where
cmd is the name of the pc-macro than you want to define,
args is its list of formal parameters. Args may include lambda-list
keywords &optional and &rest; see macro-args, but note that
here, args may not include &key or &whole.
The value of body should be an ACL2 ``error triple,'' i.e., have the
form (mv erp xxx state) for some erp and xxx. If erp is
nil, then xxx is handed off to the proof-checker's instruction
interpreter. Otherwise, evaluation typically halts. We may write
more on the full story later if there is interest in reading it.
Major Section: PROOF-CHECKER
Built-in proof-checker meta commands include undo and restore, and
others (lisp, exit, and sequence); see proof-checker-commands.
The advanced proof-checker user can define these as well. See ACL2
source file proof-checker-b.lisp for examples, and contact the ACL2
implementors if those examples do not provide sufficient
documentation.
Major Section: PROOF-CHECKER
Example:
:instructions (induct prove promote (dive 1) x
(dive 2) = top (drop 2) prove)
See 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 proof-checker and
see 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.
Major Section: PROOF-CHECKER
The proof-checker (see 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 verify) and will ``expand'' into zero or more commands.
The latter is similar, except that the undoing mechanism
(see acl2-pc::undo) understands atomic macro commands to
represent single interactive commands. Also see acl2-pc::comm
and see acl2-pc::commands for a discussion of the display of
interactive commands.
Also see toggle-pc-macro for how to change a macro command to
an atomic macro command, and vice versa.
Major Section: 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.
attempt an equality (or equivalence) substitution
same as (lisp x)
add an abbreviation
call the ACL2 theorem prover's simplifier
prove the current goal using bdds
move backward one argument in the enclosing term
insert matching ``bookends'' comments
split into two cases
change to another goal.
change to another goal.
add a new hypothesis
display instructions from the current interactive session
display instructions from the current interactive session
insert a comment
same as contrapose
switch a hypothesis with the conclusion, negating both
move top-level hypotheses to the conclusion
move to the indicated subterm
run the given instructions
run the given instructions, halting once there is a ``failure''
run the given instructions, halting once there is a ``failure''
drop top-level hypotheses
move to the indicated subterm
call the ACL2 theorem prover's elimination process
attempt an equality (or congruence-based) substitution
exit after possibly saving the state
exit the interactive proof-checker
expand the current function call without simplification
cause a failure
forward chain from an implication in the hyps
create a ``free variable''
perform a generalization
list the names of goals on the stack
proof-checker help facility
proof-checker help facility
same as help!
print the hypotheses
illegal instruction
set the current proof-checker theory
generate subgoals using induction
evaluate the given form in Lisp
proof-checker help facility
proof-checker help facility
run the given instructions, and ``succeed'' if and only if they ``fail''
used for interpreting control-d
run instructions with output
move forward one argument in the enclosing term
run the first instruction; if (and only if) it ``fails'', run the
second
prettyprint the current term
prettyprint the conclusion, highlighting the current term
prettyprint the current term
print the result of evaluating the given form
print all the (as yet unproved) goals
print the original goal
repeatedly apply promote
move antecedents of conclusion's implies term to top-level
hypotheses
run the given instructions, reverting to existing state upon
failure
call the ACL2 theorem prover to prove the current goal
substitute for a ``free variable''
run instructions without output
same as rewrite
call the ACL2 theorem prover's simplifier
call the ACL2 prover without induction, after going into
induction
remove one or more abbreviations
repeat the given instruction until it ``fails''
auxiliary to repeat
replay one or more instructions
remove the effect of an UNDO command
drop all but the indicated top-level hypotheses
re-enter the proof-checker
apply a rewrite rule
auxiliary toxae THEN
auxiliary to then
simplify the current subterm
simplify propositionally
save the proof-checker state (state-stack)
run the given list of instructions according to a multitude of
options
display the current abbreviations
display the applicable rewrite rules
``succeed'' without doing anything
simplify with lemmas
split the current goal into cases
same as SHOW-REWRITES
run the given instructions, and ``succeed''
print the top-level hypotheses and the current subterm
apply one instruction to current goal and another to new subgoals
move to the top of the goal
display the type-alist from the current context
undo some instructions
remove a proof-checker state
move to the parent (or some ancestor) of the current subterm
use a lemma instance
expand and (maybe) simplify function call at the current subterm
expand function call at the current subterm, without simplifying
attempt an equality (or equivalence) substitution
Major Section: PROOF-CHECKER-COMMANDS
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.
same as (lisp x)
Major Section: PROOF-CHECKER-COMMANDS
Example: (acl2-wrap (pe :here))Same asGeneral Form: (acl2-wrap form)
(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).
add an abbreviation
Major Section: PROOF-CHECKER-COMMANDS
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.
call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS
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.
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).
prove the current goal using bdds
Major Section: PROOF-CHECKER-COMMANDS
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 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 bdd.
move backward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: bkFor 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.
insert matching ``bookends'' comments
Major Section: PROOF-CHECKER-COMMANDS
Example: (bookmark final-goal)Run the instructions inGeneral Form: (bookmark name &rest instruction-list)
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.
split into two cases
Major Section: PROOF-CHECKER-COMMANDS
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.
change to another goal.
Major Section: PROOF-CHECKER-COMMANDS
Examples: (cg (main . 1)) -- change to the goal (main . 1) cg -- change to the next-to-top goalSame asGeneral Form: (CG &OPTIONAL goal-name)
(change-goal goal-name t), i.e. change to the indicated
and move the current goal to the end of the goal stack.
change to another goal.
Major Section: PROOF-CHECKER-COMMANDS
Examples: (change-goal (main . 1)) -- change to the goal (main . 1) change-goal -- change to the next-to-top goalChange to the goal with the nameGeneral Form: (change-goal &optional goal-name end-flg)
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.
add a new hypothesis
Major Section: PROOF-CHECKER-COMMANDS
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.
display instructions from the current interactive session
Major Section: PROOF-CHECKER-COMMANDS
Examples: comm (comm 10)Prints out instructions in reverse order. This is actually the same asGeneral Form: (comm &optional n)
(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 ...) .
display instructions from the current interactive session
Major Section: PROOF-CHECKER-COMMANDS
Examples: commands (commands 10 t)Note: If there are more thanGeneral 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.
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)).
insert a comment
Major Section: PROOF-CHECKER-COMMANDS
Example: (comment now begin difficult final goal)This instruction makes no change in the state except to insert theGeneral Form: (comment &rest x)
comment instruction.
Some comments can be used to improve the display of commands; see
documentation for comm.
same as contrapose
Major Section: PROOF-CHECKER-COMMANDS
see documentation for contrapose
switch a hypothesis with the conclusion, negating both
Major Section: PROOF-CHECKER-COMMANDS
Example: (contrapose 3)The (optional) argumentGeneral Form: (contrapose &optional n)
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).
move top-level hypotheses to the conclusion
Major Section: PROOF-CHECKER-COMMANDS
Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5For 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.
move to the indicated subterm
Major Section: PROOF-CHECKER-COMMANDS
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.
run the given instructions
Major Section: PROOF-CHECKER-COMMANDS
Example: (do-all induct p prove)Run the indicated instructions until there is a hard ``failure''. The instruction ``succeeds'' if and only if each instruction inGeneral Form: (do-all &rest instruction-list)
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)).
run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER-COMMANDS
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.
run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER-COMMANDS
Example: (do-strict induct p prove)Run the indicated instructions until there is a (hard or soft) ``failure''. In factGeneral Form: (do-strict &rest instruction-list)
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.
drop top-level hypotheses
Major Section: PROOF-CHECKER-COMMANDS
Examples: (drop 2 3) -- drop the second and third hypotheses drop -- drop all top-level hypothesesNote: If there are no top-level hypotheses, then the instructionGeneral Forms: (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.
drop -- Drop all the top-level hypotheses.
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.
move to the indicated subterm
Major Section: PROOF-CHECKER-COMMANDS
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.
call the ACL2 theorem prover's elimination process
Major Section: PROOF-CHECKER-COMMANDS
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!
attempt an equality (or congruence-based) substitution
Major Section: PROOF-CHECKER-COMMANDS
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.
exit after possibly saving the state
Major Section: PROOF-CHECKER-COMMANDS
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.
exit the interactive proof-checker
Major Section: PROOF-CHECKER-COMMANDS
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.
expand the current function call without simplification
Major Section: PROOF-CHECKER-COMMANDS
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 new-goals-flg keep-all-guards-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
new-goals-flg: default of nil means to introduce APPLY for guards
keep-all-guards-flg: default of nil means that the system should make
a weak attempt to prove the guards from the
current context
See also x, which allows simplification.
cause a failure
Major Section: PROOF-CHECKER-COMMANDS
Examples: fail (fail t)This is probably only of interest to writers of macro commands. The only function ofGeneral Form: (fail &optional hard)
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-flag is not nil. See also do-strict, do-all, and sequence.
forward chain from an implication in the hyps
Major Section: PROOF-CHECKER-COMMANDS
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.
create a ``free variable''
Major Section: PROOF-CHECKER-COMMANDS
Example: (free x)MarkGeneral Form: (free var)
var as a ``free variable''. Free variables are only of
interest for the put command; see its documentation for an
explanation.
perform a generalization
Major Section: PROOF-CHECKER-COMMANDS
Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w))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 formGeneral Form: (generalize &rest substitution)
(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).
list the names of goals on the stack
Major Section: PROOF-CHECKER-COMMANDS
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.
proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS
Examples:The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type(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!
(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).
proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS
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.
same as help!
Major Section: PROOF-CHECKER-COMMANDS
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).
print the hypotheses
Major Section: PROOF-CHECKER-COMMANDS
Examples: hyps -- print all (top-level) hypotheses (hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4 (hyps (1 3) t) -- print hypotheses 1 and 3 and all governorsPrint the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here,General Form: (hyps &optional hyps-indices govs-indices)
hyps-indices and
govs-indices should be lists of indices of hypotheses and governors
(respectively), except that the atom t may be used to indicate that
one wants all hypotheses or governors (respectively).
The list of ``governors'' is defined as follows. Actually, we
define here the notion of the governors for a pair of the form
<term, address>]; we're interested in the special case where the
term is the conclusion and the address is the current address. If
the address is nil, then there are no governors, i.e., the list of
governors is nil. If the term is of the form (if x y z) and the
address is of the form (2 . rest) or (3 . rest), then the list of
governors is the result of consing x or its negation (respectively)
onto the list of governors for the pair <y, rest> or the pair
<z, rest> (respectively). If the term is of the form (implies x y)
and the address is of the form (2 . rest), then the list of
governors is the result of consing x onto the list of governors for
the pair <y, rest>. Otherwise, the list of governors for the pair
<term, (n . rest)> is exactly the list of governors for the pair
<argn, rest> where argn is the nth argument of term.
If all goals have been proved, a message saying so will be printed. (as there will be no current hypotheses or governors!).
The hyps command never causes an error. It ``succeeds'' (in fact
its value is t) if the arguments (when supplied) are appropriate,
i.e. either t or lists of indices of hypotheses or governors,
respectively. Otherwise it ``fails'' (its value is nil).
illegal instruction
Major Section: PROOF-CHECKER-COMMANDS
Example: (illegal -3)Probably not of interest to most users; always ``fails'' since it expands to theGeneral Form: (illegal instruction)
fail command.
The illegal command is used mainly in the implementation. For
example, the instruction 0 is ``read'' as (illegal 0), since dive
expects positive integers.
set the current proof-checker theory
Major Section: PROOF-CHECKER-COMMANDS
Example: (in-theory (union-theories *s-prop-theory* '(true-listp binary-append)))If the argument is not supplied, then this command sets the current proof-checker theory (see below for explanation) to agree with the current ACL2 theory. Otherwise, the argument should be a theory expression, and in that case the proof-checker theory is set to the value of that theory expression.General Form: (in-theory &optional atom-or-theory-expression)
The current proof-checker theory is used in all calls to the ACL2
theorem prover and rewriter from inside the proof-checker. Thus,
the most recent in-theory instruction in the current state-stack has
an effect in the proof-checker totally analogous to the effect
caused by an in-theory hint or event in ACL2. However, in-theory
instructions in the proof-checker have no effect outside the
proof-checker's interactive loop.
If the most recent in-theory instruction in the current state of the
proof-checker has no arguments, or if there is no in-theory
instruction in the current state of the proof-checker, then the
proof-checker will use the current ACL2 theory. This is true even
if the user has interrupted the interactive loop by exiting and
changing the global ACL2 theory. However, if the most recent
in-theory instruction in the current state of the proof-checker had
an argument, then global changes to the current theory will have no
effect on the proof-checker state.
generate subgoals using induction
Major Section: PROOF-CHECKER-COMMANDS
Examples:
induct, (induct t)
-- induct according to a heuristically-chosen scheme, creating
a new subgoal for each base and induction step
(induct (append (reverse x) y))
-- as above, but choose an induction scheme based on the term
(append (reverse x) y) rather than on the current goal
General Form:
(induct &optional term)
Induct as in the corresponding :induct hint given to the theorem
prover, creating new subgoals for the base and induction steps. If
term is t or is not supplied, then use the current goal to determine
the induction scheme; otherwise, use that term.Note: As usual, abbreviations are allowed in the term.
Note: Induct actually calls the prove command with all processes
turned off. Thus, you must be at top of the goal for an induct
instruction.
evaluate the given form in Lisp
Major Section: PROOF-CHECKER-COMMANDS
Example: (lisp (assign xxx 3))EvaluateGeneral Form: (lisp form)
form. The lisp command is mainly of interest for side
effects. See also print, skip, and fail.
The rest of the documentation for lisp is of interest only to
those who use it in macro commands. If the Lisp evaluation (by
trans-eval) of form returns an ``error triple'' of the form
(mv erp ((NIL NIL STATE) . (erp-1 val-1 &)) state), then the
lisp command returns the appropriate error triple
(mv (or erp erp-1)
val-1
state) .
Otherwise, the trans-eval of form must return an ``error triple''
of the form (mv erp (cons stobjs-out val) &), and the lisp
command returns the appropriate error triple
(mv erp
val
state).
Note that the output signature of the form has been lost. The user
must know the signature in order to use the output of the lisp
command. Trans-eval, which is undocumented except by comments in
the ACL2 source code, has replaced, in val, any occurrence of
the current state or the current values of stobjs by simple symbols
such as REPLACED-STATE. The actual values of these objects may
be recovered, in principle, from the state returned and the
user-stobj-alist within that state. However, in practice, the
stobjs cannot be recovered because the user is denied access to
user-stobj-alist. The moral is: do not try to write macro
commands that manipulate stobjs. Should the returned val
contain REPLACED-STATE the value may simply be ignored and
state used, since that is what REPLACED-STATE denotes.
proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS
Continues documentation of last proof-checker command visited with
help.
Invoke help for documentation about the proof-checker help
facility.
proof-checker help facility
Major Section: PROOF-CHECKER-COMMANDS
Continues documentation of last proof-checker command visited with
help, until all documentation on that command is printed out.
Invoke help for documentation about the proof-checker help facility.
run the given instructions, and ``succeed'' if and only if they ``fail''
Major Section: PROOF-CHECKER-COMMANDS
Example: (negate prove)
General form: (negate &rest instruction-list)Run the indicated instructions exactly in the sense of
do-all, and
``succeed'' if and only if they ``fail''.
Note: Negate instructions will never produce hard ``failures''.
used for interpreting control-d
Major Section: PROOF-CHECKER-COMMANDS
Example and General form: nil(or,
control-d).
The whole point of this command is that in some Lisps (including
akcl), if you type control-d then it seems, on occasion, to get
interpreted as nil. Without this command, one seems to get into an
infinite loop.
run instructions with output
Major Section: PROOF-CHECKER-COMMANDS
Example: (noise induct prove)Run theGeneral Form: (noise &rest instruction-list)
instruction-list through the top-level loop with output.
In fact, having output is the default. Noise is useful inside a
surrounding call of quiet, when one temporarily wants output. For
example, if one wants to see output for a prove command immediately
following an induct command but before an s command, one may want to
submit an instruction like (quiet induct (noise prove) s). See also
quiet.
move forward one argument in the enclosing term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: nxFor example, if the conclusion is
(= x (* (- y) z)) and the
current subterm is x, then after executing nx, the current
subterm will be (* (- y) z).
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.
run the first instruction; if (and only if) it ``fails'', run the
second
Major Section: PROOF-CHECKER-COMMANDS
Example: (orelse top (print "Couldn't move to the top"))Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.General form: (orelse instr1 instr2)
This instruction ``succeeds'' if and only if either instr1
``succeeds'', or else instr2 ``succeeds''. If it ``fails'', then
the failure is soft.
prettyprint the current term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: p
Prettyprint the current term. The usual user syntax is used, so
that for example one would see (and x y) rather than (if x y 'nil).
(See also pp.) Also, abbreviations are inserted where appropriate;
see add-abbreviation.
The ``current term'' is the entire conclusion unless dive commands
have been given, in which case it may be a subterm of the
conclusion.
If all goals have been proved, a message saying so will be printed
(as there will be no current term!).
prettyprint the conclusion, highlighting the current term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: p-topFor example, if the conclusion is
(equal (and x (p y)) (foo z)) and
the current subterm is (p y), then p-top will print
(equal (and x (*** (p y) ***)) (foo z)).
Prettyprint the the conclusion, highlighting the current term. The
usual user syntax is used, as with the command p (as opposed to pp).
This is illustrated in the example above, where one would *not* see
(equal (if x (*** (p y) ***) 'nil) (foo z)).
Note (obscure): In some situations, a term of the form (if x t y)
occurring inside the current subterm will not print as (or x y),
when x isn't a call of a boolean primitive. There's nothing
incorrect about this, however.
prettyprint the current term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: pp
This is the same as p (see its documentation), except that raw
syntax (internal form) is used. So for example, one would see
(if x y 'nil) rather than (and x y). Abbreviations are however
still inserted, as with p.
print the result of evaluating the given form
Major Section: PROOF-CHECKER-COMMANDS
Example: (print (append '(a b) '(c d))) Print the list (a b c d) to the terminalPrettyprints the result of evaluating form. The evaluation ofGeneral Form: (print form)
form
should return a single value that is not state or a single-threaded
object (see stobj).
If the form you want to evaluate does not satisfy the criterion
above, you should create an appropriate call of the lisp command
instead. Notice that this command always returns
(mv nil nil state) where the second result will always be
REPLACED-STATE.
print all the (as yet unproved) goals
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: print-all-goals
Prints all the goals that remain to be proved, in a pleasant
format.
print the original goal
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: print-main
Prints the goal as originally entered.
repeatedly apply promote
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: pro
Apply the promote command until there is no change. This command
``succeeds'' exactly when at least one call of promote ``succeeds''.
In that case, only a single new proof-checker state will be
created.
move antecedents of conclusion's implies term to top-level
hypotheses
Major Section: PROOF-CHECKER-COMMANDS
Examples: promote (promote t)For example, if the conclusion is
(implies (and x y) z), then
after execution of promote, the conclusion will be z and the terms x
and y will be new top-level hypotheses.
General Form: (promote &optional do-not-flatten-flag)Replace conclusion of
(implies hyps exp) or (if hyps exp t) with
simply exp, adding hyps to the list of top-level hypotheses.
Moreover, if hyps is viewed as a conjunction then each conjunct will
be added as a separate top-level hypothesis. An exception is that
if do-not-flatten-flag is supplied and not nil, then only one
top-level hypothesis will be added, namely hyps.
Note: You must be at the top of the conclusion in order to use this
command. Otherwise, first invoke top.
run the given instructions, reverting to existing state upon
failure
Major Section: PROOF-CHECKER-COMMANDS
Example: (protect induct p prove)General Form: (protect &rest instruction-list)
Protect is the same as do-strict, except that as soon as an
instruction ``fails'', the state-stack reverts to what it was before
the protect instruction began, and restore is given the same meaning
that it had before the protect instruction began. See the
documentation for do-strict.
call the ACL2 theorem prover to prove the current goal
Major Section: PROOF-CHECKER-COMMANDS
Examples:
prove -- attempt to prove the current goal
(prove :otf-flg t
:hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar)))
-- attempt to prove the current goal, with the indicated hints
and with OTF-FLG set
General Form:
(prove &rest rest-args)
Attempt to prove the current goal, where rest-args is as in the
keyword arguments to defthm except that only :hints and :otf-flg are
allowed. The command succeeds exactly when the corresponding defthm
would succeed, except that it is all right for some goals to be
given ``bye''s. Each goal given a ``bye'' will be turned into a new
subgoal. (See hints for an explanation of :by hints.)
Note: Use (= t) instead if you are not at the top of the
conclusion. Also note that if there are any hypotheses in the
current goal, then what is actually attempted is a proof of
(implies hyps conc), where hyps is the conjunction of the
top-level hypotheses and conc is the goal's conclusion.
Note: It is allowed to use abbreviations in the hints.
substitute for a ``free variable''
Major Section: PROOF-CHECKER-COMMANDS
Example: (put x 17)SubstituteGeneral Form: (put var expr)
expr for the ``free variable'' var, as explained below.
A ``free variable'' is, for our purposes, a variable var such that
the instruction (free var) has been executed earlier in the
state-stack. What (free var) really does is to let var be an
abbreviation for the term (hide var) (see documentation for
add-abbreviation). What (put var expr) really does is to unwind the
state-stack, replacing that free instruction with the instruction
(add-abbreviation var expr), so that future references to (? var)
become reference to expr rather than to (hide var), and then to
replay all the other instructions that were unwound. Because hide
was used, the expectation is that in most cases, the instructions
will replay successfully and put will ``succeed''. However, if any
replayed instruction ``fails'', then the entire replay will abort
and ``fail'', and the state-stack will revert to its value before
the put instruction was executed.
If (put var expr) ``succeeds'', then (remove-abbreviation var) will
be executed at the end.
Note: The restore command will revert the state-stack to its value
present before the put instruction was executed.
run instructions without output
Major Section: PROOF-CHECKER-COMMANDS
Example: (quiet induct prove)Run theGeneral Form: (quiet &rest instruction-list)
instruction-list through the top-level loop with no output.
See also noise.
same as rewrite
Major Section: PROOF-CHECKER-COMMANDS
Example: (r 3)See the documentation forGeneral Form: (rewrite &optional rule-id substitution ;; below are rare arguments, used for disambiguation: target-lhs target-rhs target-hyps target-equiv)
rewrite, as r and rewrite are identical.
call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS
Examples:
reduce -- attempt to prove the current goal without using induction
(reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal by without using
induction, with the indicated hints
General Form:
(reduce &rest hints)
Attempt to prove the current goal without using induction, using the
indicated hints (if any). A subgoal will be created for each goal
that would have been pushed for proof by induction in an ordinary
proof.
Notice that unlike prove, the arguments to reduce are spread out,
and are all hints.
Note: Induction will be used to the extent that it is ordered
explicitly in the hints.
call the ACL2 prover without induction, after going into
induction
Major Section: PROOF-CHECKER-COMMANDS
Examples:
reduce-by-induction
-- attempt to prove the current goal after going into induction,
with no further inductions
(reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal after going into induction,
with no further inductions, using the indicated hints
General Form:
(reduce-by-induction &rest hints)
A subgoal will be created for each goal that would have been
pushed for proof by induction in an ordinary proof, except that the
proof begins with a top-level induction.
Notice that unlike prove, the arguments to reduce-by-induction are
spread out, and are all hints. See also prove, reduce, and bash.
Note: Induction and the various processes will be used to the
extent that they are ordered explicitly in the :induct and :do-not
hints.
remove one or more abbreviations
Major Section: PROOF-CHECKER-COMMANDS
Examples:
remove-abbreviations -- remove all abbreviations
(remove-abbreviations v w)
-- assuming that V and W currently abbreviate
terms, then they are ``removed'' in the
sense that they are no longer considered to
abbreviate those terms
General Forms:
(remove-abbreviations &rest vars)
If vars is not empty (i.e., not nil), remove the variables in vars
from the current list of abbreviations, in the sense that each
variable in vars will no longer abbreviate a term.Note: The instruction fails if at least one of the arguments fails to be a variable that abbreviates a term.
See also the documentation for add-abbreviation, which contains a
discussion of abbreviations in general, and show-abbreviations.
repeat the given instruction until it ``fails''
Major Section: PROOF-CHECKER-COMMANDS
Example: (repeat promote)The givenGeneral Form: (repeat instruction)
instruction is run repeatedly until it ``fails''.
Note: There is nothing here in general to prevent the instruction
from being run after all goals have been proved, though this is
indeed the case for primitive instructions.
auxiliary to repeat
Major Section: PROOF-CHECKER-COMMANDS
See documentation for repeat.
replay one or more instructions
Major Section: PROOF-CHECKER-COMMANDS
Examples:
REPLAY -- replay all instructions in the current session
(i.e., state-stack)
(REPLAY 5) -- replay the most recent 5 instructions
(REPLAY 5
(COMMENT deleted dive command here))
-- replace the 5th most recent instruction with the
indicated comment instruction, and then replay it
followed by the remaining 4 instructions
General Form:
(REPLAY &OPTIONAL n replacement-instruction)
Replay the last n instructions if n is a positive integer; else n
should be nil or not supplied, and replay all instructions.
However, if replacement-instruction is supplied and not nil, then
before the replay, replace the nth instruction (from the most
recent, as shown by commands) with replacement-instruction.
If this command ``fails'', then the restore command will revert the
state-stack to its value present before the replay instruction was
executed.
remove the effect of an UNDO command
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: restore
Restore removes the effect of an undo command. This always works as
expected if restore is invoked immediately after undo, without
intervening instructions. However, other commands may also interact
with restore, notably ``sequencing'' commands such as do-all,
do-strict, protect, and more generally, sequence.
Note: Another way to control the saving of proof-checker state is
with the save command; see the documentation for save.
The restore command always ``succeeds''; it returns
(mv nil t state).
drop all but the indicated top-level hypotheses
Major Section: PROOF-CHECKER-COMMANDS
Example:
(RETAIN 2 3) -- keep the second and third hypotheses, and drop
the rest
General Form:
(retain &rest args)
Drop all top-level hypotheses except those with the indicated
indices.
There must be at least one argument, and all must be in range (i.e.
integers between one and the number of top-level hypotheses,
inclusive).
re-enter the proof-checker
Major Section: PROOF-CHECKER-COMMANDS
Examples: (retrieve associativity-of-permutationp) retrieveMust be used fromGeneral Form: (retrieve &optional name)
outside the interactive proof-checker loop. If
name is supplied and not nil, this causes re-entry to the
interactive proof-checker loop in the state at which save was last
executed for the indicated name. (See documentation for save.) If
name is nil or is not supplied, then the user is queried regarding
which proof-checker state to re-enter. The query is omitted,
however, if there only one proof-checker state is present that was
saved with save, in which case that is the one that is used. See
also unsave.
apply a rewrite rule
Major Section: PROOF-CHECKER-COMMANDS
Examples:
(rewrite reverse-reverse)
-- apply the rewrite rule `reverse-reverse'
(rewrite (:rewrite reverse-reverse))
-- same as above
(rewrite 2)
-- apply the second rewrite rule, as displayed by show-rewrites
rewrite
-- apply the first rewrite rule, as displayed by show-rewrites
(rewrite transitivity-of-< ((y 7)))
-- apply the rewrite rule transitivity-of-< with the substitution
that associates 7 to the ``free variable'' y
General Form:
(rewrite &optional rule-id substitution)
Replace the current subterm with a new term by applying a rewrite
rule. If rule-id is a positive integer n, then the nth rewrite
rule as displayed by show-rewrites is the one that is applied. If
rule-id is nil or is not supplied, then it is treated as the number
1. Otherwise, rule-id should be either a rune of or name of a
rewrite rule. If a name is supplied, then any rule of that name may
be used. More explanation of all of these points follows below.
Consider first the following example. Suppose that the current
subterm is (reverse (reverse y)) and that there is a rewrite rule
called reverse-reverse of the form
(implies (true-listp x)
(equal (reverse (reverse x)) x)) .
Then the instruction (rewrite reverse-reverse) would cause the
current subterm to be replaced by y and would create a new goal with
conclusion (true-listp y). An exception is that if the top-level
hypotheses imply (true-listp y) using only ``trivial reasoning''
(more on this below), then no new goal is created.
A rather important point is that if the rule-id argument is a number
or is not supplied, then the system will store an instruction of the
form (rewrite name ...), where name is the name of a rewrite rule;
this is in order to make it easier to replay instructions when there
have been changes to the history. Actually, instead of the name
(whether the name is supplied or calculated), the system stores the
rune if there is any chance of ambiguity. (Formally, ``ambiguity''
here means that the rune being applied is of the form
(:rewrite name . index), where index is not nil.)
Speaking in general, then, a rewrite instruction works as follows:
First, a rewrite rule is selected according to the arguments of the
rewrite instruction. The selection is made as explained above under
``General Form'' above. The ``disambiguating rare arguments'' will
rarely be of interest to the user; as explained just above, the
stored instruction always contains the name of the rewrite rule, so
if there is more than one rule of that name then the system creates
and stores these extra arguments in order to make the resulting
instruction unambiguous, i.e., so that only one rewrite rule
applies. For what it's worth, they correspond respectively to the
fields of a rewrite rule record named lhs, rhs, hyps, and equiv.
Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution unify-subst is found such that if one
instantiates the left-hand side of the rule with unify-subst, then
one obtains the current subterm. If this matching fails, then the
instruction fails.
Now an attempt is made to relieve the hypotheses, in much the same
sense as the theorem prover relieves hypotheses except that there is
no call to the rewriter. Essentially, this means that the
substitution unify-subst is applied to the hypotheses and the system
then checks whether all hypotheses are ``clearly'' true in the
current context. If there are variables in the hypotheses of the
rewrite rule that do not occur in the left-hand side of the
conclusion even after the user-supplied substitution (default: nil)
is applied, then a weak attempt is made to extend that substitution
so that even those hypotheses can be relieved. However, if even one
hypothesis remains unrelieved, then no automatic extension of the
substitution is made, and in fact hypotheses that contain even one
uninstantiated variable will remain unrelieved.
Finally, the instruction is applied as follows. The current subterm
is replaced by applying the final substitution, i.e., the extension
of unify-subst by the user-supplied substitution which may in turn
be extended by the system (as explained above) in order to relieve
all hypotheses, to the right-hand side of the selected rewrite rule.
And, one new subgoal is created for each unrelieved hypothesis of
the rule, whose top-level hypotheses are the governors and top-level
hypotheses of the current goal and whose conclusion and current
subterm are the instance, by that same final substitution, of that
unrelieved hypothesis.
Note: The substitution argument should be a list whose elements
have the form (variable term), where term may contain
abbreviations.
auxiliary toxae THEN
Major Section: PROOF-CHECKER-COMMANDS
See documentation for then.
auxiliary to then
Major Section: PROOF-CHECKER-COMMANDS
See documentation for then.
simplify the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples:
S -- simplify the current subterm
(S :backchain-limit 2 :normalize t :expand (append x z))
-- simplify the current subterm, but during the rewriting
process first ``normalize'' it by pushing IFs to the
top-level, and also force the term (append x z) to be
expanded during the rewriting process
General Form:
(s &key rewrite normalize backchain-limit repeat in-theory hands-off
expand)
Simplify the current subterm according to the keyword parameters
supplied. First if-normalization is applied (unless the normalize
argument is nil), i.e., each subterm of the form
(f ... (if test x y) ...) is replaced by the term
(if test (f ... x ...) (f ... y ...)) except, of course, when
f is if and the indicated if subterm is in the second or
third argument position. Then rewriting is applied (unless the
rewrite argument is nil). Finally this pair of actions is
repeated -- until the rewriting step causes no change in the term.
A description of each parameter follows.
:rewrite -- default tWhen non-
nil, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.
:normalize -- default tWhen non-
nil, instructs the system to use if-normalization (as
described above) during simplification.
:backchain-limit -- default 0Sets the number of recursive calls to the rewriter that are allowed for backchaining. Even with the default of 0, some reasoning is allowed (technically speaking, type-set reasoning is allowed) in the relieving of hypotheses.
:repeat -- default 0Sets the number of times the current term is to be rewritten. If this value is
t, then the default is used (as specified by the
constant *default-s-repeat-limit*).
:in-theory, :hands-off, :expandThese have their usual meaning; see hints.
Note: if conditional rewrite rules are used that cause case splits
because of the use of force, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal. In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.
simplify propositionally
Major Section: PROOF-CHECKER-COMMANDS
Example: s-propSimplify, using the default settings forGeneral Form: (s-prop &rest names)
s (which include
if-normalization and rewriting without real backchaining), but with
respect to a theory in which only basic functions and rules (the
ones in *s-prop-theory*), together with the names (or parenthesized
names) in the &rest argument names, are enabled.
See also the documentation for s.
save the proof-checker state (state-stack)
Major Section: PROOF-CHECKER-COMMANDS
Example: (save lemma3-attemptSaves the current proof-checker state by ``associating'' it with the given name. SubmitGeneral Form: (save &optional name do-it-flg)
(retrieve name) to Lisp to get back to this
proof-checker state. If verify was originally supplied with an
event name, then the argument can be omitted in favor of that name
as the default.
Note that if a save has already been done with the indicated name
(or the default event name), then the user will be queried regarding
whether to go ahead with the save -- except, if do-it-flg is
supplied and not nil, then there will be no query and the save will
be effected.
See also the documentation for retrieve and unsave.
run the given list of instructions according to a multitude of
options
Major Section: PROOF-CHECKER-COMMANDS
Example: (sequence (induct p prove) t)See also the definitions of commands
do-all, do-strict, protect, and
succeed.
General Form:
(sequence instruction-list
&optional
strict-flg protect-flg success-expr no-prompt-flg)
Each instruction in the list instruction-list is run, and the
instruction ``succeeds'' if every instruction in instruction-list
``succeeds''. However, it might ``succeed'' even if some
instructions in the list ``fail''; more generally, the various
arguments control a number of aspects of the running of the
instructions. All this is explained in the paragraphs below. First
we embark on a general discussion of the instruction interpreter,
including the notions of ``succeed'' and ``fail''.
Note: The arguments are not evaluated, except (in a sense) for
success-expr, as described below.
Each primitive and meta instruction can be thought of as returning
an error triple (in the standard ACL2 sense), say (erp val state).
An instruction (primitive or meta) ``succeeds'' if erp is nil and
val is not nil; otherwise it ``fails''. (When we use the words
``succeed'' or ``fail'' in this technical sense, we'll always
include them in double quotes.) If an instruction ``fails,'' we say
that that the failure is ``soft'' if erp is nil; otherwise the
failure is ``hard''. The sequence command gives the user control
over how to treat ``success'' and ``failure'' when sequencing
instructions, though we have created a number of handy macro
commands for this purpose, notably do-all, do-strict and protect.
Here is precisely what happens when a sequence instruction is run.
The instruction interpreter is run on the instructions supplied in
the argument instruction-list (in order). The interpreter halts the
first time there is a hard ``failure.'' except that if strict-flg is
supplied and not nil, then the interpreter halts the first time
there is any ``failure.'' The error triple (erp val state) returned
by the sequence instruction is the triple returned by the last
instruction executed (or, the triple (nil t state) if
instruction-list is nil), except for the following provision. If
success-expr is supplied and not nil, then it is evaluated with the
state global variables erp and val (in ACL2 package) bound to the
corresponding components of the error triple returned (as described
above). At least two values should be returned, and the first two
of these will be substituted for erp and val in the triple finally
returned by sequence. For example, if success-expr is (mv erp val),
then no change will be made to the error triple, and if instead it
is (mv nil t), then the sequence instruction will ``succeed''.
That concludes the description of the error triple returned by a
sequence instruction, but it remains to explain the effects of the
arguments protect-flg and no-prompt-flg.
If protect-flg is supplied and not nil and if also the instruction
``fails'' (i.e., the error component of the triple is not nil or the
value component is nil), then the state is reverted so that the
proof-checker's state (including the behavior of restore) is set
back to what it was before the sequence instruction was executed.
Otherwise, unless no-restore-flg is set, the state is changed so
that the restore command will now undo the effect of this sequence
instruction (even if there were nested calls to sequence).
Finally, as each instruction in instruction-list is executed, the
prompt and that instruction will be printed, unless the global state
variable print-prompt-and-instr-flg is unbound or nil and the
parameter no-prompt-flg is supplied and not nil.
display the current abbreviations
Major Section: PROOF-CHECKER-COMMANDS
Examples:
(show-abbreviations v w)
-- assuming that v and w currently abbreviate terms,
then this instruction displays them together with
the terms they abbreviate
show-abbreviations
-- display all abbreviations
See also add-abbreviation and remove-abbreviations. In
particular, the documentation for add-abbreviation contains a
general discussion of abbreviations.
General Form: (show-abbreviations &rest vars)Display each argument in
vars together with the term it abbreviates
(if any). If there are no arguments, i.e. the instruction is simply
show-abbreviations, then display all abbreviations together with the
terms they abbreviate.
If the term abbreviated by a variable, say v, contains a proper
subterm that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using (? v) to
abbreviate the term) are displayed with together with v.
display the applicable rewrite rules
Major Section: PROOF-CHECKER-COMMANDS
Example: show-rewritesDisplay rewrite rules whose left-hand side matches the current subterm. This command is useful in conjunction withGeneral Form: (show-rewrites &optional rule-id enabled-only-flg)
rewrite. If
rule-id is supplied and is a name (non-nil symbol) or a rune, then
only the corresponding rewrite rule(s) will be displayed, while if
rule-id is a positive integer n, then only the nth rule that would
be in the list is displayed. In each case, the display will point
out when a rule is currently disabled (in the interactive
environment), except that if enabled-only-flg is supplied and not
nil, then disabled rules will not be displayed at all. Finally, the
free variables of any rule (those occurring in the rule that do not
occur in the left-hand side of its conclusion) will be displayed.
See also the documentation for rewrite.
``succeed'' without doing anything
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: skip
Make no change in the state-stack, but ``succeed''. Same as
(sequence nil).
simplify with lemmas
Major Section: PROOF-CHECKER-COMMANDS
Examples: sl (sl 3)Simplify, but with all function definitions disabled (see function-theory in the top-level ACL2 loop), except for a few basic functions (the ones inGeneral Form: (sl &optional backchain-limit)
*s-prop-theory*). If
backchain-limit is supplied and not nil, then it should be a
nonnegative integer; see (help s).
split the current goal into cases
Major Section: PROOF-CHECKER-COMMANDS
Example: splitFor example, if the current goal has one hypothesis
(or x y) and a
conclusion of (and a b), then split will create four new goals:
one with hypothesis X and conclusion A one with hypothesis X and conclusion B one with hypothesis Y and conclusion A one with hypothesis Y and conclusion B.Replace the current goal by subgoals whose conjunction is equivalent (primarily by propositional reasoning) to the original goal, where each such goal cannot be similarly split.General Form: SPLIT
Note: The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of
implies. Also note that split will fail if there is exactly one new
goal created and it is the same as the existing current goal.
The way split really works is to call the ACL2 theorem prover with
only simplification (and preprocessing) turned on, and with only a
few built-in functions (especially, propositional ones) enabled,
namely, the ones in the list *s-prop-theory*. However, because the
prover is called, type-set reasoning can be used to eliminate some
cases. For example, if (true-listp x) is in the hypotheses, then
probably (true-listp (cdr x)) will be reduced to t.
same as SHOW-REWRITES
Major Section: PROOF-CHECKER-COMMANDS
Example: srSee the documentation forGeneral Form: (sr &optional rule-id)
show-rewrites, as sr and show-rewrites
are identical.
run the given instructions, and ``succeed''
Major Section: PROOF-CHECKER-COMMANDS
Example: (succeed induct p prove)Run the indicated instructions until there is a hard ``failure'', and ``succeed''. (See the documentation forGeneral Form: (succeed &rest instruction-list)
sequence for an
explanation of ``success'' and ``failure''.)
print the top-level hypotheses and the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples:
th -- print all (top-level) hypotheses and the current
subterm
(th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
and the current subterm
(th (1 3) t) -- print hypotheses 1 and 3 and all governors, and
the current subterm
General Form:
(th &optional hyps-indices govs-indices)
Print hypotheses and the current subterm. The printing of
hypotheses (and perhaps governors) are controlled as in the hyps
command; see its documentation.
Historical note: The name th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which
says to print information on the current goal.
apply one instruction to current goal and another to new subgoals
Major Section: PROOF-CHECKER-COMMANDS
Example: (then induct prove)RunGeneral Form: (then first-instruction &optional completion must-succeed-flg)
first-instruction, and then run completion (another
instruction) on each subgoal created by first-instruction. If
must-succeed-flg is supplied and not nil, then immediately remove
the effects of each invocation of completion that ``fails''.
move to the top of the goal
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: topFor example, if the conclusion is
(= x (* (- y) z)) and the
current subterm is y, then after executing top, the current subterm
will be the same as the conclusion, i.e., (= x (* (- y) z)).
Top is the same as (up n), where n is the number of times one needs
to execute up in order to get to the top of the conclusion. The top
command fails if one is already at the top of the conclusion.
See also up, dive, nx, and bk.
display the type-alist from the current context
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: type-alist
Display the current assumptions as a type-alist. Note that this
display includes the result of forward chaining.
undo some instructions
Major Section: PROOF-CHECKER-COMMANDS
Examples: (undo 7) undoNote: To remove the effect of anGeneral Forms:
(undo n) -- Undo the last n instructions. The argument n should be a positive integer.
undo -- Same as (undo 1).
undo command, use restore. See
the documentation for details.
Note: If the argument n is greater than the total number of
interactive instructions in the current session, then (undo n) will
simply take you back to the start of the session.
The undo meta command always ``succeeds''; it returns
(mv nil t state) unless its optional argument is supplied and of
the wrong type (i.e. not a positive integer) or there are no
instructions to undo.
remove a proof-checker state
Major Section: PROOF-CHECKER-COMMANDS
Example: (unsave assoc-of-append)Eliminates the association of a proof-checker state withGeneral Form: (unsave &optional name)
name, if
name is supplied and not nil. The name may be nil or not supplied,
in which case it defaults to the event name supplied with the
original call to verify (if there is one -- otherwise, the
instruction ``fails'' and there is no change). The ACL2 function
unsave may also be executed outside the interactive loop, with the
same syntax.
See also documentation for save and retrieve.
move to the parent (or some ancestor) of the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples: if the conclusion is (= x (* (- y) z)) and the
current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2) -- the current subterm becomes (* (- y) z)
(up 3) -- the current subterm becomes the entire conclusion
(up 4) -- no change; can't go up that many levels
General Form:
(up &optional n)
Move up n levels in the conclusion from the current subterm, where n
is a positive integer. If n is not supplied or is nil, then move up
1 level, i.e., treat the instruction as (up 1).
See also dive, top, nx, and bk.
use a lemma instance
Major Section: PROOF-CHECKER-COMMANDS
Example:
(USE true-listp-append
(:instance assoc-of-append (x a) (y b) (z c)))
-- Add two top-level hypotheses, one the lemma called
true-listp-append, and the other an instance of the lemma called
assoc-of-append by the substitution in which x is assigned a, y
is assigned b, and z is assigned c.
General Form:
(use &rest args)
Add the given lemma instances to the list of top-level hypotheses.
See hints for the syntax of :use hints in defthm, which is
essentially the same as the syntax here (see the example above).
This command calls the prove command, and hence should only be used
at the top of the conclusion.
expand and (maybe) simplify function call at the current subterm
Major Section: PROOF-CHECKER-COMMANDS
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.
expand function call at the current subterm, without simplifying
Major Section: PROOF-CHECKER-COMMANDS
Example: x-dumb: expand without simplification.Same asGeneral Form: (x-dumb &optional new-goals-flg keep-all-guards-flg)
(expand t new-goals-flg keep-all-guards-flg). See
documentation for expand.
See also x, which allows simplification.