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.
(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 formula we will focus on is
(defun run (s n) (if (zp n) s (run (stp s) (- n 1))))
(thm (equal (run s 7) xxx))This is not a theorem, of course. But we want to test our advice on non-theorems because we do not want the advice to work only for proofs that succeed. (In the past, we gave advice about using computed hints and that advice caused the theorem prover to run forever when given formulas that it couldn't prove -- but most of the time the system is presented with formulas it cannot prove!)
Furthermore, without some kind of additional rules, the
(run s 7)
expression in the conjecture above will not expand at all, because ACL2's
heuristics do not approve.
In fact, we do not want to take chances that
run will be
expanded -- we want to control its expansion completely.
(in-theory (disable run))
Now, what do we want? (That is always a good question to ask!) We want
(run s 7) to expand ``slowly.'' In particular, we want it to expand
(run (stp s) 6). Then we want the
stp to be expanded and
fully simplified before the
run expression is expanded again. That is,
we want to force the expansion of
run whenever the goal is stable under
simplification. This is sometimes called ``staged simplification.''
We can achieve staged simplification for any given function symbol by defining the functions shown below and then using a simple computed hint:
(thm (equal (run s 7) xxx) :hints ((stage run)))
By inspecting how
stage is defined you can see how to extend it,
but we explain as we go. To experiment, you can just paste the
definitions (and defmacro) below into your ACL2 shell and then
First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol
in a given term.
(mutual-recursion (defun find-first-call (fn term) ; Find the first call of fn in term. (cond ((variablep term) nil) ((fquotep term) nil) ((equal (ffn-symb term) fn) term) (t (find-first-call-lst fn (fargs term))))) (defun find-first-call-lst (fn lst) ; Find the first call of fn in a list of terms. (cond ((endp lst) nil) (t (or (find-first-call fn (car lst)) (find-first-call-lst fn (cdr lst)))))))
We will arrange for the computed hint to generate an
hint for the first call of
fn, whenever the goal becomes
stable under simplification. If no call is found, the
hint will do nothing. To make sure the hint will not loop
indefinitely (for example, by forcing
fn to expand only to
have the rewriter ``fold'' it back up again), we will provide
the hint with a bound that stops it after some number of
iterations. Here is the basic function that creates the
expand hint and replaces itself to count down.
(defun stage1 (fn max clause flg) ; If the clause is stable under simplification and there is a call of ; fn in it, expand it. But don't do it more than max times. (let ((temp (and flg (find-first-call-lst fn clause)))) (if temp (if (zp max) (cw "~%~%HINT PROBLEM: The maximum repetition count of ~ your STAGE hint been reached without eliminating ~ all of the calls of ~x0. You could supply a larger ~ count with the optional second argument to STAGE ~ (which defaults to 100). But think about what is ~ happening! Is each stage permanently eliminating a ~ call of ~x0?~%~%" fn) `(:computed-hint-replacement ((stage1 ',fn ,(- max 1) clause stable-under-simplificationp)) :expand (,temp))) nil)))
Suppose that when
stage1 is called,
fn is the function we want to
max is the maximum number of iterations of this expansion,
clause is the current goal clause, and
flg is the value of the
stable-under-simplificationp flag. Then if
clause is stable and we
can find a call of
fn in it, we ask whether
max is exhausted. If
so, we print an ``error message'' to the comment window with
nil (the value of
nil means the hint does
nothing. But if
max is not yet exhausted, we return a new hint. As
you can see above, the hint replaces itself with another
with the same
fn and a decremented
max to be applied to the new
clause and the then-current value of
The hint also contains an
:expand directive for the call of
Thus, if the computed hint was:
(stage1 'run 5 clause stable-under-simplificationp)
(run s 7) occurs in the clause, then it will
(:computed-hint-replacement ((stage1 'run 4 clause stable-under-simplificationp)) :expand ((run s 7)))which will in turn replace the old
stage1hint with the new one and will apply
:expand ((run s 7))to the current goal.
We can make this more convenient by defining the macro:
(defmacro stage (fn &optional (max '100)) `(stage1 ',fn ,max clause stable-under-simplificationp))Note that the macro allows us to either provide the maximum bound or let it default to 100.
Henceforth, we can type
(thm (equal (run s 7) xxx) :hints ((stage run)))to stage the opening of
runup to 100 times, or we can write
(thm (equal (run s 7) xxx) :hints ((stage run 5)))to stage it only 5 times. In the latter example, the system with print a ``error message'' after the fifth expansion.
Note that if we executed
(set-default-hints '((stage run)))then we could attack all theorems (involving
run) with staged simplification (up to bound 100), without typing an explicit hint.
(thm (equal (run s 7) xxx))
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)))