IF*

for conditional rewriting with BDDs 
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 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.