Some restrictions on the use of evaluators in meta-level rules

Note: This topic, which explains some subtleties for evaluators, can probably be skipped by most readers.

Rules of class `meta` and of class `clause-processor` are stated using so-called ``evaluator'' functions. Here we
explain some restrictions related to evaluators. Below we refer primarily to

In a nutshell, we require that a rule's evaluator does not support any
meta-extract functions in the rule or any `defaxiom` events, and
we require that the evaluator not be introduced under a non-trivial
encapsulate. We also require that no function has an attachment (see defattach) that is both ancestral in the evaluator and also ancestral in the
meta or clause-processor functions. We explain these restrictions in detail
below.

An argument given elsewhere (see meta, in particular ``Aside for the
logic-minded'') explains that the correctness argument for applying
metatheoretic simplifiers requires that one be able to ``grow'' an evaluator
(see defevaluator) to handle all functions in the current ACL2 world. Then we may, in essence, functionally instantiate the original
evaluator to the new (``grown'') evaluator, provided that the new evaluator
satisfies all of the axioms of the original. We therefore require that the
evaluator function does not support the formula of any `defaxiom` event.
This notion of ``support'' (sometimes denoted ``is an ancestor of'') is
defined recursively as follows: a function symbol supports a formula if either
it occurs in that formula, or else it supports the definition or constraint
for some function symbol that occurs in that formula. Moreover, we require
that neither the evaluator function nor its list version support meta-extract functions if they are used in the proposed

These requirements are necessary in order to carry out the functional instantiation argument alluded to above, as follows (where the reader may find it useful to have some familiarity with the paper ``Structured Theory Development for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001), pages 161-203). By the usual conservativity argument, we know that the rule follows logically from the axiomatic events for its supporters. This remains true if we functionally instantiate the evaluator with one corresponding to all the functions symbols of the current session, since none of the definitions of supporters of defaxioms or metafunctions are hit by that functional substitution.

Notice though that the argument above depends on knowing that the rule is
not itself an axiom about the evaluator! Therefore, we also restrict
evaluators so that they are not defined in the scope of a superior `encapsulate` event with non-empty signature, in order to avoid an even more
subtle problem. The aforementioned correctness argument depends on knowing
that the rule is provable from the axioms on the evaluator and metafunction
(and hypothesis metafunction, if any). The additional restriction avoids
unsoundness! The following events, if allowed, produce a proof that

; Introduce our metafunction. (defun my-cancel (term) (case-match term (('f ('g)) *t*) (& term))) ; Introduce our evaluator and prove our meta rule, but in the same ; encapsulate! (encapsulate ((f (x) t)) (local (defun f (x) (declare (ignore x)) t)) (defevaluator evl evl-list ((f x))) (defthm correctness-of-my-cancel (equal (evl x a) (evl (my-cancel x) a)) :rule-classes ((:meta :trigger-fns (f))))) ; Prove that (f x) = t. (encapsulate () (local (defstub c () t)) (local (encapsulate () (local (defun g () (c))) (local (in-theory (disable g (g)))) (local (defthm f-g (equal (f (g)) t) :rule-classes nil)) (defthm f-c (equal (f (c)) t) :hints (("Goal" :use f-g :in-theory (e/d (g) (correctness-of-my-cancel)))) :rule-classes nil))) (defthm f-t (equal (f x) t) :hints (("Goal" :by (:functional-instance f-c (c (lambda () x))))) :rule-classes nil))

To see that the term

; (defun my-cancel (term) ...) as before, then: (defun f (x) (not x)) (defun g () nil) (defevaluator evl evl-list ((f x) (g)))

These events imply the axiomatic events above, because we still have the
definition of `defevaluator` event,
and we can now prove

(defthm f-not-t (equal (f t) nil) :rule-classes nil)

It follows that the current session logically yields a contradiction!

Erik Reeber has taken the above example and modified it to prove

