Instructions to the interactive proof-builder

See proof-builder for an introduction to the interactive
``proof-builder'' 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

Thus, also see defthm for the role of `hints`. As illustrated by the following example, the value
associated with

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

See proof-builder-commands for a list of supported interactive proof-builder instructions and links to their documentation.

Below, we describe a capability for supplying `hints`.

The most basic utilities for directing the discharge of a proof obligation
are `hints` and (less commonly)

ACL2 supports `verify`, do an
interactive proof, submit

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

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

- The interactive proof-builder's theory is not sensitive to
:in-theory hints already processed in the surrounding proof. Indeed, the current theory for which proof-builder 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-builderin-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. - 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 interactive proof-builder instruction interpreter as a clause-processor.

In the example above, the input goal (

[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-BUILDER-CL-PROC replaces this goal by T.

**Remark.** This brief remark can probably be ignored, but we include it
for completeness. The `clause-processor` hint, one that
specifies `clause-processor` hint replaces the

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-BUILDER-CL-PROC to produce two new subgoals. Subgoal *1/2.2 [[ ... output omitted ... ]] Subgoal *1/2.1 [[ ... output omitted ... ]]

We have seen that an

(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

Saving proof-builder 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 interactive
proof-builder in the examples above. This default behavior prevents confusion
that could arise from use of proof-builder commands that call the theorem
prover such as

(comment inhibit-output-lst VAL)

where

(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

The following contrived example gives a sense of how one might want to use
`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 interactive proof-builder 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 ***** Goal' ([ A key checkpoint: Goal' (IMPLIES (TRUE-LISTP X) (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL) X)) Goal' is subsumed by a goal yet to be proved. ]) 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 ; show current goal ("th" for "theorem") *** Top-level hypotheses: 1. (TRUE-LISTP X) The current subterm is: (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL) X) ->: p ; show current subterm only (EQUAL (REVAPPEND (REVAPPEND X NIL) NIL) X) ->: 1 ; dive to first argument ->: 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 ; move to the top of the conclusion, making it the current subterm ->: p (EQUAL (REVAPPEND NIL (APPEND X NIL)) X) ->: prove ; finish the proof ***** Now entering the theorem prover ***** Q.E.D. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* You may wish to exit. ->: (exit t) ; the argument, t, causes :instructions to be printed (DEFTHM T (IMPLIES (TRUE-LISTP X) (EQUAL (REVERSE (REVERSE X)) X)) :INSTRUCTIONS (:BASH (:DV 1) (:REWRITE REVAPPEND-REVAPPEND) :TOP :PROVE)) 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)))) Goal' Q.E.D. Q.E.D. Q.E.D. Summary Form: ( THM ...) Rules: NIL Hint-events: ((:CLAUSE-PROCESSOR PROOF-BUILDER-CL-PROC)) 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 `hints` within

(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-builder 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-builder 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-BUILDER 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-builder instructions]] We now apply the trusted :CLAUSE-PROCESSOR function PROOF-BUILDER-CL-PROC to produce one new subgoal. Subgoal *1/3''' [[ ... output omitted ... ]] [[<1 Completed proof-builder instructions]]

The nesting levels are independent of whether or not output is enabled; for
example, if the first `retrieve`
(as indicated above); for example, a failure at level 1 would be associated
with symbol