What questions to ask at key checkpoints

We assume you've read about rewrite rules; see introduction-to-rewrite-rules-part-1.

When a proof attempt fails, ACL2 prints some *key checkpoints*. These
are formulas that we think you should look at. There are two kinds printed:
key checkpoints *before an induction*, and key checkpoints *under a
top-level induction*. (Key checkpoints under deeper inductions and
checkpoints that aren't considered ``key'' may exist in the proof attempt, but
ACL2 doesn't print them at the end of failed proofs because you shouldn't be
distracted by them.)

Below is a list of questions to ask yourself about the key checkpoints.
Initially, we recommend just picking one key checkpoint *before* an
induction (perhaps the simplest looking one) and asking these questions.
These questions may lead you to look at other key checkpoints. As you gain
more experience you'll elaborate and generalize this advice.

**(1) Do you believe this formula is a theorem?** If you don't think it
is, it's pointless to try to prove it! You should reconsider your top-level
formula in light of the special case suggested by this key checkpoint.

**(2) Can it be simplified?** Is there some combination of function
symbols in it that could be eliminated or simplified by exploiting some
simpler fact? By a ``simpler fact'' we mean a theorem about a few of the
symbols in this formula. For an example of this see dealing-with-key-combinations-of-function-symbols. Don't think about the
deep question ``how can I prove the checkpoint?'' until you've got it into its
simplest form.

**(3) Is the simpler fact already in the database?** If there is some
simpler fact that would help clean up the checkpoint but you believe the
simpler fact is already in the database, you can use `pl` `pc` `pbt` *history* commands to inspect the database; (see history
**why wasn't it used?** There are four
principal reasons:

(3a) it is disabled — so enable it; you'll learn how when you read the coming sections on introduction-to-the-database and introduction-to-hints.

(3b) its left-hand side doesn't match the target — so improve the
rule by generalizing its left-hand side or prove a new rule for this
situation; if you decide to remove the old rule from the database, see
*undo* commands in history

(3c) it is an *undo* commands in history

(3d) the hypotheses of the rule cannot be relieved for this occurrence of
the target; this can be caused by the rule's hypotheses being too strong
(requiring more than they should), or by the hypotheses of the current
conjecture being too weak (you forgot some key hypothesis), or by ACL2 not
having the rules it needs to prove that the conjecture's hypotheses really do
imply the rule's. Tools are available (

**(4) If the simpler fact is not already known, prove it.** This means
you must create a new *rule-classes*
to store your new theorem so that it will be used. See dealing-with-key-combinations-of-function-symbols. Then you must start using
The Method recursively to prove your new lemma.

**(5) Otherwise, is this formula something you'd prove by induction?**
If you can't simplify it, it may be because you ``need this fact to prove this
fact,'' in which case, induction is the right thing to do. But first,
remember that in order for a formulas to be provable by induction, it must be
very general. Why must it be general? Because in an inductive proof, the
main thing you have to work with is the induction hypothesis, which is an
instance of the theorem you're proving. If the theorem is not general enough,
you won't be able to assume an instance that will help you. ACL2 may try
induction even on formulas that are not general enough. Don't assume that the
formula is ripe for induction just because ACL2 found an induction to do!
Before you ``approve'' a formula for induction, ask whether it is perhaps a
special case of some more general theorem. See generalizing-key-checkpoints now and then come back here. If you found a
generalization, you should probably be proving that formula instead of this
one. So formulate the appropriate

**(6) If the formula is right for induction, did ACL2 do an induction for
it?** You can answer that without looking at the proof. Just see if there
are any key checkpoints after induction. If not, why didn't ACL2 induct?
Perhaps you told ACL2 not to induct! Perhaps no term in the conjecture
suggests an appropriate induction? You could remedy this by extending ACL2's
induction analysis by adding to the database. Or you could just tell ACL2
what induction to do for this formula. You'll learn about both later (when
you read coming sections of the tutorial).

**(7) If ACL2 did do an induction, was it the right one?** You can find
the induction scheme used by reading the first induction message in the output
log after you submitted the conjecture to ACL2. But most often you will
realize the ``wrong'' induction was done just by looking at the post-induction
key checkpoints, keeping in mind that each is supposed to be a natural special
case of the theorem you're proving. Is the case analysis inappropriate? Are
induction hypotheses missing? If so, you should look at the induction scheme.
If you determine the wrong induction was done, extend ACL2's induction
analysis or tell it which induction to do, which you'll learn about in the
coming sections of the tutorial. For more advice about looking at
post-induction key checkpoints, see post-induction-key-checkpoints now
and then come back here.

**(8) If the post-induction key checkpoints seems plausible,** **then
repeat the questions above for each one of them,** **perhaps starting with
the simplest.**

In any case, after successfully taking whatever action you've decided on, e.g., proving some new lemma and adding it as a rule:

**Start over trying to prove your main conjecture.** This is important!
Do not just scroll back to the key checkpoints generated the last time you
tried to prove it. Instead, re-generate them in the context of your new,
improved database and hints.

You will be following this general outline almost all of the time that you're interacting with ACL2. You will not often be asking ``Why is ACL2 making me think about this subgoal? What did ACL2 do to get here? How does ACL2 work?''

Two other ideas are helpful to keep in mind.

**Is a key checkpoint unexpectedly complicated?** Pay special attention
to the case where the complication seems to be the introduction of low-level
details you thought you'd dealt with or by the introduction of symbols you
didn't expect to see in this proof. These can be signs that you ought to
disable some rules in the database (e.g., a definition of a complicated
function about which you've proved all the necessary lemmas or some lemma that
transforms the problem as was appropriate for some other proof).

**Does the theorem prover just hang up, printing nothing?** If this
happens, you must interrupt it. How you interrupt the prover is dependent on
which Common Lisp and which interface you're using. But most Common Lisps
treat control-c as a console interrupt. If you're in Emacs running ACL2 as a
shell process, you must type control-c control-c. If you're in ACL2s, hit the
*Interrupt Session* button. Interrupting ACL2 can leave you in an
interactive loop similar in appearance but different from ACL2's top-level!
So pay careful attention to the prompt and see breaks

Once you've regained control from the ``runaway'' theorem prover, there are
several tools you can use to find out what it is doing in real-time.
Generally speaking, when the theorem prover goes silent for a very long time
it is either in some kind of rewrite loop caused by rules that cause it to
flip back and forth between various supposedly normal forms, or else it has
split the problem into a huge number of cases and suffering a combinatoric
explosion. See dmr

If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's **Back Button** now to return to introduction-to-the-theorem-prover.