		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Introductory-challenge-problem-4

Challenge problem 4 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from scratch or executing :ubt! 1.

This problem is much more open ended than the preceding ones. The challenge is to define a function that collects exactly one copy of each element of a list and to prove that it returns a subset of the list with no duplications.

(Is this all that one might want to prove? It is a good idea to think about that question, for any application; an answer for this example is at the end of this topic.)

Hint: We recommend that you read this hint to align your function names with our solution, to make comparisons easier. Our answer is shown in see introductory-challenge-problem-4-answer. In that page you'll see a definition of a function collect-once and the proofs of two theorems:

(defthm main-theorem-1-about-collect-once
  (subsetp (collect-once x) x))

(defthm main-theorem-2-about-collect-once
  (not (dupsp (collect-once x))))

The function dupsp is as defined in see introductory-challenge-problem-3. This is quite easy.

Then, we define a tail-recursive version of the method based on the pseudo-code:

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 formalize this with the function while-loop-version, where (while-loop-version x nil) is the ``semantics'' of the code above. I.e., the function while-loop-version captures the while loop in the pseudo-code above and returns the final value of a, and it should be invoked with the initial value of a being nil.

We prove (while-loop-version x nil) returns a subset of x that contains no duplications. Furthermore, we do it two ways: first ``indirectly'' by relating while-loop-version to collect-once, and second (``directly'') without using collect-once. Both of these proofs are much harder than the collect-once approach, involving about a dozen lemmas each.

Compare your solutions to ours at see introductory-challenge-problem-4-answer.

Then, use your browser's Back Button to return to introductory-challenges.

We conclude this topic by returning to the question posed earlier above: Is this all that one might want to prove? Notice that we didn't prove that every element of the given list is indeed an element of the returned list, which could be formalized as follows.

(thm
  (subsetp x (collect-once x)))