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.

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

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

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

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

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

;;;;;;;;;;
```

FINALLY, here is an example illustrating 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`.