Major Section: MISCELLANEOUS

For this topic, we assume familiarity not only with metatheorems and
metafunctions (see meta) but also with extended metafunctions
(see extended-metafunctions). The capability described here -- so-called
``meta-extract hypotheses'' for a `:meta`

rule -- provides an advanced
form of meta-level reasoning that was largely designed by Sol Swords, who
also provided a preliminary implementation.

A `:meta`

rule may now have hypotheses, known as ``meta-extract
hypotheses'', that take either of the following two forms. Here `evl`

is
the evaluator, `obj`

is an arbitrary term, `mfc`

is the variable used as
the metafunction context, `state`

is literally the symbol `STATE`

, `a`

is the second argument of `evl`

in both arguments of the conclusion of the
rule, and `aa`

is an arbitrary term.

(evl (meta-extract-contextual-fact obj mfc state) a) (evl (meta-extract-global-fact obj state) aa))Note that the first form, involving

`meta-extract-contextual-fact`

, is only
allowed if the metafunction is an extended metafunction.
These additional hypotheses may be necessary in order to prove a proposed
metatheorem, in particular when the correctness of the metafunction depends
on the correctness of utilities extracting formulas from the logical
world or facts from the metafunction context (mfc). After the
`:`

`meta`

rule is proved, however, the meta-extract hypotheses have no
effect on how the rule is applied during a proof. An argument for
correctness of using meta-extract hypotheses is given in the ACL2 source code
within a comment entitled ``Essay on Correctness of Meta Reasoning''. In the
documentation below, we focus not only the application of `:`

`meta`

rules but, rather, on how the use of meta-extract hypotheses allow you to
prove correctness of metafunctions that use facts from the logical world
or the metafunction context (mfc).

Below we describe properties of `meta-extract-contextual-fact`

and
`meta-extract-global-fact`

, but after we illustrate their utility with an
example. This example comes from the community book,
`books/clause-processors/meta-extract-simple-test.lisp`

, which presents
very basic (and contrived) examples that nevertheless illustrate meta-extract
hypotheses.

