### FREE-VARIABLES-EXAMPLES

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

The following examples illustrate ACL2's handling of free variables in rewrite and linear 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 error because of free variable.  The error message suggests
; executing the subsequent form.
(defaxiom p2-trans
(implies (and (p2 x y)
(p2 y z))
(p2 x z)))

; Allow default of :match-free :all.
(set-match-free-error nil)

; Now the same axiom produces a warning, not an error.  Supplying
; :match-free  (illustrated later, below) gets rid of the warning as
; well.
(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

; 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 multiple bindings are 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.
(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.
(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 multiple ground
; units 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.