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.