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.
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.
