Dealing With Prover Heuristics in ACL2: A Case Study Matt Kaufmann 5/21/03 On Monday (5/19/03) I decided to re-run the ACL2(r) regression suite. (ACL2(r) is the modification of ACL2 for non-standard analysis developed by Ruben Gamboa in his dissertation.) One of the proofs failed. This short talk summarizes my investigation into the problem. It wasn't a very big deal (the whole thing, including a draft of much of these notes, took under an hour), but I think it illuminates the issues a bit in developing heuristics for ACL2 and perhaps other heuristic theorem provers. First, I got to the point of failure: cd ...../v2-8/books/nonstd/nsa/ ../../../allegro-saved_acl2r (lp) (rebuild "trig-approx.lisp" 'ABS-TAYLOR-SIN-TERM-HIGH-2->N-EXPT) (defthm lemma-1 (implies (and (integerp n) (<= 0 n) (realp x) (< 0 x)) (equal (/ (2-to-the-n n)) (n-expt 1/2 n)))) The proof goes into induction: We will induct according to a scheme suggested by (EXPT '2 N)..... It gets to Subgoal *1/5'', and then: HARD ACL2 ERROR in REWRITE: The call depth limit of 1000 has been exceeded in the ACL2 rewriter. There is probably a loop caused by some set of enabled rules. To see why the limit was exceeded, try the proof again after you first execute :brr t and then execute the form (cw-gstack). See :DOC rewrite-stack-limit. ............................................................ So then, after :brr t and another try (and another abort): ............................................................ ACL2(r) !>(cw-gstack) ... 20. Attempting to apply (:DEFINITION EXPT) to (EXPT '2 N) ... 23. Attempting to apply (:REWRITE EXPT-2-X-1) to (EXPT '2 (BINARY-+ '-1 N)) ... 26. Attempting to apply (:DEFINITION EXPT) to (EXPT '2 N) ... 29. Attempting to apply (:REWRITE EXPT-2-X-1) to (EXPT '2 (BINARY-+ '-1 N)) ... ............................................................ The loop is evident above, and is confirmed by inspection of the relevant rules: ACL2(r) !>:pe expt ..... >V (DEFUN EXPT (R I) ..... (COND ((ZIP I) 1) ((= (FIX R) 0) 0) ((> I 0) (* R (EXPT R (+ I -1)))) (T (* (/ R) (EXPT R (+ I 1)))))) ACL2(r) !>:pe expt-2-x-1 ..... > (DEFTHM EXPT-2-X-1 (IMPLIES (AND (INTEGERP X) (< 0 X)) (EQUAL (EXPT 2 (+ -1 X)) (* 1/2 (EXPT 2 X)))) .....) ............................................................ The proof succeeded in v2-7, so I brought up ACL2(r) Version 2.7 and did (trace$ rewrite-atm) in both. Below I highlight the two "rewrite constant" arguments. In v2-7, (EXPT '2 N) is to be expanded (like an :EXPAND hint), while (EXPT '2 (BINARY-+ N '1)) and (EXPT '2 (BINARY-+ N '-1)) are to be left alone (like a :HANDS-OFF hint). But in v2-8, there are no such directives, which is allowing (EXPT '2 (BINARY-+ N '-1)) to rewrite to (EXPT '2 N) and back again. v2-7: 1> (REWRITE-ATM (EQUAL '1 (BINARY-* (EXPT '2 (BINARY-+ N '-1)) (N-EXPT '1/2 (BINARY-+ '-1 N)))) ..... (:STANDARD |some-enabled-structure| ((1) NIL (EXPT '2 N)) (T NIL (EXPT '2 (BINARY-+ N '1)) (EXPT '2 (BINARY-+ N '-1))) ..... ) |*the-live-state*|) v2-8: 1> (REWRITE-ATM (EQUAL '1 (BINARY-* (EXPT '2 (BINARY-+ N '-1)) (N-EXPT '1/2 (BINARY-+ '-1 N)))) ..... (:STANDARD |some-enabled-structure| ((1) NIL) (T NIL ) ..... ) |*the-live-state*|) ............................................................ This change is explained in the v2-8 :DOC topic NOTE-2-8-PROOFS: A change has been made in heuristics for controlling rewriting during proofs by induction. Formerly, during induction proofs, ACL2 suppressed rewriting of certain "induction hypothesis" terms, and forced expansion of certain "induction conclusion" terms, until rewriting had stabilized. This meddling with the rewriter is still turned off when rewriting has stabilized, but it is now turned off earlier once an ancestor has been through the rewriter and the current goal is free of "induction conclusion" terms. Thanks to Dave Greve and Matt Wilding for providing an example and associated analysis that led us to look for a heuristic modification. In the output, we can see that (EXPT 2 N) first disappears in Subgoal *1/5'', which leads to the infinite loop in v2-8: Subgoal *1/5 (IMPLIES (AND (NOT (ZIP N)) (NOT (= (FIX 2) 0)) (< 0 N) (EQUAL 1 (* (EXPT 2 (+ N -1)) (N-EXPT 1/2 (+ N -1)))) (INTEGERP N) (<= 0 N) (REALP X) (< 0 X)) (EQUAL 1 (* (EXPT 2 N) (N-EXPT 1/2 N)))). By the :executable-counterparts of = and FIX we reduce the conjecture to Subgoal *1/5' (IMPLIES (AND (NOT (ZIP N)) (< 0 N) (EQUAL 1 (* (EXPT 2 (+ N -1)) (N-EXPT 1/2 (+ N -1)))) (INTEGERP N) (<= 0 N) (REALP X) (< 0 X)) (EQUAL 1 (* (EXPT 2 N) (N-EXPT 1/2 N)))). This simplifies, using the :compound-recognizer rule ZIP-COMPOUND-RECOGNIZER, the :definition EXPT, the :executable-counterparts of EQUAL and FIX and the :rewrite rules COMMUTATIVITY-2-OF-*, COMMUTATIVITY-OF-* and COMMUTATIVITY-OF-+, to Subgoal *1/5'' (IMPLIES (AND (< 0 N) (EQUAL 1 (* (EXPT 2 (+ N -1)) (N-EXPT 1/2 (+ -1 N)))) (INTEGERP N) (<= 0 N) (REALP X) (< 0 X)) (EQUAL 1 (* 2 (N-EXPT 1/2 N) (EXPT 2 (+ N -1))))). ............................................................ Interestingly, if you instead submit Subgoal *1/5'' as a standalone theorem, you get the infinite loop in v2-7 as well. The two rules in question are inherently dangerous to keep together, and the only issue is how hard we want to avoid this problem during proofs by induction. I had perhaps feared for a moment that this example would provide evidence that we should reconsider this heuristic change. But I'm confortable with it, since the infinite loop in this example could have occurred even in v2-7 (just not during this part of an induction proof). Note: Preceding the problematic event with (in-theory (disable expt-2-x-1)) solved the problem.