Defret
Prove additional theorems about a defined
function, implicitly binding the return variables.
defret is basically defthm, but has a few extra features.
The main feature is that it automatically binds the declared return values
for a function, which defaults to the most recent function created using define.
It also supports the :hyp keyword similar to define's returns-specifiers.
Syntax:
Suppose we have a function created using define with the following
signature:
(define my-function ((a natp)
(b stringp)
(c true-listp))
:returns (mv (d pseudo-termp)
(e booleanp)
(f (tuplep 3 f)))
...)
(The guards and return types aren't important for our purposes, just the
names.)
A defret form like this:
(defret a-theorem-about-<fn>
:hyp (something-about a b c)
:pre-bind ((q (foo a b c)))
(implies (not e)
(and (consp d)
(symbolp (car d))
(equal (second d) q)))
:fn my-function ;; defaults to the most recent define
:hints ...
:rule-classes ...)
will then expand to this:
(defthm a-theorem-about-my-function
(implies (something-about a b c)
(b* ((q (foo a b c))
((mv ?d ?e ?f) (my-function a b c)))
(implies (not e)
(and (consp d)
(symbolp (car d))
(equal (second d) q)))))
:hints ...
:rule-classes ...)
The :hyp :guard and :hyp :fguard features of returns-specifiers are also supported.
Defret does not support the feature where a single function name
specifies a type of a return value. Perhaps we could support it for functions
with a single return value.
One limitation of defret is that the conclusion term can't refer to a
formal if there is a return value that has the same name. To work around this,
the :pre-bind argument accepts a list of b* bindings that occur
before the binding of the return values. You may also just want to not share
names between your formals and returns.
Features
- The return value names specified by :returns for the function are
bound in the body of the theorem. This way if the function is changed to
e.g. return an additional value, defret forms don't necessarily need to
change as long as the :returns specifiers are kept up to date.
- The return value names are substituted for appropriate expressions in the
rule-classes. E.g., in the above example, an occurrence of d in the hints
or rule-classes would be replaced by (mv-nth 0 (my-function a b c)). This
substitution may optionally also be applied to the hints by setting the
:hints-sub-returnnames option; see returns-specifiers.
- Any symbol named <CALL> (in any package) is replaced by the call of
the function in the body, hints, and rule-classes. Similarly any symbol named
<FN> is replaced by the function name or macro alias; additionally, any
symbol named <FN!> is replaced by strictly the function name (not the
macro alias).
- The substrings "<FN>" and "<FN!>" are replaced in the theorem name by
the names of the function/macro alias and function (respectively), so that
similar theorems for different functions can be copied/pasted without editing
the names.
Subtopics
- Defretgen
- Generate some defret and defret-mutual forms for a set
of functions and mutual recursions.
