		Search-engine friendly clone of the ACL2 documentation.

Failed-forcing

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 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 simplifies 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)))