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, `ACL2-count`
than `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 **measure** conjecture:

The appropriate well-foundedrelation(typicallyo<) holds between appropriate terms, because of the indicated recursive call,(F (CONS X X)) .

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

`xargs`
keyword

(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

We illustrate with a slightly more elaborate, but still contrived, example,
which we hope clearly illustrates the points above. Notice that
`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

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