#|
Lab 10

In this lab we will define set intersection, a function that takes two
true-lists and returns a list of elements common to both lists,
without duplicates. We will define a tail-recursive function and we
will prove that the functions are equivalent, using the recipe for
reasoning about accumulator-based functions.

First, a review of some definitions and theorems we know.

|#

(definec aapp (x :tl y :tl) :tl
  (if (endp x)
      y
    (cons (car x) (aapp (cdr x) y))))

(definec rrev (x :tl) :tl
  (if (endp x)
      x
    (aapp (rrev (cdr x)) (list (car x)))))

(definec revt (x :tl acc :tl) :tl
  (if (endp x)
      acc
    (revt (cdr x) (cons (car x) acc))))

(definec rev* (x :tl) :tl
  (revt x nil))

(definec in (a :all X :tl) :bool
  (and (consp X)
       (or (equal a (car X))
           (in a (cdr X)))))

(definec del-all (a :all X :tl) :tl
  (cond ((endp X) X)
        ((equal a (car X))
         (del-all a (cdr X)))
        (t (cons (car X) (del-all a (cdr X))))))

(definec nodups (x :tl) :bool
  (or (endp (cdr x))
      (and (not (in (car x) (cdr x)))
           (nodups (cdr x)))))

(defthm aapp-associative
  (implies (and (tlp x) (tlp y) (tlp z))
           (equal (aapp (aapp x y) z)
                  (aapp x (aapp y z)))))

(defthm aapp-nil
  (implies (tlp x)
           (equal (aapp x nil)
                  x)))

(defthm rrev-over-aapp
  (implies (and (tlp x) (tlp y))
           (equal (rrev (aapp x y))
                  (aapp (rrev y) (rrev x)))))

(defthm rrev-rrev
  (implies (tlp x) 
           (equal (rrev (rrev x))
                  x)))

(defthm revt-rrev
  (implies (and (tlp x) (tlp acc))
           (equal (revt x acc)
                  (aapp (rrev x) acc))))

(defthm rev*-rrev
  (implies (tlp x)
           (equal (rev* x) (rrev x))))

; There is no reason for ACL2s to use the definition of rev* anymore.
(in-theory (disable rev*-definition-rule))

#|

Defining intersect using the recipe.

Part 1: Defining functions

1. Start with a function f. (intersect)

|#

(definec intersect (x :tl y :tl) :tl
  (cond ((endp x) nil)
        ((in (car x) y)
         (cons (car x)
               (intersect (del-all (car x) (cdr x))
                          (del-all (car x) y))))
        (t (intersect (cdr x) y))))

; Q1. What is a measure for intersect?
;     Make sure you can do the full termination proof.
;     Anything interesting?
;     We will only discuss this at a high-level in lab.
;     But, do the complete proof on your own. This is a good practice
;     problem. 


; Step 2 of Part 1:
;
; Define ft, a tail-recursive version of f with an accumulator. (intersectt)

(definec intersectt (x :tl y :tl acc :tl) :tl
  (cond ((endp x) acc)
        ((in (car x) y)
         (intersectt (del-all (car x) (cdr x))
                     (del-all (car x) y)
                     (cons (car x) acc)))
        (t (intersectt (cdr x) y acc))))

; Q2. What is a measure for intersectt?
;     Make sure you can do the full termination proof.
;     Anything interesting?
;     We will only discuss this at a high-level in lab.
;     But, do the complete proof on your own. This is a good practice
;     problem. 

;

; Step 3 of Part 1:
;
; Define f*, a non-recursive function that calls ft and is logically
; equivalent to f, i.e., this is a theorem (intersect*)
;
; hyps ⇒ (f* ...) = (f ...)

; Q3: define intersect* so that the phi1 holds and make sure it runs
; in linear time.
(definec intersect* (x :tl y :tl) :tl
  (... (intersectt x y ...) ...))

; phi1:
(implies (and (tlp x) (tlp y))
         (equal (intersect* x y)
                (intersect x y)))

; Q4: prove phi1 (use the recipe!)


; Extra problem (not covered in lab)
; Q5: prove phi2 (use professional method)
; phi2: 

(implies (and (tlp x) (tlp y))
         (nodups (intersect* x y)))