A section of a proof dealing with forced assumptions
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
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,
By delaying and collecting the
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,
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, ``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
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
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,