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
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 (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
(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.
run-n+1 theorem must be initially disabled, or else it will
be applied 7 times and blast the expression open, introducing seven
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
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
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))We urge you to run the
(thm (equal (run s 7) (+ 7 s)) :hints ((run-opener-hint1 stable-under-simplificationp 7)))
thmcommand above and inspect the output. Note how
rundoes 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)))))))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.
(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)))
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
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 (
firstname.lastname@example.org) and let us know how we can
(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)))