QUANTIFIERS-USING-DEFUN-SK-EXTENDED

Major Section:  QUANTIFIERS

See quantifiers-using-defun-sk for the context of this example.

(in-package "ACL2")


; We prove that if every member A of each of two lists satisfies the
; predicate (P A), then this holds of their append; and, conversely.


; Here is a solution using explicit quantification.


(defstub p (x) t)


(defun-sk forall-p (x)
  (forall a (implies (member a x)
                     (p a))))


; The defun-sk above introduces the following axioms.  The idea is that
; (FORALL-P-WITNESS X) picks a counterexample to (forall-p x) if there is one.


#|
(DEFUN FORALL-P (X)
  (LET ((A (FORALL-P-WITNESS X)))
       (IMPLIES (MEMBER A X) (P A))))


(DEFTHM FORALL-P-NECC
  (IMPLIES (NOT (IMPLIES (MEMBER A X) (P A)))
           (NOT (FORALL-P X)))
  :HINTS (("Goal" :USE FORALL-P-WITNESS)))
|#


; The following lemma seems critical.


(defthm member-append
  (iff (member a (append x1 x2))
       (or (member a x1) (member a x2))))


; The proof of forall-p-append seems to go out to lunch, so we break into
; directions as shown below.


(defthm forall-p-append-forward
  (implies (forall-p (append x1 x2))
           (and (forall-p x1) (forall-p x2)))
  :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
           :use
           ((:instance forall-p-necc
                       (x (append x1 x2))
                       (a (forall-p-witness x1)))
            (:instance forall-p-necc
                       (x (append x1 x2))
                       (a (forall-p-witness x2)))))))


(defthm forall-p-append-reverse
  (implies (and (forall-p x1) (forall-p x2))
           (forall-p (append x1 x2)))
  :hints (("Goal"
           :use
           ((:instance forall-p-necc
                       (x x1)
                       (a (forall-p-witness (append x1 x2))))
            (:instance forall-p-necc
                       (x x2)
                       (a (forall-p-witness (append x1 x2))))))))


(defthm forall-p-append
  (equal (forall-p (append x1 x2))
         (and (forall-p x1) (forall-p x2)))
  :hints (("Goal" :use (forall-p-append-forward
                        forall-p-append-reverse))))