Defun-sk
Define a function whose body has an outermost quantifier
Examples:
(defun-sk exists-x-p0-and-q0 (y z)
(exists x
(and (p0 x y z)
(q0 x y z))))
(defun-sk exists-x-p0-and-q0 (y z) ; equivalent to the above
(exists (x)
(and (p0 x y z)
(q0 x y z))))
(defun-sk forall-x-y-p0-and-q0 (z)
(forall (x y)
(and (p0 x y z)
(q0 x y z)))
:strengthen t)
General Form:
(defun-sk fn (var1 ... varn)
dcl_1 dcl_2 ... dcl_k
body
&key
rewrite quant-ok skolem-name thm-name strengthen constrain
verbose)
where fn is the symbol you wish to define and is a new symbolic name, (var1 ... varn) is its list of formal parameters, the optional
dcl_i forms are declare forms, and body is its body, which
must be quantified as described below. The other arguments are explained
below.
For a simple example, see defun-sk-example. For a more elaborate
example, see Tutorial4-Defun-Sk-Example. See quantifier-tutorial for a careful beginner's introduction that takes you
through typical kinds of quantifier-based reasoning in ACL2. Also see quantifiers for an example illustrating how the use of recursion, rather than
explicit quantification with defun-sk, may be preferable.
Below we describe the defun-sk event precisely. First, let us
consider the examples above. The first example, again, is:
(defun-sk exists-x-p0-and-q0 (y z)
(exists x
(and (p0 x y z)
(q0 x y z))))
It is intended to represent the predicate with formal parameters y and
z that holds when for some x, (and (p0 x y z) (q0 x y z))
holds. In fact defun-sk is a macro, and the call above adds the
following two events, as shown just below. The first event guarantees
that if this new predicate holds of y and z, then the term shown,
(exists-x-p0-and-q0-witness y z), is an example of the x that is
therefore supposed to exist. (Intuitively, we are axiomatizing
exists-x-p0-and-q0-witness to pick a witness if there is one. We comment
below on the use of defun-nx; for now, consider defun-nx to be
defun.) Conversely, the second event below guarantees that if there
is any x for which the term in question holds, then the new predicate
does indeed hold of y and z.
(defun-nx exists-x-p0-and-q0 (y z)
(let ((x (exists-x-p0-and-q0-witness y z)))
(and (p0 x y z) (q0 x y z))))
(defthm exists-x-p0-and-q0-suff
(implies (and (p0 x y z) (q0 x y z))
(exists-x-p0-and-q0 y z)))
Now let us look at the third example from the introduction above:
(defun-sk forall-x-y-p0-and-q0 (z)
(forall (x y)
(and (p0 x y z)
(q0 x y z))))
The intention is to introduce a new predicate (forall-x-y-p0-and-q0 z)
which states that the indicated conjunction holds of all x and all y
together with the given z. This time, the axioms introduced are as shown
below. The first event guarantees that if the application of function
forall-x-y-p0-and-q0-witness to z picks out values x and y
for which the given term (and (p0 x y z) (q0 x y z)) holds, then the new
predicate forall-x-y-p0-and-q0 holds of z. Conversely, the
(contrapositive of) the second axiom guarantees that if the new predicate
holds of z, then the given term holds for all choices of x and
y (and that same z).
(defun-nx forall-x-y-p0-and-q0 (z)
(mv-let (x y)
(forall-x-y-p0-and-q0-witness z)
(and (p0 x y z) (q0 x y z))))
(defthm forall-x-y-p0-and-q0-necc
(implies (not (and (p0 x y z) (q0 x y z)))
(not (forall-x-y-p0-and-q0 z))))
The examples above suggest the critical property of defun-sk: it
indeed does introduce the quantified notions that it claims to introduce.
Notice that the defthm event just above,
forall-x-y-p0-and-q0-necc, may not be of optimal form as a rewrite rule.
Users sometimes find that when the quantifier is forall, it is useful to
state this rule in a form where the new quantified predicate is a hypothesis
instead. In this case that form would be as follows:
(defthm forall-x-y-p0-and-q0-necc
(implies (forall-x-y-p0-and-q0 z)
(and (p0 x y z) (q0 x y z))))
ACL2 will turn this into one :rewrite rule for each conjunct,
(p0 x y z) and (q0 x y z), with hypothesis (forall-x-y-p0-and-q0
z) in each case. In order to get this effect, use :rewrite :direct, in
this case as follows.
(defun-sk forall-x-y-p0-and-q0 (z)
(forall (x y)
(and (p0 x y z)
(q0 x y z)))
:rewrite :direct)
We now turn to a detailed description of defun-sk, starting with a
discussion of its arguments as shown in the "General Form" above.
The third argument, body, must be of the form
(Q bound-vars term)
where: Q is the symbol forall or exists, in the
"ACL2" package; bound-vars is a variable or true list of variables
disjoint from (var1 ... varn) and not including state; and
term is a term. The case that bound-vars is a single variable
v is treated exactly the same as the case that bound-vars is
(v).
The result of this event is to introduce a ``Skolem function,'' whose name
is the keyword argument skolem-name if that is supplied, and otherwise is
the result of modifying fn by suffixing "-WITNESS" to its name. The
following definition (or a corresponding rule; see the discussion of
:constrain below) and one of the following two theorems (as indicated)
are introduced for skolem-name and fn in the case that
bound-vars (see above) is a single variable v. The name of the
defthm event may be supplied as the value of the keyword argument
:thm-name; if it is not supplied, then it is the result of modifying
fn by suffixing "-SUFF" to its name in the case that the quantifier is
exists, and "-NECC" in the case that the quantifier is forall.
(defun-nx fn (var1 ... varn)
(let ((v (skolem-name var1 ... varn)))
term))
(defthm fn-suff ;in case the quantifier is EXISTS
(implies term
(fn var1 ... varn)))
(defthm fn-necc ;in case the quantifier is FORALL
(implies (not term)
(not (fn var1 ... varn))))
In the forall case, however, the keyword pair :rewrite :direct
may be supplied after the body of the defun-sk form, in which case the
contrapositive of the above form is used instead:
(defthm fn-necc ;in case the quantifier is FORALL
(implies (fn var1 ... varn)
term))
This is often a better choice for the "-NECC" rule, provided ACL2 can
parse term as a :rewrite rule. A second possible value of
the :rewrite argument of defun-sk is :default, which gives the
same behavior as when :rewrite is omitted. Otherwise, the value of
:rewrite should be the term to use as the body of the fn-necc
theorem shown above; ACL2 will attempt to do the requisite proof in this case.
If that term is weaker than the default, the properties introduced by
defun-sk may of course be weaker than they would be otherwise. Finally,
note that the :rewrite keyword argument for defun-sk only makes
sense if the quantifier is forall; it is thus illegal if the quantifier
is exists. Enough said about :rewrite!
In the case that bound-vars is a list of at least two variables, say
(bv1 ... bvk), the definition above (with no keywords) is the following
instead, but the theorem remains unchanged.
(defun-nx fn (var1 ... varn)
(mv-let (bv1 ... bvk)
(skolem-name var1 ... varn)
term))
In order to emphasize that the last element of the list, body, is a
term, defun-sk checks that the symbols forall and exists
do not appear anywhere in it. However, on rare occasions one might
deliberately choose to violate this convention, presumably because forall or exists is being used as a variable or because a macro call
will be eliminating ``calls of'' forall and exists. In these
cases, the keyword argument quant-ok may be supplied a non-nil
value. Then defun-sk will permit forall and exists in
the body, but it will still cause an error if there is a real attempt to use
these symbols as quantifiers.
The use of defun-nx above, rather than defun, disables
certain checks that are required for evaluation, for example in the passing of
multiple values. However, there is a price: calls of these defined functions
cannot be evaluated; see defun-nx. Normally that is not a problem,
since these notions involve quantifiers. But if you prefer that defun
be used instead of defun-nx, you can arrange that using declare
forms, given as the dcl_i as shown above. These will become the
declare forms in the generated defun. If the xargs declaration form :non-executable nil is supplied, then defun
will be used in place of defun-nx.
Guard verification is performed for defun-sk events under the
same conditions as for defun events. (An exception, ignored here but
discussed in a later paragraph below, occurs when keyword argument
:constrain t is supplied.) Thus, by default, guard verification will be
attempted exactly when at least one of type, :guard, or
:verify-guards t is specified in a declaration (that is, in some
dcl_i. This default behavior can be modified just as it is for
defun; see set-verify-guards-eagerness. Technical note: such
guard verification is implemented through a generated call of verify-guards after the encapsulate that surrounds the definitions
introduced; use :trans1 to see the expansion.
Defun-sk is a macro implemented using defchoose. Hence, it
should only be executed in defun-mode :logic; see defun-mode and see defchoose. You can use the command :pcb! to see the event generated by a call of the defun-sk macro. If you
want to watch the subsidiary events (including the defchoose event) as
they are being executed, use keyword option :verbose t.
An advanced feature is argument :strengthen t, which generates the
extra constraint that is generated for the corresponding defchoose event;
see defchoose. The name of that generated theorem will be obtained by
adding the suffix "-STRENGTHEN" to the function symbol being defined,
in the same package.
If you find that the rewrite rules introduced with a particular use of
defun-sk are not ideal, even when using the :rewrite keyword
discussed above (in the forall case), then at least two reasonable
courses of action are available for you. Perhaps the best option is to prove
the rewrite rules you want. If you see a pattern for creating rewrite
rules from your defun-sk events, you might want to write a macro that
executes a defun-sk followed by one or more defthm events.
Another option is to write your own variant of the defun-sk macro, say,
my-defun-sk, for example by modifying a copy of the definition of
defun-sk from the ACL2 sources.
There is one more keyword argument not explained above: :constrain.
The default is nil; otherwise this argument must be a symbol, which we
call name-def, except that in the case of t, name-def is
obtained by adding the suffix "-DEFINITION" to fn. For a
non-nil :constrain argument, this name-def is the name of a
rule of class :definition that equates (fn var1 ... varn)
with the body of the definition of fn. Furthermore, in this case of a
non-nil :constrain value the definition of fn is local to the
surrounding encapsulate, which contains a signature for fn. As
usual, the simplest way to see the effects of :constrain may be to apply
:trans1 to your defun-sk form. Note that constraining the function
can make it possible to attach to it (see defattach) and to introduce
it as a guard-verified function. Also note that when :constrain t
is specified: the guard of fn will automatically be t, no guard
verification will be performed, and fn will nevertheless be a
guard-verified (and constrained) function.
If you want to represent nested quantifiers, you can use more than one
defun-sk event. For example, in order to represent
(forall x (exists y (p x y z)))
you can use defun-sk twice, for example as follows.
(defun-sk exists-y-p (x z)
(exists y (p x y z)))
(defun-sk forall-x-exists-y-p (z)
(forall x (exists-y-p x z)))
Some distracting and unimportant warnings are inhibited during
defun-sk.
Note for ACL2(r) users (see real): In ACL2(r), the keyword
:CLASSICALP is also supported. Its legal values are t (the default)
and nil, and it determines whether or not (respectively) ACL2(r) will
consider fn to be a classical function. It must be the case that the
value is t (perhaps implicitly, by default) if and only if body is
classical.
Note that this way of implementing quantifiers is not a new idea. Hilbert
was certainly aware of it in the first half of the 20th century! Also see
conservativity-of-defchoose for a technical argument that justifies the
logical conservativity of the defchoose event in the sense of the
paper by Kaufmann and Moore entitled ``Structured Theory Development for a
Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001),
pp. 161–203).
Subtopics
- Define-sk
- A very fine alternative to defun-sk.
- Quantifier-tutorial
- A Beginner's Guide to Reasoning about Quantification in ACL2
- Defun-sk-queries
- Utilities to query defun-sk functions.
- Quantifiers
- Issues about quantification in ACL2
- Defun-sk-example
- A simple example using defun-sk
- Defund-sk
- Define a function with quantifier
and disable it and its associated rewrite rule.
- Forall
- Universal quantifier
- Def::un-sk
- An extension of defun-sk that supports automated skolemization and instantiation of quantified formulae
- Equiv
- A macro to prove that a universally quantified formula is a parameterized equivalence relation
- Exists
- Existential quantifier
- Congruence
- A macro to prove congruence rules for quantified formulae and their associated witnesses
