Major Section: RULE-CLASSES
As described elsewhere (see rule-classes), ACL2 rules are treated as
implications for which there are zero or more hypotheses
hj to prove. In
particular, rules of class
rewrite may look like this:
(implies (and h1 ... hn) (fn lhs rhs))Variables of
hiare said to occur free in the above
:rewriterule if they do not occur in
lhsor in any
j<i. (To be precise, here we are only discussing those variables that are not in the scope of a
lambdathat binds them.) We also refer to these as the free variables of the rule. ACL2 may issue a warning or error when there are free variables in a rule, as described below. (Variables of
rhsmay be considered free if they do not occur in
lhsor in any
hj. But we do not consider those in this discussion.)
In general, the free variables of rules are those variables occurring in
their hypotheses (not
lambda-bound) that are not
bound when the rule is applied. For rules of class
forward-chaining, variables are bound by a trigger term.
(See rule-classes for a discussion of the
:trigger-terms field). For
rules of class
type-prescription, variables are bound by the
Let us discuss the method for relieving hypotheses of rewrite rules with free variables. Similar considerations apply to linear and forward-chaining rules, and type-prescription rules.
See free-variables-examples for more examples of how this all works, including illustration of how the user can exercise some control over it. In particular, see free-variables-examples-rewrite for an explanation of output from the break-rewrite facility in the presence of rewriting failures involving free variables, as well as an example exploring ``binding hypotheses'' as described below.
Note that the
:match-free mechanism discussed below does not apply to
type-prescription rules. See free-variables-type-prescription for a
discussion of how to control free-variable matchng for type-prescription
We begin with an example. Does the proof of the
thm below succeed?
(defstub p2 (x y) t) (defaxiom p2-trans (implies (and (p2 x y) (p2 y z)) (equal (p2 x z) t)) :rule-classes ((:rewrite :match-free :all))) (thm (implies (and (p2 a c) (p2 a b) (p2 c d)) (p2 a d)))Consider what happens when the proof of the
thmis attempted. The ACL2 rewriter attempts to apply rule
p2-transto the conclusion,
(p2 a d). So, it binds variables
zfrom the left-hand side of the conclusion of
d, respectively, and then attempts to relieve the hypotheses of
p2-trans. The first hypothesis of
(p2 x y), is considered first. Variable
yis free in that hypothesis, i.e., it has not yet been bound. Since
xis bound to
a, the rewriter looks through the context for a binding of
(p2 a y)is true, and it so happens that it first finds the term
(p2 a b), thus binding
b. Now it goes on to the next hypothesis,
(p2 y z). At this point
zhave already been bound to
(p2 b d)cannot be proved.
So, in order for the proof of the
thm to succeed, the rewriter needs to
backtrack and look for another way to instantiate the first hypothesis of
:match-free :all has been specified, backtracking
does take place. This time
y is bound to
c, and the subsequent
instantiated hypothesis becomes
(p2 c d), which is true. The application
(p2-trans) succeeds and the theorem is proved.
:match-free :all had been replaced by
:match-free :once in
p2-trans, then backtracking would not occur, and the proof of the
thm would fail.
Next we describe in detail the steps used by the rewriter in dealing with free variables.
ACL2 uses the following sequence of steps to relieve a hypothesis with free
variables, except that steps (1) and (3) are skipped for
:forward-chaining rules and step (3) is skipped for
:type-prescription rules. First, if the hypothesis is of the form
(force hyp0) or
(case-split hyp0), then replace it with
(1) Suppose the hypothesis has the form
(equiv var term)where
varis free and no variable of
termis free, and either
equivis a known equivalence relation and
termis a call of
double-rewrite. We call this a ``binding hypothesis.'' Then bind
varto the result of rewriting
termin the current context.
(2) Look for a binding of the free variables of the hypothesis so that the corresponding instance of the hypothesis is known to be true in the current context.
(3) Search all
enabled, hypothesis-free rewrite rules of the form
(equiv lhs rhs), where
lhshas no variables (other than those bound by
rhsis known to be true in the current context, and
equalbut can be any equivalence relation appropriate for the current context (see congruence); then attempt to bind the free variables so that the instantiated hypothesis is
If all attempts fail and the original hypothesis is a call of
case-split, where forcing is enabled (see force) then the hypothesis
is relieved, but in the split-off goals, all free variables are bound to
unusual names that call attention to this odd situation.
When a rewrite or linear rule has free variables in the hypotheses,
the user generally needs to specify whether to consider only the first
instance found in steps (2) and (3) above, or instead to consider them all.
Below we discuss how to specify these two options as ``
:all'' (the default), respectively.
Is it better to specify
:all? We believe that
generally the better choice because of its greater power, provided the user
does not introduce a large number of rules with free variables, which has
been known to slow down the prover due to combinatorial explosion in the
search (Steps (2) and (3) above).
Either way, it is good practice to put the ``more substantial'' hypotheses
first, so that the most likely bindings of free variables will be found first
(in the case of
:all) or found at all (in the case of
example, a rewrite rule like
(implies (and (p1 x y) (p2 x y)) (equal (bar x) (bar-prime x)))may never succeed if
p1is nonrecursive and enabled, since we may well not find calls of
p1in the current context. If however
p2is disabled or recursive, then the above rule may apply if the two hypotheses are switched. For in that case, we can hope for a match of
(p2 x y)in the current context that therefore binds
y; then the rewriter's full power may be brought to bear to prove
(p1 x y)for that
Moreover, the ordering of hypotheses can affect the efficiency of the rewriter. For example, the rule
(implies (and (rationalp y) (foo x y)) (equal (bar x) (bar-prime x)))may well be sub-optimal. Presumably the intention is to rewrite
(bar-prime x)in a context where
(foo x y)is explicitly known to be true for some rational number
ywill be bound first to the first term found in the current context that is known to represent a rational number. If the 100th such
ythat is found is the first one for which
(foo x y)is known to be true, then wasted work will have been done on behalf of the first 99 such terms
:oncehas been specified, in which case the rule will simply fail after the first binding of
(rationalp y)is known to be true. Thus, a better form of the above rule is almost certainly the following.
(implies (and (foo x y) (rationalp y)) (equal (bar x) (bar-prime x)))
Specifying `once' or `all'.
As noted above, the following discussion applies only to rewrite, linear, and forward-chaining rules. See free-variables-type-prescription for a discussion of analogous considerations for type-prescription rules.
One method for specifying
:all for free-variable matching is
to provide the
:match-free field of the
:rule-classes of the rule,
(:rewrite :match-free :all). See rule-classes. However,
there are global events that can be used to specify
see set-match-free-default and see add-match-free-override. Here are some
(set-match-free-default :once) ; future rules without a :match-free field ; are stored as :match-free :once (but this ; behavior is local to a book) (add-match-free-override :once t) ; existing rules are treated as ; :match-free :once regardless of their ; original :match-free fields (add-match-free-override :once (:rewrite foo) (:rewrite bar . 2)) ; the two indicated rules are treated as ; :match-free :once regardless of their ; original :match-free fields
Some history. Before Version 2.7 the ACL2 rewriter performed Step (2)
above first. More significantly, it always acted as though
been specified. That is, if Step (2) did not apply, then the rewriter took
the first binding it found using either Steps (1) or (3), in that order, and
proceeded to relieve the remaining hypotheses without trying any other
bindings of the free variables of that hypothesis.