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
Now suppose you want to specify the concept that ``there exists some
If you submit the above form in ACL2 you will see that the theorem prover
specifies two functions
Similarly, you can talk about the concept that ``for all
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
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 Asuch that Pholds for Aand then use exists-P-suff.
RT2: If you assume
exists-Pin your hypothesis, use the definition of exists-pto know that Pholds for 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
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
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
For the remainder of this note we will assume that we have two stubbed out
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))
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.
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.
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)))))
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:
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
(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))
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
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
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
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))))