How to deal with a proof failure in a forcing round
See forcing-round for a background discussion of the notion of forcing rounds. When a proof fails during a forcing round it means that the ``gist'' of the proof succeeded but some ``technical detail'' failed. The first question you must ask yourself is whether the forced goals are indeed theorems. We discuss the possibilities below.
If you believe the forced goals are theorems, you should follow the usual methodology for ``fixing'' failed ACL2 proofs, e.g., the identification of key lemmas and their timely and proper use as rules. See failure, see gag-mode, and see proof-tree.
The rules designed for the goals of forcing rounds are often just what is needed to prove the forced hypothesis at the time it is forced. Thus, you may find that when the system has been ``taught'' how to prove the goals of the forcing round no forcing round is needed. This is intended as a feature to help structure the discovery of the necessary rules.
If a hint must be provided to prove a goal in a forcing round, the
appropriate ``goal specifier'' (the string used to identify the goal to which
the hint is to be applied) is just the text printed on the line above the
If you solve a forcing problem by giving explicit hints for the goals of forcing rounds, you might consider whether you could avoid forcing the assumption in the first place by giving those hints in the appropriate places of the main proof. This is one reason that we print out the origins of each forced assumption. An argument against this style, however, is that an assumption might be forced in hundreds of places in the main goal and proved only once in the forcing round, so that by delaying the proof you actually save time.
We now turn to the possibility that some goal in the forcing round is not a theorem.
There are two possibilities to consider. The first is that the original theorem has insufficient hypotheses to ensure that all the forced hypotheses are in fact always true. The ``fix'' in this case is to amend the original conjecture so that it has adequate hypotheses.
A more difficult situation can arise and that is when the conjecture has sufficient hypotheses but they are not present in the forcing round goal. This can be caused by what we call ``premature'' forcing.
Because ACL2 rewrites from the inside out, it is possible that it will
force hypotheses while the context is insufficient to establish them.
Consider trying to prove
On the other hand, suppose we did not attack
Here, just for concreteness, is an example you can try. In this example,
(defun p1 (x) (not (rationalp x))) (defun p (x y)(if (rationalp x) (equal x y) (p1 x))) (defun foo (x) x) (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x))) (in-theory (disable foo))
The attempt then to do
Since all ``formulas'' are presented to the theorem prover as single terms
with no hypotheses (e.g., since implies is a function), this problem
would occur routinely were it not for the fact that the theorem prover expands
certain ``simple'' definitions immediately without doing anything that can
cause a hypothesis to be forced. See simple. This does not
solve the problem, since it is possible to hide the propositional structure
arbitrarily deeply. For example, one could define
Therefore, the problem remains: what do you do if an impossible goal is forced and yet you know that the original conjecture was adequately protected by hypotheses?
One alternative is to disable forcing entirely. See disable-forcing. Another is to disable the rule that caused the force.
A third alternative is to prove that the negation of the main goal implies the forced hypothesis. For example,
(defthm not-p-implies-rationalp (implies (not (p x (foo x))) (rationalp x)) :rule-classes nil)
Observe that we make no rules from this formula. Instead, we merely
(thm (p x (foo x)) :hints (("Goal" :use not-p-implies-rationalp)))
When we said, above, that
A fourth alternative is to weaken your desired theorem so as to make explicit the required hypotheses, e.g., to prove
(defthm rationalp-implies-main (implies (rationalp x) (p x (foo x))) :rule-classes nil)
This of course is unsatisfying because it is not what you originally intended. But all is not lost. You can now prove your main theorem from this one, letting the implies here provide the necessary case split.
(thm (p x (foo x)) :hints (("Goal" :use rationalp-implies-main)))