Challenge problem 4 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from
scratch or executing

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

(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

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

We prove

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)))