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

```