Major Section: BDD
The function IF* is defined to be IF, but it is used in a
special way by ACL2's BDD package.
As explained elsewhere (see bdd-algorithm), ACL2's BDD
algorithm gives special treatment to terms of the form
(IF* TEST TBR FBR). In such cases, the algorithm simplifies
TEST first, and the result of that simplification must be a
constant (normally t or nil, but any non-nil explicit value is
treated like t here). Otherwise, the algorithm aborts.
Thus, IF* may be used to implement a sort of conditional
rewriting for ACL2's BDD package, even though this package only
nominally supports unconditional rewriting. The following contrived
example should make this point clear.
Suppose that we want to prove that (nthcdr (length x) (append x y))
is equal to y, but that we would be happy to prove this only for
lists having length 4. We can state such a theorem as follows.
(let ((x (list x0 x1 x2 x3)))
(equal (nthcdr (length x) (append x y))
y))
If we want to prove this formula with a :BDD hint, then we need to
have appropriate rewrite rules around. First, note that LENGTH is
defined as follows (try :PE LENGTH):
(length x)
=
(if (stringp x)
(len (coerce x 'list))
(len x))
Since BDD-based rewriting is merely very simple unconditional
rewriting (see bdd-algorithm), we expect to have to prove a
rule reducing STRINGP of a CONS:
(defthm stringp-cons
(equal (stringp (cons x y))
nil))
Now we need a rule to compute the LEN of X, because the definition
of LEN is recursive and hence not used by the BDD package.
(defthm len-cons
(equal (len (cons a x))
(1+ (len x))))
We imagine this rule simplifying (LEN (LIST X0 X1 X2 X3)) in terms of
(LEN (LIST X1 X2 X3)), and so on, and then finally (LEN nil) should
be computed by execution (see bdd-algorithm).We also need to imagine simplifying (APPEND X Y), where still X is
bound to (LIST X0 X1 X2 X3). The following two rules suffice for
this purpose (but are needed, since APPEND, actually BINARY-APPEND,
is recursive).
(defthm append-cons
(equal (append (cons a x) y)
(cons a (append x y))))
(defthm append-nil
(equal (append nil x)
x))
Finally, we imagine needing to simplify calls of NTHCDR, where the
first argument is a number (initially, the length of
(LIST X0 X1 X2 X3), which is 4). The second lemma below is the
traditional way to accomplish that goal (when not using BDDs), by
proving a conditional rewrite rule. (The first lemma is only proved
in order to assist in the proof of the second lemma.)
(defthm fold-constants-in-+
(implies (and (syntaxp (quotep x))
(syntaxp (quotep y)))
(equal (+ x y z)
(+ (+ x y) z))))
(defthm nthcdr-add1-conditional
(implies (not (zp (1+ n)))
(equal (nthcdr (1+ n) x)
(nthcdr n (cdr x)))))
The problem with this rule is that its hypothesis makes it a
conditional rewrite rule, and conditional rewrite rules
are not used by the BDD package. (See bdd-algorithm for a
discussion of ``BDD rules.'') (Note that the hypothesis cannot
simply be removed; the resulting formula would be false for n = -1
and x = '(a), for example.) We can solve this problem by using
IF*, as follows; comments follow.
(defthm nthcdr-add1
(equal (nthcdr (+ 1 n) x)
(if* (zp (1+ n))
x
(nthcdr n (cdr x)))))
How is nthcdr-add1 applied by the BDD package? Suppose that the BDD
computation encounters a term of the form (NTHCDR (+ 1 N) X).
Then the BDD package will apply the rewrite rule nthcdr-add1. The
first thing it will do when attempting to simplify the right hand
side of that rule is to attempt to simplify the term (ZP (1+ N)).
If N is an explicit number (which is the case in the scenario we
envision), this test will reduce (assuming the executable
counterparts of ZP and BINARY-+ are enabled) to t or
to nil. In fact, the lemmas above (not including the lemma
nthcdr-add1-conditional) suffice to prove our goal:
(thm (let ((x (list x0 x1 x2 x3)))
(equal (nthcdr (length x) (append x y))
y))
:hints (("Goal" :bdd (:vars nil))))
If we execute the following form that disables the definition and
executable counterpart of the function ZP
(in-theory (disable zp (zp)))before attempting the proof of the theorem above, we can see more clearly the point of using
IF*. In this case, the prover makes
the following report.
ACL2 Error in ( THM ...): Unable to resolve test of IF* for term (IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X))) under the bindings ((X (CONS X0 (CONS X1 (CONS X2 #)))) (N '3)) -- use SHOW-BDD to see a backtrace.If we follow the advice above, we can see rather clearly what happened. See show-bdd.
ACL2 !>(show-bdd)
BDD computation on Goal yielded 21 nodes.
==============================
BDD computation was aborted on Goal, and hence there is no
falsifying assignment that can be constructed. Here is a backtrace
of calls, starting with the top-level call and ending with the one
that led to the abort. See :DOC show-bdd.
(LET ((X (LIST X0 X1 X2 X3)))
(EQUAL (NTHCDR (LENGTH X) (APPEND X Y)) Y))
alist: ((Y Y) (X3 X3) (X2 X2) (X1 X1) (X0 X0))
(NTHCDR (LENGTH X) (APPEND X Y))
alist: ((X (LIST X0 X1 X2 X3)) (Y Y))
(IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))
alist: ((X (LIST* X0 X1 X2 X3 Y)) (N 3))
ACL2 !>
Each of these term-alist pairs led to the next, and the test of the
last one, namely (ZP (+ 1 N)) where N is bound to 3, was
not simplified to t or to nil.What would have happened if we had used IF in place of IF* in
the rule nthcdr-add1? In that case, if ZP and its executable
counterpart were disabled then we would be put into an infinite
loop! For, each time a term of the form (NTHCDR k V) is
encountered by the BDD package (where k is an explicit number), it
will be rewritten in terms of (NTHCDR k-1 (CDR V)). We would
prefer that if for some reason the term (ZP (+ 1 N)) cannot be
decided to be t or to be nil, then the BDD computation should
simply abort.
Even if there were no infinite loop, this kind of use of IF* is
useful in order to provide feedback of the form shown above whenever
the test of an IF term fails to simplify to t or to nil.
