|
|
|---|
|
|
|
|---|
Answer to challenge problem 4 for the new user of ACL2
This topic solves a challenge problem presented elsewhere; see introductory-challenge-problem-4. 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
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
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 precedes the ; last occurrence of 3 in '(2 4 1 3 1 2 3 4)), then the collected 2 precedes ; 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 precede 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 the rewrite rule ; (iff (subsetp a (append b (cons e c))) ; (subsetp a (cons e (append b c)))) ; in order to rewrite the first call of SUBSETP shown in the key term above ; to the second call. ; 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 and ; 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 additionally 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.