		Search-engine friendly clone of the ACL2 documentation.

Meta

Meta-implicit-hypothesis

A potentially more efficient way of coding a hypothesis metafunction

We assume familiarity with meta rules. In this topic, we discuss a relatively advanced capability of meta reasoning in ACL2 that can increase its efficiency.

Introduction

In brief: if a metafunction application to a term, u, evaluates to a result of the form (if TEST NEW-TERM u), then TEST is treated as an ``implicit hypothesis,'' which must rewrite to true in order for the meta rule to simplify the input term. We now explain in more detail.

Recall the general form of a meta rule:

(implies (and (pseudo-termp x)        ; this hyp is optional
              (alistp a)              ; this hyp is optional
              (ev (hyp-fn x ...) a)   ; this hyp is optional
              ; meta-extract hyps may also be included (see below)
              )
         (equiv (ev x a)
                (ev (fn x ...) a)))

When this rule is to be applied to a term, x, then (hyp-fn x ...) is evaluated to produce a term, which must rewrite to true in order to evaluate the call (fn x ...), which is then rewritten to a replacement for x. But it may be that these calls of hyp-fn and fn share a sub-computation. ACL2 provides the ``implicit hypothesis'' mechanism in order to share such a sub-computation. The next section illustrates how this mechanism works. The final section provides a precise specification of implicit hypotheses and how they are used in metareasoning.

Example

The following example is trivial but illustrates the sort of situation for which implicit hypotheses can be useful. First let us introduce a function and an evaluator (see defevaluator).

(defun foo (x y)
  (+ x y))

(defevaluator evl evl-list
  ((if x y z)
   (foo x y)
   (binary-+ x y)
   (unary-- x)
   (acl2-numberp x)
   (not x)))

Let us write a meta function and associated hypothesis metafunction that apply a common function, meta-helper, to a term, term, to return one of two multiple values: (mv nil term) in the case that there is no simplification; else (mv hyp new-term), where the following is a theorem: `(implies ,hyp (equal ,term ,new-term)). Of course, the following definition introduces a function whose calls can be evaluated very quickly; but for purposes of this example, let us pretend that calls of meta-helper take a great deal of time to evaluate.

(defun meta-helper (term) ; PRETEND that his function is expensive to compute!
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    (('foo x ('foo y ('unary-- x)))
     (declare (ignore x))
     (mv `(acl2-numberp ,y)
         y))
    (& (mv nil term))))

We can now define our meta function and hypothesis metafunction and prove a meta rule based on them.

(defun meta-fn (term)
  (declare (xargs :guard (pseudo-termp term)))
  (mv-let (hyp new-term)
          (meta-helper term)
          (if hyp new-term term)))

(defun meta-hyp-fn (term)
  (declare (xargs :guard (pseudo-termp term)))
  (mv-let (hyp new-term)
          (meta-helper term)
          (declare (ignore new-term))
          (or hyp ''nil)))

(defthm meta-fn-correct
  (implies (evl (meta-hyp-fn x) a)
           (equal (evl x a)
                  (evl (meta-fn x) a)))
  :rule-classes ((:meta :trigger-fns (foo))))

In order to see this meta rule in action, let us disable foo and try a little test.

(in-theory (disable foo))

(defthm meta-fn-correct-test
  (implies (acl2-numberp b)
           (equal (foo a (foo b (- a)))
                  b)))

Happily, the test succeeds, with the summary showing that our meta rule, meta-fn-correct, was indeed used in the proof. But if we first submit the form (trace$ meta-fn meta-hyp-fn meta-helper), we will see that meta-helper is called twice on the term (FOO A (FOO B (UNARY-- A))): once on behalf of meta-fn and once on behalf of meta-hyp-fn. This would be unfortunate if meta-helper were expensive to compute.

So let us back up and try a different approach, which illustrates the idea of using an ``implicit hypothesis'' in order to avoid recomputation. This time, we avoid defining a hypothesis metafunction, but instead we define meta-fn to return a term of the form (if TEST NEW-TERM term). Here, TEST is `(acl2-numberp ,y); we call this an ``implicit hypothesis.''

:ubt! meta-fn

(defun meta-fn (term)
  (declare (xargs :guard (pseudo-termp term)))
  (mv-let (hyp new-term)
          (meta-helper term)
          (if hyp ; the interesting case
              `(if ,hyp ,new-term ,term)
            term)))

There is nothing remarkable in the proof of the corresponding meta rule.

(defthm meta-fn-correct
  (equal (evl x a)
         (evl (meta-fn x) a))
  :rule-classes ((:meta :trigger-fns (foo))))

Let us test our new implementation. If we first evaluate the form (trace$ meta-fn meta-helper), we will see that this time, meta-helper is called only once on the term (FOO A (FOO B (UNARY-- A))).

(in-theory (disable foo))

(defthm meta-fn-correct-test
  (implies (acl2-numberp b)
           (equal (foo a (foo b (- a)))
                  b)))

Note that the following proof attempt fails but does not loop. Naively, one might expect it to loop, since the false branch of the IF term returned by meta-fn has the original (input) term as its false branch. However, ACL2 notices the special form (if TEST NEW-TERM term) of the term returned by calling meta-fn, and treats this result as though TEST is the term returned by a hypothesis metafunction and NEW-TERM is the term returned by the metafunction.

(thm ; FAILS but does not loop!
 (equal (foo a (foo b (- a)))
        b))

Suppose that instead we had defined meta-fn as follows, that is, with the `then' and `else' branches swapped.

(defun meta-fn (term)
  (declare (xargs :guard (pseudo-termp term)))
  (mv-let (hyp new-term)
          (meta-helper term)
          (if hyp ; the interesting case ;
              `(if (not ,hyp) ,term ,new-term)
            term)))

Then the events above go through as before, up to the thm form. But that form loops, because the generated IF term no longer has the special form (if TEST NEW-TERM term). In the (likely rare) case that really wishes to allow an unresolved case split for which one branch is the original term, this swapping of branches is available to defeat the recognition of an implicit hypothesis.

Precise specification

Consider a meta rule:

(implies (and (pseudo-termp x)        ; this hyp is optional
              (alistp a)              ; this hyp is optional
              (ev (hyp-fn x ...) a)   ; this hyp is optional
              ; meta-extract hyps may also be included (see below)
              )
         (equiv (ev x a)
                (ev (fn x ...) a)))

Recall that when this rule is applied to a term, term, then a list of hypotheses is initially generated as follows, where each generated hypothesis must be rewritten to a non-nil value in order for the rule to fire.

If there is a hypothesis metafunction, hyp-fn, then let hyps be the list of hypothesis terms returned by the call of hyp-fn on term. More precisely, the term returned by the call of hyp-fn is flattened into a list of ``hypothesis terms,'' so that for example the (translated) conjunction (if a (if b c 'nil) 'nil) generates the list (a b c) of hypothesis terms.
Otherwise, let hyps be nil.

When this rule is applied by calling fn on a term, term, we say that a term, test, is an ``implicit hypothesis'' if the value returned by that call of fn is a term of the form (if test new-term term): that is, test is the test of the resulting if term and the input term is the false branch of that if term. In this case, ACL2 recognizes test as an implicit hypothesis, which triggers two changes made in how this meta rule is applied. First, hyps is extended by the flattened list of hypotheses generated from test. Second, instead of applying hyp-fn to the original term, term, hyp-fn is applied to new-term.