META-EXTRACT

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