INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

This answer is in the form of a script sufficient to lead ACL2 to a proof.

; Trying subsetp-reflexive at this point produces the key checkpoint:

; (IMPLIES (AND (CONSP X)
;               (SUBSETP (CDR X) (CDR X)))
;          (SUBSETP (CDR X) X))

; which suggests the generalization:

(defthm subsetp-cdr
  (implies (subsetp a (cdr b))
           (subsetp a b)))

; And now subsetp-reflexive succeeds.

(defthm subsetp-reflexive
  (subsetp x x))

; A weaker version of the lemma, namely the one in which we
; add the hypothesis that b is a cons, is also sufficient.

;    (defthm subsetp-cdr-weak
;      (implies (and (consp b)
;                    (subsetp a (cdr b)))
;               (subsetp a b)))

; But the (consp b) hypothesis is not really necessary in
; ACL2's type-free logic because (cdr b) is nil if b is
; not a cons.  For the reasons explained in the tutorial, we
; prefer the strong version.

Use your browser's Back Button now to return to introductory-challenge-problem-2.