|
|
|---|
|
|
|
|---|
Proof tree displays
A view of ACL2 proofs may be obtained by way of ``proof tree displays,'' which appear in proof output (see proofs-co) when proof-tree output is enabled (see below) When ACL2 starts a proof and proof-tree output is enabled, the proof output begins with the following string.
<< Starting proof tree logging >>
Then for each goal encountered during the proof, a corresponding proof tree
display (as described below) is printed into the proof output: first the
characters in the constant string
External tools may present proof tree displays in a separate window. In
particular, a tool distributed with the ACL2 community books customizes the
emacs environment to provide window-based proof tree displays together with
commands for traversing the proof transcript; see the discussion of ``ACL2
proof-tree support'' in file
The command
Here is an example of a proof tree display, with comments. Lines marked with ``c'' are considered ``checkpoints,'' i.e., goals whose scrutiny may be of particular value.
( 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
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
| <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. 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.