Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
This answer is in the form of a script sufficient to lead ACL2 to a proof, with a brief prologue.
We wish to collect one copy of each element in x. We'll actually define the method two ways, primitive recursively and tail-recursively, the latter method being analogous to the program:
a = nil;
while (x not empty) {
a = if (member (car x) a) then a else (cons (car x) a);
x = (cdr x);
}
return a;
We'll prove the two ``equivalent'' and we'll prove that they return a subset
of x that contains no duplications.
This page is organized into four sections. (A) We will start by proving that
the primitive recursive version correct: it returns a subset of its argument
that is duplication free. This will be straightforward. (B) Then we'll
define the while-loop version and we will prove it ``equivalent'' to the
primitive recursive version. This will be challenging primarily because the
two methods collect their answers in different orders; even stating the
relationship between the two is interesting. Proving it will involve a few
lemmas. But once we prove their ``equivalence'' the correctness of the
while-loop version will be straightforward from the correctness of the
primitive recursive version. (C) We will disable the rules we prove about
the while-loop version and prove it correct directly, without exploiting the
primitive recursive version. This requires leading the theorem prover more
carefully because reasoning about tail-recursive functions that accumulate
results is sometimes delicate. (D) Lessons learned -- a narrative that
summarizes what we learn from these examples.
We follow The Method, which, recall, involves us in recursive attempts to prove lemmas. We use a notation to indicate our sequence of proof attempts. Here is an example (although in actual use we print things across multiple lines). The number in bracket indicates our ``stack depth''. The ``key term'' is some term from a Key Checkpoint in the failed proof which is responsible for our subsequent action. Sometimes instead of a Key Term we just give an English explanation of what we're thinking.
[0] (defthm main ...) Failed! Key Term: ... [1] (defthm lemma-1 ...) Succeeded! [0] (defthm main ...) Failed! Key Term: ... [1] (defthm lemma-2 ...) Failed! Key Term: ... [2] (defthm lemma-2a ...) Succeeded! [2] (defthm lemma-2b ...) Succeeded! [1] (defthm lemma-2 ...) Succeeded! [0] (defthm main ...) Succeeded!
The rest of this page is just a re-playable script.
; ----------------------------------------------------------------- ; Section A: The Primitive Recursive Version and Its Correctness; The property of having duplications is defined as:
(defun dupsp (x) (if (endp x) nil (if (member (car x) (cdr x)) t (dupsp (cdr x)))))
; The primitive recursive method of collecting one copy of each element is:
(defun collect-once (x) (if (endp x) nil (if (member (car x) (cdr x)) (collect-once (cdr x)) (cons (car x) (collect-once (cdr x))))))
; [0] (defthm main-theorem-1-about-collect-once (subsetp (collect-once x) x)) ; Succeeded!
; [0] ; (defthm main-theorem-2-about-collect-once ; (not (dupsp (collect-once x)))) ; Failed! ; Key Term: (MEMBER (CAR X) (COLLECT-ONCE (CDR X)))
; [1] (defthm member-collect-once (iff (member e (collect-once a)) (member e a))) ; Succeeded!
; [0] (defthm main-theorem-2-about-collect-once (not (dupsp (collect-once x)))) ; Succeeded!
; That was really easy!
;----------------------------------------------------------------- ; Section B: The While-Loop Version and Its Correctness -- ; presented in two parts: its equivalence to the primitive recursive ; version and then its correctness proved via that equivalence
; The tail-recursive, or while-loop version, is defined as follows. The ; function below is the loop itself and it ought to be called with a = nil to ; implement the initialization of a in the pseudo-code above.
(defun while-loop-version (x a) (if (endp x) a (while-loop-version (cdr x) (if (member (car x) a) a (cons (car x) a)))))
; We wish to prove that the two are equivalent. But they are actually ; very different. For example,
; (collect-once '(2 4 1 3 1 2 3 4)) = (1 2 3 4) ; (while-loop-version '(2 4 1 3 1 2 3 4) nil) = (3 1 4 2)
; Things get a little more complicated if a is non-nil: ; (while-loop-version '(2 4 1 3 1 2 3 4) '(2 2 4 4)) = (3 1 2 2 4 4)
; Several observations help explain what is happening. (1) Collect-once ; collects the last occurrence of each element, in the order of their last ; occurrences. So, for example, since the last occurrence of 2 preceeds the ; last occurrence of 3 in '(2 4 1 3 1 2 3 4)), then the collected 2 preceeds ; the collected 3 in the answer. But while-loop-version collects the first ; occurrence of each element, in the reverse order of that occurrence. So it ; adds 2 to its accumulator first and adds 3 last, making 3 preceed 2 in the ; answer.
; (2) The while-loop-version does not collect anything already in a and indeed ; just adds stuff to the front of a, returning everything initially in a plus ; one occurrence of everything in x not in a.
; To state the relationship that holds between these two we have to define two ; other functions.
; This is our familiar list reverse function... (defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))
; And this function ``removes'' from x all the elements in y, i.e., copies x ; while dropping the elements of y.
(defun list-minus (x y) (if (endp x) nil (if (member (car x) y) (list-minus (cdr x) y) (cons (car x) (list-minus (cdr x) y)))))
; The specific equivalence we're really interested in is ; (equal (while-loop-version x nil) ; (collect-once (rev x)))
; But we will not be able to prove that by induction because it has the ; constant nil where we need a variable, a, in order to admit an appropriate ; inductive instance. So we will attack the most general problem. What is ; (while-loop-version x a) equal to, in terms of collect-once?
; The most general relationship between the two collection functions is:
; (equal (while-loop-version x a) ; (append (collect-once (list-minus (rev x) a)) a))
; This formula bears thinking about! If you're like us, you won't believe it ; until it is proved!
; [0] ; (defthm general-equivalence ; (equal (while-loop-version x a) ; (append (collect-once (list-minus (rev x) a)) a))) ; Failed! ; Key term in checkpoint: ; (LIST-MINUS (APPEND (REV (CDR X)) (LIST (CAR X))) A)
; [1] (defthm list-minus-append (equal (list-minus (append a b) c) (append (list-minus a c) (list-minus b c)))) ; Succeeded!
; [0] ; (defthm general-equivalence ; (equal (while-loop-version x a) ; (append (collect-once (list-minus (rev x) a)) a))) ; Failed! ; Key term in checkpoint: ; (COLLECT-ONCE (APPEND (LIST-MINUS (REV (CDR X)) A) (LIST (CAR X))))
; [1] ; (defthm collect-once-append ; (equal (collect-once (append a b)) ; (append (list-minus (collect-once a) b) ; (collect-once b)))) ; Failed! ; Key term: ; (MEMBER (CAR A) (APPEND (CDR A) B))
; [2] (defthm member-append (iff (member e (append a b)) (or (member e a) (member e b)))) ; Succeeded!
; [1] (defthm collect-once-append (equal (collect-once (append a b)) (append (list-minus (collect-once a) b) (collect-once b)))) ; Succeeded!
; [0] ; (defthm general-equivalence ; (equal (while-loop-version x a) ; (append (collect-once (list-minus (rev x) a)) a))) ; Failed! ; Key term: ; (APPEND (APPEND (LIST-MINUS (COLLECT-ONCE (LIST-MINUS (REV (CDR X)) A))
; [1] (defthm assoc-append (equal (append (append a b) c) (append a (append b c)))) ; Succeeded!
; [0] ; (defthm general-equivalence ; (equal (while-loop-version x a) ; (append (collect-once (list-minus (rev x) a)) a))) ; Failed! ; Key term: ; (LIST-MINUS (COLLECT-ONCE (LIST-MINUS (REV (CDR X)) A)) ...)
; This key term makes us think of the lemma to move the LIST-MINUS inside the ; COLLECT-ONCE. But when that's done, we will have two LIST-MINUS terms ; nestled together and we will want to combine them into one. Call these two ; lemmas (a) and (b).
; [1] (a) ; (defthm list-minus-collect-once ; (equal (list-minus (collect-once x) a) ; (collect-once (list-minus x a)))) ; Failed! ; Key term: ; (MEMBER (CAR X) (LIST-MINUS (CDR X) A))
; [2] (A pretty fact) (defthm member-list-minus (iff (member e (list-minus x a)) (and (member e x) (not (member e a))))) ; Succeeded!
; [1] (a) (defthm list-minus-collect-once (equal (list-minus (collect-once x) a) (collect-once (list-minus x a)))) ; Succeeded!
; [1] (b) (defthm list-minus-list-minus (equal (list-minus (list-minus x a) b) (list-minus x (append b a)))) ; Succeeded!
; [0] (defthm general-equivalence (equal (while-loop-version x a) (append (collect-once (list-minus (rev x) a)) a))) ; Succeeded!
; That completes the proof of the ``equivalence'' of the two methods.
; Now we prove (1) that the result of while-loop-version is a subset, and (2) ; that it contains no duplications. We prove the two conjuncts separately.
; [0] (defthm main-theorem-1-about-while-loop (subsetp (while-loop-version x nil) x)) ; Succeeded!
; But the theorem prover works harder to do the proof above than one might have ; expected because it doesn't turn into an instance of ; main-theorem-1-about-collect-once because of the presence of the rev term. ; However, we're content that ACL2 managed to do the proof on its own.
; [0] (defthm main-theorem-2-about-while-loop (not (dupsp (while-loop-version x nil))))
; So we see that the proof of correctness of while-loop-version isn't hard, ; after we establish the relationship with the primitive recursive version. ; But finding and proving the relationship is fairly challenging.
; ----------------------------------------------------------------- ; Section C: A Direct Proof of the Correctness of the While-Loop Version
; Some would consider the proof in Section B ``indirect'' because we first showed ; how while-loop-version could be expressed as a collect-once and then proved ; our main theorems about while-loop-version, which means those main proofs ; were conducted in terms of collect-once, not while-loop-version.
; It is interesting to compare this proof with the ``direct'' one in which ; we don't use collect-once at all and reason only about while-loop-version.
; So to do that comparison, let's disable all the lemmas we've proved about ; while-loop-version and try to prove the two main theorems above about ; while-loop-version.
(in-theory (disable general-equivalence main-theorem-1-about-while-loop main-theorem-2-about-while-loop))
; [0] ; (defthm main-theorem-1-about-while-loop-redux ; (subsetp (while-loop-version x nil) x)) ; Failed! [Well, the truth is below...]
; We don't even submit this event above because we recognize that it is not ; general enough to permit proof by induction. We need to deal with the nil in ; the second argument of while-loop-version. Experience with induction tells ; us this should be a variable, so we can assume an appropriate inductive ; instance. Therefore, we adopt this subgoal immediately:
; [1] ; (defthm main-lemma-1-about-while-loop-version ; (subsetp (while-loop-version x a) (append x a))) ; Failed! ; Key Term: Does the wrong induction.
; [1] ; (defthm main-lemma-1-about-while-loop-version ; (subsetp (while-loop-version x a) (append x a)) ; :hints (("Goal" :induct (while-loop-version x a)))) ; Failed! Two key terms are suggested ; Key term: (IMPLIES (AND ... (SUBSETP (WHILE-LOOP-VERSION (CDR X) A) (APPEND (CDR X) A))) ; (SUBSETP (WHILE-LOOP-VERSION (CDR X) A) (CONS ... (APPEND (CDR X) A)))) ; Key term: (SUBSETP A A) ; So we'll prove both before trying again. ; [2] (defthm subsetp-cons (implies (subsetp a b) (subsetp a (cons e b)))) ; Succeeded!
; [2] (defthm subsetp-reflexive (subsetp a a)) ; Succeeded!
; [1] ; (defthm main-lemma-1-about-while-loop-version ; (subsetp (while-loop-version x a) (append x a)) ; :hints (("Goal" :induct (while-loop-version x a)))) ; Failed! ; Key Term: ; (IMPLIES (AND ... ; (SUBSETP (WHILE-LOOP-VERSION (CDR X) (CONS (CAR X) A)) ; (APPEND (CDR X) (CONS (CAR X) A)))) ; (SUBSETP (WHILE-LOOP-VERSION (CDR X) (CONS (CAR X) A)) ; (CONS (CAR X) (APPEND (CDR X) A))))
; We'd be done if we could rewrite the ; (APPEND (CDR X) (CONS (CAR X) A)) ; to ; (CONS (CAR X) (APPEND (CDR X) A)) ; These two terms are not equal! But they are ``set-equal'' and this kind of ; rewriting is possible using user-defined equivalences and congruence rules. ; But the new user should not dive into congruences yet. So we will do this ; with ordinary lemmas:
; The plan then is to prove ; (iff (subsetp a (append b (cons e c))) ; (subsetp a (cons e (append b c))))
; Consider the first half of this bi-implication: ; (implies (subsetp a (append b (cons e c))) ; hyp1 ; (subsetp a (cons e (append b c)))) ; concl ; Notice that if we knew ; (subsetp (append b (cons e c)) (cons e (append b c))) ; hyp2 ; then we could use hyp1 and hyp2 together with the transitivity of ; subsetp to get concl.
; The proof in the other direction is comparable but requires the ; (subsetp (cons e (append b c)) (append b (cons e c)))
; Thus, our plan is prove ; (a) transitivity of subsetp ; (b) (subsetp (append b (cons e c)) (cons e (append b c))) ; (c) (subsetp (cons e (append b c)) (append b (cons e c)))
; in order to prove ; (d) (iff (subsetp a (append b (cons e c))) ; (subsetp a (cons e (append b c))))
; [2] (a) (defthm trans-subsetp (implies (and (subsetp a b) (subsetp b c)) (subsetp a c))) ; Succeeded!
; [2] (b) (defthm append-cons-v-cons-append-1 (subsetp (append b (cons e c)) (cons e (append b c)))) ; Succeeded!
; [2] (c) (defthm append-cons-v-cons-append-2 (subsetp (cons e (append b c)) (append b (cons e c)))) ; Succeeded!
; [2] (d) (defthm subsetp-append-cons-cons-append (iff (subsetp a (append b (cons e c))) (subsetp a (cons e (append b c))))) ; Succeeded!
; [1] (defthm main-lemma-1-about-while-loop-version (subsetp (while-loop-version x a) (append x a)) :hints (("Goal" :induct (while-loop-version x a)))) ; Succeeded!
; [0] ; (defthm main-theorem-1-about-while-loop-version ; (subsetp (while-loop-version x nil) x)) ; Failed! [But the truth is below...]
; But we don't submit this because we don't expect it to be proved ; from the main lemma just proved: they don't match! But ; note that if we instantiated the main lemma, replacing a by nil, ; we get:
; (subsetp (while-loop-version x nil) (append x nil))
; and we could simplify the (append x nil) to x in this context, with ; another congruence rule -- if we were using them. So let's prove ; first that we can simplify (append x nil) inside a subsetp:
; [1] (defthm subsetp-append-nil (iff (subsetp x (append y nil)) (subsetp x y))) ; Succeeded!
; and then just tell ACL2 how to use the lemma to get the main theorem. Note ; that we give a hint to instantiate main-lemma-1... but we also disable ; main-lemma-1... because otherwise it will rewrite itself away! Once the ; instance of main-lemma-1... is sitting around as a hypothesis, ; subsetp-append-nil will rewrite the (append x nil) to x for us and finish the ; proof.
; [0] (defthm main-theorem-1-about-while-loop-version (subsetp (while-loop-version x nil) x) :hints (("Goal" :use (:instance main-lemma-1-about-while-loop-version (x x) (a nil)) :in-theory (disable main-lemma-1-about-while-loop-version)))) ; Succeeded!
; Recall that the main-theorem-1... just proved is just half of what we want. ; We also want:
; [0] ; (defthm main-theorem-2-about-while-loop-version ; (not (dupsp (while-loop-version x nil)))) ; Failed! [But the truth is below...]
; But, again, we don't submit that because the nil makes it not general enough for ; induction. Instead we go immediately to:
; [1] (defthm main-lemma-2-about-while-loop-version (implies (not (dupsp a)) (not (dupsp (while-loop-version x a))))) ; Succeeded!
; This time we know our main-lemma-2... will match (there's no (append x nil) ; in there to mess things up) and so we can complete the proof with:
; [0] (defthm main-theorem-2-about-while-loop-version (not (dupsp (while-loop-version x nil)))) ; Succeeded!
;----------------------------------------------------------------- ; Section D: Lessons Learned
; The most obvious lesson is that it is easier to reason about the primitive ; recursive collect-once than about the while-loop-version. Thus, if your only ; need is for a function that collects one occurrence of each element of a list ; and you don't care about the order in which you collect them and you don't ; need it to be very sparing of stack space when it executes, then use the ; primitive recursive definition and don't even think about while loops!
; So why might you be driven to while-loop-version? One possibility is that ; the list you wish to process is very long and the primitive recursive version ; would produce a stack overflow. In ACL2, that would mean the list would have ; to be several thousand long. Is your application really so demanding?
; Another possibility is that you are modeling in Lisp a while loop expressed ; in some other programming language. In that case, the fidelity of your model to ; the artifact being modeled is important and you should use while-loop-version.
; Another possibility is that for some reason order matters and you really are ; interested in collecting the first occurrence rather than the last. Of ; course this is most likely to be relevant in more interesting applications ; where the occurrences are somehow distinguishable.
; If you are forced to deal with the while-loop-version the question is do you ; do an indirect proof as in Section B or a direct proof as in Section C? ; The indirect proof involved 10 theorems and the direct proof involved 11. ; That is not a significant difference.
; But our sense is that the indirect proof is easier to find, once you figure ; out the basic shape of the relation between while-loop-version collect-once. ; In particular, we had to give the theorem prover two hints in the direct ; proof (versus no hints in the indirect proof). One of our hints was about ; what induction to do and the other was about how to use a previously proved ; instance of a lemma involving an accumulator. Furthermore, we had to think ; carefully about the use of the transitivity of subsetp and we had to hack our ; way around rewriting (append a (cons e b)) to (cons e (append a b)) in a ; subsetp-expression.
; Some of these ``set'' problems could have been handled a lot more elegantly by ; defining set-equal as an equivalence relation and proving the congruence ; rules to allow the rewriting of set-equal terms to set-equal terms inside ; certain expressions like subsetp and member. However, that involves a lot of ; overhead in the form of congruence rules showing that set-equality is ; maintained by replacement of set-equals by set-equals in various argument ; positions of the various functions. See :doc congruence. In general, we ; find congruence-based reasoning extremely neat and powerful when the ; appropriate infrastructure has been built up. But because the infrastructure ; is ``heavy'' we tend not to invest in it for small projects.
; In summary, different users might take home different lessons about whether a ; direct or indirect proof is better here. This is in part due to the ; complexity of the functional relationship between collect-once and ; while-loop-version, which additionall involved append, list-minus, and rev. ; Had the relationship been simpler, the indirect proof would have been ; preferred.
; An undeniable lesson, however, is that it is helpful to know both styles of ; proof and to be able to explore both as needed in your applications.
Use your browser's Back Button now to return to introductory-challenge-problem-4.