|
|
|---|
|
|
|
|---|
Quantification example with details
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))))