QUANTIFIER-TUTORIAL.html -- ACL2 Version 6.2

QUANTIFIER-TUTORIAL

A Beginner's Guide to Reasoning about Quantification in ACL2

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

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

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

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

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

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

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

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

(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 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 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 x such that (R x) and suppose that all x satisfy (P x). Then prove that there exists x such that (P x) & (R x). (See http://www.cs.utexas.edu/users/moore/acl2/contrib/quantifier-exercise-1-solution.html for a solution.)

Exercise 2. Recall the example just before the preceding exercise, where 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 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?