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.
(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.
Therefore, disable run.
(in-theory (disable run-n+1))
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
once, to (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
try the thm command.
First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol fn
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 :EXPAND
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
expand, 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 cw and
return nil (the value of cw). That 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 stage1 hint
with the same fn and a decremented max to be applied to the new
clause and the then-current value of stable-under-simplificationp.
The hint also contains an :expand directive for the call of fn
found.
Thus, if the computed hint was:
(stage1 'run 5 clause stable-under-simplificationp)
and (run s 7) occurs in the clause, then it will
generate
(:computed-hint-replacement ((stage1 'run 4 clause stable-under-simplificationp)) :expand ((run s 7)))which will in turn replace the old
stage1 hint 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 run up 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 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)))
