POST-INDUCTION-KEY-CHECKPOINTS

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

Each post-induction key checkpoint is a theorem if and only if the original conjecture was a theorem. The reason is that each subgoal produced by induction concludes with the original formula and simplification preserves equivalence.

So if you see a post-induction key checkpoint that is not a theorem, stop looking at the checkpoints! Your original conjecture is not a theorem! Fix it.

If you're convinced all the post-induction conjectures are theorems, ask whether each has the hypotheses you'd need to prove it. If the case analysis feels inappropriate or induction hypotheses seem to be missing, then ACL2 might have done the wrong induction. Find the induction scheme it did by reading the first induction message printed after the conjecture was submitted. If it is wrong, then extend ACL2's induction analysis or tell ACL2 what induction to do, as explained shortly.

But before you decide the induction hypothesis is missing, look closely for contradictions among the hypotheses of the checkpoint formula. For example, perhaps one of the hypotheses is (MEMBER e x) and another is (NOT (MEMBER e' x')) where e, x, e', and x' are possibly complicated expressions.

Is it possible that e and e' are equal and x and x' are equal? If so, then the two hypotheses are contradictory and the checkpoint would be proved if you could find rules that would simplify those expressions to their common forms. So look for theorems about those subexpressions.

Or maybe you can get e and e' to reduce to some common d but but find that x and x' are really different. Then ask whether

(implies (member d x) (member d x'))

If you have been working your way through the tutorial introduction to the theorem prover, use your browser's Back Button now to introduction-to-key-checkpoints.