BIND-FREE

Major Section:  MISCELLANEOUS

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)))))

Some Related Topics

• BIND-FREE-EXAMPLES -- examples pertaining to bind-free hypotheses

General Forms:

(BIND-FREE term var-list)
(BIND-FREE term t)
(BIND-FREE term)

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 occuring 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 may use state. 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)))

(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)))).

(RATIONALP (binary-+ '3
                      (binary-+ (expt a n) (foo a c)))).

(FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
                                      (binary-+ (expt a n) (foo a c)))
                          '(binary-+ (bar b) (expt a n))).

((X . (EXPT A N))
 (LHS . (binary-+ '3
                   (binary-+ (expt a n) (foo a c))))
 (RHS . (binary-+ (bar b) (expt a n)))),

(EQUAL (+ (- X) LHS) (+ (- X) RHS))
==>
(EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
       (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

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 or a list of variables. If it is not provided, it defaults to t. If it is a 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 the list of variables. We strongly recommend the use of this list of variables, as it allows some consistency checks to be performed at the time of the rule's admittance which are not possible otherwise.

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)))

(defaxiom p2-instance
  (p2 v (cons v 4)))

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)))))

(defthm p2-implies-p1-better
  (implies (and (bind-free (my-alists x)
                           (y)) ; the second argument, (y), is optional
                (p2 x y))
           (p1 x)))

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.