Define-sk
A very fine alternative to defun-sk.
Introduction
define-sk is an extension of defun-sk with many define-like features and other enhancements:
- Support for define-style syntax including: extended formals with
embedded guards/docs and &key/&optional arguments via macro aliases,
xdoc integration and automatic function signatures, :prepwork and
/// sections, :returns specifiers, etc.
- Better support for guard verification which avoids theory problems
and provides smarter handling of implies forms; see define-sk-implies-handling.
- It automatically infers when using :rewrite :direct is possible, which
generally gives you a better theorem for universally quantified functions.
Example
(define-sk distances-bounded-p ((bound rationalp "Maximum length to allow.")
(cluster setp "All nodes to consider."))
:short "Do all nodes in a cluster lie within some certain bound?"
(forall ((weaker "Lesser of the two nodes to consider.")
(stronger "Greater of the two nodes to consider."))
(implies (and (in lesser cluster)
(in greater cluster)
(weaker-p weaker stronger))
(<= (distance lesser greater) bound)))
///
(defthm sensible-when-sensible-bound-p
(implies (and (distances-bounded-p bound cluster)
(sensible-bound-p bound))
(sensible-cluster-p cluster))))
Syntax
(define-sk name formals
(quantifier extended-vars body)
[/// other-events]) ;; optional, starts with the symbol ///
Where:
- The name is just the name of the new quantified function to be defined, as
in defun-sk.
- The formals are a list of extended-formals. This could be
as simple as a list of variables, but can also specify guards and documentation
fragments as in define. The special &key/&optional arguments
are allowed. No extra keyword arguments are accepted on individual
formals.
- The quantifier should be either forall or exists.
- The extended-vars are a list of extended-formals that are
being quantified over. Like the formals, these can have documentation
fragments. Special restrictions: guards are not allowed here and neither are
&key/&optional arguments. No additional keyword arguments are
accepted for individual extended vars.
- The body is as in defun-sk.
- The other-events are as in define; this is just a grouping
mechanism that allows you to put related theorems and events here.
Additionally, optional :keyword value arguments may be interspersed
anywhere between name and ///.
Guard Related Features
A common problem when trying to use guard verification with defun-sk is that implies isn't lazy, so you won't be able to assume
that your hypotheses hold in your conclusion. define-sk tries to help
with this by smartly handling implies forms in your function body. See
define-sk-implies-handling for a detailed explanation of the
problem.
Guard Options
- :verify-guards val
- Like define, we try to verify guards by default, but you can avoid
this by setting :verify-guards nil.
- :guard guard
- Usually it's most convenient to embed your guards within the extended-formals, but the :guard option is sometimes useful for giving
additional guards.
- :guard-hints hints
- :guard-debug bool
- These are passed to the guard verification attempt as you would
expect.
- :implies mode
- By default we use :implies :smart, which means that uses of
implies are automatically converted into if terms in the body. To
avoid this, use :implies :dumb.
Other Keyword Options
- :enabled val
- By default the quantified function and its necc/suff theorem
will both be disabled after the /// events are finished. You can control
this with :enabled:
- :enabled :all -- enable the function and the theorem
- :enable :thm -- disable the function but enable the theorem
- :enable :fn -- enable the function but disable the theorem
- :enable nil -- disable the function and theorem (default)
- :rewrite val
- This is similar to the same option for defun-sk, except that by
default we look at your function's body to infer whether :rewrite :direct
can be used. If for whatever reason you don't like the rewrite rule that gets
generated, you can customize it by adding :rewrite <custom-term>.
- :returns spec
- By default we try to prove that your quantified function returns a booleanp. However, note that it is possible to define ``weird'' quantifiers
that return non-boolean or multiple values. For instance, here is a quantified
function that logically just always returns 0:
(set-ignore-ok t)
(defun-sk weird-quantifier (x) (forall elem 0))
(thm (equal (weird-quantifier x) 0))
- Similarly, here is a quantified function that actually returns multiple
values:
(defun-sk weirder-quantifier (x) (forall elem (mv x x)))
(thm (equal (weirder-quantifier x) (mv x x)))
- If you try to introduce such a function with define-sk, or if your
predicate just happens to not return a proper t or nil boolean, then
you may need to provide a custom :returns form; see returns-specifiers for details.
- :strengthen val
- Submits the underlying defchoose event with the strengthen
option.
- :ignore-ok val
- Submits (set-ignore-ok val) before the definition. This option is
local to the define-sk and does not affect the other-events.
- :irrelevant-formals-ok val
- Submits (set-irrelevant-formals-ok val) before the definition. This
option is local to the define-sk and does not affect the
other-events.
- :parents parents
- :short string
- :long string
- These are defxdoc-style options for documenting the function. They
are passed to a defsection for this definition.
- :prepwork events
- These are arbitrary events that you want to put before the definition
itself. For instance, it might include any local lemmas.
- :progn val
- Normally a define-sk expands to an (encapsulate nil ...). This
means for instance that you can use local in your prepwork,
other-events, to make changes that are local to the define-sk form.
In certain special cases, you may want to avoid this use of encapsulate
and instead submit the events using progn.
- :verbosep val
- By default some output is suppressed, but yu can set :verbosep t to
avoid this. This may be useful when debugging failed define-sk
forms.
Subtopics
- Define-sk-implies-handling
- Explanation of the :implies :smart option for define-sk.
