Returns-specifiers
A concise way to name, document, and prove basic type-like theorems
about a function's return values.
The define macro and some other std/util macros
support a :returns option. This option provides a concise way to name,
document, and prove basic type-like theorems about the return values of your
functions. Named return values also allow your function to be used with the
special ret binder for b*.
The general form is:
:returns return-spec ;; for single-value functions
or :returns (mv return-spec*) ;; for multiple-valued functions
There should be exactly one return-spec per return value. Each
return-spec has the form:
name ;; just for naming return values
or (name [option]*) ;; for naming, documenting, and proving theorems
where name is a symbol and the options can come in any order. To
distinguish between the two forms of :returns, it is not legal to use
mv as the name of a return value. The options are:
- <xdoc>, any string literal
- You can document each return value with a string literal. The string may
make use of xdoc::markup and xdoc::preprocessor directives.
Typically these descriptions should be short and not include
document-structuring tags like <p>, <ul>, <h3>, and so forth.
See the section on xdoc integration, below, for more details.
- <return-type>, a symbol or term
- When provided, the return type is used to generate a basic type-like
theorems about the return values. A default hint is provided if no :hints
keyword is present; see the discussion of :hints below.
- Important Note in the multiple-valued case, this approach assumes
you are using the tools/mv-nth book. The theorems we prove target terms
like (mv-nth 0 (f ...)) and (mv-nth 1 (f ...)). This will not work
well if mv-nth is enabled, especially about the 0th return value. For
your convenience, define automatically includes the tools/mv-nth
book. You really should be using it, you know.
- As a convenient shorthand, you can use a single symbol like evenp.
The theorem to be proven in this case might be, e.g., (evenp (f x)) for a
single-valued function, or (evenp (mv-nth 3 (f x))) if this is the
fourth (because of zero-indexing) return value of a multiply-valued function.
The symbol t is explicitly allowed and results in no theorem. The symbol
nil and keyword symbols are explicitly invalid as return types.
- In certain cases, you may wish to prove a more complex theorem, e.g., say
we want to prove this return value is always greater than 5. To support this,
you can write a return type like (< 5 ans), where ans is the
name of this return value. You can also refer to the names of other
return values in this term. To make it easy to distinguish return types from
other options, the return type term must be a cons and must not begin with
quote.
- :hyp hyp-term
- This option only makes sense when there is a return-type term. By default,
the return-type theorem is unconditional. If the theorem needs a hypothesis,
you can put it here.
- Frequently, the hypothesis you want for a type-like theorem is for the
guards of the function to be met. As a convenient shorthand, hyp-term may
be:
- :guard -- use the function's guard as the hypothesis
- :fguard -- like :guard, but force the entire guard
If neither of these is what you want, you can provide an arbitrary
hyp-term. Typically this term should mention only the formals of your
function. The return values of the theorem will not be bound in scope of the
hyp, so trying to refer to them in a hypothesis is generally an error.
- :hints hints-term
- This option only makes sense when there is a return-type term; when
specified, the given hints are passed to the proof attempt for the associated
return-type. When no :hints keyword is present, a default hint is taken
from the std::returnspec entry of the std::default-hints-table table,
but this is overridden if the :hints keyword is present, even for
:hints nil. To change the default hints, you may use
set-returnspec-default-hints. The setting for this provided in the
std/util books provides an induction and expand hint when the
function introduced is singly-recursive.
- A few special symbols (and even substrings of symbols) are substituted into
hints; see the section "Substitutions" below.
- :rule-classes classes
- This option only makes sense when there is a return-type term. By default,
the return-type theorem is added as a :rewrite rule. If you want to use
other ACL2::rule-classes, then you will want to override this default.
- A few special symbols (and even substrings of symbols) are substituted into
hints; see the section "Substitutions" below.
- :name name
- This allows you to control the name of the associated theorem.
- The default value of name is type-of-your-function.
For example, natp-of-foo.
- :hints-sub-returnnames
- This option determines whether the
return-name substitution is applied to the hints. See "Substitutions"
below.
Substitutions
Certain symbols and certain substrings of symbols are
replaced in the theorem body, hints, and rule-classes.
The following substitutions replace any symbol matching the given name in
all three places (body, hints, and rule-classes):
- <CALL> is replaced by the function applied to the formals.
- <FN> is replaced by the function's macro alias, if it has one, or else its name. That is, for a form that introduces foo with macro arguments, creating a function named foo-fn, this produces foo.
- <FN!> is replaced by the functions name, strictly, i.e. foo-fn in the example above.
- <VALUES> is replaced by the list of return value names.
In the hints, the substrings <FN> and <FN!> of symbol names are
also substituted as above. This allows hints to refer to defret-style
theorem names.
In the rule-classes, the return value names are substituted for appropriate
terms; i.e., if the second return value of foo is named bar, then
bar becomes (mv-nth 1 (foo ...)). This substitution may also
optionally be applied to the hints by setting the :hints-sub-returnnames option.
This return name substitution is not applied to the theorem body, but the let-binding
of the return names to the function call has a similar effect.
Configuration Object
Similar to define, a configuration object can be set up to set some
options globally (local to a book). At the moment only the
:hints-sub-returnnames option is read from this configuration object. The
following form sets that option:
(make-returnspec-config :hints-sub-returnnames t)
Subtopics
- ACL2::patbind-ret
- b* binder for named return values from functions.
- Defret
- Prove additional theorems about a defined
function, implicitly binding the return variables.
- Tuple
- A way to use mv-like return specifiers for tuples.
- Defret-mutual
- Prove additional theorems about a mutual-recursion created using defines, implicitly binding the return variables.
- More-returns
- Prove additional return-value theorems about a defined
function.
