FORCING-ROUND

Major Section:  MISCELLANEOUS

If ACL2 ``forces'' some hypothesis of some rule to be true, it is obliged later to prove the hypothesis. See force. ACL2 delays the consideration of forced hypotheses until the main goal has been proved. It then undertakes a new round of proofs in which the main goal is essentially the conjunction of all hypotheses forced in the preceding proof. Call this round of proofs the ``Forcing Round.'' Additional hypotheses may be forced by the proofs in the Forcing Round. The attempt to prove these hypotheses is delayed until the Forcing Round has been successfully completed. Then a new Forcing Round is undertaken to prove the recently forced hypotheses and this continues until no hypotheses are forced. Thus, there is a succession of Forcing Rounds.

The Forcing Rounds are enumerated starting from 1. The Goals and Subgoals of a Forcing Round are printed with the round's number displayed in square brackets. Thus, "[1]Subgoal 1.3" means that the goal in question is Subgoal 1.3 of the 1st forcing round. To supply a hint for use in the proof of that subgoal, you should use the goal specifier "[1]Subgoal 1.3". See goal-spec.

When a round is successfully completed -- and for these purposes you may think of the proof of the main goal as being the 0th forcing round -- the system collects all of the assumptions forced by the just-completed round. Here, an assumption should be thought of as an implication, (implies context hyp), where context describes the context in which hyp was assumed true. Before undertaking the proofs of these assumptions, we try to ``clean them up'' in an effort to reduce the amount of work required. This is often possible because the forced assumptions are generated by the same rule being applied repeatedly in a given context.

For example, suppose the main goal is about some term (pred (xtrans i) i) and that some rule rewriting pred contains a forced hypothesis that the first argument is a good-inputp. Suppose that during the proof of Subgoal 14 of the main goal, (good-inputp (xtrans i)) is forced in a context in which i is an integerp and x is a consp. (Note that x is irrelevant.) Suppose finally that during the proof of Subgoal 28, (good-inputp (xtrans i)) is forced ``again,'' but this time in a context in which i is a rationalp and x is a symbolp. Since the forced hypothesis does not mention x, we deem the contextual information about x to be irrelevant and discard it from both contexts. We are then left with two forced assumptions: (implies (integerp i) (good-inputp (xtrans i))) from Subgoal 14, and (implies (rationalp i) (good-inputp (xtrans i))) from Subgoal 28. Note that if we can prove the assumption required by Subgoal 28 we can easily get that for Subgoal 14, since the context of Subgoal 28 is the more general. Thus, in the next forcing round we will attempt to prove just

(implies (rationalp i) (good-inputp (xtrans i)))

By delaying and collecting the forced assumptions until the completion of the ``main goal'' we gain two advantages. First, the user gets confirmation that the ``gist'' of the proof is complete and that all that remains are ``technical details.'' Second, by delaying the proofs of the forced assumptions ACL2 can undertake the proof of each assumption only once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were responsible for which forced assumptions, we print a sentence explaining the origins of each newly forced goal. For example,

[1]Subgoal 1, below, will focus on
(GOOD-INPUTP (XTRANS I)),
which was forced in
 Subgoal 14, above,
  by applying (:REWRITE PRED-CRUNCHER) to
  (PRED (XTRANS I) I),
 and
 Subgoal 28, above,
  by applying (:REWRITE PRED-CRUNCHER) to
  (PRED (XTRANS I) I).

In this entry, ``[1]Subgoal 1'' is the name of a goal which will be proved in the next forcing round. On the next line we display the forced hypothesis, call it x, which is (good-inputp (xtrans i)) in this example. This term will be the conclusion of the new subgoal. Since the new subgoal will be printed in its entirety when its proof is undertaken, we do not here exhibit the context in which x was forced. The sentence then lists (possibly a succession of) a goal name from the just-completed round and some step in the proof of that goal that forced x. In the example above we see that Subgoals 14 and 28 of the just-completed proof forced (good-inputp (xtrans i)) by applying (:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof steps applied to Subgoals 14 and 28 one would find the word ``forced'' (or sometimes ``forcibly'') occurring in the commentary. Whenever you see that word in the output, you know you will get a subsequent forcing round to deal with the hypotheses forced. Similarly, if at the beginning of a forcing round a rune is blamed for causing a force in some subgoal, inspection of the commentary for that subgoal will reveal the word ``forced'' after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier. When the simplifier encounters a hypothesis of the form (force hyp) it first attempts to establish it by rewriting hyp to, say, hyp'. If the truth or falsity of hyp' is known, forcing is not required. Otherwise, the simplifier actually forces hyp'. That is, the x mentioned above is hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals, it proceeds to the next forcing round, where those goals are individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to the global enabled structure. For example, suppose some rune, rune, is globally enabled. Suppose in some event you disable the rune at "Goal" and successfully prove the goal but force "[1]Goal". Then during the proof of "[1]Goal", rune is enabled ``again.'' The right way to think about this is that the rune is ``still'' enabled. That is, it is enabled globally and each forcing round resumes with the global enabled structure.