Major Section: PROGRAMMING
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.
(mbt x) equals
x. However, in raw Lisp
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
<base> are intended to be terms
involving only the variable
(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
(implies <test> (o< (acl2-countBut suppose we need to know that
<rec-x>) (acl2-count x)))
<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
(mbt <g>), then evaluation of every recursive call of
foowill cause the evaluation of (the appropriate instance of)
<g>. But since
(mbt <g>)expands to
tin 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,
<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-countHere is a specific example based on one sent by Vernon Austel.
<rec-x>) (acl2-count x)))
(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 )))))If you
(defthm recurX2-0 (equal (recurX2 n) 0))
acl2-count), you will see that evaluation of
(recurX2 2)causes several calls of
verify-guards. But this evaluation does not call
verify-guards, because the ACL2 evaluation mechanism uses raw Lisp to do the evaluation, and the form
(mbt (< (acl2-count call) n))macroexpands to
tin Common Lisp.