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

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

name ;; just for naming return values or (name [option]*) ;; for naming, documenting, and proving theorems

where

<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 thetools/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 thetools/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 symbolt is explicitly allowed and results in no theorem. The symbolnil 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) , whereans is thename 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 withquote . :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

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 thestd::returnspec entry of thestd::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 useset-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 istype -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.

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 introducesfoo with macro arguments, creating a function namedfoo-fn , this producesfoo .<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

In the rule-classes, the return value names are substituted for appropriate
terms; i.e., if the second return value of

Similar to define, a configuration object can be set up to set some
options globally (local to a book). At the moment only the

(make-returnspec-config :hints-sub-returnnames t)

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