Using the

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,

(defun stp (s) (+ 1 s)) (defun run (s n) (if (zp n) s (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 formula we will focus on is

(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

In fact, we do not want to take chances that

(in-theory (disable run))

Now, what do we want? (That is always a good question to ask!) We want

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

First, define this pair of mutually recursive functions.

(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

(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 `cw` and
return

Thus, if the computed hint was:

(stage1 'run 5 clause stable-under-simplificationp)

and

(:computed-hint-replacement ((stage1 'run 4 clause stable-under-simplificationp)) :expand ((run s 7)))

which will in turn replace the old

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

(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

(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 community book

Here is another example of using the

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