Major Section: ACL2 Documentation
A view of ACL2 proofs may be obtained by way of ``proof tree
displays.'' The emacs environment is easily customized to provide
window-based proof tree displays that assist in traversing and
making sense of the proof transcript; see proof-tree-emacs.
Proof tree displays may be turned on with the command :
start-proof-tree
and may be turned off with the command :
stop-proof-tree
;
see start-proof-tree and see stop-proof-tree.
( DEFTHM PLUS-TREE-DEL ...) ;currently proving PLUS-TREE-DEL 1 Goal preprocess ;"Goal" creates 1 subgoal by preprocessing 2 | Goal' simp ;"Goal'" creates 2 subgoals by simplification c 0 | | Subgoal 2 PUSH *1 ;"Subgoal 2" pushes "*1" for INDUCT ++++++++++++++++++++++++++++++ ;first pass thru waterfall completed c 6 *1 INDUCT ;Proof by induction of "*1" has | <5 more subgoals> ; created 6 top-level subgoals. At ; this point, one of those 6 has been ; proved, and 5 remain to be proved. ; We are currently working on the ; first of those 5 remaining goals.See proof-tree-examples for many examples that contain proof tree displays. But first, we summarize the kinds of lines that may appear in a proof tree display. The simplest form of a proof tree display is a header showing the current event, followed by list of lines, each having one of the following forms.
n <goal> <process> ...Says that the indicated goal created
n
subgoals using the
indicated process. Here ``...'' refers to possible additional
information.
c n <goal> <process> ...As above, but calls attention to the fact that this goal is a ``checkpoint'' in the sense that it may be of particular interest. Some displays may overwrite ``c'' with ``>'' to indicate the current checkpoint being shown in the proof transcript.
| <goal> ... | | <k subgoals>Indicates that the goal just above this line, which is pointed to by the rightmost vertical bar (``|''), has
k
subgoals, none of which
have yet been processed.
| <goal> ... | | <k more subgoals>As above, except that some subgoals have already been processed.
++++++++++++++++++++++++++++++Separates successive passes through the ``waterfall''. Thus, this ``fencepost'' mark indicates the start of a new proof by induction or of a new forcing round.
See proof-tree-examples for detailed examples. To learn how to
turn off proof tree displays or to turn them back on again,
see stop-proof-tree and see start-proof-tree,
respectively. See checkpoint-forced-goals to learn how to mark
goals as checkpoints that force the creation of goals in forcing
rounds. Finally, see proof-tree-details for some points not
covered elsewhere.