A Beginner's Guide to Reasoning about Quantification in ACL2

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

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

(defstub P (*) => *)

Now suppose you want to specify the concept that ``there exists some

(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

1. (defun exists-P () (P (exists-P-witness))) 2. (defthm exists-P-suff (implies (p x) (exists-p)))

Here

[Note:

Similarly, you can talk about the concept that ``for all

(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

(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

We first model these things using `defun-sk`. Below,

(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

(in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))

Let us now prove that there is some

(defthm exists-r-holds (exists-r) :hints (("Goal" :use ((:instance exists-r-suff)))))

Let us now prove the theorem that for all

(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

For the remainder of this note we will assume that we have two stubbed out
unary functions

(defstub M (*) => *) (defstub N (*) => *)

Let us now define the predicates

(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

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

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:

How can we prove this? This involves assuming a quantified predicate

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

Since the hypothesis is a disjunction, we will just prove each case
individually instead of proving the theorem by a

(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

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

Applying RT5, we will again decompose this into two implications. So
consider first the one-way implication:

Here we get to assume

(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 universally 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

(defun-sk none-M () (forall x (not (M x)))) (in-theory (disable none-M none-M-necc))

So we now want to prove:

As before, we should prove this as a pair of implications. So let us prove
first:

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

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

(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

(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

[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

(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

So the formula we want to prove is:

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

(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

(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

(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

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

So we are now proving:

Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3. We have proved that for all naturals

(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

(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 exists

**Exercise 2**. Recall the example just before the preceding exercise,
where we showed that if there exists a natural number

(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 `solution-to-ACL2-quantifier-exercise-2` for a solution.

- Solution-to-ACL2-quantifier-exercise-2
- A solution to
`quantifier-tutorial`Exercise 2