### INTRODUCTORY-CHALLENGE-PROBLEM-4

challenge problem 4 for the new user of ACL2
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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.

**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.