(defthm plus-identity-2-meta (implies (and (nthmeta-ev (meta-extract-global-fact '(:formula bar-posp) state) (list (cons 'u (nthmeta-ev (cadr (cadr term)) a)))) (nthmeta-ev (meta-extract-contextual-fact `(:typeset ,(caddr term)) mfc state) a)) (equal (nthmeta-ev term a) (nthmeta-ev (plus-identity-2-metafn term mfc state) a))) :rule-classes ((:meta :trigger-fns (binary-+))))The two hypotheses illustratate the two basic kinds of meta-extract hypotheses: applications of the evaluator to a call of

`meta-extract-global-fact`

and to a call of
`meta-extract-contextual-fact`

. Here is the definition of the metafunction
used in the above rule, slightly simplified here from what is found in the
above book (but adequate for proving the two events that follow it in the
above book).
(defun plus-identity-2-metafn (term mfc state) (declare (xargs :stobjs state :verify-guards nil)) (case-match term (('binary-+ ('bar &) y) (cond ((equal (meta-extract-formula 'bar-posp state) '(POSP (BAR U))) (if (ts= (mfc-ts y mfc state :forcep nil) *ts-character*) (cadr term) term)) (t term))) (& term)))This metafunction returns its input term unchanged except in the case that the term is of the form

`(binary-+ (bar x) y)`

and the following two
conditions are met, in which case it returns `(bar x)`

.
(1) (equal (meta-extract-formula 'bar-posp state) '(POSP (BAR U))) (2) (ts= (mfc-ts y mfc state :forcep nil) *ts-character*)So suppose that term is

`(list 'binary-+ (list 'bar x) y)`

. We show how
the meta-extract hypotheses allow together with (1) and (2) imply that the
conclusion of the above `:meta`

rule holds. Here is that conclusion after
a bit of simplification.
(equal (nthmeta-ev (list 'binary-+ (list 'bar x) y) a) (nthmeta-ev (list 'bar x) a))This equality simplifies as follows using the evaluator properties of

`nthmeta-ev`

.
(equal (binary-+ (bar (nthmeta-ev x a)) (nthmeta-ev y a)) (bar (nthmeta-ev x a)))Clearly it suffices to show:

(A) (posp (bar (nthmeta-ev x a))) (B) (characterp (nthmeta-ev y a))It remains then to show that these follow from (1) and (2) together with the meta-extract hypotheses.

First consider (A). We show that it is just a simplification of the first meta-extract hypothesis.

(nthmeta-ev (meta-extract-global-fact '(:formula bar-posp) state) (list (cons 'u (nthmeta-ev (cadr (cadr term)) a)))) = {by our assumption that term is (list 'binary-+ (list 'bar x) y)} (nthmeta-ev (meta-extract-global-fact '(:formula bar-posp) state) (list (cons 'u (nthmeta-ev x a)))) = {by definition of meta-extract-global-fact, as discussed later} (nthmeta-ev (meta-extract-formula 'bar-posp state) (list (cons 'u (nthmeta-ev x a)))) = {by (1)} (nthmeta-ev '(posp (bar u)) (list (cons 'u (nthmeta-ev x a)))) = {by evaluator properties of nthmeta-ev} (posp (bar (nthmeta-ev x a)))

Now consider (B). We show that it is just a simplification of the second meta-extract hypothesis.

(nthmeta-ev (meta-extract-contextual-fact `(:typeset ,(caddr term)) mfc state) a) = {by our assumption that term is (list 'binary-+ (list 'bar x) y)} (nthmeta-ev (meta-extract-contextual-fact (list ':typeset y) mfc state) a) = {by definition of meta-extract-contextual-fact, as discussed later} (nthmeta-ev (list 'typespec-check (list 'quote (mfc-ts y mfc state :forcep nil)) y) a) = {by (2)} (nthmeta-ev (list 'typespec-check (list 'quote *ts-character*) y) a) = {by evaluator properties of nthmeta-ev} (typespec-check *ts-character* (nthmeta-ev y a)) = {by definition of typespec-check} (characterp (nthmeta-ev y a))

Note the use of `:forcep nil`

above. All of the `mfc-xx`

functions take
a keyword argument `:forcep`

. Calls of `mfc-xx`

functions made on behalf
of `meta-extract-contextual-fact`

always use `:forcep nil`

, so in order
to reason about these calls in your own metafunctions, you will want to use
`:forcep nil`

. We are contemplating adding a utility like
`meta-extract-contextual-fact`

that allows forcing but returns a tag-tree
(see ttree).

Finally, we document what is provided logically by calls of
`meta-extract-global-fact`

and `meta-extract-contextual-fact`

. Of
course, you are invited to look at the definitions of these function in the
ACL2 source code, or by using `:`

`pe`

. Note that both of these
functions are non-executable (their bodies are inside a call of
`non-exec`

); their function is purely logical, not for execution. The
functions return `*t*`

, i.e., `(quote t)`

, in cases that they provide no
information.

First we consider the value of `(meta-extract-global-fact obj state)`

for
various values of `obj`

.

Case

`obj`

= (list :formula FN):

The value reduces to the value of`(meta-extract-formula FN state)`

, which returns the ``formula'' of`FN`

in the following sense. If`FN`

is a function symbol with formals`(X1 ... Xk)`

, then the formula is the constraint on`FN`

if`FN`

is constrained or introduced by`defchoose`

, and otherwise is`(equal (FN X1 ... Xk) BODY)`

, where`BODY`

is the (unsimplified) body of the definition of`FN`

. Otherwise, if`FN`

is the name of a theorem, the formula is just what is stored for that theorem. Otherwise, the formula is`*t*`

.Case

`obj`

= (list :lemma FN N):

Assume`N`

is a natural number; otherwise, treat`N`

as 0. If`FN`

is a function symbol with more than`N`

associated lemmas -- ``associated'' in the sense of being either a`:`

`definition`

rule for`FN`

or a`:`

`rewrite`

rule for`FN`

whose left-hand side has a top function symbol of`FN`

-- then the value is the`N`

th such lemma (with zero-based indexing). Otherwise the value is`*t*`

.For any other values of

`obj`

, the value is`*t*`

.

Finally, the value of `(meta-extract-contextual-fact obj mfc state)`

is as follows for various values of `obj`

.

Case

`obj`

= (list :typeset TERM ...):

The value is the value of`(typespec-check ts TERM)`

, where`ts`

is the value of`(mfc-ts TERM mfc state :forcep nil :ttreep nil)`

, and where`(typespec-check ts val)`

is defined to be true when`val`

has type-set`ts`

. (Exception: If`val`

satisfies`bad-atom`

then`typespec-check`

is true when`ts`

is negative.)Case

`obj`

= (list :rw+ TERM ALIST OBJ EQUIV ...):

We assume below that`EQUIV`

is a symbol that represents an equivalence relation, where`nil`

represents`equal`

,`t`

represents`iff`

, and otherwise`EQUIV`

represents itself (an equivalence relation in the current logical world). For any other`EQUIV`

the value is`*t*`

. Now let`rhs`

be the value of`(mfc-rw+ TERM ALIST OBJ EQUIV mfc state :forcep nil :ttreep nil)`

. Then the value is the term`(list 'equv (sublis-var ALIST TERM) rhs)`

, where equv is the equivalence relation represented by`EQUIV`

, and`sublis-var`

is defined to substitute a variable-binding alist into a term.Case

`obj`

= (list :rw TERM OBJ EQUIV ...):

The value is the same as above but for an`ALIST`

of`nil`

, i.e., for the case that`obj`

is`(list :rw+ TERM nil OBJ EQUIV ...)`

.Case

`obj`

= (list :ap TERM ...):

The value is`(list 'not TERM)`

if`(mfc-ap TERM mfc state :forcep nil :ttreep nil)`

is true, else is`*t*`

.Case

`obj`

= (list :relieve-hyp HYP ALIST RUNE TARGET BKPTR ...):

The value is`(sublis-var alist hyp)`

-- see above for a discussion of`sublis-var`

-- if the following is true.(mfc-relieve-hyp hyp alist rune target bkptr mfc state :forcep nil :ttreep nil)Otherwise the value is`*t*`

.If no case above applies, then the value is

`*t*`

.