		Search-engine friendly clone of the ACL2 documentation.
Introduction-to-the-theorem-prover
Introductory-challenge-problem-3-answer

Answer to challenge problem 3 for the new user of ACL2
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.