State and context sensitive metafunctions

General Form of an Extended :Meta theorem: (implies (and (pseudo-termp x) ; this hyp is optional (alistp a) ; this hyp is optional (ev (hyp-fn x mfc state) a) ; this hyp is optional ; meta-extract hyps may also be included (see below) ) (equiv (ev x a) (ev (fn x mfc state) a)))

where the restrictions are as described in the documentation for
`meta` where `state`
is made available.

See meta for a discussion of vanilla flavored metafunctions. This
documentation assumes you are familiar with the simpler situation, in
particular, how to define a vanilla flavored metafunction,

To test your extended metafunctions outside of proof attempts, see trust-mfc.

Additional hypotheses are supported, called ``meta-extract hypotheses'', that allow metafunctions to depend on the validity of certain terms extracted from the context or the logical world. These hypotheses provide an even more advanced form of metatheorem so we explain them elsewhere; see meta-extract.

The metafunction context,

`syntaxp` or `bind-free` hypothesis, in which case, returns the
unifying substitution present at the start of that evaluation.

`world`.

(equal (mfc-rw term t t mfc state) *t*)

The constant

(implies (and ... (syntaxp (... (mfc-rw `(bar ,x) ...) ...)) ...) (equal (... x ...) ...))

Here,

(implies (and ... (syntaxp (... (mfc-rw+ '(bar v) `((v . ,x)) ...) ...)) ...) (equal (... x ...) ...))

However, you may find that the additional rewriting done by

`rune` at (one-based) position `force` or `case-split`. (If you need such a feature, feel free
to request it of the ACL2 implementors.)

We explain the

During the execution of a metafunction by the theorem prover, the
expressions above compute the results specified. Typically, you should
imagine that there are no axioms about the `meta` rules; see meta-extract. But we assume
for the rest of the present documentation topic that you do not use
meta-extract hypotheses. Thus, in the proof of the correctness of a
metafunction, no information is available about the results of these
functions: you should *use these functions for heuristic purposes
only*.

For example, your metafunction may use these functions to decide whether to
perform a given transformation, but the transformation must be sound
regardless of the value that your metafunction returns. We illustrate this
below. It is sometimes possible to use the hypothesis metafunction,

We conclude with a script that defines, verifies, and uses several extended metafunctions. This script is based on one provided by Robert Krug, who was instrumental in the development of this style of metafunction and whose help we gratefully acknowledge.

; Here is an example. I will define (foo i j) simply to be (+ i j). ; But I will keep its definition disabled so the theorem prover ; doesn't know that. Then I will define an extended metafunction ; that reduces (foo i (- i)) to 0 provided i has integer type and the ; expression (< 10 i) occurs as a hypothesis in the clause. ; Note that (foo i (- i)) is 0 in any case. (defun foo (i j) (+ i j)) (defevaluator eva eva-lst ((foo i j) (unary-- i) ; I won't need these two cases until the last example below, but I ; include them now. (if x y z) (integerp x))) (set-state-ok t) (defun metafn (x mfc state) (cond ((and (consp x) (equal (car x) 'foo) (equal (caddr x) (list 'unary-- (cadr x)))) ; So x is of the form (foo i (- i)). Now I want to check some other ; conditions. (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state) *ts-integer*) (member-equal `(NOT (< '10 ,(cadr x))) (mfc-clause mfc))) (quote (quote 0))) (t x))) (t x))) (defthm metafn-correct (equal (eva x a) (eva (metafn x mfc state) a)) :rule-classes ((:meta :trigger-fns (foo)))) (in-theory (disable foo)) ; The following will fail because the metafunction won't fire. ; We don't know enough about i. (thm (equal (foo i (- i)) 0)) ; Same here. (thm (implies (and (integerp i) (< 0 i)) (equal (foo i (- i)) 0))) ; But this will work. (thm (implies (and (integerp i) (< 10 i)) (equal (foo i (- i)) 0))) ; This won't, because the metafunction looks for (< 10 i) literally, ; not just something that implies it. (thm (implies (and (integerp i) (< 11 i)) (equal (foo i (- i)) 0))) ; Now I will undo the defun of metafn and repeat the exercise, but ; this time check the weaker condition that (< 10 i) is provable ; (by rewriting it) rather than explicitly present. (ubt 'metafn) (defun metafn (x mfc state) (cond ((and (consp x) (equal (car x) 'foo) (equal (caddr x) (list 'unary-- (cadr x)))) (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state) *ts-integer*) (equal (mfc-rw `(< '10 ,(cadr x)) t t mfc state) *t*)) ; The mfc-rw above rewrites (< 10 i) with objective t and iffp t. The ; objective means the theorem prover will try to establish it. The ; iffp means the theorem prover can rewrite maintaining propositional ; equivalence instead of strict equality. (quote (quote 0))) (t x))) (t x))) (defthm metafn-correct (equal (eva x a) (eva (metafn x mfc state) a)) :rule-classes ((:meta :trigger-fns (foo)))) (in-theory (disable foo)) ; Now it will prove both: (thm (implies (and (integerp i) (< 10 i)) (equal (foo i (- i)) 0))) (thm (implies (and (integerp i) (< 11 i)) (equal (foo i (- i)) 0))) ; Now I undo the defun of metafn and change the problem entirely. ; This time I will rewrite (integerp (foo i j)) to t. Note that ; this is true if i and j are integers. I can check this ; internally, but have to generate a hyp-fn to make it official. (ubt 'metafn) (defun metafn (x mfc state) (cond ((and (consp x) (equal (car x) 'integerp) (consp (cadr x)) (equal (car (cadr x)) 'foo)) ; So x is (integerp (foo i j)). Now check that i and j are ; ``probably'' integers. (cond ((and (ts-subsetp (mfc-ts (cadr (cadr x)) mfc state) *ts-integer*) (ts-subsetp (mfc-ts (caddr (cadr x)) mfc state) *ts-integer*)) *t*) (t x))) (t x))) ; To justify this transformation, I generate the appropriate hyps. (defun hyp-fn (x mfc state) (declare (ignore mfc state)) ; The hyp-fn is run only if the metafn produces an answer different ; from its input. Thus, we know at execution time that x is of the ; form (integerp (foo i j)) and we know that metafn rewrote ; (integerp i) and (integerp j) both to t. So we just produce their ; conjunction. Note that we must produce a translated term; we ; cannot use the macro AND and must quote constants! Sometimes you ; must do tests in the hyp-fn to figure out which case the metafn ; produced, but not in this example. `(if (integerp ,(cadr (cadr x))) (integerp ,(caddr (cadr x))) 'nil)) (defthm metafn-correct (implies (eva (hyp-fn x mfc state) a) (equal (eva x a) (eva (metafn x mfc state) a))) :rule-classes ((:meta :trigger-fns (integerp)))) (in-theory (disable foo)) ; This will not be proved. (thm (implies (and (rationalp x) (integerp i)) (integerp (foo i j)))) ; But this will be. (thm (implies (and (rationalp x) (integerp i) (integerp j)) (integerp (foo i j))))

- Metafunction-context
- A structure that holds data supporting extended meta reasoning
- Trust-mfc
- A macro that supports testing of extended metafunctions)