Proof-builder
An interactive tool for controlling ACL2's proof processes.
Call this up with (verify ...).
The interactive proof-builder provides a way to explore the
development of ACL2 proofs below the level of the ACL2 prover (as typically
used by thm and events such as defthm). To use this
tool, invoke the verify command, for example as follows.
ACL2 !>(verify (equal (append (append x y) z)
(append x (append y z))))
->:
Then at the "->:" prompt, one submits commands that operate on a
stack of goals, starting with the single goal that was supplied to VERIFY
as shown above. The final command (or ``instruction'') can be an exit
command, which can print out a defthm event if the goal stack is
empty; see proof-builder-commands, in particular the exit command.
That resulting defthm event includes an :instructions
parameter, which directs replay of the interactive proof-builder commands (for
example during certification of a book containing that event; see books).
If you exit the interactive proof-builder's loop, you may re-enter that
session at the same point using the command (verify), i.e., with no
arguments. The commands save and retrieve may be invoked to manage
more than one session.
The interactive proof-builder can be invoked on a specific subgoal, and the
resulting :instructions can be given as a hint to the theorem prover for
that subgoal. See instructions.
A tutorial is available here.
That tutorial illustrates more than just the interactive proof-builder. The
portion relevant to the proof-builder may be accessed directly here.
See set-evisc-tuple for how to arrange that output is printed in
abbreviated form. In general, the interactive proof-builder uses the
:TERM evisc-tuple described in that documentation.
Individual proof-builder commands are documented in subsection proof-builder-commands. Note that the package name (see symbol-package-name is irrelevant for these commands (though not their
arguments); for example (dive 3), (acl2::dive 3), (acl2-pc::dive
3), and (:dive 3) are all equivalent. For a list of perhaps the most
commonly used commands, see proof-builder-commands-short-list.
The proof-builder supports user-defined macros, which are tactics that
generate proof-builder instructions. See define-pc-macro.
Remark. The ``pc-'' prefix, for example in ``define-pc-macro''
above, stems from an earlier name for the proof-builder, which was
``proof-checker''. That also accounts for the string "PC" in the
package name, "ACL2-PC".
Subtopics
- Instructions
- Instructions to the interactive proof-builder
- Proof-builder-commands
- List of commands for the interactive proof-builder
- Proof-builder-commands-short-list
- Perhaps the most commonly used proof-builder commands
- Dive-into-macros-table
- Right-associated function information for the proof-builder
- Verify
- Enter the interactive proof-builder
- Define-pc-macro
- Define a proof-builder macro command
- Macro-command
- Compound command for the interactive proof-builder
- Define-pc-help
- Define a macro command whose purpose is to print something
- Toggle-pc-macro
- Change an ordinary macro command to an atomic macro, or vice-versa
- Define-pc-meta
- Define a proof-builder meta command
- Retrieve
- Re-enter a (specified) proof-builder state
- Unsave
- Remove a proof-builder state
- Proof-checker
- Old name for proof-builder
