Original Date: February 14, 2005.
Last Updated: November 9, 2008.
[Note: This version includes some of the changes to the
original documentation made by Matt Kaufmann to
incorporate this tutorial into the ACL2 User's Manual. Click here
for the version in the User's Manual.]
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 P
is.
(defstub P (*) => *)Now suppose you want to specify the concept that ``there exists some
x
such that (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
and 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-witness
is 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 x
such that
(P x)
holds, then you know that exists-p
holds. Think of the other
constraint (definition of exists-p
) as going the other way. That is, it
says that if exists-p
holds, then there is some x
, call it
(exists-p-witness)
, for which P
holds. Notice that nothing else is
known about exists-p-witness
than the two constraints above.
[Note: exists-p-witness
above is actually defined in ACL2 using a special
form called 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 x
(P x)
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-witness
as producing some x
which does not satisfy P
, if such a thing exists. The constraint
forall-p-necc
merely says that if forall-p
holds then P
is
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-p
does 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 objectA
such thatP
holds forA
and then useexists-P-suff
.RT2: If you assume
exists-P
in your hypothesis, use the definition ofexists-p
to know thatP
holds forexists-p-witness
. To use this to prove a theorem, you must be able to derive the theorem based on the hypothesis thatP
holds for something, whatever the something is.RT3: To prove
forall-P
, prove the theorem(P x)
(that is, thatP
holds for an arbitraryx
), and then simply instantiate the definition offorall-p
, that is, show thatP
holds for the witness.RT4: If you assume
forall-p
in 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 thatP
holds for some specific set ofx
values. Then use the theoremforall-p-necc
by instantiating it for the specificx
values 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 x
(r x)
holds.
We first model these things using defun-sk
. Below, 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)))ACL2 does not have too much reasoning support for quantifiers. So in most cases, one would need(defun-sk exists-r () (exists x (r x))) (defun-sk forall-r () (forall x (r x)))
:use
hints to reason about
quantifiers. In order to apply :use
hints, 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
x
such that (r
x)
holds. Since we want to prove exists-r
, we
must use exists-r-suff
by RT1. We do not need to
construct any instance here since r
holds for all
x
by 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
x
, (r
x)
holds. By RT3, we must be able to prove it by definition of
forall-r
.
(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
exists-r-holds
and
forall-r-holds
above. The theorems shown are only for
demonstration purposes.
For the remainder of this note we will assume that we have two stubbed
out unary functions M
and N
, and we will
look at proving some quantified properties of these functions.
(defstub M (*) => *) (defstub N (*) => *)Let us now define the predicates
all-M
,
all-N
, ex-M
, and ex-N
specifying 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)))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:(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))
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
some-MN
and all-MN
to 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))))First consider proving property 1. The formal statement of this theorem would be:(in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))
(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 some-MN
.
Since the conclusion involves a disjunction of two quantified predicates, by
RT1 we must be able to construct two objects A
and B
such that either
M
holds for A
or N
holds for B
, so that we can then invoke
some-M-suff
and some-N-suff
to prove the conclusion. But now notice
that if 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-M-suff
and
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)))))))Note that the hints above are simply applications of RT6 as in(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)))))))
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-M
and all-N
. Thus
by RT4 we can use all-M-necc
and 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 y
with all-MN-witness
. Note
that the hypothesis lets us assume (M x)
and (N
x)
to be theorems. Thus to justify we need to instantiate
x
with 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)))))))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:(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)))))
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 first: (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 below.
(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
x
which satisfies M
, then there is a least
natural number y
that satisfies M
.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 x
.
(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
x
is the
least number satisfying M
.
(defun-sk none-below (y) (forall r (implies (and (natp r) (< r y)) (not (M r)))))) (in-theory (disable none-below none-below-necc))The predicate(defun-sk min-M () (exists y (and (M y) (natp y) (none-below y)))) (in-theory (disable min-M min-M-suff))
none-below
says that no natural number less
than y
satisfies M
. The predicate
min-M
says that there is some natural number
y
satisfying M
such that
none-below
holds for y
.
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 that satisfies
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 least-M
below.
(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))))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(defun least-M (bound) (least-M-aux 0 bound))
M
, assuming that bound
is a
natural number that satisfies M
.
(defthm least-aux-produces-an-M (implies (and (natp i) (natp bound) (<= i bound) (M bound)) (M (least-M-aux i bound))))So we have done that, and hopefully this is all that we need about(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)))
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
forall
(from
none-below
) and an outer exists
(from
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 forall
and then use it to
prove what we need about the exists
.
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 numbers r
<
y
, (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 will instantiate 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 bound
),
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
bound
satisfies M
.
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
< (least-M bound)
, i
does
not satisfy M
(lemma
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, that is, (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 (least-M
bound)
where bound
is an object which must satisfy
M
and 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 is just a simple exercise for you to test if you understand the reasoning process.
Exercise:
In the example above we showed that if there exists a natural number
x
satisfying M
then there is another natural
number y
such that y
satisfies
M
and for every natural number z
<
y
, z
does not. What would happen if we
remove the restriction of x
, y
, and
z
being naturals? Of course, we will not talk about
<
any more, but suppose you use the total order on all
ACL2 objects (from "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)The question is whether(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))))
(implies (some-M) (min-M2))
is a
theorem. Can you prove it? Can you disprove it?