INSTRUCTIONS.html -- ACL2 Version 6.2

INSTRUCTIONS

instructions to the proof checker

Major Section:  PROOF-CHECKER

See proof-checker for an introduction to the interactive ``proof-checker'' goal manager, which supports much more direct control of the proof process than is available by direct calls to the prover (as are normally made using defthm or thm). In brief, typical use is to evaluate the form (verify SOME-GOAL), where SOME-GOAL is a formula (i.e., term) that you would like to prove. Various commands (instructions) are available at the resulting prompt; see proof-checker-commands. When the proof is completed, suitable invocation of the exit command will print out a form containing an :instructions field that provides the instructions that you gave interactively, so that this form can be evaluated non-interactively.

Thus, also see defthm for the role of :instructions in place of :hints. As illustrated by the following example, the value associated with :instructions is a list of proof-checker commands.

Example:
(defthm associativity-of-append
        (equal (append (append x y) z)
               (append x (append y z)))
        :instructions
        (:induct (:dv 1) (:dv 1) :x :up :x (:dv 2) := (:drop 2)
         :top (:dv 2) :x :top :s :bash))

When you are inside the interactive loop (i.e., after executing verify), you may invoke help to get a list of legal instructions and (help instr) to get help for the instruction instr.

Below, we describe a capability for supplying :instructions as :hints.

The most basic utilities for directing the discharge of a proof obligation are :hints and (less commonly) :instructions. Individual instructions may call the prover with :hints; in that sense, prover hints may occur inside instructions. We now describe how, on the other hand, instructions may occur inside hints.

