		Search-engine friendly clone of the ACL2 documentation.

Measure-debug

Generate markers to indicate sources of measure proof obligations

When ACL2 is asked to accept a recursive (or mutually recursive) function definition, it generates a goal often called the ``measure conjecture.'' That goal can split into numerous goals, some of which may not be theorems if the definition being processed has bugs. This documentation topic explains a capability provided by ACL2 to help find such bugs. For a similar utility appropriate for guard verification, see guard-debug.

We begin with the following simple, admittedly artificial, example.

(defun f (x)
  (if (consp x)
      (f (cons x x))
    x))

ACL2 generates the following proof obligation..

(IMPLIES (CONSP X)
         (O< (ACL2-COUNT (CONS X X))
             (ACL2-COUNT X)))

In this simple example, it is obvious that ACL2 cannot prove the goal because in fact, (CONS X X) does not have a smaller ACL2-count than X, even assuming (CONSP X). But you can get ACL2 to show explicitly the source of this proof obligation by specifying :measure-debug t in an xargs declare form, as follows.

ACL2 !>(defun f (x)
         (declare (xargs :measure-debug t))
         (if (consp x)
             (f (cons x x))
           x))

For the admission of F 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 (AND (EXTRA-INFO '(:MEASURE (:RELATION F))
                          '(F (CONS X X)))
              (CONSP X))
         (O< (ACL2-COUNT (CONS X X))
             (ACL2-COUNT X))).

The extra-info call is telling us the following about the measure conjecture:

The appropriate well-founded relation (typically o<) holds between appropriate terms, because of the indicated recursive call, (F (CONS X X)).

We now describe the measure-debug utility in some detail.

(Extra-info x y) always returns t by definition. However, if the measure conjecture takes place with a non-nil value for the xargs keyword :measure-debug, then the goals generated will include hypotheses that are calls of extra-info. Such a hypothesis has one of the following forms.

(extra-info '(:MEASURE (:RELATION function-name))
            'recursive-call)

(extra-info '(:MEASURE (:DOMAIN function-name))
            '(D (M term)))

The first form says that the goal is to show that the measure decreases for the indicated recursive call in the body of the function named function-name. The second form says that the goal is to show that the measure always returns a suitable value.

We illustrate with a slightly more elaborate, but still contrived, example, which we hope clearly illustrates the points above. Notice that :measure-debug t need only be specified for a single defun form in a call of mutual-recursion. Also notice in the output that when there is more than one source for a goal, each source is indicated by its own call of extra-info.

ACL2 !>(defstub my-measure (x) t) ; for the contrived example below
[[ .. output omitted here .. ]]
ACL2 !>(mutual-recursion
         (defun f1 (x)
           (declare (xargs :measure (my-measure x) :measure-debug t))
           (if (consp x)
               (f2 (cons x (cdr x)))
             t))
         (defun f2 (x)
           (declare (xargs :measure (my-measure x)))
           (if (consp x)
               (f1 (cons (make-list (car x)) (cdr x)))
             nil)))

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

Goal
(AND (IMPLIES (AND (EXTRA-INFO '(:MEASURE (:RELATION F1))
                               '(F2 (CONS X (CDR X))))
                   (CONSP X))
              (O< (MY-MEASURE (CONS X (CDR X)))
                  (MY-MEASURE X)))
     (IMPLIES (AND (EXTRA-INFO '(:MEASURE (:RELATION F2))
                               '(F1 (CONS (MAKE-LIST-AC (CAR X) NIL NIL)
                                          (CDR X))))
                   (CONSP X))
              (O< (MY-MEASURE (CONS (MAKE-LIST-AC (CAR X) NIL NIL)
                                    (CDR X)))
                  (MY-MEASURE X)))
     (IMPLIES (AND (EXTRA-INFO '(:MEASURE (:DOMAIN F2))
                               '(O-P (MY-MEASURE X)))
                   (EXTRA-INFO '(:MEASURE (:DOMAIN F1))
                               '(O-P (MY-MEASURE X))))
              (O-P (MY-MEASURE X)))).

All rules (see rune) associated with extra-info are disabled by default, so that hypotheses of the form described above are not simplified to t. These hypotheses are intended to ride along for free: you can generally expect the proof to have the same structure whether or not the :measure-debug option is supplied, though on rare occasions the proofs may diverge.