USING-COMPUTED-HINTS-6.html -- ACL2 Version 3.1

USING-COMPUTED-HINTS-6

Using the computed-hint-replacement feature

Major Section:  MISCELLANEOUS

So far none of our computed hints have used the :COMPUTED-HINT-REPLACEMENT feature. We now illustrate that.

The :computed-hint-replacement feature can easily lead to loops. So as you experiment with the examples in this section and your own hints using this feature, be ready to interrupt the theorem prover and abort!

A non-looping use of the :computed-hint-replacement feature would be a hint like this:

(if (certain-terms-present clause)
    '(:computed-hint-replacement t
      :in-theory (enable lemma25))
    '(:computed-hint-replacement t
      :in-theory (disable lemma25)))

In this hint, if certain terms are present in clause, as determined by the function with the obvious name (here undefined), then this hint enables lemma25 and otherwise disables it. Lemma25 might be a very expensive lemma, e.g., one that matches frequently and has an expensive and rarely established hypothesis. One might wish it enabled only under certain conditions. Recall that theories are inherited by children. So once lemma25 is enabled it ``stays'' enabled for the children, until disabled; and vice versa. If the :computed-hint-replacement feature were not present and computed hints were always deleted after they had been used, then lemma25 would be left enabled (or disabled) for all the childen produced by the first firing of the hint. But with the arrangement here, every subgoal gets a theory deemed suitable by the hint, and the hint persists.

Now we will set up a toy to allow us to play with computed hints to understand them more deeply. To follow the discussion it is best to execute the following events.

(defstub wrapper (x) t)
(defaxiom wrapper-axiom (wrapper x) :rule-classes nil)

Now submit the following event and watch what happens.

(thm (equal u v)
  :hints (`(:use (:instance wrapper-axiom (x a)))))

The theorem prover adds (wrapper a) to the goal and then abandons the proof attempt because it cannot prove the subgoal. Since the computed hint is deleted upon use, the hint is not applied to the subgoal (i.e., the child of the goal).

What happens if we do the following?

(thm (equal u v)
  :hints (`(:computed-hint-replacement t
            :use (:instance wrapper-axiom (x a)))))

One might expect this to loop forever: The hint is applied to the child and adds the hypothesis again. However, when the hint fires, nothing is actually changed, since (wrapper a) is already in the subgoal. The theorem prover detects this and stops. (Careful inspection of the output will reveal that the hint actually did fire a second time without apparent effect.)

So let's change the experiment a little. Let's make the hint add the hypothesis (wrapper p) where p is the first literal of the clause. This is silly but it allows us to explore the behavior of computed hints a little more.

  
(thm (equal u v)
  :hints (`(:use (:instance wrapper-axiom (x ,(car clause))))))

So in this case, the theorem prover changes the goal to

(IMPLIES (WRAPPER (EQUAL U V)) (EQUAL U V))

which then simplifies to

(IMPLIES (WRAPPER NIL) (EQUAL U V))

because the concluding equality can be assumed false in the hypothesis (e.g., think of the contrapositive version). Nothing else happens because the hint has been removed and so is not applicable to the child.

Now consider the following -- and be ready to interrupt it and abort!

  
(thm (equal u v)
  :hints (`(:computed-hint-replacement t
            :use (:instance wrapper-axiom (x ,(car clause))))))

This time the hint is not removed and so is applied to the child. So from Goal we get

Goal'
(IMPLIES (WRAPPER (EQUAL U V))
         (EQUAL U V))

and then

Goal''
(IMPLIES (AND (WRAPPER (NOT (WRAPPER (EQUAL U V))))
              (WRAPPER (EQUAL U V)))
         (EQUAL U V))

etc.

First, note that the hint is repeatedly applied to its children. That is because we wrote :computed-hint-replacement t. But second, note that Goal' is not even being simplified before Goal'' is produced from it. If it were being simplified, the (equal u v)'s in the hypotheses would be replaced by nil. This is a feature. It means after a computed hint has fired, other hints are given a chance at the result, even the hint itself unless it is removed from the list of hints.

As an exercise, let's arrange for the hint to stay around and be applied indefinitely but with a simplification between each use of the the hint. To do this we need to pass information from one application of the hint to the next, essentially to say ``stay around but don't fire.''

