Free variables in rules

As described elsewhere (see rule-classes), ACL2 rules are
treated as implications for which there are zero or more hypotheses `rewrite` may look like
this:

(implies (and h1 ... hn) (fn lhs rhs))

Variables of *free* in the above
`let`/`let*`/*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

In general, the *free variables* of rules are those variables
occurring in their hypotheses (not `let`/`let*`/`linear` and `forward-chaining`, variables are bound by a trigger
term. (See rule-classes for a discussion of the `type-prescription`, variables are
bound by the

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.

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. Note that the

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

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

If instead `thm` would fail.

Next we describe in detail the steps used by the rewriter in dealing with free variables.

The ACL2 rewriter uses the following sequence of steps to relieve a
hypothesis with free variables, except that steps (1) and (3) are skipped for

(1) Suppose the hypothesis has the form

(equiv var term) wherevar is free and no variable ofterm is free, and eitherequiv isequalor elseequiv is a known equivalence relation andterm is a call ofdouble-rewrite. We call this a ``binding hypothesis.'' Then bindvar to the result of rewritingterm in 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) , wherelhs has no variables (other than those bound bylet,let*, orlambda ),rhs is known to be true in the current context, andequiv is typicallyequal but can be any equivalence relation appropriate for the current context (see congruence); then attempt to bind the free variables so that the instantiated hypothesis islhs .

For cases (2) and (3), the first instance found may ultimately fail because
the remaining hypotheses are not all relieved under the extended bindings. In
that case, should the attempt to relieve hypotheses fail, or should the search
continue to find other instances for (2) or (3)? The answer depends on which
of two options is in force for the so-called ``match-free'' of the rule.
Below we discuss how to specify these two options as ``

Suppose that the original hypothesis is a call of `force` or `case-split`, where forcing is enabled (see enable-forcing) . Also
suppose that one of the following two cases applies: no instances are found for
(2) and also none for (3), or else the ``match-free'' option for the rule is

Is it better to specify

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

(implies (and (p1 x y) (p2 x y)) (equal (bar x) (bar-prime x)))

may never succeed if

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

(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

(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

- Add-match-free-override
- Set
:match-free value to:once or:all in existing rules - Set-match-free-default
- Provide default for
:match-free in future rules - Free-variables-type-prescription
- Matching for free variable in type-prescription rules
- Set-match-free-error
- Control error vs. warning when
:match-free is missing - Free-variables-examples
- Examples pertaining to free variables in rules