Major Section: MISCELLANEOUS
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 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 formula, e.g., "[1]Subgoal *1/3''".
See goal-spec.
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 (p x (foo x)). We first rewrite the
formula in an empty context, i.e., assuming nothing. Thus, we
rewrite (foo x) in an empty context. If rewriting (foo x) forces
anything, that forced assumption will have to be proved in an empty
context. This will likely be impossible.
On the other hand, suppose we did not attack (foo x) until after we
had expanded p. We might find that the value of its second
argument, (foo x), is relevant only in some cases and in those cases
we might be able to establish the hypotheses forced by (foo x). Our
premature forcing is thus seen to be a consequence of our ``over
eager'' rewriting.
Here, just for concreteness, is an example you can try. In this
example, (foo x) rewrites to x but has a forced hypothesis of
(rationalp x). P does a case split on that very hypothesis
and uses its second argument only when x is known to be rational.
Thus, the hypothesis for the (foo x) rewrite is satisfied. On
the false branch of its case split, p simplies to (p1 x) which
can be proved under the assumption that x is not rational.
(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
(thm (p x (foo x))) forces the unprovable
goal (rationalp x).
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 p, above, recursively so that the test
that x is rational and the subsequent first ``real'' use of y
occurred arbitrarily deeply.
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
:use it in the subgoal where we must establish (rationalp x).
(thm (p x (foo x))
:hints (("Goal" :use not-p-implies-rationalp)))
When we said, above, that (p x (foo x)) is first rewritten in an
empty context we were misrepresenting the situation slightly. When
we rewrite a literal we know what literal we are rewriting and we
implicitly assume it false. This assumption is ``dangerous'' in
that it can lead us to simplify our goal to nil and give up -- we
have even seen people make the mistake of assuming the negation of
what they wished to prove and then via a very complicated series of
transformations convince themselves that the formula is false.
Because of this ``tail biting'' we make very weak use of the
negation of our goal. But the use we make of it is sufficient to
establish the forced hypothesis above.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)))
