Major Section: PROGRAMMING
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).
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.
