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