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.