Exercise 1. Formalize and prove the following theorem. Suppose there exists
(R x)and suppose that all
(P x). Then prove that there exists
(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))))))