		Search-engine friendly clone of the ACL2 documentation.

Free-variables-examples

Free-variables-examples-rewrite

Examples pertaining to free variables in rewrite rules

The following examples illustrate ACL2's handling of free variables in rewrite rules, as well as user control over how such free variables are handled. See free-variables for a background discussion.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Example 1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defstub p2 (x y) t) ; introduce unconstrained function

; Get warning because of free variable.  This would be an error if you had
; first executed (set-match-free-error t) in order to force yourself to
; specify :match-free (illustrated later, below).
(defaxiom p2-trans
  (implies (and (p2 x y)
                (p2 y z))
           (p2 x z)))

; Succeeds.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

; The following causes an error because p2-trans is not a rune.
(add-match-free-override :once p2-trans)

; After the following, the rewrite rule p2-trans will only allow one
; attempt per hypothesis to bind free variables.
(add-match-free-override :once (:rewrite p2-trans))

; Now this same theorem fails to be proved.  Here's why.  The
; context for proving (p2 a d) happens to include the hypotheses in
; reverse order.  So when the first hypothesis of p2-trans, namely
; (p2 x y), is relieved, where x is bound to a (as we are attempting
; to rewrite the current literal (p2 a d)), we find (p2 a b) in the
; context before (p2 a c) and hence y is bound to b.  The
; instantiated second hypothesis of p2-trans is thus (p2 b d), and
; the proof fails.  Before the add-match-free-override form above,
; the proof succeeded because the rewriter was allowed to backtrack
; and find the other binding for the first hypothesis of p2-trans,
; namely, y bound to c.  Then the instantiated second hypothesis of
; p2-trans is (p2 c d), which is known to be true in the current
; context.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

; Return to original behavior for binding free variables.
(add-match-free-override :all t)

; Succeeds once again.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

(u) ; undo (add-match-free-override :all t)

; This is an error, since no further arguments should appear after
; :clear.
(add-match-free-override :clear t)

; Return all rules to original behavior for binding free variables,
; regardless of which previous add-match-free-override forms have
; been executed.
(add-match-free-override :clear)

; This succeeds just as it did originally.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

