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:

In this case, you can evaluate the indicatedSaving proof-checker error state; see :DOC instructions. To retrieve:

(RETRIEVE :ERROR1)

`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))))))Note that such a(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))))))

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

The nesting levels are independent of whether or not output is enabled; for example, if the first[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]]

`(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`

.