; Below, after defining our usual memb, ap, and rev, I define two ways of
; removing duplicates from a list. The first way is called CMP (for
; ``compress''). Operationally, it scans the list left-to-right and collects
; an element if that element is not a member of the rest of the list. The
; second way is called CMP1 and it takes an additional argument used as an
; accumulator. CMP1 puts each element of its first argument into the
; accumulator unless it is already in the accumulator.
; Both remove all duplicates, but they return lists that may be in
; different orders, as illustrated by this example:
#|
ACL2 >(let ((x '(1 2 3 4 1 4 2 3 3 3 5)))
(list (cmp1 x nil)
(cmp x)))
((5 4 3 2 1)
(1 4 2 3 5))
|#
; This file contains two challenges:
; Challenge 1: Define the notion of ``duplicate-free''
; and prove that both (cmp x) and (cmp1 x nil) are duplicate-free.
; Challenge 2: State and prove the relationship between (cmp1 x nil) and (cmp x).
; -----------------------------------------------------------------
; Definitions
(in-package "ACL2")
(defun memb (e x)
(if (endp x)
nil
(if (equal e (car x))
t
(memb e (cdr x)))))
(defun ap (x y)
(if (endp x)
y
(cons (car x)
(ap (cdr x) y))))
(defun rev (x)
(if (endp x)
nil
(ap (rev (cdr x))
(list (car x)))))
(defun cmp (x)
(cond ((endp x) nil)
((memb (car x) (cdr x))
(cmp (cdr x)))
(t (cons (car x) (cmp (cdr x))))))
(defun cmp1 (x a)
(cond ((endp x) a)
(t (cmp1 (cdr x) (if (memb (car x) a) a (cons (car x) a))))))
; -----------------------------------------------------------------
; Challenge 1: As a warm up exercise, define the notion of ``duplicate-free''
; and prove that both (cmp x) and (cmp1 x nil) are duplicate-free.
;
; -----------------------------------------------------------------
; Challenge 2: State and prove the relationship between (cmp1 x nil) and (cmp x).
;