Major Section: MISCELLANEOUS

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

`meta`

or a
`:`

`clause-processor`

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

A meta rule or clause-processor rule may have so-called ``meta-extract''
hypotheses that take forms displayed below. Here `evl`

is the evaluator,
`obj`

is an arbitrary term, `mfc`

is the metafunction context (which is a
variable other than the symbol `STATE`

that represents the metafunction
context; see extended-metafunctions), `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)) ; equivalent to the next form (evl (meta-extract-global-fact+ obj state state) aa) (evl (meta-extract-global-fact+ obj st state) aa)The first form is only legal for

`:meta`

rules for which the metafunction
is an extended metafunction. The remaining forms are legal for both
`:meta`

rules and `:clause-processor`

rules.Sol Swords has contributed a community book,
`clause-processors/meta-extract-user.lisp`

, that uses a Skolemization trick
to allow one to use at most one `meta-extract-global-fact+`

hypothesis and
at most one `meta-extract-contextual-fact`

hypothesis.

These additional hypotheses may be necessary in order to prove a proposed
metatheorem or (for the second type of hypothesis above) clause-processor
rule, in particular when the correctness of the metafunction depends on the
correctness of utilities extracting formulas from the logical world or
(for the first type) facts from the metafunction context (mfc). After the
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 primarily on `:`

`meta`

rules, since the use of
`meta-extract-global-fact`

hypotheses in `:`

`clause-processor`

rules
is entirely analogous. (At the end, though, we discuss the last of the four
forms displayed above.) And for `:meta`

rules we focus not on the
application of 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 only after we illustrate their utility with
an example. But even before we present that example, we first give a sense
of how to think about these functions by showing a theorem that one can prove
about the first of them. If this snippet doesn't help your intuition, then
just skip over it and start with the example.

(defevaluator evl evl-list ((binary-+ x y) (typespec-check x y))) (thm (implies (not (bad-atom (cdr (assoc-equal 'x alist)))) (equal (evl (meta-extract-contextual-fact (list :typeset 'x) mfc state) alist) (not (equal 0 ; indicates non-empty intersection (logand (type-set-quote ; type-set of a constant (cdr (assoc-equal 'x alist))) (mfc-ts-fn 'x mfc state nil)))))))

The following example comes from the community book,
`books/clause-processors/meta-extract-simple-test.lisp`

(after it defines
the evaluator), 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 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)))Since a positive number plus a character is that number, it clearly 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 have contemplated adding a utility like
`meta-extract-contextual-fact`

that allows forcing but returns a tag-tree
(see ttree), and may do so if there is demand for it.

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 (each of their bodies is inside a call of
`non-exec`

); their purpose 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`

. When we refer below to concepts like ``body'' and
``evaluation'', we refer to these with respect to the logical world of the
input `state`

.

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*`

.Case

`obj`

=`(list :fncall FN ARGLIST)`

:

Assume that`FN`

is a`:`

`logic`

-mode function symbol and that`ARGLIST`

is a true list of values of the same length as list of formal parameters for`FN`

(i.e., as the input arity of`FN`

). Also assume that the application of`FN`

to actual parameter list`ARGLIST`

returns a result`(mv nil x)`

. Let`(QARG1 ... QARGk)`

be the result of quoting each element of`ARGLIST`

, i.e., replacing each`y`

in`ARGLIST`

by the two-element list`(quote y)`

. Then the value is the term`(equal (FN QARG1 ... QARGk) (quote x))`

.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`

. Note a difference from the semantics
of `meta-extract-global-fact`

: below, the relevant logical world is the one
stored in the metafunction context, `mfc`

, not in the input `state`

.

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

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*`

.

We conclude by considering the fourth of the four forms above (and implicitly, its special case represented by the third form above):

(evl (meta-extract-global-fact+ obj st state) aa)The discussion above is for the function

`meta-extract-global-fact+`

, but
assumes that the logical worlds of `st`

and `state`

are equal;
otherwise the value returned is `*t*`

. Of course, since a call of
`meta-extract-global-fact`

expands to a corresponding call of
`meta-extract-global-fact+`

in which the last two arguments are both
`state`

, that condition holds automatically for that case. But the
`state`

mentioned in the meta-extract hypotheses of a meta rule or
clause-processor rule is in essence an initial state. In the case of a
clause-processor rule, the clause-processor function may modify that initial
state (say, by printing or modifying some state globals) without changing its
world, and then pass that modified state to `fncall-term`

. While
`fncall-term`

may produce a different result for this modified state than
for the initial state, both are valid: the state used for heuristic purposes,
such as determining whether guard-checking may cause an error. A useful
instance of the hypothesis displayed above will be one in which `st`

is
that modified state.