Introduce measure and termination predicates for a partial function definition

We begin with a motivating example. Suppose we want to admit factorial without the need to prove termination, as follows.

(fact x) = (if (equal x 0) 1 (* x (fact (1- x))))

Of course, this ``definition'' is non-terminating on negative number
inputs. But with

(defun fact-test (x) (equal x 0)) (defun fact-step (x) (1- x))

Now we can execute our utility: we provide it with the names of the two functions above, and it generates a measure, a termination predicate, and a potentially helpful theory, respectively.

(defpm fact-test fact-step fact-measure fact-terminates fact-theory)

Here are the events exported by the

; The first three lemmas can be useful for reasoning about the termination ; predicate, FACT-TERMINATES. (DEFTHM FACT-TERMINATES-BASE (IMPLIES (FACT-TEST X) (FACT-TERMINATES X))) (DEFTHM FACT-TERMINATES-STEP (IMPLIES (NOT (FACT-TEST X)) (EQUAL (FACT-TERMINATES (FACT-STEP X)) (FACT-TERMINATES X)))) (DEFTHMD FACT-TERMINATES-STEP-COMMUTED (IMPLIES (AND (SYNTAXP (SYMBOLP X)) (NOT (FACT-TEST X))) (EQUAL (FACT-TERMINATES X) (FACT-TERMINATES (FACT-STEP X))))) (THEORY-INVARIANT (INCOMPATIBLE (:REWRITE FACT-TERMINATES-STEP) (:REWRITE FACT-TERMINATES-STEP-COMMUTED))) ; The next two lemmas can be useful for defining functions whose termination ; is ensured by the measure just introduced. (DEFTHM FACT-MEASURE-TYPE (O-P (FACT-MEASURE X))) (DEFTHM FACT-MEASURE-DECREASES (IMPLIES (AND (FACT-TERMINATES X) (NOT (FACT-TEST X))) (O< (FACT-MEASURE (FACT-STEP X)) (FACT-MEASURE X)))) ; Finally, the four enabled rewrite rules above are collected into a theory. (DEFTHEORY FACT-THEORY '(FACT-TERMINATES-BASE FACT-TERMINATES-STEP FACT-MEASURE-TYPE FACT-MEASURE-DECREASES))

With the events above, we can introduce the following definition, which in
effect guards the body with the termination predicate. (Perhaps at some point
we will extend `in-theory` hint below was carefully crafted to allow the proof to
succeed very quickly.

(defun fact (x) (declare (xargs :measure (fact-measure x) :hints (("Goal" :in-theory (union-theories (theory 'fact-theory) (theory 'minimal-theory)))))) (if (fact-terminates x) (if (fact-test x) 1 (* x (fact (fact-step x)))) 1 ; don't-care ))

With the events above (not necessarily including the definition of

(defthm-domain fact-terminates-holds-on-natp (implies (natp x) (fact-terminates x)) :measure (nfix x))

See defthm-domain.

General form:

(defpm ; or equivalently, def-partial-measure ; ; TEST STEP MEASURE TERMINATES THEORY :formals FORMALS ; default is (x) :verbose VERBOSE ; default is nil )

where there is no output unless

First consider the case that

(defun foo (x) (declare (xargs :measure (MEASURE x) :hints (("Goal" :in-theory (union-theories (theory 'THEORY) (theory 'minimal-theory)))))) (if (TERMINATES x) (if (TEST x) ... (... (fact (STEP x)) ...) ...))

The generated

(defthm TERMINATES-base (implies (TEST x) (TERMINATES x))) (defthm TERMINATES-step (implies (not (TEST x)) (equal (TERMINATES (STEP x)) (TERMINATES x)))) (defthmd TERMINATES-step-commuted (implies (AND (syntaxp (symbolp x)) (not (TEST x))) (equal (TERMINATES x) (TERMINATES (STEP x))))) (theory-invariant (incompatible (:rewrite TERMINATES-step) (:rewrite TERMINATES-step-commuted))) (defthm MEASURE-type (o-p (MEASURE x))) (defthm MEASURE-decreases (implies (and (TERMINATES x) (not (TEST x))) (o< (MEASURE (STEP x)) (MEASURE x)))) (deftheory THEORY '(TERMINATES-base TERMINATES-step MEASURE-type MEASURE-decreases))

For arbitrary formals the situation is similar, except that there is one
step function per formal, obtained by adding the formal name as a suffix to
the specified

(defthm TERMINATES-base (implies (TEST y1 ... yk) (TERMINATES y1 ... yk))) (defthm TERMINATES-step (implies (not (TEST y1 ... yk)) (equal (TERMINATES (STEP-y1 y1 ... yk) ... (STEP-yk y1 ... yk)) (TERMINATES y1 ... yk)))) (defthm TERMINATES-step-commuted (implies (AND (syntaxp (symbolp y1)) ... (syntaxp (symbolp yk)) (not (TEST y1 ... yk))) (equal (TERMINATES (STEP-y1 y1 ... yk) ... (STEP-yk y1 ... yk)) (TERMINATES y1 ... yk)))) (theory-invariant (incompatible (:rewrite TERMINATES-step) (:rewrite TERMINATES-step-commuted))) (defthm MEASURE-type (o-p (MEASURE y1 ... yk))) (defthm MEASURE-decreases (implies (and (TERMINATES y1 ... yk) (not (TEST y1 ... yk))) (o< (MEASURE (STEP-y1 y1 ... yk) ... (STEP-yk y1 ... yk)) (MEASURE y1 ... yk)))) (deftheory THEORY '(TERMINATES-base TERMINATES-step MEASURE-type MEASURE-decreases))

The implementation of `trans1` on your

The community book

Related work of Dave Greve, in particular his utility `defthm-domain` were developed
independently using an approach that seems considerably simpler than Greve's
development. However, his utility is much more powerful in that it generates
a termination test, rather than requiring the user to provide it, and also it
handles reflexive functions — definitions with recursive calls like