Bind-free
To bind free variables of a rewrite, definition, or linear rule
Examples:
(IMPLIES (AND (RATIONALP LHS)
(RATIONALP RHS)
(BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
(EQUAL (EQUAL LHS RHS)
(EQUAL (+ (- X) LHS) (+ (- X) RHS))))
(IMPLIES (AND (BIND-FREE
(FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE)
(X))
(RATIONALP X)
(CASE-SPLIT (NOT (EQUAL X 0))))
(EQUAL (< LHS RHS)
(IF (< 0 X)
(< (* (/ X) LHS) (* (/ X) RHS))
(< (* (/ X) RHS) (* (/ X) LHS)))))
General Forms:
(BIND-FREE term var-list)
(BIND-FREE term t)
(BIND-FREE term)
A rule which uses a bind-free hypothesis has similarities to both a
rule which uses a syntaxp hypothesis and to a :meta rule.
Bind-free is like syntaxp, in that it logically always returns
t but may affect the application of a :rewrite, :rewrite-quoted-constant, :definition, or :linear
rule when it is called at the top-level of a hypothesis. It is like a
:meta rule, in that it allows the user to perform transformations
of terms under programmatic control.
Note that a bind-free hypothesis does not, in general, deal with the
meaning or semantics or values of the terms, but rather with their syntactic
forms. Before attempting to write a rule which uses bind-free, the user
should be familiar with syntaxp and the internal form that ACL2 uses
for terms. This internal form is similar to what the user sees, but there are
subtle and important differences. Trans can be used to view this
internal form.
Just as for a syntaxp hypothesis, there are two basic types of
bind-free hypotheses. The simpler type of bind-free hypothesis may
be used as the nth hypothesis in a :rewrite, :definition, or :linear rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided term
is a term, term contains at least one variable, and every variable
occurring freely in term occurs freely in lhs or in some hypi,
i<n. In addition, term must not use any stobjs. Later below we
will describe the second type, an extended bind-free hypothesis,
which is similar except that it may use state and mfc.
Whether simple or extended, a bind-free hypothesis may return an alist
that binds free variables, as explained below, or it may return a list of such
alists. We focus on the first of these cases: return of a single binding
alist. We conclude our discussion with a section that covers the other case:
return of a list of alists.
We begin our description of bind-free by examining the first example
above in some detail.
We wish to write a rule which will cancel ``like'' addends from both sides
of an equality. Clearly, one could write a series of rules such as
(DEFTHM THE-HARD-WAY-2-1
(EQUAL (EQUAL (+ A X B)
(+ X C))
(EQUAL (+ A B)
(FIX C))))
with one rule for each combination of positions the matching addends might
be found in (if one knew before-hand the maximum number of addends that would
appear in a sum). But there is a better way. (In what follows, we assume the
presence of an appropriate set of rules for simplifying sums.)
Consider the following definitions and theorem:
(DEFUN INTERSECTION-EQUAL (X Y)
(COND ((ENDP X)
NIL)
((MEMBER-EQUAL (CAR X) Y)
(CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y)))
(T
(INTERSECTION-EQUAL (CDR X) Y))))
(DEFUN PLUS-LEAVES (TERM)
(IF (EQ (FN-SYMB TERM) 'BINARY-+)
(CONS (FARGN TERM 1)
(PLUS-LEAVES (FARGN TERM 2)))
(LIST TERM)))
(DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS)
(IF (AND (EQ (FN-SYMB LHS) 'BINARY-+)
(EQ (FN-SYMB RHS) 'BINARY-+))
(LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS)
(PLUS-LEAVES RHS))))
(IF COMMON-ADDENDS
(LIST (CONS 'X (CAR COMMON-ADDENDS)))
NIL))
NIL))
(DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL
(IMPLIES (AND (RATIONALP LHS)
(RATIONALP RHS)
(BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
(EQUAL (EQUAL LHS RHS)
(EQUAL (+ (- X) LHS) (+ (- X) RHS)))))
How is this rule applied to the following term?
(equal (+ 3 (expt a n) (foo a c))
(+ (bar b) (expt a n)))
As mentioned above, the internal form of an ACL2 term is not always what
one sees printed out by ACL2. In this case, by using :trans one
can see that the term is stored internally as
(equal (binary-+ '3
(binary-+ (expt a n) (foo a c)))
(binary-+ (bar b) (expt a n))).
When ACL2 attempts to apply cancel-matching-addends-equal to the term
under discussion, it first forms a substitution that instantiates the
left-hand side of the conclusion so that it is identical to the target term.
This substitution is kept track of by the substitution alist:
((LHS . (binary-+ '3
(binary-+ (expt a n) (foo a c))))
(RHS . (binary-+ (bar b) (expt a n)))).
ACL2 then attempts to relieve the hypotheses in the order they were given.
Ordinarily this means that we instantiate each hypothesis with our
substitution and then attempt to rewrite the resulting instance to true.
Thus, in order to relieve the first hypothesis, we rewrite:
(RATIONALP (binary-+ '3
(binary-+ (expt a n) (foo a c)))).
Let us assume that the first two hypotheses rewrite to t. How do we
relieve the bind-free hypothesis? Just as for a syntaxp
hypothesis, ACL2 evaluates (find-match-in-plus-nests lhs rhs) in an
environment where lhs and rhs are instantiated as determined by the
substitution. In this case we evaluate
(FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
(binary-+ (expt a n) (foo a c)))
'(binary-+ (bar b) (expt a n))).
Observe that, just as in the case of a syntaxp hypothesis, we
substitute the quotation of the variables bindings into the term to be
evaluated. See syntaxp for the reasons for this. The result of this
evaluation, ((X . (EXPT A N))), is then used to extend the substitution
alist:
((X . (EXPT A N))
(LHS . (binary-+ '3
(binary-+ (expt a n) (foo a c))))
(RHS . (binary-+ (bar b) (expt a n)))),
and this extended substitution determines
cancel-matching-addends-equal's result:
(EQUAL (+ (- X) LHS) (+ (- X) RHS))
==>
(EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
(+ (- (EXPT A N)) (BAR B) (EXPT A N))).
Question: What is the internal form of this result?
Hint: Use :trans.
When this rule fires, it adds the negation of a common term to both sides
of the equality by selecting a binding for the otherwise-free variable x,
under programmatic control. Note that other mechanisms such as the binding of
free-variables may also extend the substitution alist.
Just as for a syntaxp test, a bind-free form signals failure
by returning nil. However, while a syntaxp test signals success
by returning true, a bind-free form signals success by returning an alist
which is used to extend the current substitution alist. Because of this use
of the alist, there are several restrictions on it — in particular the
alist must only bind variables, these variables must not be already bound by
the substitution alist, and the variables must be bound to ACL2 terms. If
term returns an alist and the alist meets these restrictions, we append
the alist to the substitution alist and use the result as the new current
substitution alist. This new current substitution alist is then used when we
attempt to relieve the next hypothesis or, if there are no more, instantiate
the right hand side of the rule.
There is also a second, optional, var-list argument to a
bind-free hypothesis. If provided, it must be either t, nil,
or a non-empty list of variables. If it is not provided, it defaults to
t; and it is also treated as t if the value provided is nil.
If it is a non-empty list of variables, this second argument is used to place
a further restriction on the possible values of the alist to be returned by
term: any variables bound in the alist must be present in that list of
variables. We strongly recommend the use of this list of variables, as that
list is considered to contribute to the list of variables in the hypotheses of
a linear rule; see linear, in particular condition (b) mentioned there
regarding a requirement that maximal terms and hypotheses must suffice for
instantiating all the variables in the conclusion. If var-list is t
(either explicitly or implicitly, as described above), then that condition is
considered to be met trivially; this could prevent ACL2 from rejecting
ineffective linear rules.
An extended bind-free hypothesis is similar to the simple type
described above, but it uses two additional variables, mfc and
state, which must not be bound by the left hand side or an earlier
hypothesis of the rule. They must be the last two variables mentioned by
term: first mfc, then state. These two variables give access
to the functions mfc-xxx; see extended-metafunctions. As
described there, mfc is bound to the so-called metafunction-context and
state to ACL2's state. See bind-free-examples for
examples of the use of these extended bind-free hypotheses.
SECTION: Returning a list of alists.
As promised above, we conclude with a discussion of the case that
evaluation of the bind-free term produces a list of alists, x,
rather than a single alist. In this case each member b of x is
considered in turn, starting with the first and proceeding through the list.
Each such b is handled exactly as discussed above, as though it were the
result of evaluating the bind-free term. Thus, each b extends the
current variable binding alist, and all remaining hypotheses are then
relieved, as though b had been the value obtained by evaluating the
bind-free term. As soon as one such b leads to successful relieving
of all remaining hypotheses, the process of relieving hypotheses concludes, so
no further members of x are considered.
We illustrate with a simple pedagogical example. First introduce functions
p1 and p2 such that a rewrite rule specifies that p2 implies
p1, but with a free variable.
(defstub p1 (x) t)
(defstub p2 (x y) t)
(defaxiom p2-implies-p1
(implies (p2 x y)
(p1 x)))
If we add the following axiom, then (p1 x) follows logically for all
x.
(defaxiom p2-instance
(p2 v (cons v 4)))
Unfortunately, evaluation of (thm (p1 a)) fails, because ACL2 fails to
bind the free variable y in order to apply the rule p2-instance.
Let's define a function that produces a list of alists, each binding the
variable y. Of course, we know that only the middle one below is
necessary in this simple example. In more complex examples, one might use
heuristics to construct such a list of alists.
(defun my-alists (x)
(list (list (cons 'y (fcons-term* 'cons x ''3)))
(list (cons 'y (fcons-term* 'cons x ''4)))
(list (cons 'y (fcons-term* 'cons x ''5)))))
The following rewrite rule uses bind-free to return a list of
candidate alists binding y.
(defthm p2-implies-p1-better
(implies (and (bind-free (my-alists x)
(y)) ; the second argument, (y), is optional
(p2 x y))
(p1 x)))
Now the proof succeeds for (thm (p1 a)). Why? When ACL2 applies the
rewrite rule p2-implies-p1-better, it evaluates my-alists, as
we can see from the following trace, to bind y in three different
alists.
ACL2 !>(thm (p1 a))
1> (ACL2_*1*_ACL2::MY-ALISTS A)
<1 (ACL2_*1*_ACL2::MY-ALISTS (((Y CONS A '3))
((Y CONS A '4))
((Y CONS A '5))))
Q.E.D.
The first alist, binding y to (cons a '3), fails to allow the
hypothesis (p2 x y) to be proved. But the next binding of y, to
(cons a '4), succeeds: then the current binding alist is ((x . a) (y
. (cons a '4))), for which the hypothesis (p2 x y) rewrites to true
using the rewrite rule p2-instance.
Subtopics
- Bind-free-examples
- Examples pertaining to bind-free hypotheses