First, we will define a function to use in the hint. This is more than a mere convenience; it allows the hint to ``reproduce itself'' in the replacement.

(defun wrapper-challenge (clause parity)
  (if parity
      `(:computed-hint-replacement ((wrapper-challenge clause nil))
        :use (:instance wrapper-axiom (x ,(car clause))))
      `(:computed-hint-replacement ((wrapper-challenge clause t)))))

Note that this function is not recursive, even though it uses its own name. That is because the occurrence of its name is in a quoted constant.

Now consider the following. What will it do?

(thm (equal u v)
  :hints ((wrapper-challenge clause t)))

First, observe that this is a legal hint because it is a term that mentions only the free variable CLAUSE. When defining hint functions you may sometimes think their only arguments are the four variables id, clause, world, and stable-under-simplificationp. That is not so. But in your hints you must call those functions so that those are the only free variables. Note also that the occurrence of clause inside the :computed-hint-replacement is not an occurrence of the variable clause but just a constant. Just store this note away for a moment. We'll return to it momentarily.

Second, the basic cleverness of this hint is that every time it fires it reproduces itself with the opposite parity. When the parity is t it actually changes the goal by adding a hypothesis. When the parity is nil it doesn't change the goal and so allows simplification to proceed -- but it swaps the parity back to t. What you can see with this simple toy is that we can use the computed hints to pass information from parent to child.

Ok, so what happens when the event above is executed? Try it. You will see that ACL2 applied the hint the first time. It doesn't get around to printing the output because an error is caused before it can print. But here is a blow-by-blow description of what happens. The hint is evaluated on Goal with the clause ((equal u v)). It produces a hint exactly as though we had typed:

("Goal" :use (:instance wrapper-axiom (x (equal u v))))

which is applied to this goal. In addition, it produces the new hints argument

:hints ((wrapper-challenge clause nil)).

By applying the "Goal" hint we get the new subgoal

Goal'
(implies (wrapper (equal u v))
         (equal u v))

but this is not printed because, before printing it, the theorem prover looks for hints to apply to it and finds

(wrapper-challenge clause nil)

That is evaluated and produces a hint exactly as though we had typed:

("Goal'" )

and the new hints argument:

:hints ((wrapper-challenge clause nil)).

But if you supply the hint ("Goal'" ), ACL2 will signal an error because it does not allow you to specify an empty hint! So the definition of wrapper-challenge above is almost correct but fatally flawed. We need a non-empty ``no-op'' hint. One such hint is to tell the system to expand a term that will always be expanded anyway. So undo wrapper-challenge, redefine it, and try the proof again. Now remember the observation about clause that we asked you to ``store'' above. The new definition of wrapper-challenge illustrates what we meant. Note that the first formal parameter of wrapper-challenge, below, is no longer named clause but is called cl instead. But the ``call'' of wrapper-challenge in the replacements is on clause. This may seem to violate the rule that a function definition cannot use variables other than the formals. But the occurrences of clause below are not variables but constants in an object that will eventually be treated as hint term.

:ubt wrapper-challenge

(defun wrapper-challenge (cl parity)
  (if parity
      `(:computed-hint-replacement ((wrapper-challenge clause nil))
        :use (:instance wrapper-axiom (x ,(car cl))))
      `(:computed-hint-replacement ((wrapper-challenge clause t))
        :expand ((atom zzz)))))


(thm (equal u v)
  :hints ((wrapper-challenge clause t)))

This time, things go as you might have expected! Goal' is produced and simplified, to

Goal''
(implies (wrapper nil)
         (equal u v)).

Simplification gets a chance because when the new hint (wrapper-challenge clause nil) is fired it does not change the goal. But it does change the parity in the hints argument so that before Goal'' is simplified again, the hint fires and adds the hypothesis:

Goal'''
(IMPLIES (AND (WRAPPER (NOT (WRAPPER NIL)))
              (WRAPPER NIL))
         (EQUAL U V)).

This simplifies, replacing the first (NOT (WRAPPER NIL)) by NIL, since (WRAPPER NIL) is known to be true here. Thus the goal simplifies to

Goal'4'
(IMPLIES (WRAPPER NIL) (EQUAL U V)).

The process repeats indefinitely.

So we succeeded in getting a hint to fire indefinitely but allow a full simplification between rounds.