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.