Major Section: DEFUN-SK
The initial version of this tutorial was written by Sandip Ray. Additions and revisions are welcome. Sandip has said:
``This is a collection of notes that I wrote to remind myself of how to reason about quantifiers when I just started. Most users after they have gotten the hang of quantifiers probably will not need this and will be able to use their intuitions to guide them in the process. But since many ACL2 users are not used to quantification, I am hoping that this set of notes might help them to think clearly while reasoning about quantifiers in ACL2.''
Many ACL2 papers start with the sentence ``ACL2 is a quantifier-free
first-order logic of recursive functions.'' It is true that the syntax
of ACL2 is quantifier-free; every formula is assumed to be universally
quantified over all free variables in the formula. But the logic in
fact does afford arbitrary first-order quantification. This is obtained in
ACL2 using a construct called
defun-sk. See defun-sk.
Many ACL2 users do not think in terms of quantifiers. The focus is
almost always on defining recursive functions and reasoning about them using
induction. That is entirely justified, in fact, since proving theorems about
recursive functions by induction plays to the strengths of the theorem
prover. Nevertheless there are situations where it is reasonable and often
useful to think in terms of quantifiers. However, reasoning about
quantifiers requires that you get into the mindset of thinking about theorems
in terms of quantification. This note is about how to do this effectively
given ACL2's implementation of quantification. This does not discuss
defun-sk in detail, but merely shows some examples. A detailed
explanation of the implementation is in the ACL2 documentation
(see defun-sk); also see conservativity-of-defchoose.
[Note: Quantifiers can be used for some pretty cool things in ACL2. Perhaps the most interesting example is the way of using quantifiers to introduce arbitrary tail-recursive equations; see the paper ``Partial Functions in ACL2'' by Panagiotis Manolios and J Strother Moore. This note does not address applications of quantifiers, but merely how you would reason about them once you think you want to use them.]
Assume that you have some function
P. I have just left
P as a unary
function stub below, since I do not care about what
(defstub P (*) => *)Now suppose you want to specify the concept that ``there exists some
(P x)holds''. ACL2 allows you to write that directly using quantifiers.
(defun-sk exists-P () (exists x (P x)))If you submit the above form in ACL2 you will see that the theorem prover specifies two functions
exists-p-witness, and exports the following constraints:
1. (defun exists-P () (P (exists-P-witness))) 2. (defthm exists-P-suff (implies (p x) (exists-p)))Here
exists-P-witnessis a new function symbol in the current ACL2 theory. What do the constraints above say? Notice the constraint
exists-p-suff. It says that if you can provide any
(P x)holds, then you know that
exists-pholds. Think of the other constraint (definition of
exists-p) as going the other way. That is, it says that if
exists-pholds, then there is some
x, call it
(exists-p-witness), for which
Pholds. Notice that nothing else is known about
exists-p-witnessthan the two constraints above.
exists-p-witness above is actually defined in ACL2 using a special
defchoose. See defchoose. This note does not talk about
defchoose. So far as this note is concerned, think of
exists-p-witness as a new function symbol that has been generated somehow
in ACL2, about which nothing other than the two facts above is known.]
Similarly, you can talk about the concept that ``for all
holds.'' This can be specified in ACL2 by the form:
(defun-sk forall-P () (forall x (P x)))This produces the following two constraints:
1. (defun forall-P () (P (forall-p-witness))) 2. (defthm forall-p-necc (implies (not (P x)) (not (forall-p))))To understand these, think of
for-all-p-witnessas producing some
xwhich does not satisfy
P, if such a thing exists. The constraint
forall-p-neccmerely says that if
Pis satisfied for every
x. (To see this more clearly, just think of the contrapositive of the formula shown.) The other constraint (definition of
forall-p) implies that if
forall-pdoes not hold then there is some
x, call it
(forall-p-witness), which does not satisfy
P. To see this, just consider the following formula which is immediately derivable from the definition.
(implies (not (forall-p)) (not (P (forall-witness))))The description above suggests that to reason about quantifiers, the following Rules of Thumb, familiar to most any student of logic, are useful.
RT1: To prove
(exists-p), construct some object
Aand then use
RT2: If you assume
exists-Pin your hypothesis, use the definition of
exists-pto know that
exists-p-witness. To use this to prove a theorem, you must be able to derive the theorem based on the hypothesis that
Pholds for something, whatever the something is.
RT3: To prove
forall-P, prove the theorem
(P x)(that is, that
Pholds for an arbitrary
x), and then simply instantiate the definition of
forall-p, that is, show that
Pholds for the witness.
RT4: If you assume
forall-pin the hypothesis of the theorem, see how you can prove your conclusion if indeed you were given
(P x)as a theorem. Possibly for the conclusion to hold, you needed that
Pholds for some specific set of
xvalues. Then use the theorem
forall-p-neccby instantiating it for the specific
xvalues you care about.
Perhaps the above is too terse. In the remainder of the note, we will consider several examples of how this is done to prove theorems in ACL2 that involve quantified notions.
Let us consider two trivial theorems. Assume that for some unary function
r, you have proved
(r x) as a theorem. Let us see how you can prove
that (1) there exists some x such that
(r x) holds, and (2) for all
(r x) holds.
We first model these things using
r is simply
some function for which
(r x) is a theorem.
(encapsulate (((r *) => *)) (local (defun r (x) (declare (ignore x)) t)) (defthm r-holds (r x))) (defun-sk exists-r () (exists x (r x))) (defun-sk forall-r () (forall x (r x)))ACL2 does not have too much reasoning support for quantifiers. So in most cases, one would need
:usehints to reason about quantifiers. In order to apply
:usehints, it is preferable to keep the function definitions and theorems disabled.
(in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))Let us now prove that there is some
(r x)holds. Since we want to prove
exists-r, we must use
exists-r-suffby RT1. We do not need to construct any instance here since
rholds for all
xby the theorem above.
(defthm exists-r-holds (exists-r) :hints (("Goal" :use ((:instance exists-r-suff)))))Let us now prove the theorem that for all
(r x)holds. By RT3, we must be able to prove it by definition of
(defthm forall-r-holds (forall-r) :hints (("Goal" :use ((:instance (:definition forall-r))))))[Note: Probably no ACL2 user in his or her right mind would prove the theorems
forall-r-holdsabove. The theorems shown are only for demonstration purposes.]
For the remainder of this note we will assume that we have two stubbed out
N, and we will look at proving some quantified
properties of these functions.
(defstub M (*) => *) (defstub N (*) => *)Let us now define the predicates
ex-Nspecifying the various quantifications.
(defun-sk all-M () (forall x (M x))) (defun-sk all-N () (forall x (N x))) (defun-sk some-M () (exists x (M x))) (defun-sk some-N () (exists x (N x))) (in-theory (disable all-M all-N all-M-necc all-N-necc)) (in-theory (disable some-M some-N some-M-suff some-N-suff))Let us prove the classic distributive properties of quantification: the distributivity of universal quantification over conjunction, and the distributivity of existential quantification over disjunction. We can state these properties informally in ``pseudo ACL2'' notation as follows:
1. (exists x: (M x)) or (exists x: (N x)) <=> (exists x: (M x) or (N x)) 2. (forall x: (M x)) and (forall: x (N x)) <=> (forall x: (M x) and (N x))To make these notions formal we of course need to define the formulas at the right-hand sides of 1 and 2. So we define
all-MNto capture these concepts.
(defun-sk some-MN () (exists x (or (M x) (N x)))) (defun-sk all-MN () (forall x (and (M x) (N x)))) (in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))First consider proving property 1. The formal statement of this theorem would be:
(iff (some-MN) (or (some-M) (some-N))).
How do we prove this theorem? Looking at RT1-RT4 above, note that they suggest how one should reason about quantification when one has an ``implication''. But here we have an ``equivalence''. This suggests another rule of thumb.
RT5: Whenever possible, prove an equivalence involving quantifiers by proving two implications.
Let us apply RT5 to prove the theorems above. So we will first prove:
(implies (some-MN) (or (some-M) (some-N)))
How can we prove this? This involves assuming a quantified predicate
(some-MN), so we must use RT2 and apply the definition of
Since the conclusion involves a disjunction of two quantified predicates, by
RT1 we must be able to construct two objects
B such that either
M holds for
N holds for
B, so that we can then invoke
some-N-suff to prove the conclusion. But now notice
some-MN is true, then there is already an object, in fact
some-MN-witness, such that either
M holds for it, or
N holds for
it. And we know this is the case from the definition of
some-MN! So we
will simply prove the theorem instantiating
some-N-suff with this witness. The conclusion is that the following
event will go through with ACL2.
(defthm le1 (implies (some-MN) (or (some-M) (some-N))) :rule-classes nil :hints (("Goal" :use ((:instance (:definition some-MN)) (:instance some-M-suff (x (some-MN-witness))) (:instance some-N-suff (x (some-MN-witness)))))))This also suggests the following rule of thumb:
RT6: If a conjecture involves assuming an existentially quantified predicate in the hypothesis from which you are trying to prove an existentially quantified predicate, use the witness of the existential quantification in the hypothesis to construct the witness for the existential quantification in the conclusion.
Let us now try to prove the converse of le1, that is:
(implies (or (some-M) (some-N)) (some-MN))
Since the hypothesis is a disjunction, we will just prove each case
individually instead of proving the theorem by a :
cases hint. So we
prove the following two lemmas.
(defthm le2 (implies (some-M) (some-MN)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition some-M)) (:instance some-MN-suff (x (some-M-witness))))))) (defthm le3 (implies (some-N) (some-MN)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition some-N)) (:instance some-MN-suff (x (some-N-witness)))))))Note that the hints above are simply applications of RT6 as in
le1. With these lemmas, of course the main theorem is trivial.
(defthmd |some disjunction| (iff (some-MN) (or (some-M) (some-N))) :hints (("Goal" :use ((:instance le1) (:instance le2) (:instance le3)))))Let us now prove the distributivity of universal quantification over conjunction, that is, the formula:
(iff (all-MN) (and (all-M) (all-N)))
Applying RT5, we will again decompose this into two implications. So
consider first the one-way implication:
(implies (and (all-M) (all-N)) (all-MN)).
Here we get to assume
all-N. Thus by RT4 we can use
all-N-necc to think as if we are given the formulas
(M x) and
(N x) as theorems. The conclusion here is also a universal
quantification, namely we have to prove
all-MN. Then RT3 tells us to
proceed as follows. Take any object
y. Try to find an instantiation
z of the hypothesis that implies
(and (M y) (N y)). Then instantiate
all-MN-witness. Note that the hypothesis lets us assume
(M x) and
(N x) to be theorems. Thus to justify we need to
y, and in this case, therefore, with
all-MN-witness. To make the long story short, the following event goes
through with ACL2:
(defthm lf1 (implies (and (all-M) (all-N)) (all-MN)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition all-MN)) (:instance all-M-necc (x (all-MN-witness))) (:instance all-N-necc (x (all-MN-witness)))))))This suggests the following rule of thumb which is a dual of RT6:
RT7: If a conjecture assumes some universally quantified predicate in the hypothesis and its conclusion asserts a universallly quantified predicate, then instantiate the ``necessary condition'' (
forall-mn-necc) of the hypothesis with the witness of the conclusion to prove the conjecture.
Applying RT7 now we can easily prove the other theorems that we need to show that universal quantification distributes over conjunction. Let us just go through this motion in ACL2.
(defthm lf2 (implies (all-MN) (all-M)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition all-M)) (:instance all-MN-necc (x (all-M-witness))))))) (defthm lf3 (implies (all-MN) (all-N)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition all-N)) (:instance all-MN-necc (x (all-N-witness))))))) (defthmd |all conjunction| (iff (all-MN) (and (all-M) (all-N))) :hints (("Goal" :use ((:instance lf1) (:instance lf2) (:instance lf3)))))The rules of thumb for universal and existential quantification should make you realize the duality of their use. Every reasoning method about universal quantification can be cast as a way of reasoning about existential quantification, and vice versa. Whether you reason using universal and existential quantifiers depends on what is natural in a particular context. But just for the sake of completeness let us prove the duality of universal and existential quantifiers. So what we want to prove is the following:
3. (forall x (not (M x))) = (not (exists x (M x)))We first formalize the notion of
(forall x (not (M x)))as a quantification.
(defun-sk none-M () (forall x (not (M x)))) (in-theory (disable none-M none-M-necc))So we now want to prove:
(equal (none-M) (not (some-M))).
As before, we should prove this as a pair of implications. So let us prove
(implies (none-M) (not (some-M))).
This may seem to assert an existential quantification in the conclusion, but
rather, it asserts the negation of an existential quantification. We
are now trying to prove that something does not exist. How do we do that?
We can show that nothing satisfies
M by just showing that
(some-M-witness) does not satisfy
M. This suggests the following
rule of thumb:
RT8: When you encounter the negation of an existential quantification think in terms of a universal quantification, and vice-versa.
Ok, so now applying RT8 and RT3 you should be trying to apply the definition of
some-M. The hypothesis is just a pure (non-negated) universal quantification
so you should apply RT4. A blind application lets us prove the theorem as
(defthm nl1 (implies (none-M) (not (some-M))) :rule-classes nil :hints (("Goal" :use ((:instance (:definition some-M)) (:instance none-M-necc (x (some-M-witness)))))))How about the converse implication? I have deliberately written it as
(implies (not (none-M)) (some-M))instead of switching the left-hand and right-hand sides of
nl1, which would have been equivalent. Again, RH8 tells us how to reason about it, in this case using RH2, and we succeed.
(defthm nl2 (implies (not (none-M)) (some-M)) :rule-classes nil :hints (("Goal" :use ((:instance (:definition none-M)) (:instance some-M-suff (x (none-M-witness)))))))So finally we just go through the motions of proving the equality.
(defthmd |forall not = not exists| (equal (none-M) (not (some-M))) :hints (("Goal" :use ((:instance nl1) (:instance nl2)))))Let us now see if we can prove a slightly more advanced theorem which can be stated informally as: If there is a natural number
M, then there is a least natural number
[Note: Any time I have had to reason about existential quantification I have had to do this particular style of reasoning and state that if there is an object satisfying a predicate, then there is also a ``minimal'' object satisfying the predicate.]
Let us formalize this concept. We first define the concept of existence of a
natural number satisfying
(defun-sk some-nat-M () (exists x (and (natp x) (M x)))) (in-theory (disable some-nat-M some-nat-M-suff))We now talk about what it means to say that
xis the least number satisfying
(defun-sk none-below (y) (forall r (implies (and (natp r) (< r y)) (not (M r)))))) (in-theory (disable none-below none-below-necc)) (defun-sk min-M () (exists y (and (M y) (natp y) (none-below y)))) (in-theory (disable min-M min-M-suff))The predicate
none-belowsays that no natural number less than
M. The predicate
min-Msays that there is some natural number
So the formula we want to prove is:
(implies (some-nat-M) (min-M)).
Since the formula requires that we prove an existential quantification, RT1
tells us to construct some object satisfying the predicate over which we are
quantifying. We should then be able to instantiate
min-M-suff with this
object. That predicate says that the object must be the least natural number
M. Since such an object is uniquely computable if we know
that there exists some natural number satisfying
M, let us just write a
recursive function to compute it. This function is
(defun least-M-aux (i bound) (declare (xargs :measure (nfix (- (1+ bound) i)))) (cond ((or (not (natp i)) (not (natp bound)) (> i bound)) 0) ((M i) i) (t (least-M-aux (+ i 1) bound)))) (defun least-M (bound) (least-M-aux 0 bound))Let us now reason about this function as one does typically. So we prove that this object is indeed the least natural number that satisfies
M, assuming that
boundis a natural number that satisfies
(defthm least-aux-produces-an-M (implies (and (natp i) (natp bound) (<= i bound) (M bound)) (M (least-M-aux i bound)))) (defthm least-<=bound (implies (<= 0 bound) (<= (least-M-aux i bound) bound))) (defthm least-aux-produces-least (implies (and (natp i) (natp j) (natp bound) (<= i j) (<= j bound) (M j)) (<= (least-M-aux i bound) j))) (defthm least-aux-produces-natp (natp (least-M-aux i bound))) (defthmd least-is-minimal-satisfying-m (implies (and (natp bound) (natp i) (< i (least-M bound))) (not (M i))) :hints (("Goal" :in-theory (disable least-aux-produces-least least-<=bound) :use ((:instance least-<=bound (i 0)) (:instance least-aux-produces-least (i 0) (j i)))))) (defthm least-has-m (implies (and (natp bound) (m bound)) (M (least-M bound)))) (defthm least-is-natp (natp (least-M bound)))So we have done that, and hopefully this is all that we need about
least-M. So we disable everything.
(in-theory (disable least-M natp))Now of course we note that the statement of the conjecture we are interested in has two quantifiers, an inner
none-below) and an outer
min-M). Since ACL2 is not very good with quantification, we hold its hands to reason with the quantifier part. So we will first prove something about the
foralland then use it to prove what we need about the
RT9: When you face nested quantifiers, reason about each nesting separately.
So what do we want to prove about the inner quantifier? Looking carefully at
the definition of
none-below we see that it is saying that for all natural
(M r) does not hold. Well, how would we want to
use this fact when we want to prove our final theorem? We expect that we
min-M-suff with the object
(least-M bound) where we
know (via the outermost existential quantifier) that
M holds for
bound, and we will then want to show that
none-below holds for
(least-M bound). So let us prove that for any natural number (call it
none-below holds for
(least-M bound). For the final
theorem we only need it for natural numbers satisfying
M, but note that
from the lemma
least-is-minimal-satisfying-m we really do not need that
So we are now proving:
(implies (natp bound) (none-below (least-M bound))).
Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3. We have proved that for all naturals
i does not satisfy
least-is-minimal-satisfying-M), so we merely need the instantiation of
that lemma with
none-below-witness of the thing we are trying to prove,
(least-M bound). The theorem below thus goes through.
(defthm least-is-minimal (implies (natp bound) (none-below (least-M bound))) :hints (("Goal" :use ((:instance (:definition none-below) (y (least-M bound))) (:instance least-is-minimal-satisfying-m (i (none-below-witness (least-M bound))))))))Finally we are in the outermost existential quantifier, and are in the process of applying
min-M-suff. What object should we instantiate it with? We must instantiate it with
boundis an object which must satisfy
Mand is a natural. We have such an object, namely
(some-nat-M-witness)which we know have all these qualities given the hypothesis. So the proof now is just RT1 and RT2.
(defthm |minimal exists| (implies (some-nat-M) (min-M)) :hints (("Goal" :use ((:instance min-M-suff (y (least-M (some-nat-M-witness)))) (:instance (:definition some-nat-M))))))
If you are comfortable with the reasoning above, then you are comfortable with quantifiers and probably will not need these notes any more. In my opinion, the best way of dealing with ACL2 is to ask yourself why you think something is a theorem, and the rules of thumb above are simply guides to the questions that you need to ask when you are dealing with quantification.
Here are a couple of simple exercises for you to test if you understand the reasoning process.
Exercise 1. Formalize and prove the following theorem. Suppose there
x such that
(R x) and suppose that all
(P x). Then prove that there exists
x such that
(P x) & (R x).
for a solution.)
Exercise 2. Recall the example just before the preceding exercise,
where we showed that if there exists a natural number
then there is another natural number
y such that
and for every natural number
z does not. What would
happen if we remove the restriction of
naturals? Of course, we will not talk about
< any more, but suppose you
use the total order on all ACL2 objects (from community book
"books/misc/total-order"). More concretely, consider the definition of
some-M above. Let us now define two other functions:
(include-book "misc/total-order" :dir :system) (defun-sk none-below-2 (y) (forall r (implies (<< r y) (not (M r))))) (defun-sk min-M2 () (exists y (and (M y) (none-below-2 y))))The question is whether
(implies (some-M) (min-M2))is a theorem. Can you prove it? Can you disprove it?