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; Disallow default for :match-free. (set-match-free-error nil)
; 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 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. 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 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. (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))))
