INTRODUCTION-TO-KEY-CHECKPOINTS

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

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 , and other history commands to inspect the database; (see history ). But if you find the allegedly relevant simpler fact in the database, you must ask: 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 IFF rule but the target doesn't occur propositionally -- so see if you you can strengthen the rule to an EQUAL rule or weaken the context of the target by changing the conjecture to use the target propositionally; if you decide to remove the old rule from the database, see 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 (:see brr ) help you figure out why the rule failed, so use them and improve the rule, or the current conjecture, or the database as appropriate.

(4) If the simpler fact is not already known, prove it. This means you must create a new defthm event with appropriate 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 defthm and use The Method recursively to prove it.

(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 and, perhaps, see accumulated-persistence .

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.