PROOF-TREE

proof tree displays 
Major Section:  ACL2 Documentation

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.

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 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.












































































CHECKPOINT-FORCED-GOALS

Cause forcing goals to be checkpointed in proof trees 
Major Section:  PROOF-TREE


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

proof tree details not covered elsewhere 
Major Section:  PROOF-TREE

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-EXAMPLES

proof tree example 
Major Section:  PROOF-TREE

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' ELIM
The ``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-ROUND
appears 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 *1


( DEFTHM PLUS-TREE-DEL ...)
   1 Goal preprocess
   2 |  Goal' simp
c  0 |  |  Subgoal 2 PUSH *1
++++++++++++++++++++++++++++++
c  6 *1 INDUCT
     |  <5 more subgoals>
The 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.

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 *1
is 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-PROOF-TREE

start displaying proof trees during proofs 
Major Section:  PROOF-TREE

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-PROOF-TREE

stop displaying proof trees during proofs 
Major Section:  PROOF-TREE

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.