Major Section: MISCELLANEOUS
Many users develop proof scripts in an Emacs buffer and submit one
event at a time to the theorem prover running in a *shell* buffer.
The script buffer is logically divided into two regions: the events
that have been accepted by the theorem prover and those that have
not yet been accepted. An imaginary ``barrier'' divides these two
regions. The region above the barrier describes the state of the
*shell* buffer (and ACL2's logical world). The region below the
barrier is the ``to do'' list.
We usually start a proof project by typing the key lemmas, and main goal into the to do list. Definitions are here just regarded as theorems to prove (i.e., the measure conjectures). Then we follow ``The Method.''
(1) Think about the proof of the first theorem in the to do list. Structure the proof either as an induction followed by simplification or just simplification. Have the necessary lemmas been proved? That is, are the necessary lemmas in the done list already? If so, proceed to Step 2. Otherwise, add the necessary lemmas at the front of the to do list and repeat Step 1.
(2) Call the theorem prover on the first theorem in the to do list and let the output stream into the *shell* buffer. Abort the proof if it runs more than a few seconds.
(3) If the theorem prover succeeded, advance the barrier past the successful command and go to Step 1.
(4) Otherwise, inspect the failed proof attempt, starting from the beginning, not the end. Basically you should look for the first place the proof attempt deviates from your imagined proof. If your imagined proof was inductive, inspect the induction scheme used by ACL2. If that is ok, then find the first subsequent subgoal that is stable under simplification and think about why it was not proved by the simplifier. If your imagined proof was not inductive, then think about the first subgoal stable under simplification, as above. Modify the script appropriately. It usually means adding lemmas to the to do list, just in front of the theorem just tried. It could mean adding hints to the current theorem. In any case, after the modifications go to Step 1.
We do not seriously suggest that this or any rotely applied algorithm will let you drive ACL2 to difficult proofs. Indeed, to remind you of this we call this ``The Method'' rather than ``the method.'' That is, we are aware of the somewhat pretentious nature of any such advice. But these remarks have helped many users approach ACL2 in a constructive and disciplined way.
We say much more about The Method in the ACL2 book. See the home page.
Learning to read failed proofs is a useful skill. There are several kinds of ``checkpoints'' in a proof: (1) a formula to which induction is being (or would be) applied, (2) the first formula stable under simplification, (3) a formula that is possibly generalized, either by cross-fertilizing with and throwing away an equivalence hypothesis or by explicit generalization of a term with a new variable.
At the induction checkpoint, confirm that you believe the formula being proved is a theorem and that it is appropriately strong for an inductive proof. Read the selected induction scheme and make sure it agrees with your idea of how the proof should go.
At the post-simplification checkpoint, which is probably the most
commonly seen, consider whether there are additional rewrite rules
you could prove to make the formula simplify still further. Look
for compositions of function symbols you could rewrite. Look for
contradictions among hypotheses and prove the appropriate
implications: for example, the checkpoint might contain the two
hypotheses (P (F A)) and (NOT (Q (G (F A)))) and you might
realize that (implies (p x) (q (g x))) is a theorem. Look for
signs that your existing rules did not apply, e.g., for terms that
should have been rewritten, and figure out why they were not.
Possible causes include that they do not exactly match your old
rules, that your old rules have hypotheses that cannot be relieved
here -- perhaps because some other rules are missing, or perhaps
your old rules are disabled. If you cannot find any further
simplifications to make in the formula, ask yourself whether it is
valid. If so, sketch a proof. Perhaps the proof is by appeal to a
combination of lemmas you should now prove?
At the two generalization checkpoints --- where hypotheses are discarded or terms are replaced by variables --- ask yourself whether the result is a theorem. It often is not. Think about rewrite rules that would prove the formula. These are often restricted versions of the overly-general formulas created by the system's heuristics.
See proof-tree for a discussion of a tool to help you navigate through
ACL2 proofs.