META-EXTRACT

meta reasoning using valid terms extracted from context or world 
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 Nth 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.