QUANTIFIERS

issues about quantification in ACL2 
Major Section:  DEFUN-SK

ACL2 supports first-order quantifiers exists and forall by way of the defun-sk event. However, proof support for quantification is quite limited. Therefore, we recommend using recursion in place of defun-sk when possible (following common ACL2 practice).

For example, the notion ``every member of x has property p'' can be defined either with recursion or explicit quantification, but proofs may be simpler when recursion is used. We illustrate this point with two proofs of the same informal claim, one of which uses recursion which the other uses explicit quantification. Notice that with recursion, the proof goes through fully automatically; but this is far from true with explicit quantification (especially notable is the ugly hint).

The informal claim for our examples is: If every member a of each of two lists satisfies the predicate (p a), then this holds of their append; and, conversely.

See quantifiers-using-recursion for a solution to this example using recursion.

See quantifiers-using-defun-sk for a solution to this example using defun-sk. Also See quantifiers-using-defun-sk-extended for an elaboration on that solution.


QUANTIFIERS-USING-DEFUN-SK

quantification example 
Major Section:  QUANTIFIERS

See quantifiers for the context of this example. It should be compared to a corresponding example in which a simpler proof is attained by using recursion in place of explicit quantification; see quantifiers-using-recursion. 

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


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


(defthm forall-p-append
  (equal (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)))
            (: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))))))))

Also see quantifiers-using-defun-sk-extended for an elaboration on this example.


QUANTIFIERS-USING-DEFUN-SK-EXTENDED

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



QUANTIFIERS-USING-RECURSION

recursion for implementing quantification 
Major Section:  QUANTIFIERS

The following example illustrates the use of recursion as a means of avoiding proof difficulties that can arise from the use of explicit quantification (via defun-sk). See quantifiers for more about 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 recursively-defined functions.


(defstub p (x) t)


(defun all-p (x)
  (if (atom x)
      t
    (and (p (car x))
         (all-p (cdr x)))))


(defthm all-p-append
  (equal (all-p (append x1 x2))
         (and (all-p x1) (all-p x2))))