Deflist
Introduce a recognizer for a typed list.
Deflist lets you to quickly introduce recognizers for typed lists
like nat-listp. It defines the new recognizer function, sets up a basic
theory with rules about len, append, member, etc., and
generates basic, automatic xdoc documentation.
General Form
(deflist name formals
element
[keyword options]
[/// other events]
)
Options Defaults
:negatedp nil
:true-listp nil
:elementp-of-nil :unknown
:guard t
:verify-guards t
:guard-hints nil
:guard-debug nil
:non-emptyp nil
:mode current defun-mode
:cheap nil
:verbosep nil
:parents nil
:short nil
:long nil
:prepwork nil
Basic Examples
The following introduces a new function, my-integer-listp, which
recognizes lists whose every element satisfies integerp, and also
introduces many theorems about this new function.
(deflist my-integer-listp (x)
(integerp x))
Note: x is treated in a special
way. It refers to the whole list in formals and guards, but refers to
individual elements of the list in the element portion. This is similar
to how other macros like defalist, defprojection, and defmapappend handle x.
Here is a recognizer for lists with no natural numbers:
(deflist nat-free-listp (x)
(natp x)
:negatedp t)
Here is a recognizer for lists whose elements must exceed some minimum:
(deflist all-greaterp (min x)
(> x min)
:guard (and (natp min)
(nat-listp x)))
Usage and Optional Arguments
Let pkg be the package of name. All functions, theorems, and
variables are created in this package. One of the formals must be pkg::x,
and this argument represents the list to check. Otherwise, the only
restriction on the formals is that you may not use the names pkg::a,
pkg::n, or pkg::y, because we use these variables in the theorems we
generate.
The optional :negatedp keyword can be used to recognize a list whose
every element does not satisfy elementp.
The optional :true-listp keyword can be used to require that the new
recognizer is "strict" and will only accept lists that are
nil-terminated; by default the recognizer will be "loose" and will not
pay attention to the final cdr. There are various reasons to prefer one
behavior or another; see strict-list-recognizers for details.
The optional :elementp-of-nil keyword can be used when (elementp nil
...) is always known to be t or nil. When it is provided,
deflist can generate slightly better theorems.
The optional :guard, :verify-guards, :guard-debug, and
:guard-hints are options for the defun we introduce. These are for
the guards of the new list recognizer, not the element recognizer.
The optional :mode keyword can be set to :logic or :program
to introduce the recognizer in logic or program mode. The default is whatever
the current default defun-mode is for ACL2, i.e., if you are already in program
mode, it will default to program mode, etc.
The optional :verbosep flag can be set to t if you want deflist to
print everything it's doing. This may be useful if you run into any failures,
or if you are simply curious about what is being introduced.
The optional :cheap flag can be set to t to produce cheaper, less
effective rule-classes for some rules; this may be convenient when the element
type is a very common function such as consp, in which case adding
stronger rules might significantly slow down proofs.
The optional :parents, :short, and :long keywords are as in
defxdoc. Typically you only need to specify :parents, perhaps
implicitly with ACL2::set-default-parents, and suitable documentation
will be automatically generated for :short and :long. If you don't
like this documentation, you can supply your own :short and/or :long
to override it.
The optional :prepwork may provide a list of event forms that are
submitted just before the generated events. These are preparatory events,
e.g. local lemmas to help prove :elementp-of-nil.
Pluggable Architecture
Beginning in ACL2 6.5, deflist no longer hard-codes the set of theorems to
be produced about every list recognizer. Instead, def-listp-rule forms
pertaining to a generic list recognizer called element-list-p are used as
templates and instantiated for each deflist invocation. These forms may be
scattered throughout various libraries, so the set of books you have loaded
determines the set of rules produced by a deflist invocation. See ACL2::std/lists/abstract for more information about these rules and how to
control what theorems are produced by deflist.
"std/util/deflist.lisp" includes books that compose a set of rules to
instantiate that should be more or less backward compatible with the theorems
produced by deflist in ACL2 6.4 and previous. "std/util/deflist-base.lisp"
includes a much more basic set of rules.
Support for Other Events
Deflist implements the same /// syntax as other macros like define. This allows you to put related events near the definition and have
them included in the automatic documentation. As with define, the new
recognizer is enabled during the /// section. Here is an example:
(deflist even-integer-list-p (x)
(even-integer-p x)
:true-listp t
///
(defthm integer-listp-when-even-integer-list-p
(implies (even-integer-list-p x)
(integer-listp x))))
Deprecated. The optional :rest keyword was a precursor to ///.
It is still implemented, but its use is now discouraged. If both :rest
and /// events are used, we arbitrarily put the :rest events
first.
Deprecated. The optional :already-definedp keyword can be set if you
have already defined the function. This was previously useful when you wanted
to generate the ordinary deflist theorems without generating a defund
event, e.g., because you are dealing with mutually recursive recognizers. We
still accept this option for backwards compatibility but it is useless, because
deflist is now smart enough to notice that the function is already
defined.
Subtopics
- Strict-list-recognizers
- Should your list recognizers require nil-terminated lists?