(ubt! 'p2-trans) ; back to the start, except retain the defstub

; Require that :match-free be specified for :linear and :rewrite rules with
; free variables.
(set-match-free-error t)

; Fails because :match-free is missing.
(defaxiom p2-trans
  (implies (and (p2 x y)
                (p2 y z))
           (p2 x z)))

; Fails because :match-free must be followed by :once or :all.
(defaxiom p2-trans
  (implies (and (p2 x y)
                (p2 y z))
           (p2 x z))
  :rule-classes ((:rewrite :match-free nil)))

; Succeeds, this time with no warning at all.
(defaxiom p2-trans
  (implies (and (p2 x y)
                (p2 y z))
           (p2 x z))
  :rule-classes ((:rewrite :match-free :once)))

; Fails because we only bind once (see earlier long comment).
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

; Treat p2-trans as though `:match-free :all' had been specified.
(add-match-free-override :all (:rewrite p2-trans))

; Succeeds since more than one binding is allowed for p2-trans.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

(u)
(u)

; Specify that future :linear and :rewrite rules with free variables
; that do not have :match-free specified are treated as though
; `:match-free :once' were specified.
(set-match-free-default :once)

; Succeeds without error since `:match-free' is specified, as described
; above.  But there is a warning, since :match-free is not specified for this
; :rewrite rule.
(defaxiom p2-trans
  (implies (and (p2 x y)
                (p2 y z))
           (p2 x z)))

; Fails since only single bindings are allowed for p2-trans.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

; Treat p2-trans as though `:match-free :all' had been specified.
(add-match-free-override :all t)

; Succeeds.
(thm (implies (and (p2 a c)
                   (p2 a b)
                   (p2 c d))
              (p2 a d)))

; Test searching of ground units, i.e. rewrite rules without variables on the
; left side of the conclusion, for use in relieving hypotheses with free
; variables.  This is a very contrived example.

(ubt! 1) ; back to the start

(encapsulate
 (((p1 *) => *)
  ((p2 * *) => *)
  ((p3 *) => *)
  ((a) => *)
  ((b) => *))
 (local (defun p1 (x) x))
 (local (defun p2 (x y) (list x y)))
 (local (defun p3 (x) x))
 (local (defun a () 0))
 (local (defun b () 0)))

; Allow default of :match-free :all (form may be omitted).
(set-match-free-error nil)

(defaxiom ax1
  (implies (and (p2 x y)
                (p1 y))
           (p3 x)))

(defaxiom p2-a-b
  (p2 (a) (b)))

(defaxiom p2-a-a
  (p2 (a) (a)))

(defaxiom p1-b
  (p1 (b)))

; Succeeds; see long comment below on next attempt to prove this
; theorem.
(thm (implies (p2 (a) y)
              (p3 (a))))

; Now ax1 will only relieve hypothesis (p2 x y) for one binding of y:
(add-match-free-override :once t)

; Fails when ax1 attempts to rewrite the conclusion to true, because
; the most recent ground unit for hypothesis (p2 x y) with x bound
; to (a) is rule p2-a-a, which binds y to (a).  If more than one ground
; unit could be used then we would backtrack and apply rule p2-a-b,
; which binds y to (b) and hence hypothesis (p1 y) of ax1 is
; relieved by rule p1-b.
(thm (implies (p2 (a) y)
              (p3 (a))))

; Return rules to original :match-free behavior.
(add-match-free-override :clear)

; Succeeds once again.
(thm (implies (p2 (a) y)
              (p3 (a))))

; Just for kicks, change the behavior of a built-in rule irrelevant
; to the proof at hand.
(add-match-free-override :once (:rewrite string<-l-trichotomy))

; Still succeeds.
(thm (implies (p2 (a) y)
              (p3 (a))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Example 2
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The next example illustrates the use of the break-rewrite facility to get information about handling of free variables by the rewriter. Explanation is given after this (edited) transcript. Input begins on lines with a prompt (search for ``ACL2''); the rest is output.

ACL2 !>(encapsulate
        ((p1 (u x) t)
         (bad (x) t)
         (p2 (x y z) t)
         (bar (x y) t)
         (foo (x y) t)
         (poo (x y) t)
         (prop (u) t))

        (local (defun p1 (u x) (declare (ignore u x)) nil))
        (local (defun bad (x) (declare (ignore x)) nil))
        (local (defun p2 (x y z) (declare (ignore x y z)) nil))
        (local (defun bar (x y) (declare (ignore x y)) nil))
        (local (defun foo (x y) (declare (ignore x y)) nil))
        (local (defun poo (x y) (declare (ignore x y)) nil))
        (local (defun prop (u) (declare (ignore u)) t))

        (defthm foo-poo
          (implies (syntaxp (equal y 'y3))
                   (equal (foo x y)
                          (poo x y))))

        (defthm lemma-1
          (implies (and (p1 u x)
                        (bad x)
                        (p2 x y z)
                        (bar x y)
                        (equal x x) ; admittedly silly!
                        (foo x y))
                   (prop u))
          :rule-classes ((:rewrite :match-free :all))))

; [[ output omitted ]]

Summary
Form:  ( ENCAPSULATE ((P1 ...) ...) ...)
Rules: NIL
Warnings:  Subsume and Non-rec
Time:  0.08 seconds (prove: 0.00, print: 0.01, other: 0.06)
 T
ACL2 !>:brr t
The monitored runes are:
NIL
 T
ACL2 !>:monitor (:rewrite lemma-1) t
(((:REWRITE LEMMA-1) 'T))
ACL2 !>(thm (implies (and (p1 u0 x1)
                          (bad x1)
                          (bad x3)
                          (bar x3 y1)
                          (bar x3 y3)
                          (p1 u0 x2)
                          (p1 u0 x3)
                          (p2 x3 y1 z1)
                          (p2 x3 y3 z1))
                     (prop u0)))

(1 Breaking (:REWRITE LEMMA-1) on (PROP U0):
1 ACL2 >:eval

1x (:REWRITE LEMMA-1) failed because :HYP 1 contains free variables.
The following display summarizes the attempts to relieve hypotheses
by binding free variables; see :DOC free-variables.

    [1] X : X1
Failed because :HYP 3 contains free variables Y and Z, for which no
suitable bindings were found.
    [1] X : X2
Failed because :HYP 2 rewrote to (BAD X2).
    [1] X : X3
        [3] Z : Z1
            Y : Y1
Failed because :HYP 6 rewrote to (FOO X3 Y1).
        [3] Z : Z1
            Y : Y3
Failed because :HYP 6 rewrote to (POO X3 Y3).

1 ACL2 >:unify-subst
     U : U0
1 ACL2 >

The :eval command above asks the rewriter to attempt to apply the rewrite rule lemma-1 to the term (prop u0), shown just above the line with :eval. As we can see at the end, the variable u in the conclusion of lemma-1 is being bound to the variable u0 in the conjecture. The first hypothesis of lemma-1 is (p1 u x), so the rewriter looks for some x for which (p1 u0 x) is known to be true. It finds x1, and then goes on to consider the second hypothesis, (bad x). Since the theorem we are proving has (bad x1) in the hypothesis and x is currently bound to x1, the rewriter is satisfied and moves on to the third hypothesis of lemma-1, (p2 x y z). However, x is bound to x1 and there are no instances of y and z for which (p2 x1 y z) is known in the current context. All of the above analysis is summarized in the first part of the output from :eval above:

    [1] X : X1
Failed because :HYP 3 contains free variables Y and Z, for which no
suitable bindings were found.

Thus, the binding of x to x1 on behalf of the first hypothesis has failed.

The rewriter now backs up to look for other values of x that satisfy the first hypothesis, and finds x2 because our current theorem has a hypothesis of (p1 u0 x2). But this time, the second hypothesis of lemma-1, (bad x), is not known to be true for x; that is, (bad x2) does not rewrite to t; in fact, it rewrites to itself. That explains the next part of the output from :eval above:

    [1] X : X2
Failed because :HYP 2 rewrote to (BAD X2).

The rewriter now backs up again to look for other values of x that satisfy the first hypothesis, and finds x3 because our current theorem has a hypothesis of (p1 u0 x3). This time, the second hypothesis of lemma-1 is not a problem, and moreover, the rewriter is able to bind y and z to y1 and z1, respectively, in order to satisfy the third hypothesis, (p2 x y z): that is, (p2 x2 y1 z1) is known in the current context. That explains more of the above output from :eval:

[1] X : X3
    [3] Z : Z1
        Y : Y1

Unfortunately, the sixth hypothesis, (foo x y), rewrites to itself under the above bindings:

Failed because :HYP 6 rewrote to (FOO X3 Y1).

So the rewriter looks for other bindings to satisfy the third hypothesis and finds these.

[3] Z : Z1
    Y : Y3

This time, the sixth hypothesis can be rewritten under the above bindings, from (foo x3 y3) to (poo x3 y3) by lemma foo-poo, but still not to t.

Failed because :HYP 6 rewrote to (POO X3 Y3).

There are no more free variable bindings to try, so this concludes the output from :eval.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Example 3
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The next pair of examples illustrates so-called ``binding hypotheses'' (see free-variables) and explores some of their subtleties. The first shows binding hypotheses in action on a simple example. The second shows how binding hypotheses interact with equivalence relations and explains the role of double-rewrite.

Our first example sets up a theory with two user-supplied rewrite rules, one of which has a binding hypothesis. Below we explain how that binding hypothesis contributes to the proof.

; Define some unary functions.
(defun f (x) (declare (ignore x)) t)
(defun g (x) x)
(defun h (x) x)
(defun k (x) x)

; Prove some simple lemmas.  Note the binding hypothesis in g-rewrite.
(defthm f-k-h
  (f (k (h x))))
(defthm g-rewrite
       (implies (and (equal y (k x)) ; binding hypothesis
                     (f y))
                (equal (g x) y)))

; Restrict to a theory that includes the above lemmas but avoids the above
; definitions.
(in-theory (union-theories (theory 'minimal-theory)
                           '(f-k-h g-rewrite)))

; Prove a theorem.
(thm (equal (g (h a)) (k (h a))))

Let us look at how ACL2 uses the above binding hypothesis in the proof of the preceding thm form. The rewriter considers the term (g (h a)) and finds a match with the left-hand side of the rule g-rewrite, binding x to (h a). The first hypothesis binds y to the result of rewriting (k x) in the current context, where the variable x is bound to the term (h a); thus y is bound to (k (h a)). The second hypothesis, (f y), is then rewritten under this binding, and the result is t by application of the rewrite rule f-k-h. The rule g-rewrite is then applied under the already-mentioned binding of x to (h a). This rule application triggers a recursive rewrite of the right-hand side of g-rewrite, which is y, in a context where y is bound (as discussed above) to (k (h a)). The result of this rewrite is that same term, (k (h a)). The original call of equal then trivially rewrites to t.

We move on now to our second example, which is similar but involves a user-defined equivalence relation. You may find it helpful to review :equivalence rules; see equivalence.

Recall that when a hypothesis is a call of an equivalence relation other than equal, the second argument must be a call of double-rewrite in order for the hypothesis to be treated as a binding hypothesis. That is indeed the case below; an explanation follows.

; Define an equivalence relation.
(defun my-equiv (x y) (equal x y))
(defequiv my-equiv) ; introduces rule MY-EQUIV-IS-AN-EQUIVALENCE

; Define some unary functions
(defun f (x) (declare (ignore x)) t)
(defun g (x) x)
(defun h1 (x) x)
(defun h2 (x) x)

; Prove some simple lemmas.  Note the binding hypothesis in lemma-3.
(defthm lemma-1
  (my-equiv (h1 x) (h2 x)))
(defthm lemma-2
  (f (h2 x)))
(defthm lemma-3
       (implies (and (my-equiv y (double-rewrite x)) ; binding hypothesis
                     (f y))
                (equal (g x) y)))

; Restrict to a theory that includes the above lemmas but avoids the above
; definitions.
(in-theory (union-theories (theory 'minimal-theory)
                           '(lemma-1 lemma-2 lemma-3
                                     my-equiv-is-an-equivalence)))

; Prove a theorem.
(thm (equal (g (h1 a)) (h2 a)))

The proof succeeds much as in the first example, but the following observation is key: when ACL2 binds y upon considering the first hypothesis of lemma-3, it rewrites the term (double-rewrite x) in a context where it need only preserve the equivalence relation my-equiv. At this point, x is bound by applying lemma-3 to the term (g (h1 a)); so, x is bound to (h1 a). The rule lemma-1 then applies to rewrite this occurrence of x to (h2 a), but only because it suffices to preserve my-equiv. Thus y is ultimately bound to (h2 a), and the proof succeeds as one would expect.

If we tweak the above example slightly by disabling the user's equivalence rune, then the proof of the thm form fails because the above rewrite of (double-rewrite x) is done in a context where it no longer suffices to preserve my-equiv as we dive into the second argument of my-equiv in the first hypothesis of lemma-3; so, lemma-1 does not apply this time.

(in-theory (union-theories (theory 'minimal-theory)
                           '(lemma-1 lemma-2 lemma-3)))

; Proof fails in this case!
(thm (equal (g (h1 a)) (h2 a)))