Major Section: MISCELLANEOUS

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 (equiv (ev x a) (ev (fn x mfc state) a)))where the restrictions are as described in

`meta`

and, in
addition, `mfc`

and `state`

, are distinct variable symbols
(different also from `x`

and `a`

) and `state`

is literally the
symbol `STATE`

. A `:meta`

theorem of the above form installs
`fn`

as a metatheoretic simplifier with hypothesis function
`hyp-fn`

, exactly as for vanilla metafunctions. The only
difference is that when the metafunctions are applied, some
contextual information is passed in via the `mfc`

argument and
the ACL2 `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,
`fn`

, and its associated hypothesis metafunction, `hyp-fn`

, and
how to state and prove metatheorems installing such functions.
Defining extended metafunctions requires that you also be
familiar with many ACL2 implementation details. This documentation
is sketchy on these details; see the ACL2 source code or talk to the
implementors if you need more help.

The metafunction context, `mfc`

, is a list containing many
different data structures used by various internal ACL2 functions.
We do not document the form of `mfc`

. Your extended
metafunction should just take `mfc`

as its second formal and pass
it into the functions mentioned below. The ACL2 `state`

is
well-documented. The following expressions may be useful in
defining extended metafunctions.

`(mfc-clause mfc)`

: returns the current goal, in clausal form. A
clause is a list of ACL2 terms, implicitly denoting the disjunction
of the listed terms. The clause returned by `mfc-clause`

is the
clausal form of the translation (see trans) of the goal or subgoal
on which the rewriter is working. When a metafunction calls
`mfc-clause`

, the term being rewritten by the metafunction either
occurs somewhere in this clause or, more commonly, is being
rewritten on behalf of some lemma to which the rewriter has
backchained while trying to rewrite a term in the clause.

`(mfc-type-alist mfc)`

: returns the type-alist governing the occurrence
of the term, `x`

, being rewritten by the metafunction. A type-alist
is an association list, each element of which is of the form
`(term ts . ttree)`

. Such an element means that the term `term`

has the type-set `ts`

. The `ttree`

component is probably
irrelevant here. All the terms in the type-alist are in translated
form (see trans). The `ts`

are numbers denoting finite
sets of ACL2's primitive types, as explained in the documentation for
type-set. The type alist includes not only that gleaned from the
conditions governing the term being rewritten but also that gleaned
from forward chaining from the other literals in the clause returned
by `mfc-clause`

.

`(w state)`

: returns the ACL2 logical `world`

.

`(mfc-ts term mfc state)`

: returns the `type-set`

of `term`

in
the current context.

`(mfc-rw term obj iffp mfc state)`

: returns the result of rewriting
`term`

in the current context, `mfc`

, with objective `obj`

and
the equivalence relation described by `iffp`

. `Obj`

must be
`t`

, `nil`

, or `?`

, and describes your objective: try to
show that `term`

is true, false, or anything. `Iffp`

is either
`nil`

or non-`nil`

. The former means return a term that is
`equal`

to `term`

. The latter means return a term that is
propositionally equivalent (i.e., in the `iff`

sense) to `term`

.
Generally, if you wish to establish that `term`

is true in the current
context, use the idiom

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

`*t*`

is set to the internal form of the constant
term `t`

, i.e., `'t`

.
`(mfc-ap term mfc state)`

: returns `t`

or `nil`

according to whether
linear arithmetic can determine that `term`

is false. To the
cognoscenti: returns the contradiction flag produced by
linearizing `term`

and adding it to the `linear-pot-lst`

.

During the execution of a metafunction by the theorem prover, the
expressions above compute the results specified. However, there are
no axioms about `mfc-ts`

and `mfc-rw`

: they are uninterpreted
function symbols. Thus, in the proof of the correctness of a
metafunction, no information is available about the results of these
functions. Thus,
*these functions can be used 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. We illustrate this below. It is
sometimes possible to use the hypothesis metafunction, `hyp-fn`

,
to generate a sufficient hypothesis to justify the transformation.
The generated hypothesis might have already been ``proved''
internally by your use of `mfc-ts`

or `mfc-rw`

, but the system
will have to prove it ``officially'' by relieving it. We illustrate
this below also.

We conclude with a script that defines, verifies, and uses several extended metafunctions. This script was 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))) ''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.

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