wrapper.tex

The community book ``clause-processors/meta-extract-user.lisp'' is
designed to allow more convenient use of the meta-extract facility.
The main contribution of this book is in the event-generating macro
\href{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2\_\_\_\_DEF-META-EXTRACT}{\underline{\tt def-meta-extract}}. For a given pseudo-evaluator \texttt{evl},
\texttt{def\-/meta\-/extract} produces macros
\texttt{evl\-/meta\-/extract\-/contextual\-/facts} and
\texttt{evl\-/meta\-/extract\-/global\-/facts} that expand to meta-extract
hypotheses where the \texttt{obj} argument is a call of a ``bad-guy'' (Skolem)
% Reviewer 1 says:
%%% section 3, line 5: I understand the "bad-guy" from experience with other ACL2
%%% utilities and with defun-sk, but I wonder if it should be explained in slightly
%%% more detail.
% That's a fair point.  In fact, although I get the bad-guy idea in
% general (pick a counterexample if there is one, and then by asserting
% that it's not a counterexample one is asserting the universal
% closure), I'm not completely sure that I'm getting it here.  I
% *think* we're picking an obj for which
% (evl (meta-extract-contextual-fact obj mfc state) a) fails, if there
% is one.  I've made my edits under that assumption, but please
% correct this if I'm wrong!
function.  This essentially universally quantifies the \texttt{obj}
argument: informally, the term
\begin{lstlisting}
  <$\var{obj}_0 = $> (evl-meta-extract-contextual-bad-guy a mfc state)
\end{lstlisting}
is
some {\tt obj} for which the formula
\begin{lstlisting}
  <$\varphi = $> (evl (meta-extract-contextual-fact obj mfc state) a)
\end{lstlisting}
is false, if any such {\tt obj} exists; so by
asserting that $\varphi$ is true for $\var{obj}_0$, we assert $(\forall\ \var{obj})\ 
\varphi$.  Therefore,
\begin{verbatim}
  (evl (meta-extract-contextual-fact
         (evl-meta-extract-contextual-bad-guy a mfc state)
         mfc state)
       a)
\end{verbatim}
implies that for any \texttt{obj},
\begin{verbatim}
  (evl (meta-extract-contextual-fact obj mfc state) a).
\end{verbatim}

The \texttt{def\-/meta\-/extract} utility also proves several theorems
about the pseudo-evaluator.  They are proven by
functional instantiation of similar theorems proved in
``meta-extract-user.lisp'' about a base evaluator that only supports
the six functions {\tt typespec-check}, {\tt if}, {\tt equal}, {\tt
  not}, {\tt iff}, and {\tt implies}; this means that {\tt evl} must
also support at least these six functions for the utility to work.


The theorems proved by \texttt{def\-/meta\-/extract} obviate the need for the user to reason about
the specifics of the definitions of
\texttt{meta\-/extract\-/contextual\-/fact} and
\texttt{meta\-/extract\-/global\-/fact+} and the proper construction
of their \texttt{obj} arguments, while still supporting all the facilities listed in Section~\ref{sec:general}.
For example, this rule shows that
\texttt{(evl\-/meta\-/extract\-/global\-/facts)} implies the correctness of \texttt{meta\-/extract\-/formula} (and makes no reference to the form of the \texttt{obj} argument to \texttt{meta\-/extract\-/global\-/fact}):
\begin{verbatim}
 (defthm evl-meta-extract-formula
   (implies (and (evl-meta-extract-ev-global-facts)
                 (equal (w st) (w state)))
            (evl (meta-extract-formula name st) a)))

\end{verbatim}
This rule shows that
\texttt{(evl\-/meta\-/extract\-/contextual\-/facts a)} implies the correctness
of \texttt{mfc-rw+} (specifically, when \texttt{nil}, meaning
\texttt{equal}, is given as the equivalence relation argument):
\begin{verbatim}
 (defthm evl-meta-extract-rw+-equal
    (implies (evl-meta-extract-contextual-facts a)
             (equal (evl (mfc-rw+
                          term alist obj nil
                          mfc state :forcep nil)
                         a)
                    (evl (sublis-var alist term) a))))
\end{verbatim}
The above rule involves the system function {\tt sublis-var}, which
substitutes {\tt alist} into {\tt term} but reduces ground calls of
primitive functions\footnote{By ``primitive functions'' we mean
  built-in functions such as {\tt binary-+} that do not have defining
  events --- that is, those found in the ACL2 constant {\tt
    *primitive-formals-and-guards*}.} to their values.  In order to
reason about {\tt sublis-var}, the pseudo-evaluator should support all of
the primitive functions that it treats specially.  The community book
``clause-processors/sublis-var-meaning.lisp'' defines a
pseudo-evaluator {\tt cterm-ev} that supports exactly these functions
and proves the following theorem that describes how {\tt sublis-var}
evaluates:
\begin{verbatim}
(defthm eval-of-sublis-var
  (implies (and (pseudo-termp x)
                (not (assoc nil alist)))
           (equal (cterm-ev (sublis-var alist x) a)
                  (cterm-ev x (append (cterm-ev-alist alist a) a)))))
\end{verbatim}

To reason about {\tt mfc-rw+}, {\tt mfc-rw}, and {\tt
  mfc-relieve-hyp}, whose meta-extract assumptions all involve {\tt
  sublis-var}, one can define a pseudo-evaluator that supports both
the functions required for \texttt{def\-/meta\-/extract} and for {\tt
  sublis-var}.  Community book ``centaur/misc/context-rw.lisp'', for
example, defines a pseudo-evaluator supporting all these functions,
uses {\tt def-meta-extract}, and functionally instantiates the above
theorem about {\tt sublis-var} to allow it to reason about {\tt
  mfc-rw+}.


% \begin{comment}
% Sol, the list above seems to be more or less just
%   saying that the theorems provided by def-meta-extract are those
%   described in Section~\ref{sec:general} (file meta-extract.tex).
%   That's probably fine, but we should make the connection, I think.
%   I've attempted to do that by saying, at the start of
%   Section~\ref{sec:general}, that ``These forms correspond to the
%   theorems described at the end of Section~\ref{sec:user}.''  Is that
%   sufficient?

%   [Sol] - I switched it around so that instead of listing the theorems
%   here I just say they try to support all the forms listed in Section
%   \ref{sec:general}.

%   I could add a little bit about what it would look like to prove
%   (say) the theorem from the second example using one bad-guy hyp
%   instead of three specific hyps but I'm not sure if it would clarify
%   much.

%   [Matt] Thanks --- looks good.  Yep, I think it's probably not be
%   worth showing how a bad-guy hypothesis is used, though if you decide
%   you want to do that, I won't object.  More useful might be giving an
%   example of using context-rw.lisp.  The description above made sense
%   on a sort of word-by-word basis, but I feel sort of fuzzy about it,
%   and outlining an example would probably help.  (But don't bother
%   unless you feel like doing that.)

% \end{comment}