USING-COMPUTED-HINTS-7

Using the stable-under-simplificationp flag
Major Section:  MISCELLANEOUS

A problem with the example in using-computed-hints-6 is that exactly one simplification occurs between each (effective) firing of the hint. Much more commonly we wish to fire a hint once a subgoal has become stable under simplification.

A classic example of this is when we are dealing with an interpreter for some state machine. We typically do not want the ``step'' function to open up on the symbolic representation of a state until that state has been maximally simplified. We will illustrate with a simple state machine.

Let us start by defining the step function, stp, and the corresponding run function that applies it a given number of times. We also prove two theorems for forcing the run function open.

(defun stp (s)
  (+ 1 s))

(defun run (s n) (if (zp n) s (run (stp s) (- n 1))))

(defthm run-0 (equal (run s 0) s))

(defthm run-n+1 (implies (and (integerp n) (< 0 n)) (equal (run s n) (run (stp s) (- n 1)))))

The step function here is trivial: a state is just a number and the step function increments it. In this example we will not be interested in the theorems we prove but in how we prove them. The theorem we will focus on is
(thm (equal (run s 7) (+ 7 s)))
As you can see by trying it, the theorem above is proved trivially.

In the proof, (run s 7) is expanded by run-n+1 to (run (stp s) 6). We want (stp s) to be fully simplified before run is opened again. We sometimes call this ``staged simplification.'' In this example, stp is so simple that it (stp s) is fully simplified as soon as it is expanded! But imagine that it takes several passes through the simplifier to normalize that expression. Our goal is thus to prove the theorem ``slowly,'' expanding and fully simplifying each step before the next step is taken.

The run-n+1 theorem must be initially disabled, or else it will be applied 7 times and blast the expression open, introducing seven calls of stp and (for realistic stp functions) swamping the system with case analysis as all these calls open prematurely.

(in-theory (disable run-n+1))

We will present several solutions. A key idea in our solutions will be to restrict run-n+1 so that it is applicable to one integer. If you are not familiar with the :restrict hint, see hints.

In our first solution, the user must supply a hint that includes the number of times run-n+1 is to be applied. In this example, that number is 7. The hint will enable run-n+1 the first time it fires. (It will actually enable it every time it fires, but that is unimportant because it will be enabled always after the first time, by the inheritance of theories by children.) In addition, the hint must be able to compute the appropriate restriction of run-n+1, which in this case is just the number. The hint will count this number down, using the technique of using-computed-hints-6 to reproduce itself, but using the stable-under-simplificationp flag to trigger the next step. Here is the solution.

(defun run-opener-hint1 (flg n)  ; flg = stable-under-simplificationp
  (if flg
      `(:computed-hint-replacement 
         ((run-opener-hint1 stable-under-simplificationp ,(- n 1)))
        :in-theory (enable run-n+1)
        :restrict ((run-n+1 ((n ,n)))))
      nil))

(thm (equal (run s 7) (+ 7 s)) :hints ((run-opener-hint1 stable-under-simplificationp 7)))

We urge you to run the thm command above and inspect the output. Note how run does not expand all at once but in seven separate stages. Each stage could involve an arbitrary number of simplifications and cases, but in this example each stage only requires one simplification.

In our second solution we will search through the clause and find the first occurrence of run applied to a positive integer and use it generate the restriction. This way, the same hint will work for many different theorems, as long as the second argument of run is a numeric constant.

(mutual-recursion
 (defun find-run-number (term)
   ; Return nil or an integer i such that (run ... 'i) occurs in term.
   (cond ((variablep term) nil)
         ((fquotep term) nil)
         ((and (eq (ffn-symb term) 'run)
               (quotep (fargn term 2))
               (integerp (cadr (fargn term 2)))
               (< 0 (cadr (fargn term 2))))
          (cadr (fargn term 2)))
         (t (find-run-number-lst (fargs term)))))
 (defun find-run-number-lst (lst)
    ; Return nil or an integer i such that (run ... 'i) occurs
    ; in some element of lst.
    (cond ((endp lst) nil)
          (t (or (find-run-number (car lst))
                 (find-run-number-lst (cdr lst)))))))

(defun run-opener-hint2 (clause flg) ; If the clause is stable under simplification and there is a ; suitable i, then enable run-n+1 restricted to i. Else, no hint. (if (and flg (find-run-number-lst clause)) `(:computed-hint-replacement t :in-theory (enable run-n+1) :restrict ((run-n+1 ((n ,(find-run-number-lst clause)))))) nil))

(thm (equal (run s 7) (+ 7 s)) :hints ((run-opener-hint2 clause stable-under-simplificationp)))

This solution is more general than the other because we look in the clause to determine the necessary restriction of the lemma we want to fire.

Note that if we executed

(set-default-hints '((run-opener-hint2 clause stable-under-simplificationp)))
then we could prove the theorem using our new strategy
(thm (equal (run s 7) (+ 7 s)))
without explicitly including the hint.

Using techniques similar to those above we have implemented ``priority phased simplification'' and provided it as a book. See books/misc/priorities.lisp. This is an idea suggested by Pete Manolios, by which priorities may be assigned to rules and then the simplifier simplifies each subgoal maximally under the rules of a given priority before enabling the rules of the next priority level. The book above documents both how we implement it with computed hints and how to use it.

Here is another example of using the stable-under-simplificationp flag to delay certain actions. It defines a default hint, see DEFAULT-HINTS, which will enable non-linear-arithmetic on precisely those goals which are stable-under-simplificationp. It also uses the HISTORY and PSPV variables to determine when toggling non-linear-arithmetic is appropriate. These variables are documented only in the source code. If you start using these variables extensively, please contact the developers of ACL2 or Robert Krug (rkrug@cs.utexas.edu) and let us know how we can help.

(defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
  (cond (stable-under-simplificationp
         (if (not (access rewrite-constant
                          (access prove-spec-var pspv :rewrite-constant)
                          :nonlinearp))
             '(:computed-hint-replacement t
               :nonlinearp t)
           nil))
        ((access rewrite-constant
                 (access prove-spec-var pspv :rewrite-constant)
                 :nonlinearp)
         (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
             '(:computed-hint-replacement t
               :nonlinearp nil)
           nil))
        (t
         nil)))