# Solution to ACL2 Quantifier Exercise 1

### Author: Sandip Ray

In ACL2
documentation topic QUANTIFIER-TUTORIAL
(Version 3.5 and later) one finds the following exercise.
**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)`

.

Below is a solution to that exercise from Sandip Ray.

(in-package "ACL2")
(defstub P (*) => *)
(defstub R (*) => *)
;; First I define the concepts exists-P, forall-R, and exists-P-and-R.
(defun-sk exists-R ()
(exists x (R x)))
(defun-sk forall-P ()
(forall x (P x)))
(defun-sk exists-P-and-R ()
(exists x (and (P x) (R x))))
;; Now disable everything, since I hate to get ACL2 to do any
;; reasoning with quantifiers unless I know what I am doing.
(in-theory (disable exists-R exists-R-suff forall-P forall-P-necc
exists-P-and-R exists-P-and-R-suff))
;; Now prove it! For pedagogical reason I leave comments that
;; associate each hint instance with the different rules of thumb
;; explained in quantifier-tutorial. (See :DOC quantifier-tutorial).
(defthm |exists x (P x) and (R x)|
(implies (and (exists-R)
(forall-P))
(exists-P-and-R))
:hints (("Goal"
:use (
;; The x that satisfies P and R is the x that
;; satisfies R (since everything satisfies P).
(:instance exists-P-and-R-suff
(x (exists-R-witness)))
;; Now show that this particular x satisfies P,
;; invoking the -necc lemma
(:instance forall-P-necc
(x (exists-R-witness)))
;; and show that it satisfies R using the definition
;; of Q.
(:instance (:definition exists-R))))))