Solution to ACL2 Quantifier Exercise 1

Author: Sandip Ray

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