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