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.