#### FREE-VARIABLES-EXAMPLES-REWRITE

examples pertaining to free variables in rewrite rules
```Major Section:  FREE-VARIABLES-EXAMPLES
```

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.

; 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.

; 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.

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

; 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.

; 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:

; 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.

; 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)
(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)
(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)
(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)))
```