THE-METHOD

how to find proofs
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.