defpm

(in-package "ACL2")

(defpointer defpm def-partial-measure)

(defxdoc def-partial-measure
  :parents (macro-libraries)
  :short "Introduce measure and termination predicates for a partial function
 definition"
  :long "<h3>Introduction By Way of an Example</h3>

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

 @({
 (fact x)
 =
 (if (equal x 0)
     1
   (* x (fact (1- x))))
 })

 <p>Of course, this ``definition'' is non-terminating on negative number
 inputs.  But with @('def-partial-measure'), or @('defpm') for short, we can
 admit a suitable definition for this partial function as follows.  First, we
 define a function to represent the termination test and another function to
 represent the actual parameter of the recursive call.</p>

 @({
 (defun fact-test (x)
   (equal x 0))
 (defun fact-step (x)
   (1- x))
 })

 <p>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.</p>

 @({
 (defpm fact-test fact-step
   fact-measure fact-terminates fact-theory)
 })

 <p>Here are the @(see events) exported by the @('defpm') call above.</p>

 @({
 ; 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))
 })

 <p>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 @('defpm') to create this definition automatically.)  The
 @(':')@(tsee in-theory) hint below was carefully crafted to allow the proof to
 succeed very quickly.</p>

 @({
 (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
     ))
 })

 <p>With the events above (not necessarily including the definition of
 @('fact')), we can prove that @('fact') terminates on natural number inputs.
 A second macro, @('defthm-domain'), automates much of that task:</p>

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

 <p>See @(see defthm-domain).</p>

 <h3>Detailed Documentation</h3>

 <p>General form:</p>

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

 <p>where there is no output unless @('VERBOSE') is non-@('nil').  The
 remaining arguments are as follows.</p>

 <p>First consider the case that @('FORMALS') is the default, @('(x)').  The
 arguments @('TEST') and @('STEP') are conceptually ``inputs'': they should
 name existing functions on the indicated value for formals (which by default
 is @('(x)')).  Then @('defpm') will attempt to generate a measure and
 termination predicate on those formals, with the indicated names (@('MEASURE')
 and @('TERMINATES'), respectively).  These theorems are suitable for admitting
 a function of the following form, where capitalized names refer to those in
 the @('defpm') call above, and where additional code may appear as indicated
 with ``...''.</p>

 @({
 (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)) ...)
     ...))
 })

 <p>The generated @('THEORY') names the four rules generated by the @('defpm')
 call, as in the example above.</p>

 @({
 (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))
 })

 <p>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 @('STEP') separated by a hyphen.  Thus we have the following
 events when @('FORMALS') is @('(y1 ... yk)').</p>

 @({
 (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))
 })

 <h3>Implementation</h3>

 <p>The implementation of @('defpm') (i.e., @('def-partial-measure') has been
 designed to make proofs efficient.  It should be completely unnecessary to
 know anything about the implementation in order to use @('defpm') effectively.
 If however you are interested, you can execute @(':')@(tsee trans1) on your
 @('defpm') call to see the @(see events) that it generates.</p>

 <h3>More Information</h3>

 <p>The community book @('misc/defpm.lisp') illustrates how to use @('defpm')
 and @('defthm-domain') to define ``partial'' functions.  Search for calls of
 @('my-test') in that book to see examples.</p>

 <p>Related work of Dave Greve, in particular his utility @('def::ung'), may be
 found in community books directory @('books/coi/defung/').  Our utilities
 @('def-partial-measure') and @(tsee 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 &mdash; definitions with recursive calls like
 @('(mc91 (mc91 (+ n 11)))') &mdash; while ours were not designed to do
 so.</p>")

(defxdoc defthm-domain
  :parents (macro-libraries)
  :short "Prove termination on a given domain"
  :long "<p>This utility can be useful after executing a call of @('defpm');
 see @(see def-partial-measure).  Indeed, we assume that you have read the
 example in that @(see documentation) topic describing this call:</p>

 @({
 (defpm fact-test fact-step
   fact-measure fact-terminates fact-theory)
 })

 <h3>Introduction By Way of an Example</h3>

 <p>Consider the following form.</p>

 @({
 (defthm-domain trfact-terminates-holds-on-natp
   (implies (natp x)
            (trfact-terminates x acc))
   :test trfact-test ; optional test name: can be deduced by the tool ;
   :step trfact-step ; optional step name: can be deduced by the tool ;
   :measure (nfix x) ; required argument ;
   )
 })

 <p>This call produces a proof of the indicated formula, where the first
 argument of @('implies'), @('(natp x)'), provides a ``domain hypothesis.''
 You can use @(':')@(tsee trans1) to see the macroexpansion of this
 @('defthm-domain') call.  In short, @(see hints) are supplied to automate all
 ``boilerplate'' reasoning.  The @(':measure') is used to guide a proof by
 induction.  At this stage of development, the best way to use this macro is
 probably to submit the form in the hope that the proof will complete
 automatically; but if it doesn't, then use @(':')@(tsee trans1) to see what
 the form generates, and modify that event manually in order to fix the failed
 proofs.</p>

 <h3>Detailed Documentation</h3>

 <p>General form:</p>

 @({
 (defthm-domain NAME
   (implies DOMAIN-TERM
            (TERMINATES FORMAL-1 ... FORMAL-K))
   :test TEST
   :step STEP
   :measure MEASURE
   :verbose VERBOSE
   :root ROOT
   )
 })

 <p>where there is no output unless @('VERBOSE') is non-@('nil').  It is
 allowed to replace the @(tsee implies) call above by its second argument (the
 @('TERMINATES') call) if @('DOMAIN-TERM') is @('t').  The remaining arguments
 are as follows.</p>

 <p>The keywords @(':test') and @(':step') both have value @('nil') by default.
 So does @(':root'), unless @('TERMINATES') has a @(tsee symbol-name) of the
 form @('"root-TERMINATES"'), in which case :root is the symbol in the
 package of @('TERMINATES') whose name is that string, @('root').  If
 @(':root') has a value of @('nil'), even after taking this default into
 account, then both @(':test') and @(':step') must have a non-@('nil') value.
 The reason for this requirement is that when @(':test') and/or @(':step') is
 omitted, the value is computed from the root by adding the suffix
 @('"-TEST"') or @('"-STEP"') to the root (respectively).  The functions
 introduced for @(':test') and @(':step') are exactly as for @('defpm'); see
 @(see def-partial-measure).  Note however that the formals are those from the
 call of @('TERMINATES').</p>

 <p>See the discussion above about ``boilerplate'' reasoning for hints on how
 to deal with failures of @('defthm-domain') calls.</p>

 <h3>More Information</h3>

 <p>The community book @('misc/defpm.lisp') illustrates how to use @('defpm')
 and @('defthm-domain') to define ``partial'' functions.  Search for calls of
 @('my-test') in that book to see examples.</p>")

(make-event (pprogn (f-put-global 'defpm-arithmetic-top-book
      (extend-pathname (cbd) "arithmetic-top-theory" state)
      state)
    (value '(value-triple :defpm-arithmetic-top-book-set)))
  :check-expansion t)