ACL2 supports :instructions as a hints keyword. The following example forms the basis for our running example. This example does not actually need hints, but imagine that the inductive step -- which is "Subgoal *1/2" -- was proving difficult. You could submit that goal to verify, do an interactive proof, submit (exit t) to obtain the list of :instructions (answering with `N' at the prompt, to complete the exit), and then paste in those instructions. When you submit the result event, you might see the following. Below we'll explain the hint processing.

ACL2 !>(thm (equal (append (append x y) z)
                   (append x (append y z)))
            :hints (("Subgoal *1/2"
                     :instructions
                     (:promote (:dv 1) (:dv 1) :x :up :x (:dv 2) :=
                      (:drop 2) :top (:dv 2) :x :top :s))))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Three induction schemes are
suggested by this conjecture.  Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.

We will induct according to a scheme suggested by (BINARY-APPEND X Y).
This suggestion was produced using the :induction rule BINARY-APPEND.
If we let (:P X Y Z) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z))
              (:P X Y Z))
     (IMPLIES (ENDP X) (:P X Y Z))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

[Note:  A hint was supplied for our processing of the goal below.
Thanks!]

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                     (APPEND (CDR X) Y Z)))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
this goal by T.

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

But simplification reduces this to T, using the :definition BINARY-APPEND
and primitive type reasoning.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND))
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)

Proof succeeded.
ACL2 !>

To understand how the :instructions supplied above were processed, observe proof-checker instruction interpreter may be viewed as a ``clause-processor'': a function that takes an input goal and returns a list of goals (which can be the empty list). Such a function has the property that if all goals in that returned list are theorems, then so is the input goal. This view of the proof-checker instruction interpreter as a clause-processor leads to the following crucial observation.

IMPORTANT!. Each call of the proof-checker instruction interpreter is treated as a standalone clause-processor that is insensitive to the surrounding prover environment. In particular:

o The proof-checker's theory is not sensitive to :in-theory hints already processed in the surrounding proof. Indeed, the current theory for which proof-checker commands are processed is just the current theory of the ACL2 logical world, i.e., the value of (current-theory :here). Moreover, references to (current-theory :here) in a proof-checker in-theory command, even implicit references such as provided by enable and disable expressions, are also references to the current theory of the ACL2 logical world.
o The runes used during an :instructions hint are not tracked beyond that hint, hence may not show up in the summary of the overall proof. Again, think of the :instructions hint as a clause-processor call, which has some effect not tracked by the surrounding proof other than for the child goals that it returns.

We continue now with our discussion of the proof-checker instruction interpreter as a clause-processor.

In the example above, the input goal ("Subgoal *1/2") was processed by the proof-checker instruction interpreter. The result was the empty goal stack, therefore proving the goal, as reported in the output, which we repeat here.

[Note:  A hint was supplied for our processing of the goal below.
Thanks!]

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                     (APPEND (CDR X) Y Z)))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
this goal by T.

Remark. This brief remark can probably be ignored, but we include it for completeness. The :CLAUSE-PROCESSOR message above may be surprising, since the hint attached to "Subgoal *1/2" is an :instructions hint, not a :clause-processor hint. But :instructions is actually a custom keyword hint (see custom-keyword-hints), and may be thought of as a macro that expands to a :clause-processor hint, one that specifies proof-checker-cl-proc as the clause-processor function. The keen observer may notice that the clause-processor is referred to as ``trusted'' in the above output. Normally one needs a trust tag (see defttag) to install a trusted clause-processor, but that is not the case for the built-in clause-processor, proof-checker-cl-proc. Finally, we note that :instructions hints are ``spliced'' in: the appropriate :clause-processor hint replaces the :instructions hint, and the other hints remain intact. It may seems surprising that one can thus, for example, use :instructions and :in-theory together; but although the :in-theory hint will have no effect on execution of the :instructions (see first bullet above), the :in-theory hint will apply in the usual manner to any child goes (see hints-and-the-waterfall). End of Remark.

Now consider the case that the supplied instructions do not prove the goal. That is, suppose that the execution of those instructions results in a non-empty goal stack. In that case, the resulting goals become children of the input goals. The following edited log provides an illustration using a modification of the above example, this time with a single instruction that splits into two cases.

ACL2 !>(thm (equal (append (append x y) z)
                   (append x (append y z)))
            :hints (("Subgoal *1/2"
                     :instructions
                     ((:casesplit (equal x y))))))

[[ ... output omitted ... ]]

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                     (APPEND (CDR X) Y Z)))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

We now apply the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC
to produce two new subgoals.

Subgoal *1/2.2

[[ ... output omitted ... ]]

Subgoal *1/2.1

[[ ... output omitted ... ]]

We have seen that an :instructions hint may produce zero or more subgoals. There may be times where you wish to insist that it produce zero subgoals, i.e., that it prove the desired goal. The proof-checker `finish' command works nicely for this purpose. For example, the following form is successfully admitted, but if you delete some of the commands (for example, the :s command at the end), you will see an informative error message.

(thm (equal (append (append x y) z)
            (append x (append y z)))
     :hints (("Subgoal *1/2"
              :instructions
              ((finish :promote (:dv 1) (:dv 1) :x :up :x (:dv 2) :=
                       (:drop 2) :top (:dv 2) :x :top :s)))))

If an :instructions hint of the form ((finish ...)) fails to prove the goal, the clause-processor is deemed to have caused an error. Indeed, any ``failure'' of a supplied proof-checker instruction will be deemed to cause an error. In this case, you should see an error message such as the following:


Saving proof-checker error state; see :DOC instructions.  To retrieve:

(RETRIEVE :ERROR1)

In this case, you can evaluate the indicated retrieve command in the ACL2 read-eval-print loop, to get to the point of failure.

You may have noticed that there is no output from the proof-checker in the examples above. This default behavior prevents confusion that could arise from use of proof-checker commands that call the theorem prover such as prove, bash, split, and induct. These commands produce output for what amounts to a fresh proof attempt, which could confuse attempts to understand the surrounding proof log. You can override the default behavior by providing a command of the form

(comment inhibit-output-lst VAL)

where VAL is either the keyword :SAME (indicating that no change should be made to which output is inhibited) or else is a legal value for inhibited output; see set-inhibit-output-lst. The following two variants of the immediately preceding THM form will each produce output from the proof-checker commands, assuming in the first variant that output hasn't already been inhibited.

(thm (equal (append (append x y) z)
                   (append x (append y z)))
            :hints (("Subgoal *1/2"
                     :instructions
                     ((comment inhibit-output-lst :same)
                      (:casesplit (equal x y))))))

(thm (equal (append (append x y) z)
                   (append x (append y z)))
            :hints (("Subgoal *1/2"
                     :instructions
                     ((comment inhibit-output-lst (proof-tree))
                      (:casesplit (equal x y))))))

Note that such a comment instruction must be provided explicitly (i.e., not by way of a proof-checker macro-command) as the first instruction, in order to have the effect on inhibited output that is described above.

The following contrived example gives a sense of how one might want to use :instructions within :hints. If you submit the following theorem

(thm (implies (true-listp x)
              (equal (reverse (reverse x)) x)))

then you will see the following checkpoint printed with the summary.

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (EQUAL (REVAPPEND (REVAPPEND (CDR X) NIL) NIL)
                     (CDR X))
              (TRUE-LISTP (CDR X)))
         (EQUAL (REVAPPEND (REVAPPEND (CDR X) (LIST (CAR X)))
                           NIL)
                X))

