free variables in rules
Major Section:  RULE-CLASSES


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



See free-variables-examples for examples of how this all works, including illustration of how the user can exercise some control over it.

(defstub p2 (x y) t)







The ACL2 rewriter uses the following sequence of steps to relieve hypotheses with free variables. (1) If the hypothesis has the form (equal var term) where var is free and no variable of term is free, then bind var to the result of rewriting term 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), where lhs has no variables (other than those bound by let, let*, or lambda), rhs is known to be true in the current context, and equiv is typically equal 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 is lhs. If all attempts fail and the hypothesis is a call of force or 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.




(implies (and (p1 x y)
              (p2 x y))


(implies (and (rationalp y)
              (foo x y))
(implies (and (foo x y)
              (rationalp y))


                                  ; behavior is local to a book)
                                  ; :match-free :once regardless of their
                                  ; original :match-free fields
                                  ; the two indicated rules are treated as
                                  ; :match-free :once regardless of their
                                  ; original :match-free fields


Interaction with the break-rewrite utility. You may find that the break-rewrite utility (see break-rewrite) gives surprising error messages such as the following when a hypothesis has free variables.

:HYP 1 contains a free variable that we could not bind appropriately.
See :DOC free-variables.
What may be surprising is that the hypothesis being ``blamed'' (in this case, 1) is not the one that you imagine is failing. Consider the following example.
(defstub p (x) t)

(defaxiom p-closed (implies (and (p y) (< x y)) (p x)) :rule-classes ((:rewrite :match-free :all)))

:brr t

:monitor (:rewrite p-closed) t

Below is an ACL2 transcript illustrating this issue. In that proof attempt, ACL2 does successfully bind the free variable y of rule p-closed to a. However, it is then unable to relieve the second hypothesis of p-closed, namely (< x y), where x is bound to a and y is bound to (* a a). The rewriter then backtracks to look for new potential bindings of y besides a, and is unable to find any. So it blames the failure on the first hypothesis rather than on the second. (Even if :match-free :once had been specified, the result would be the same. More information may be provided in future releases, especially if users express a need for improvement.)

ACL2 !>(thm (implies (and (integerp a) (< 1 a) (p (* a a)))
                     (p a)))


(1 Breaking (:REWRITE P-CLOSED) on (P A): 1 ACL2 >:eval 1x (:REWRITE P-CLOSED) failed because :HYP 1 contains a free variable that we could not bind appropriately. See :DOC free-variables. 1 ACL2 >

Incidentally, if one proves the rule
(defthm helper (implies (and (integerp a) (< 1 a)) (< a (* a a))))
then the above theorem can be proved by ACL2.