proof tree displays
Parent topic: Home
A view of ACL2 proofs may be obtained by way of ``proof tree
displays.'' Environments such as emacs may be customized to provide
window-based versions of proof tree displays. (See for example
documentation of the emacs function start-proof-tree,
co-written with Michael K. Smith, that the implementors are happy to
make available.) Proof tree displays may be turned on with the
command :start-proof-tree and may be turned off with the
command :start-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.
Cause forcing goals to be checkpointed in proof trees
Parent topic: PROOF-TREE Home
Example forms: (checkpoint-forced-goals t) (checkpoint-forced-goals nil)Also see proof-tree.
By default, goals are not marked as checkpoints by a proof tree
display (as described in the documentation for proof-tree)
merely because they force some hypotheses, thus possibly
contributing to a forcing round. However, some users may want such
behavior, which will occur once the command (checkpoint-forced-goals)
t) has been executed. To return to the default behavior, use the
command (checkpoint-forced-goals nil).
proof tree details not covered elsewhere
Parent topic: PROOF-TREE Home
See proof-tree for an introduction to proof trees, and for a list of related topics. Here we present some details not covered elsewhere.
1. When proof tree display is enabled (because the command
:stop-proof-tree has not been executed, or has been superseded by a
later :start-proof-tree command), then time summaries will include
the time for proof tree display. This time includes the time spent
computing with proof trees, such as the pruning process described
briefly above. Even when proof trees are not displayed, such as
when their display is turned off in the middle of a proof, this time
will be printed if it is not 0.
2. When a goal is given a :bye in a proof (see hints), it is
treated for the purpose of proof tree display just as though it had
been proved.
3. Several state global variables affect proof tree display.
(@ proof-tree-indent) is initially the string "| ": it is
the string that is laid down the appropriate number of times to
effect indentation. (@ proof-tree-buffer-width) is initially the
value of (fmt-soft-right-margin state), and is used to prevent
printing of the annotation ``(forced ...)'' in any greater column
than this value. However, (assign proof-tree-buffer-width nil)
to avoid any such suppression. Finally,
(@ checkpoint-processors) is a list of processors from the
constant list *preprocess-clause-ledge*, together with
:induct. You may remove elements of (@ checkpoint-processors)
to limit which processes are considered checkpoints.
4. When :otf-flg is not set to t in a proof, and the prover then
decides to revert to the original goal and prove it by induction,
the proof tree display will reflect this fact as shown here:
c 0 | | Subgoal 2 PUSH (reverting)5.
Proof-tree display is turned off during calls of
certify-book.6. The usual failure message is printed as part of the prooftree display when a proof has failed.
proof tree example
Parent topic: PROOF-TREE Home
See proof-tree for an introduction to proof trees, and for a list of related topics. Here we present a detailed example followed by a shorter example that illustrates proof by induction.
Consider the guard proof for the definition of a function
cancel_equal_plus; the body of this definition is of no importance
here. The first proof tree display is:
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <18 subgoals>
This is to be read as follows.
At this stage of the proof we have encountered the top-level goal, named "Goal", which generated 18 subgoals using the ``preprocess'' process. We have not yet begun to work on those subgoals.The corresponding message from the ordinary prover output is:
By case analysis we reduce the conjecture to the following 18 conjectures.Note that the field just before the name of the goal (
"Goal"),
which here contains the number 18, indicates the number of cases
(children) created by the goal using the indicated process. This
number will remain unchanged as long as this goal is displayed.The next proof tree display is:
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
| | <1 subgoal>
| <17 more subgoals>
which indicates that at this point, the prover has used the
simplification (``simp'') process on Subgoal 18 to create one
subgoal (``<1 subgoal>''). The vertical bar (``|'') below ``Subgoal
18'', accompanied by the line below it, signifies that there are 17
siblings of Subgoal 18 that remain to be processed.The next proof tree displayed is:
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
c 2 | | Subgoal 18' ELIM
| | | <2 subgoals>
| <17 more subgoals>
Let us focus on the fourth line of this display:
c 2 | | Subgoal 18' ELIMThe ``c'' field marks this goal as a ``checkpoint'', i.e., a goal worthy of careful scrutiny. In fact, any goal that creates children by a process other than ``preprocess'' or ``simp'' is marked as a checkpoint. In this case, the destructor-elimination (``ELIM'') process has been used to create subgoals of this goal. The indentation shows that this goal, Subgoal 18', is a child of Subgoal 18. The number ``2'' indicates that 2 subgoals have been created (by ELIM). Note that this information is consistent with the line just below it, which says ``<2 subgoals>''.
Finally, the last line of this proof tree display,
| <17 more subgoals>
is connected by vertical bars (``|'') up to the string
"Subgoal 18", which suggests that there are 17 immediate
subgoals of Goal remaining to process after Subgoal 18. Note that
this line is indented one level from the second line, which is the
line for the goal named "Goal". The display is intended to
suggest that the subgoals of Goal that remain to be proved consist
of Subgoal 18 together with 17 more subgoals.The next proof tree display differs from the previous one only in that now, Subgoal 18' has only one more subgoal to be processed.
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
c 2 | | Subgoal 18' ELIM
| | | <1 more subgoal>
| <17 more subgoals>
Note that the word ``more'' in ``<1 more subgoal>'' tells us that
there was originally more than one subgoal of Subgoal 18. In fact
that information already follows from the line above, which (as
previously explained) says that Subgoal 18' originally created 2
subgoals.The next proof tree display occurs when the prover completes the proof of that ``1 more subgoal'' referred to above.
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <17 more subgoals>
Then, Subgoal 17 is processed and creates one subgoal, by
simplification:
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 17 simp
| | <1 subgoal>
| <16 more subgoals>
... and so on.Later in the proof one might find the following successive proof tree displays.
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <9 more subgoals>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 9 simp (FORCED)
| <8 more subgoals>
These displays tell us that Subgoal 9 simplified to t (note that
the ``0'' shows clearly that no subgoals were created), but that
some rule's hypotheses were forced. Although this goal is not
checkpointed (i.e., no ``c'' appears on the left margin), one can
cause such goals to be checkpointed;
see checkpoint-forced-goals.In fact, the proof tree displayed at the end of the ``main proof'' (the 0-th forcing round) is as follows.
( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED) 0 | Subgoal 8 simp (FORCED) 0 | Subgoal 7 simp (FORCED) 0 | Subgoal 6 simp (FORCED) 0 | Subgoal 4 simp (FORCED) 0 | Subgoal 3 simp (FORCED)This is followed by the following proof tree display at the start of the forcing round.
18 Goal preprocess
0 | Subgoal 9 simp (FORCED [1]Subgoal 4)
0 | Subgoal 8 simp (FORCED [1]Subgoal 6)
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
0 | Subgoal 6 simp (FORCED [1]Subgoal 3)
0 | Subgoal 4 simp (FORCED [1]Subgoal 5)
0 | Subgoal 3 simp (FORCED [1]Subgoal 2)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
2 | [1]Subgoal 6 preprocess
| | <2 subgoals>
| <5 more subgoals>
This display shows which goals to ``blame'' for the existence of
each goal in the forcing round. For example, Subgoal 9 is to blame
for the creation of [1]Subgoal 4.
Actually, there is no real goal named "[1]Goal". However, the
line
6 [1]Goal FORCING-ROUNDappears in the proof tree display to suggest a ``parent'' of the six top-level goals in that forcing round. As usual, the numeric field before the goal name contains the original number of children of that (virtual, in this case) goal -- in this case, 6.
In our example proof, Subgoal 6 eventually gets proved, without doing any further forcing. At that point, the proof tree display looks as follows.
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 9 simp (FORCED [1]Subgoal 4)
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
0 | Subgoal 6 simp (FORCED [1]Subgoal 3)
0 | Subgoal 4 simp (FORCED [1]Subgoal 5)
0 | Subgoal 3 simp (FORCED [1]Subgoal 2)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
| <5 more subgoals>
Notice that the line for Subgoal 8,
0 | Subgoal 8 simp (FORCED [1]Subgoal 6)no longer appears. That is because the goal [1]Subgoal 6 has been proved, along with all its children; and hence, the proof of Subgoal 8 no longer depends on any further reasoning.
The final two proof tree displays in our example are as follows.
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
2 | [1]Subgoal 1 preprocess
1 | | [1]Subgoal 1.1 preprocess
1 | | | [1]Subgoal 1.1' simp
c 3 | | | | [1]Subgoal 1.1'' ELIM
| | | | | <1 more subgoal>
( DEFUN CANCEL_EQUAL_PLUS ...)
<<PROOF TREE IS EMPTY>>
The explanation for the empty proof tree is simple: once
[1]Subgoal 1.1.1 was proved, nothing further remained to be proved.
In fact, the much sought-after ``Q.E.D.'' appeared shortly after the
final proof tree was displayed.Let us conclude with a final, brief example that illustrates proof by induction. Partway through the proof one might come across the following proof tree display.
( DEFTHM PLUS-TREE-DEL ...)
1 Goal preprocess
2 | Goal' simp
c 0 | | Subgoal 2 PUSH *1
| | <1 more subgoal>
This display says that in the attempt to prove a theorem called
plus-tree-del, preprocessing created the only child Goal' from Goal,
and Goal' simplified to two subgoals. Subgoal 2 is immediately
pushed for proof by induction, under the name ``*1''. In fact if
Subgoal 1 simplifies to t, then we see the following successive
proof tree displays after the one shown above.
( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1The separator ``+++++...'' says that we are beginning another trip through the waterfall. In fact this trip is for a proof by induction (as opposed to a forcing round), as indicated by the word ``INDUCT''. Apparently *1.6 was proved immediately, because it was not even displayed; a goal is only displayed when there is some work left to do either on it or on some goal that it brought (perhaps indirectly) into existence.( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 ++++++++++++++++++++++++++++++ c 6 *1 INDUCT | <5 more subgoals>
Once a proof by induction is completed, the ``PUSH'' line that refers to that proof is eliminated (``pruned''). So for example, when the present proof by induction is completed, the line
c 0 | | Subgoal 2 PUSH *1is eliminated, which in fact causes the lines above it to be eliminated (since they no longer refer to unproved children). Hence, at that point one might expect to see:
( DEFTHM PLUS-TREE-DEL ...) <<PROOF TREE IS EMPTY>>However, if the proof by induction of *1 necessitates further proofs by induction or a forcing round, then this ``pruning'' will not yet be done.
start displaying proof trees during proofs
Parent topic: PROOF-TREE Home
Also see proof-tree and see stop-proof-tree. Note that
:start-proof-tree works by removing 'proof-tree from the
inhibit-output-lst; see set-inhibit-output-lst.
Proof tree displays are explained in the documentation for
proof-tree. :start-proof-tree causes proof tree display to be
turned on, once it has been turned off by :stop-proof-tree.
Do not attempt to invoke start-proof-tree during an interrupt in the
middle of a proof.
stop displaying proof trees during proofs
Parent topic: PROOF-TREE Home
Also see proof-tree and see start-proof-tree. Note that
:stop-proof-tree works by adding 'proof-tree to the
inhibit-output-lst; see set-inhibit-output-lst.
Proof tree displays are explained in the documentation for
proof-tree. :Stop-proof-tree causes proof tree display to be
turned off.
It is permissible to submit the form (stop-proof-tree) during a
break. Thus, you can actually turn off proof tree display in the
middle of a proof by interrupting ACL2 and submitting the form
(stop-proof-tree) in raw Lisp.