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.
; Tryingdupsp-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 useiff instead ofequal since ;member is not a Boolean function. ; Having proved this lemma, we return todupsp-append and succeed: (defthm dupsp-append (implies (not (member e x)) (equal (dupsp (append x (list e))) (dupsp x)))) ; So now we return todups-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 ourdupsp-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. Thedups-append rule has the hypothesis(not ; (member e x)) and after the match with the left-hand side,e ; is(CAR X) andx 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 ; provemember-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.