(in-package "ACL2") (defun my-cancel (term) (case-match term (('f ('g)) *t*) (('f2 ('g2)) *t*) (& term))) (defun f2 (x) (not x)) (defun g2 () nil) (encapsulate ((f (x) t)) (local (defun f (x) (declare (ignore x)) t)) (defevaluator evl evl-list ((f x) (f2 x) (g2))) (defthm correctness-of-my-cancel (equal (evl x a) (evl (my-cancel x) a)) :rule-classes ((:meta :trigger-fns (f))))) (encapsulate () (local (defstub c () t)) (local (encapsulate () (local (defun g () (c))) (local (in-theory (disable g (g)))) (local (defthm f-g (equal (f (g)) t) :rule-classes nil)) (defthm f-c (equal (f (c)) t) :hints (("Goal" :use f-g :in-theory (e/d (g) (correctness-of-my-cancel)))) :rule-classes nil))) (defthm f-t (equal (f x) t) :hints (("Goal" :by (:functional-instance f-c (c (lambda () x))))) :rule-classes nil)) (defun g () nil) ; Below is the expansion of the following defevaluator, changed slightly as ; indicated by comments. ; (defevaluator evl2 evl2-list ((f x) (f2 x) (g) (g2))) (ENCAPSULATE (((EVL2 * *) => *) ((EVL2-LIST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN EVL2 (X A) (DECLARE (XARGS :VERIFY-GUARDS NIL :MEASURE (ACL2-COUNT X) :WELL-FOUNDED-RELATION O< :MODE :LOGIC)) (COND ((SYMBOLP X) (CDR (ASSOC-EQ X A))) ((ATOM X) NIL) ((EQ (CAR X) 'QUOTE) (CAR (CDR X))) ((CONSP (CAR X)) (EVL2 (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (EVL2-LIST (CDR X) A)))) ((EQUAL (CAR X) 'F) ; changed f to f2 just below (F2 (EVL2 (CAR (CDR X)) A))) ((EQUAL (CAR X) 'F2) (F2 (EVL2 (CAR (CDR X)) A))) ((EQUAL (CAR X) 'G) (G)) ((EQUAL (CAR X) 'G2) (G2)) (T NIL))) (DEFUN EVL2-LIST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (EVL2 (CAR X-LST) A) (EVL2-LIST (CDR X-LST) A))))))) (DEFTHM EVL2-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (EVL2 X A) (CDR (ASSOC-EQ X A))))) (DEFTHM EVL2-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'QUOTE)) (EQUAL (EVL2 X A) (CADR X)))) (DEFTHM EVL2-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (EVL2 X A) (EVL2 (CADDAR X) (PAIRLIS$ (CADAR X) (EVL2-LIST (CDR X) A)))))) (DEFTHM EVL2-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (EVL2-LIST X-LST A) NIL))) (DEFTHM EVL2-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (EVL2-LIST X-LST A) (CONS (EVL2 (CAR X-LST) A) (EVL2-LIST (CDR X-LST) A))))) (DEFTHM EVL2-CONSTRAINT-6 (IMPLIES (AND (NOT (CONSP X)) (NOT (SYMBOLP X))) (EQUAL (EVL2 X A) NIL))) (DEFTHM EVL2-CONSTRAINT-7 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F)) (EQUAL (EVL2 X A) ; changed f to f2 just below (F2 (EVL2 (CADR X) A))))) (DEFTHM EVL2-CONSTRAINT-8 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F2)) (EQUAL (EVL2 X A) (F2 (EVL2 (CADR X) A))))) (DEFTHM EVL2-CONSTRAINT-9 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G)) (EQUAL (EVL2 X A) (G)))) (DEFTHM EVL2-CONSTRAINT-10 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G2)) (EQUAL (EVL2 X A) (G2))))) (defthm f2-t (equal (f2 x) t) :hints (("Goal" :by (:functional-instance f-t (f f2) (evl evl2) (evl-list evl2-list))))) (defthm bug-implies-nil nil :hints (("Goal" :use ((:instance f2-t (x t))))) :rule-classes nil)

Finally, we also require that no function has an attachment (see defattach) that is both ancestral in the evaluator and also ancestral in the
meta or clause-processor functions. (If you don't use `defattach` or
`apply$` — more specifically, warrants — then you can
ignore this condition.) Without this restriction, the following events prove

(in-package "ACL2") (defstub f () t) (defevaluator evl evl-list ((f))) (defun my-meta-fn (x) (if (equal x '(f)) (list 'quote (f)) x)) (defthm my-meta-fn-correct (equal (evl x a) (evl (my-meta-fn x) a)) :rule-classes ((:meta :trigger-fns (f)))) (defun constant-nil () (declare (xargs :guard t)) nil) (defattach f constant-nil) (defthm f-is-nil ; proved using my-meta-fn-correct (equal (f) nil) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :use ((:functional-instance f-is-nil (f (lambda () t)))))) :rule-classes nil)

Here is an example that doesn't use `defattach` explicitly, but uses
warrants, which essentially have attachments so that every call of a
warrant evaluates to

(in-package "ACL2") (include-book "projects/apply/top" :dir :system) (defevaluator evl evl-list ((apply$ fn args))) (encapsulate () (local (defun$ f () (declare (xargs :guard t)) t)) (local (defun my-meta-fn (x) (if (and (equal x '(apply$ 'f 'nil)) (apply$-warrant-f)) *t* x))) (local (defthm my-meta-fn-correct (equal (evl x a) (evl (my-meta-fn x) a)) :rule-classes ((:meta :trigger-fns (apply$))))) (defthm unwarranted-fact-about-quote-f (equal (apply$ 'f nil) t) :rule-classes nil)) (defun$ f () nil) (defthm apply$-warrant-f-false (not (apply$-warrant-f)) :hints (("Goal" :use unwarranted-fact-about-quote-f)) :rule-classes nil) ; But apply$-warrant-f is a function with no non-trivial constraint. (defthm contradiction nil :hints (("Goal" :use (:functional-instance apply$-warrant-f-false (apply$-warrant-f (lambda () t)) (apply$-userfn (lambda (fn args) nil)) (badge-userfn (lambda (fn) '(APPLY$-BADGE 0 1 . T)))))) :rule-classes nil)

To see why this restriction is sufficient, see a comment in the ACL2 source code entitled ``; Essay on Correctness of Meta Reasoning.''