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))
(< 0 (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.