FORCE

Major Section:  MISCELLANEOUS

Force is the identity function: (force x) is equal to x. However, for rules of many classes (see rule-classes), a hypothesis of the form (force term) is given special treatment, as described below. This treatment takes place for rule classes :rewrite, :linear, :type-prescription, :definition, :meta (actually in that case, the result of evaluating the hypothesis metafunction call), and :forward-chaining.

When a hypothesis of a conditional rule (of one of the classes listed above) has the form (force hyp), it is logically equivalent to hyp but has a pragmatic effect. In particular, when the rule is considered, the needed instance of the hypothesis, hyp', may be assumed if the usual process fails to prove it or its negation. In that situation, if the rule is eventually applied, then a special case is generated, requiring the system to prove that hyp' is true in the current context. The proofs of all such ``forced assumptions'' are, by default, delayed until the successful completion of the main goal. See forcing-round and see immediate-force-modep.

Forcing is generally used on hypotheses that are always expected to be true, as is commonly the case for guards of functions. All the power of the theorem prover is brought to bear on a forced hypothesis and no backtracking is possible. Forced goals can be attacked immediately (see immediate-force-modep) or in a subsequent forcing round (see forcing-round). Also see case-split for a related utility. If the :executable-counterpart of the function force is disabled, then no hypothesis is forced. For more on enabling and disabling forcing, see enable-forcing and see disable-forcing.

It sometimes happens that a conditional rule is not applied because some hypothesis, hyp, could not be relieved, even though the required instance of hyp, hyp', can be shown true in the context. This happens when insufficient resources are brought to bear on hyp' at the time we try to relieve it. A sometimes desirable alternative behavior is for the system to assume hyp', apply the rule, and to generate explicitly a special case to show that hyp' is true in the context. This is called ``forcing'' hyp. It can be arranged by restating the rule so that the offending hypothesis, hyp, is embedded in a call of force, as in (force hyp). By using the :corollary field of the rule-classes entry, a hypothesis can be forced without changing the statement of the theorem from which the rule is derived.

Technically, force is just a function of one argument that returns that argument. It is generally enabled and hence evaporates during simplification. But its presence among the hypotheses of a conditional rule causes case splitting to occur if the hypothesis cannot be conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is otherwise applicable, forcing should be used only on hypotheses that are expected always to be true.

A particularly common situation in which some hypotheses should be forced is in ``most general'' type-prescription lemmas. If a single lemma describes the ``expected'' type of a function, for all ``expected'' arguments, then it is probably a good idea to force the hypotheses of the lemma. Thus, every time a term involving the function arises, the term will be given the expected type and its arguments will be required to be of the expected type. In applying this advice it might be wise to avoid forcing those hypotheses that are in fact just type predicates on the arguments, since the routine that applies type-prescription lemmas has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing mechanism to interact with the ACL2 rewriter to establish the hypotheses of type-prescription rules. To understand this remark, think of the ACL2 type reasoning system as a rather primitive rule-based theorem prover for questions about Common Lisp types, e.g., ``does this expression produce a consp?'' ``does this expression produce some kind of ACL2 number, e.g., an integerp, a rationalp, or a complex-rationalp?'' etc. It is driven by type-prescription rules. To relieve the hypotheses of such rules, the type system recursively invokes itself. This can be done for any hypothesis, whether it is ``type-like'' or not, since any proposition, p, can be phrased as the type-like question ``does p produce an object of type nil?'' However, as you might expect, the type system is not very good at establishing hypotheses that are not type-like, unless they happen to be assumed explicitly in the context in which the question is posed, e.g., ``If p produces a consp then does p produce nil?'' If type reasoning alone is insufficient to prove some instance of a hypothesis, then the instance will not be proved by the type system and a type-prescription rule with that hypothesis will be inapplicable in that case. But by embedding such hypotheses in force expressions you can effectively cause the type system to ``punt'' them to the rest of the theorem prover. Of course, as already noted, this should only be done on hypotheses that are ``always true.'' In particular, if rewriting is required to establish some hypothesis of a type-prescription rule, then the rule will be found inapplicable because the hypothesis will not be established by type reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem. It is therefore possible that the type system will force a hypothesis that the rewriter could establish. Before a forced hypothesis is reported out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A type-prescription rule fails to apply because some true hypothesis is not being relieved. The user changes the rule so as to force the hypothesis. The system then applies the rule but reports no forcing. How can this happen? The type system ``punted'' the forced hypothesis to the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force when there is an if term present in the goal being simplified. Since and terms and or terms are merely abbreviations for if terms, they also prevent forcing. Note that if terms are ultimately eliminated using the ordinary flow of the proof (but see set-case-split-limitations), allowing force ultimately to function as intended. Moreover, forcing can be disabled, as described above; also see disable-forcing.