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.]

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 a hang of quantifiers probably will not need this and will be able to have 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 `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 object`A`

such that`P`

holds for`A`

and then use`exists-P-suff`

.

RT2:If you assume`exists-P`

in your hypothesis, use the definition of`exists-p`

to know that`P`

holds for`exists-p-witness`

. To use this to prove a theorem, you must be able to derive the theorem based on the hypothesis that`P`

holds for something, whatever the something is.

RT3:To prove`forall-P`

, prove the theorem`(P x)`

(that is, that`P`

holds for an arbitrary`x`

), and then simply instantiate the definition of`forall-p`

, that is, show that`P`

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 that`P`

holds for some specific set of`x`

values. Then use the theorem`forall-p-necc`

by instantiating it for the specific`x`

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))))))

`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:

Ok, so now applying RT8 and RT3 you should be trying to apply the definition ofRT8:When you encounter the negation of an existential quantification think in terms of a universal quantification, and vice-versa.

`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?