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:


; 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:


; 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.