Force
Identity function used to force a hypothesis
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.
Note that the only time that ACL2 gives special treatment to calls of
force is when it is considering the hypotheses of a conditional rule, as
discussed above. In particular, when the rewriter encounters a subterm of the
goal currently being simplified, a call of force is not treated
specially. For example, if you provide a :use hint (see hints)
that replaces a goal G by the goal
(implies (implies (and ... (force HYP) ...)
concl)
G)
then the rewriter will not give any special treatment to (force
HYP). Instead, it will first rewrite HYP to, say, HYP'; and
then, using the fact that force is the identity function, the rewriter
will return HYP' as the rewritten value for (force HYP).
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 application
of type-prescription lemmas generally has fairly thorough knowledge of
the types of all terms (see type-prescription for relevant
background).
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. See type-reasoning for relevant
background for the following explanation. If type reasoning alone is
insufficient to prove some instance of a hypothesis, then the instance will
not be proved by type reasoning 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.
The discussion above may give the impression that a forcing round only
takes place because of a failure to relieve a forced hypothesis. A notable
exception, however, is due to linear-arithmetic. Consider the
following example:
(implies (not (equal 0 x))
(or (< 0 x) (< x 0)))
This is not a theorem; in particular, it fails when x is nil.
What is missing is the hypothesis, (acl2-numberp x). If you try to prove
the displayed formula above and you look at the proof using :pso,
you'll see the following.
But forced simplification reduces this to T, using the :executable-
counterpart of FORCE and linear arithmetic.
Thus, no specific rule created this forcing round (see also forcing-round). Rather, ACL2 was able to prove the goal using linear
arithmetic, but it needed to force the assumption that x is a number.
This is clear when we look at output for the forcing round:
[1]Goal, below, will focus on
(ACL2-NUMBERP X),
which was forced in
Goal'
by the linearization of
(EQUAL 0 X).
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.
Function: force
(defun force (x)
(declare (xargs :guard t))
x)
Subtopics
- Forcing-round
- A section of a proof dealing with forced assumptions
- Failed-forcing
- How to deal with a proof failure in a forcing round
- Immediate-force-modep
- When the executable-counterpart is enabled,
forced hypotheses are attacked immediately
- Disable-forcing
- To disallow forced case-splits
- Enable-forcing
- To allow forced case splits
- Disable-immediate-force-modep
- forced hypotheses are not attacked immediately
- Enable-immediate-force-modep
- forced hypotheses are attacked immediately
