Proof-builder-commands
List of commands for the interactive proof-builder
This documentation section contains documentation for individual
commands that can be given inside the interactive proof-builder loop
that is entered using verify. For a summary of (arguably) the most
useful commands, see proof-builder-commands-short-list.
Subtopics
- ACL2-pc::rewrite
- (primitive)
apply a rewrite rule
- ACL2-pc::apply-linear
- (primitive)
apply a linear rule
- ACL2-pc::sequence
- (meta)
run the given list of instructions according to a multitude of
options
- Proof-builder-commands-short-list
- Perhaps the most commonly used proof-builder commands
- ACL2-pc::=
- (atomic macro)
attempt an equality (or equivalence) substitution
- ACL2-pc::s
- (primitive)
simplify the current subterm
- ACL2-pc::exit
- (meta) exit the interactive proof-builder
- ACL2-pc::type-alist
- (macro)
display the type-alist from the current context
- ACL2-pc::in-theory
- (primitive)
set the current proof-builder theory
- ACL2-pc::equiv
- (primitive)
attempt an equality (or congruence-based) substitution
- ACL2-pc::comm
- (macro)
display instructions from the current interactive session
- ACL2-pc::casesplit
- (primitive)
split into two cases
- ACL2-pc::add-abbreviation
- (primitive)
add an abbreviation
- ACL2-pc::dv
- (atomic macro)
move to the indicated subterm
- ACL2-pc::hyps
- (macro)
print the hypotheses
- ACL2-pc::prove-termination
- (macro)
Prove termination efficiently by using a previous termination theorem.
- ACL2-pc::prove-guard
- (macro)
Verify guards efficiently by using a previous guard theorem.
- ACL2-pc::x
- (atomic macro)
expand and (maybe) simplify function call at the current subterm
- ACL2-pc::pot-lst
- (macro)
display the linear arithmetic database based on the current context
- ACL2-pc::fancy-use
- (macro)
Use one or more previously-proved theorems efficiently.
- ACL2-pc::dive
- (primitive)
move to the indicated subterm
- ACL2-pc::generalize
- (primitive)
perform a generalization
- ACL2-pc::lisp
- (meta)
evaluate the given form in Lisp
- ACL2-pc::show-rewrites
- (macro)
display the applicable rewrite rules
- ACL2-pc::claim
- (atomic macro)
add a new hypothesis
- ACL2-pc::put
- (macro)
substitute for a ``free variable''
- ACL2-pc::split
- (atomic macro)
split the current goal into cases
- ACL2-pc::geneqv
- (macro)
show the generated equivalence relation maintained at the current subterm
- ACL2-pc::prove
- (primitive)
call the ACL2 theorem prover to prove the current goal
- ACL2-pc::help
- (macro)
proof-builder help facility
- ACL2-pc::save
- (macro)
save the proof-builder state (state-stack)
- ACL2-pc::do-all
- (macro)
run the given instructions
- ACL2-pc::demote
- (primitive)
move top-level hypotheses to the conclusion
- ACL2-pc::wrap1
- (primitive)
combine goals into a single goal
- ACL2-pc::show-abbreviations
- (macro)
display the current abbreviations
- ACL2-pc::promote
- (primitive) move antecedents of conclusion's implies term to
top-level hypotheses
- ACL2-pc::retrieve
- (macro)
re-enter the proof-builder
- ACL2-pc::reduce
- (atomic macro)
call the ACL2 theorem prover's simplifier
- ACL2-pc::forwardchain
- (atomic macro)
forward chain from an implication in the hyps
- ACL2-pc::doc
- (macro) access documentation inside the interactive proof-builder
- ACL2-pc::bash
- (atomic macro)
call the ACL2 theorem prover's simplifier
- ACL2-pc::p-top
- (macro)
prettyprint the conclusion, highlighting the current term
- ACL2-pc::print
- (macro)
print the result of evaluating the given form
- ACL2-pc::expand
- (primitive)
expand the current function call without simplification
- ACL2-pc::bk
- (atomic macro)
move backward one argument in the enclosing term
- ACL2-pc::wrap
- (atomic macro)
execute the indicated instructions and combine all the new goals
- ACL2-pc::remove-abbreviations
- (primitive)
remove one or more abbreviations
- ACL2-pc::reduce-by-induction
- (macro)
call the ACL2 prover without induction, after going into
induction
- ACL2-pc::induct
- (atomic macro)
generate subgoals using induction
- ACL2-pc::unsave
- (macro)
remove a proof-builder state
- ACL2-pc::undo
- (meta)
undo some instructions
- ACL2-pc::top
- (atomic macro)
move to the top of the goal
- ACL2-pc::restore
- (meta)
remove the effect of an UNDO command
- ACL2-pc::replay
- (macro)
replay one or more instructions
- ACL2-pc::psog
- (macro)
print the most recent proof attempt from inside the proof-builder
- ACL2-pc::p
- (macro)
prettyprint the current term in the usual user-level (untranslated) syntax
- ACL2-pc::nx
- (atomic macro)
move forward one argument in the enclosing term
- ACL2-pc::noise
- (meta)
run instructions with prover output
- ACL2-pc::contrapose
- (primitive)
switch a hypothesis with the conclusion, negating both
- ACL2-pc::wrap-induct
- (atomic macro)
same as induct, but create a single goal
- ACL2-pc::pso!
- (macro)
print the most recent proof attempt from inside the proof-builder
- ACL2-pc::pso
- (macro)
print the most recent proof attempt from inside the proof-builder
- ACL2-pc::up
- (primitive)
move to the parent (or some ancestor) of the current subterm
- ACL2-pc::then
- (macro)
apply one instruction to current goal and another to new subgoals
- ACL2-pc::th
- (macro)
print the top-level hypotheses and the current subterm
- ACL2-pc::sl
- (atomic macro)
simplify with lemmas
- ACL2-pc::show-type-prescriptions
- (macro)
display the applicable type-prescription rules
- ACL2-pc::bdd
- (atomic macro)
prove the current goal using bdds
- ACL2-pc::repeat
- (macro)
repeat the given instruction until it ``fails''
- ACL2-pc::pr
- (macro)
print the rules for a given name
- ACL2-pc::pl
- (macro)
print the rules for a given name
- ACL2-pc::finish
- (macro) require completion of instructions; save error if inside
:hints
- ACL2-pc::commands
- (macro)
display instructions from the current interactive session
- ACL2-pc::change-goal
- (primitive)
change to another goal.
- ACL2-pc::use
- (atomic macro)
use a lemma instance
- ACL2-pc::show-linears
- (macro)
display the applicable linear rules
- ACL2-pc::s-prop
- (atomic macro)
simplify propositionally
- ACL2-pc::runes
- (macro)
print the runes (definitions, lemmas, ...) used
- ACL2-pc::protect
- (macro)
run the given instructions, reverting to existing state upon
failure
- ACL2-pc::instantiate
- Instantiate a theorem
- ACL2-pc::insist-all-proved
- (macro)
Run the given instructions, then fail if there remain unproved goals
- ACL2-pc::fail
- (macro)
cause a failure
- ACL2-pc::clause-processor
- (atomic macro)
use a clause-processor
- ACL2-pc::bookmark
- (macro)
insert matching ``bookends'' comments
- ACL2-pc::retain
- (atomic macro)
drop all but the indicated top-level hypotheses
- ACL2-pc::quiet!
- (meta)
run instructions without prover output
- ACL2-pc::pro
- (atomic macro)
repeatedly apply promote
- ACL2-pc::orelse
- (macro)
run the first instruction; if (and only if) it ``fails'', run the
second
- ACL2-pc::goals
- (macro)
list the names of goals on the stack
- ACL2-pc::drop
- (primitive)
drop top-level hypotheses
- ACL2-pc::do-strict
- (macro)
run the given instructions, halting once there is a ``failure''
- ACL2-pc::print-all-concs
- (macro)
print all the conclusions of (as yet unproved) goals
- ACL2-pc::do-all-no-prompt
- (macro)
run the given instructions, halting once there is a ``failure''
- ACL2-pc::x-dumb
- (atomic macro)
expand function call at the current subterm, without simplifying
- ACL2-pc::succeed
- (macro)
run the given instructions, and ``succeed''
- ACL2-pc::print-all-goals
- (macro)
print all the (as yet unproved) goals
- ACL2-pc::pp
- (macro)
prettyprint the current term in internal (translated) form
- ACL2-pc::noise!
- (meta)
run instructions with prover and proof-tree output
- ACL2-pc::nil
- (macro) used for interpreting control-d
- ACL2-pc::negate
- (macro)
run the given instructions, and ``succeed'' if and only if they ``fail''
- ACL2-pc::illegal
- (macro)
illegal instruction
- ACL2-pc::elim
- (atomic macro)
call the ACL2 theorem prover's elimination process
- ACL2-pc::sls
- (macro)
same as SHOW-LINEARS
- ACL2-pc::quiet
- (meta)
run instructions without prover output
- ACL2-pc::claim-simple
- (atomic macro) add a new hypothesis, without promotion
- ACL2-pc::cg
- (macro)
change to another goal.
- ACL2-pc::pro-or-skip
- (atomic macro) repeatedly apply promote, if possible
- ACL2-pc::ex
- (macro)
exit after possibly saving the state
- ACL2-pc::comment
- (primitive)
insert a comment
- ACL2-pc::ACL2-wrap
- (macro) same as (lisp x)
- ACL2-pc::when-not-proved
- (macro)
Run the given instructions unless all goals have been proved
- ACL2-pc::skip
- (macro)
``succeed'' without doing anything
- ACL2-pc::retain-or-skip
- (atomic macro) drop all but the indicated top-level hypotheses
- ACL2-pc::repeat-until-done
- A proof-builder command that repeats the given instructions
until all goals have been proved
- ACL2-pc::free
- (atomic macro)
create a ``free variable''
- ACL2-pc::drop-or-skip
- (atomic macro) drop top-level hypotheses
- ACL2-pc::cg-or-skip
- (atomic macro) change goals when needed
- ACL2-pc::by
- (atomic macro) prove using an existing theorem
- ACL2-pc::split-in-theory
- Split using an optional theory
- ACL2-pc::st
- (macro)
same as SHOW-TYPE-PRESCRIPTIONS
- ACL2-pc::sr
- (macro)
same as SHOW-REWRITES
- ACL2-pc::print-main
- (macro)
print the original goal
- ACL2-pc::lemmas-used
- (macro)
print the runes (definitions, lemmas, ...) used
- ACL2-pc::cl-proc
- (macro) same as clause-processor
- ACL2-pc::al
- (macro)
same as apply-linear
- ACL2-pc::run-instr-on-new-goals
- (macro) auxiliary to then
- ACL2-pc::run-instr-on-goal
- (macro)
auxiliary to THEN
- ACL2-pc::repeat-rec
- (macro) auxiliary to repeat
- ACL2-pc::r
- (macro)
same as rewrite
- ACL2-pc::contradict
- (macro) same as contrapose
