Meta reasoning using valid terms extracted from context or world

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 (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

Sol Swords has contributed a community book,

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
`clause-processor`
rules is entirely analogous. (At the end, though, we discuss the last of the
four forms displayed above.) And for

Below we describe properties of

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

Next we present an example, which comes from the community book,

Our example includes this meta rule.

(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 illustrate the two basic kinds of meta-extract
hypotheses: applications of the evaluator to a call of

(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

(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

(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

(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

Finally, we document what is provided logically by calls of
`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

First we consider the value of

CASE

obj =(list :formula FN) :In this case

(meta-extract-global-fact obj state) is equal to(meta-extract-formula FN state) . That, in turn, evaluates to the ``formula'' ofFN in the following sense whenstate is the ACL2 ``live'' state object. IfFN is a function symbol with formals(X1 ... Xk) , then the formula is the constraint onFN ifFN is constrained or introduced bydefchoose, and otherwise is(equal (FN X1 ... Xk) BODY) , whereBODY is the (unsimplified) body of the definition ofFN . Otherwise, ifFN 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, treatN as 0. Then(meta-extract-global-fact obj state) is equal to the term naturally constructed from therewrite-rule record structure(nth N (getpropc FN 'lemmas nil (w state))) ifN is in range, else*t* . (The ACL2 source functionrewrite-rule-term does this construction of a term from arewrite-rule record structure. It has a guard oft ; a version that may execute more quickly but has a less trivial guard isrewrite-rule-term-exec .) Thus, ifFN is a function symbol with more thanN associated lemmas — ``associated'' in the sense of being either a: definitionrule forFN or a: rewriterule forFN whose left-hand side has a top function symbol ofFN — then whenstate is the actual ACL2 ``live'' state object,(meta-extract-global-fact obj state) evaluates to theN th such lemma (with zero-based indexing).CASE

obj =(list :linear-lemma FN N) :Assume

N is a natural number; otherwise, treatN as 0. Then(meta-extract-global-fact obj state) is equal to the term naturally constructed from thelinear-lemma record structure(nth N (getpropc FN 'linear-lemmas nil (w state))) ifN is in range, else*t* . (The ACL2 source functionlinear-lemma-term does this construction of a term from alinear-lemma record structure. It has a guard oft ; a version that may execute more quickly but has a less trivial guard islinear-lemma-term-exec .) Thus, ifFN is a function symbol with more thanN associated linear-lemmas — ``associated'' in the sense of being a: linearrule that has a max-term whose top function symbol isFN — then whenstate is the actual ACL2 ``live'' state object,(meta-extract-global-fact obj state) evaluates to theN th such linear lemma (with zero-based indexing).CASE

obj =(list :fncall FN ARGLIST) :Consider the term

(magic-ev-fncall FN ARGLIST state t nil) , which is axiomatized to return a multiple values pair(mv erp val) , and moreover: ifstate is the actual ACL2 ``live'' state anderp isnil , thenval is the result of applyingfn toarglist . For example, after submitting(defun foo (z) (mv (cdr z) (car z))) , we can evaluate a corresponding call ofmagic-ev-fncall as follows, noting that for this purpose the macromvis given its logical meaning,list:ACL2 !>(magic-ev-fncall 'foo '((a b c)) state t nil) (NIL ((B C) A)) ACL2 !>Let

erp andval be as above: more precisely, let them abbreviate the terms(nth '0 (magic-ev-fncall FN ARGLIST state t nil)) and(nth '1 (magic-ev-fncall FN ARGLIST state t nil)) , respectively. Then(meta-extract-global-fact obj state) is either*t* , in the ``error case'' thaterp is notnil , or else is a term that equatesval with the application ofFN toARGLIST , as follows. Assume thatFN is a: logic-mode function symbol and thatARGLIST is a true list of values of the same length as list of formal parameters forFN (i.e., as the input arity ofFN ). Let(QARG1 ... QARGk) be the result of quoting each element ofARGLIST , i.e., replacing eachy inARGLIST by the two-element list(quote y) . Then(meta-extract-global-fact obj state) reduces to the term(equal (FN QARG1 ... QARGk) (quote val)) .CASE otherwise:

For any other values of

obj , the value is*t* .

Finally, the value of

CASE

obj = (list :typeset TERM ...):The value is the value of

(typespec-check ts TERM) , wherets is the value of(mfc-ts TERM mfc state :forcep nil :ttreep nil) , and where(typespec-check ts val) is defined to be true whenval has type-setts . (Exception: Ifval satisfiesbad-atom thentypespec-check is true whents is negative.)CASE

obj = (list :rw+ TERM ALIST OBJ EQUIV ...):We assume below that

EQUIV is a symbol that represents an equivalence relation, wherenil representsequal,t representsiff, and otherwiseEQUIV represents itself (an equivalence relation in the current logical world). For any otherEQUIV the value is*t* . Now letrhs 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 byEQUIV , andsublis-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 ofnil , i.e., for the case thatobj 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 ofsublis-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* .CASE otherwise:

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

- Def-meta-extract
- Generate macros and theorems convenient for using meta-extract with a given evaluator.
- Fn-get-def
- Look up a function's definition from the world.