INTRODUCTORY-CHALLENGE-PROBLEM-3-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 dupsp-rev at this point produces the key checkpoint:

; (IMPLIES (AND (CONSP X)
;               (NOT (MEMBER (CAR X) (CDR X)))
;               (EQUAL (DUPSP (REV (CDR X)))
;                      (DUPSP (CDR X))))
;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
;                 (DUPSP (CDR X))))

; which suggests the lemma

; (defthm dupsp-append
;   (implies (not (member e x))
;            (equal (dupsp (append x (list e)))
;                   (dupsp x))))

; However, attempting to prove that, produces a key checkpoint
; containing (MEMBER (CAR X) (APPEND (CDR X) (LIST E))).
; So we prove the lemma:

(defthm member-append
  (iff (member e (append a b))
       (or (member e a)
           (member e b))))

; Note that we had to use iff instead of equal since member is not a
; Boolean function.

; Having proved this lemma, we return to dupsp-append and succeed:

(defthm dupsp-append
  (implies (not (member e x))
           (equal (dupsp (append x (list e)))
                  (dupsp x))))

; So now we return to dups-rev, expecting success.  But it fails
; with the same key checkpoint:

; (IMPLIES (AND (CONSP X)
;               (NOT (MEMBER (CAR X) (CDR X)))
;               (EQUAL (DUPSP (REV (CDR X)))
;                      (DUPSP (CDR X))))
;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
;                 (DUPSP (CDR X))))

; Why wasn't our dupsp-append lemma applied?  We have two choices here:
; (1) Think.  (2) Use tools.

; Think:  When an enabled rewrite rule doesn't fire even though the left-hand
; side matches the target, the hypothesis couldn't be relieved.  The dups-append
; rule has the hypothesis (not (member e x)) and after the match with the left-hand side,
; e is (CAR X) and x is (REV (CDR X)).  So the system couldn't rewrite
; (NOT (MEMBER (CAR X) (REV (CDR X)))) to true, even though it knows that
; (NOT (MEMBER (CAR X) (CDR X))) from the second hypothesis of the checkpoint.
; Obviously, we need to prove member-rev below.

; Use tools:  We could enable the ``break rewrite'' facility, with

; ACL2 !>:brr t

; and then install an unconditional monitor on the rewrite rule
; dupsp-append, whose rune is (:REWRITE DUPSP-APPEND), with:

; :monitor (:rewrite dupsp-append) t

; Then we could re-try our main theorem, dupsp-rev.  At the resulting
; interactive break we type :eval to evaluate the attempt to relieve the
; hypotheses of the rule.

; (1 Breaking (:REWRITE DUPSP-APPEND) on 
; (DUPSP (BINARY-APPEND (REV #) (CONS # #))):
; 1 ACL2 >:eval

; 1x (:REWRITE DUPSP-APPEND) failed because :HYP 1 rewrote to 
; (NOT (MEMBER (CAR X) (REV #))).

; Note that the report above shows that hypothesis 1 of the rule
; did not rewrite to T but instead rewrote to an expression
; involving (member ... (rev ...)).  Thus, we're led to the
; same conclusion that Thinking produced.  To get out of the
; interactive break we type:

; 1 ACL2 >:a!
; Abort to ACL2 top-level

; and then turn off the break rewrite tool since we won't need it
; again right now, with:

; ACL2 !>:brr nil

; In either case, by thinking or using tools, we decide to prove:

(defthm member-rev
  (iff (member e (rev x)) 
       (member e x)))

; which succeeds.  Now when we try to prove dups-rev, it succeeds.

(defthm dupsp-rev
  (equal (dupsp (rev x))
         (dupsp x)))

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