Mbt
Introduce a test into the logic that, however, evaluates to t
The macro mbt (``must be true'') can be used in order to add
code in order to admit function definitions in :logic mode,
without paying a cost in execution efficiency. Examples below illustrate its
intended use.
Semantically, (mbt x) equals x. However, in raw Lisp (mbt
x) ignores x entirely, and macroexpands to t. ACL2's guard
verification mechanism ensures that the raw Lisp code is only evaluated when
appropriate, since a guard proof obligation (equal x t) is generated.
See verify-guards and, for general discussion of guards, see guard.
Also see mbe, which stands for ``must be equal.'' Although mbt
is more natural in many cases, mbe has more general applicability. In
fact, (mbt x) is essentially defined to be (mbe :logic x :exec
t). Another related utility is mbt*, which generates the same proof
obligation as mbt but logically, is simply t.
We can illustrate the use of mbt on the following generic example,
where <g>, <test>, <rec-x>, and <base> are intended to be
terms involving only the variable x.
(defun foo (x)
(declare (xargs :guard <g>))
(if <test>
(foo <rec-x>)
<base>))
In order to admit this function, ACL2 needs to discharge the proof
obligation that <rec-x> is smaller than x, namely:
(implies <test>
(o< (acl2-count <rec-x>)
(acl2-count x)))
But suppose we need to know that <g> is true in order to prove this.
Since <g> is only the guard, it is not part of the logical
definition of foo. A solution is to add the guard to the definition of
foo, as follows.
(defun foo (x)
(declare (xargs :guard <g>))
(if (mbt <g>)
(if <test>
(foo <rec-x>)
<base>)
nil))
If we do this using <g> rather than (mbt <g>), then evaluation of
every recursive call of foo will cause the evaluation of (the appropriate
instance of) <g>. But since (mbt <g>) expands to t in raw
Lisp, then once we verify the guards of foo, the evaluations of <g>
will be avoided (except at the top level, when we check the guard before
allowing evaluation to take place in Common Lisp).
Other times, the guard isn't the issue, but rather, the problem is that a
recursive call has an argument that itself is a recursive call. For example,
suppose that <rec-x> is of the form (foo <expr>). There is no way
we can hope to discharge the termination proof obligation shown above. A
standard solution is to add some version of this test:
(mbt (o< (acl2-count <rec-x>) (acl2-count x)))
Here is a specific example based on one sent by Vernon Austel.
(defun recurX2 (n)
(declare (xargs :guard (and (integerp n) (<= 0 n))
:verify-guards nil))
(cond ((zp n) 0)
(t (let ((call (recurX2 (1- n))))
(if (mbt (< (acl2-count call) n))
(recurX2 call)
1 ;; this branch is never actually taken
)))))
(defthm recurX2-0
(equal (recurX2 n) 0))
(verify-guards recurX2)
If you (trace$ acl2-count), you will see that evaluation
of (recurX2 2) causes several calls of ACL2-count before the
verify-guards. But this evaluation does not call acl2-count
after the verify-guards, because the ACL2 evaluation mechanism uses raw
Lisp to do the evaluation, and the form (mbt (< (acl2-count call) n))
macroexpands to t in Common Lisp.
You may occasionally get warnings when you compile functions defined using
mbt. (For commands that invoke the compiler, see compilation.)
These can be inhibited by using an ignorable declare form. Here
is a simple but illustrative example. Note that the declarations can
optionally be separated into two declare forms.
(defun foo (x y)
(declare (ignorable x)
(xargs :guard (equal x t)))
(and (mbt x) y))Subtopics
- Mbt$
- Variant of mbt that allows any non-nil value.
