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.
