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.

In brief: if a metafunction application to a term,

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,

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,

(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

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

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

: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

(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

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

Suppose that instead we had defined

(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

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,

- If there is a hypothesis metafunction,
hyp-fn , then lethyps be the list of hypothesis terms returned by the call ofhyp-fn onterm . More precisely, the term returned by the call ofhyp-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 benil .

When this rule is applied by calling