Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Consider these definitions:
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))We assume you are familiar with such ACL2 built-ins as
(defun nats-below (j) (if (zp j) '(0) (cons j (nats-below (- j 1)))))
true-listp. When we use throw-away names like
MUMbelow we mean to suggest some arbitrary function you shouldn't think about! We're just trying to train your eye to ignore irrelevant things.
Below are some terms that should suggest rewrite rules to you. Imagine that each of these terms occurs in some Key Checkpoint. What rules come to mind? Try to think of the strongest rules you can.
(TRUE-LISTP (APPEND (FOO A) (BAR B)))
Answers: See practice-formulating-strong-rules-1
(TRUE-LISTP (REV (FOO A)))
Answers: See practice-formulating-strong-rules-2
(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))
Answers: See practice-formulating-strong-rules-3
(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))
Answers: See practice-formulating-strong-rules-4
(SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))
Answers: See practice-formulating-strong-rules-5
(MEMBER (FOO A) (NATS-BELOW (BAR B)))
Answers: See practice-formulating-strong-rules-6
We recommend doing all of these little exercises. When you're finished, use your browser's Back Button to return to strong-rewrite-rules.