This suggests proving the following theorem. Here we state it using defthmd, so that it is immediately disabled. Normally disabling would be unnecessary, but for our contrived example it is useful to imagine disabling it, say because we are following a methodology that tends to keep rewrite rules disabled.

(defthmd revappend-revappend
  (equal (revappend (revappend x y) z)
         (revappend y (append x z))))

We might then enter the proof-checker to prove the original theorem interactively, as follows.

ACL2 !>(verify (implies (true-listp x)
                        (equal (reverse (reverse x)) x)))
->: bash
***** Now entering the theorem prover *****

[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

This simplifies, using the :definition REVERSE and the :type-prescription
rule REVAPPEND, to

Goal'
(IMPLIES (TRUE-LISTP X)
         (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
                X)).

But we have been asked to pretend that this goal is subsumed by the
yet-to-be-proved |PROOF-CHECKER Goal'|.

Q.E.D.


Creating one new goal:  (MAIN . 1).

The proof of the current goal, MAIN, has been completed.  However,
the following subgoals remain to be proved:
  (MAIN . 1).
Now proving (MAIN . 1).
->: th
*** Top-level hypotheses:
1. (TRUE-LISTP X)

The current subterm is:
(EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
       X)
->: 1
->: sr ; show-rewrites

1. REVAPPEND-REVAPPEND (disabled)
  New term: (REVAPPEND NIL (APPEND X NIL))
  Hypotheses: <none>
  Equiv: EQUAL

2. REVAPPEND
  New term: (AND (CONSP (REVAPPEND X NIL))
                 (REVAPPEND (CDR (REVAPPEND X NIL))
                            (LIST (CAR (REVAPPEND X NIL)))))
  Hypotheses: <none>
  Equiv: EQUAL
->: (r 1) ; rewrite with rule #1 above
Rewriting with REVAPPEND-REVAPPEND.
->: exit
Exiting....
 NIL
ACL2 !>(verify (implies (true-listp x)
                        (equal (reverse (reverse x)) x)))
->: bash
***** Now entering the theorem prover *****

[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

This simplifies, using the :definition REVERSE and the :type-prescription
rule REVAPPEND, to

Goal'
(IMPLIES (TRUE-LISTP X)
         (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
                X)).

But we have been asked to pretend that this goal is subsumed by the
yet-to-be-proved |PROOF-CHECKER Goal'|.

Q.E.D.


Creating one new goal:  (MAIN . 1).

The proof of the current goal, MAIN, has been completed.  However,
the following subgoals remain to be proved:
  (MAIN . 1).
Now proving (MAIN . 1).
->: th
*** Top-level hypotheses:
1. (TRUE-LISTP X)

The current subterm is:
(EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
       X)
->: p
(EQUAL (REVAPPEND (REVAPPEND X NIL) NIL)
       X)
->: 1
->: p
(REVAPPEND (REVAPPEND X NIL) NIL)
->: sr ; show-rewrites

1. REVAPPEND-REVAPPEND (disabled)
  New term: (REVAPPEND NIL (APPEND X NIL))
  Hypotheses: <none>
  Equiv: EQUAL

2. REVAPPEND
  New term: (AND (CONSP (REVAPPEND X NIL))
                 (REVAPPEND (CDR (REVAPPEND X NIL))
                            (LIST (CAR (REVAPPEND X NIL)))))
  Hypotheses: <none>
  Equiv: EQUAL
->: (r 1) ; rewrite with rule #1 above
Rewriting with REVAPPEND-REVAPPEND.
->: p
(REVAPPEND NIL (APPEND X NIL))
->: top
->: prove ; finish the proof
***** Now entering the theorem prover *****

But simplification reduces this to T, using the :definition REVAPPEND,
the :executable-counterpart of CONSP, primitive type reasoning and
the :rewrite rule APPEND-TO-NIL.

Q.E.D.

*!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!*
You may wish to exit.
->: (exit t) ; to get :instructions; could give name, or (exit t nil t)
(DEFTHM T
        (IMPLIES (TRUE-LISTP X)
                 (EQUAL (REVERSE (REVERSE X)) X))
        :INSTRUCTIONS (:BASH (:DV 1)
                             (:REWRITE REVAPPEND-REVAPPEND)
                             :TOP :PROVE))

ACL2 Query (ACL2-PC::EXIT):
Do you want to submit this event?  Possible replies are:
Y (Yes), R (yes and Replay commands), N (No, but exit), A (Abort exiting).
   (Y, R, N or A):  n
 NIL
ACL2 !>(thm
        (IMPLIES (TRUE-LISTP X)
                 (EQUAL (REVERSE (REVERSE X)) X))
        :hints (("Goal"
                 :INSTRUCTIONS ; copy what was printed above:
                 (:BASH (:DV 1)
                        (:REWRITE REVAPPEND-REVAPPEND)
                        :TOP :PROVE))))

[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

But the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC replaces
this goal by T.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 !>

Finally we present an even more contrived example, based on the one above. This example illustrates that there is actually no limit imposed on the nesting of :instructions within :hints within :instructions, and so on. Notice the indication of nesting levels: ``1>'' to ``<1'' for output from nesting level 1, and ``2>'' to ``<2'' for output from nesting level 2.

(thm (implies (true-listp x)
              (equal (reverse (reverse x)) x))
     :hints (("Goal"
              :instructions
              ((comment inhibit-output-lst :same)
               (:prove
                :hints (("Goal" :in-theory (disable append))
                        ("Subgoal *1/3''"
                         :instructions
                         ((comment inhibit-output-lst :same)
                          :bash
                          (:dv 1)
                          (:rewrite revappend-revappend)))))))))

Here is an edited version of the resulting log.


[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

[[1> Executing proof-checker instructions]]

->: (COMMENT INHIBIT-OUTPUT-LST :SAME)
->: (:PROVE
         :HINTS
         (("Goal" :IN-THEORY (DISABLE APPEND))
          ("Subgoal *1/3''" :INSTRUCTIONS ((COMMENT INHIBIT-OUTPUT-LST :SAME)
                                           :BASH (:DV 1)
                                           (:REWRITE REVAPPEND-REVAPPEND)))))
***** Now entering the theorem prover *****

[[ ... output omitted ... ]]

[Note:  A hint was supplied for our processing of the goal below.
Thanks!]

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (EQUAL (REVAPPEND (REVAPPEND (CDR X) NIL) NIL)
                     (CDR X))
              (TRUE-LISTP (CDR X)))
         (EQUAL (REVAPPEND (REVAPPEND (CDR X) (LIST (CAR X)))
                           NIL)
                X)).

[[2> Executing proof-checker instructions]]

->: (COMMENT INHIBIT-OUTPUT-LST :SAME)
->: :BASH
***** Now entering the theorem prover *****

[Note:  A hint was supplied for our processing of the goal above.
Thanks!]

But we have been asked to pretend that this goal is subsumed by the
yet-to-be-proved |PROOF-CHECKER Goal|.

Q.E.D.


Creating one new goal:  (MAIN . 1).

The proof of the current goal, MAIN, has been completed.  However,
the following subgoals remain to be proved:
  (MAIN . 1).
Now proving (MAIN . 1).
->: (:DV 1)
->: (:REWRITE REVAPPEND-REVAPPEND)
Rewriting with REVAPPEND-REVAPPEND.

[[<2 Completed proof-checker instructions]]

We now apply the trusted :CLAUSE-PROCESSOR function PROOF-CHECKER-CL-PROC
to produce one new subgoal.

Subgoal *1/3'''

[[ ... output omitted ... ]]

[[<1 Completed proof-checker instructions]]

The nesting levels are independent of whether or not output is enabled; for example, if the first (comment ...) form below is omitted, then we will see only the output bracketed by ``2>'' to ``<2''. Note also that these levels are part of the error states saved for access by retrieve (as indicated above); for example, a failure at level 1 would be associated with symbol :ERROR1 as indicated above, while a failure at level 2 would be associated with symbol :ERROR2.