		Search-engine friendly clone of the ACL2 documentation.

Termination-theorem-example

How to use a previously-proved measure theorem

See lemma-instance for a discussion of :termination-theorem and :termination-theorem! lemma instances, and see tthm for a related user-level query utility. In this topic, we illustrate the use of such lemma instances to take advantage of a measure theorem already proved for an existing definition, when attempting to admit a new definition. We present two examples: a basic one, and then another that shows how an existing termination theorem can be automatically functionally instantiated. For a related utility, see make-termination-theorem.

The following very simple example is contrived but should get the main idea across. Suppose that the following event was previously executed, for example when including a book, in order to define the log base 10 of x.

(encapsulate
  ()
  (local (include-book "arithmetic-5/top" :dir :system))
  (defun log10 (x) ; log base 10 of x
    (if (or (zp x)
            (< x 10))
        0
      (1+ (log10 (floor x 10))))))

Now suppose we want to admit the following definition, whose recursion pattern is similar to that above. The simplest way might be to include the same book as above, but perhaps that is impossible because the formula for some name in that book conflicts with the formula for that name in the current session. Without that book, it could be challenging to develop lemmas that allow the termination proof to succeed for this proposed definition. So we provide a hint, specifying the use of the termination theorem already proved for log10, as follows.

(defun base10-digits (x)
  (declare (xargs :hints
                  (("Goal" :use ((:termination-theorem log10))))))
  (if (or (zp x)
          (< x 10))
      (list x)
    (append (base10-digits (floor x 10))
            (list (mod x 10)))))

With this hint, the termination proof succeeds, printing the following line in the event summary.

Hint-events: ((:USE LOG10))

This line says that the only :use hint was based on the event log10. This may surprise you; perhaps you would expect to see something instead such as (:USE (:TERMINATION-THEOREM LOG10)). However, the Hint-events field of the summary is intended only to show the names of events that support the hints. For example, if you replace the :use hint in the example above with

:use ((:rewrite car-cons) (:termination-theorem log10))

then the Hint-events summary line will be as follows.

Hint-events: ((:USE CAR-CONS) (:USE LOG10))

Similarly, proof output for a :use hint (provided when not in gag-mode) is also given at the level of events. For the definition above, we get the following output.

We augment the goal with the hypothesis provided by the :USE hint.
The hypothesis can be obtained from LOG10.  We are left with the following
subgoal.

Again, perhaps one would expect to see ``obtained from the termination theorem for LOG10''. But for the modified hint shown above, using (:rewrite car-cons), we similarly see only event names, not a rune.

These hypotheses can be obtained from CAR-CONS and LOG10.

Next, we consider an example where a function symbol being defined occurs in the measure theorem.

(defun left (x)
  (car x))
(defun right (x)
  (car x))
(defun first-natp (x)
  (if (atom x)
      (if (natp x) x nil)
    (or (first-natp (left x))
        (first-natp (right x)))))

The measure (termination) theorem for first-natp is as follows.

(AND (IMPLIES (NOT (ATOM X))
              (O< (ACL2-COUNT (LEFT X))
                  (ACL2-COUNT X)))
     (IMPLIES (AND (NOT (ATOM X))
                   (NOT (FIRST-NATP (LEFT X))))
              (O< (ACL2-COUNT (RIGHT X))
                  (ACL2-COUNT X))))

Now suppose the functions left and right are disabled and we then try to admit the analogous definition below. This sort of situation may be common; imagine a library of books in which first-natp is defined followed by disabling of left and right, and we have included that book in hopes of re-using the termination theorem.

(in-theory (disable left right))

(defun first-symbolp (x)
  (if (atom x)
      (if (symbolp x) x nil)
    (or (first-symbolp (left x))
        (first-symbolp (right x)))))

This time the termination theorem is as follows.

(AND (IMPLIES (NOT (ATOM X))
              (O< (ACL2-COUNT (LEFT X))
                  (ACL2-COUNT X)))
     (IMPLIES (AND (NOT (ATOM X))
                   (NOT (FIRST-SYMBOLP (LEFT X))))
              (O< (ACL2-COUNT (RIGHT X))
                  (ACL2-COUNT X))))

Notice that this theorem is not an immediate consequence of the termination theorem for first-natp, because of the call first-symbolp in the latter that replaces the call first-natp in the former. ACL2 provides support to work around this difficulty, however. When you give a :termination-theorem lemma-instance in your :hints for the termination proof, then ACL2 automatically replaces the old function symbol (here, first-natp) in the old termination theorem by the new function symbol (here, first-symbolp), before applying the hint. So the following definition is admitted, because the old termination theorem, thus modified, is exactly the new termination theorem.

(defun first-symbolp (x)
  (declare (xargs :hints
                  (("Goal" :by (:termination-theorem first-natp)))))
  (if (atom x)
      (if (symbolp x) x nil)
    (or (first-symbolp (left x))
        (first-symbolp (right x)))))

Such a substitution is made provided the old and new function symbols each have the same number of formal parameters. In general a :termination-theorem may be used for admitting either a singly-recursive function or a nest of mutually-recursive functions; the general criterion is that the number of formals must match for corresponding functions.

The functional substitution can be provided explicitly. The following example has identical behavior to that above.

(defun first-symbolp (x)
  (declare (xargs :hints
                  (("Goal" :by (:termination-theorem
                                first-natp
                                ((first-natp first-symbolp)))))))
  (if (atom x)
      (if (symbolp x) x nil)
    (or (first-symbolp (left x))
        (first-symbolp (right x)))))

Finally, note that a :by hint is not guaranteed to work; a :use hint may be a bit slower, and may require the use of :instance (see lemma-instance, but it can be more reliable.

We conclude with a remark about what happens when the termination theorem does not exist, even though (as required) the indicated function symbol is in logic mode. (For example, imagine that you are generating such hints programmatically, without analyzing whether the indicated function symbol was defined using recursion.) In that case, using :termination-theorem will fail. Here, for example, is what happens if f was defined non-recursively.

ACL2 !>(defun g (x)
         (declare (xargs :hints
                         (("Goal" :use ((:termination-theorem f))))))
         (if (consp x)
             (g (cddr x))
           x))


ACL2 Error in ( DEFUN G ...):  The object (:TERMINATION-THEOREM F)
is an ill-formed lemma instance because there is no termination theorem
for F.  The function F is not recursive.  See :DOC lemma-instance.


Summary
Form:  ( DEFUN G ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( DEFUN G ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

The alternative, :termination-theorem!, is provided in order to avoid this sort of error. Here is the corresponding (edited) log, with gag-mode off. Notice that since there is no termination theorem stored for f, the :use hint specifies the use of T for the termination theorem.

ACL2 !>(defun g (x)
         (declare (xargs :hints
                         (("Goal" :use ((:termination-theorem! f))))))
         (if (consp x)
             (g (cddr x))
           x))

For the admission of G we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is

Goal
(IMPLIES (CONSP X)
         (O< (ACL2-COUNT (CDDR X))
             (ACL2-COUNT X))).

[Note:  A hint was supplied for the goal above.  Thanks!]

We augment the goal with the hypothesis provided by the :USE hint.
The hypothesis can be obtained from F.  We are left with the following
subgoal.

Goal'
(IMPLIES T
         (OR (NOT (CONSP X))
             (O< (ACL2-COUNT (CDDR X))
                 (ACL2-COUNT X)))).

By case analysis we reduce the conjecture to

[[.. output elided ..]]

Hint-events: ((:USE F))
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
Prover steps counted:  1121
 G
ACL2 !>