;$ACL2s-SMode$;Intermediate

 CS2800 Homework 6 - Fall 2010
; You must work in pairs on this assignment
;
; Student name 1:  TODO: PUT ONE NAME HERE
; Student name 2:  TODO: PUT OTHER NAME HERE
;
; The first part of this assignment will NOT involve ACL2s, though you may use the .lisp editor
; in ACL2s to help with code/formula formatting.  You must construct proofs
; by hand in the style presented in class, and turn them in in a lisp file
; but comment out portions of Part 1 (using #| and |#) that show your 
;hand-typed proofs, if you have attempted Part 2 and want us to grade it.
;If you want you can submit actual paper-pencil proofs
;to me, which I will grade myself, but you must write them neatly and you
;*must* follow the proof format that I show and use all the time.



; Given these definitions:

; in: all true-list -> boolean
(defun in (x A)
  "Returns boolean indicating whether the first argument is a
   inber  of the second argument list."
  (if (endp A)
      nil
    (if (= x (car A))
      t
      (in x (cdr A)))))
;subset: true-list true-list -> boolean
(defun subset (A B)
 "All members of first set are in the second argument(set)"
 (if (endp A)
     t
   (and (in (car A) B)
        (subset (cdr A) B))))


; UN: true-list true-list -> true-list
(defun un (A B)
  "Set-theoretic UNION. Returns a list with all the
   elements of both the argument lists. "
  (if (endp A)
      B
    (cons (car A)
          (un (cdr A)
              B))))

;PART 1(100 marks):
;Lets try to make in ACL2 the theory of Sets. We will use the
;above definitions to prove simple theorems of set theory.
;Once you prove a theorem, you can use it as a lemma in the later proofs.
;Any new lemmas you come up have to be proven by you.

;#|

;Assume this lemma union-def(if you want, you can prove it)
(iff (or (in x A) (in x B)) (in x (un A B)))
;Proof Hint: You can break it into 2 proofs using prop deduction, use
;tautology a <=> b = (a => b) /\ (b => a)

; 1.(10 pts) Prove this (using induction) and call it lemma union-other
(implies (not (in x B))
         (equal (in x (un A B))
                (in x A)))

; Assume this lemma, call it un-cons-other
(implies (not (= x y))
         (= (in x (un a (cons y b)))
            (in x (un a b))))

;2. (10 pts) Prove this (using induction) and call it lemma union-commutative
;    (Hint: Use lemmas!  (Here and for the rest...))
(equal (in x (un a b))
       (in x (un b a)))

;3. (10 pts) Prove this (using induction) and call it lemma in-union1
(implies (in x a)
         (in x (un a b)))

;4. (10 pts) Prove this--without induction, just using lemmas--and call it in-union2
(implies (in x b)
         (in x (un a b)))

;Practice Questions
;Prove the following(and in the process come up with general
; lemmas and prove them):

;P1 (union-subset1)
(subset X (un X Y)) ;Hint: Use lemma from previous Hwk

;P2 (union-subset2)
(subset X (un Y X)) ;Hint: Use theorem(Part Y) from previous hwk

;P3 (subset-is-transitive)
(implies (and (subset A B)
              (subset B C))
         (subset A C);hint: Choose to induct on (subset A B) 

;P4 (cummuted-union-subset)
(subset (un X Y) (un Y X));hint, use above lemmas and come up with one more.


;Now consider this accumulator style (tail-recursive) definition:
; un*-acc: true-list true-list -> true-list
(defun un*-acc (a b)
 "Set-theoretic UNION using tail recursion. Returns a list with all the
  elements of both the argument lists."
  (if (endp a)
    b
    (un*-acc (cdr a)
             (cons (car a)
                   b))))

;5 (20 pts) Prove the following, but note that only one induction scheme would work,
;if you dont use the right induction scheme, you will get stuck in which
;case try the other choices:
(implies (in x (un*-acc a b))
         (in x (un a b)))

;Practice Question(Hard, dont try unless you do the rest):
;P5 (un-acc*-is-set-equal-to-un)
(and (subset (un*-acc a b) (un a b))
     (subset (un a b) (un*-acc a b)))


;Consider the factorial function:
(defun fact (n)
  "compute factorial of n"
  (if (zp n)
      1
    (* n (fact (- n 1)))))

;here is the accumulator style version of fact
(defun fact*-acc(n acc)
 "accumulate the partial answer(fact) in acc and return it"
 (if (zp n)
     acc
   (fact*-acc (- n 1) (* n acc))))
(defun fact* (n)
 "compute factorial of n using a acc-style helper function"
  (fact*-acc n 1))

;6.(15 pts) Prove that the faster accumulator-style factorial gives the
;same answer as our original fact
(equal (fact* n) (fact n))

;Consider the scale function:
;; scale: true-list Int -> true-list
(defun scale (l n)
  "adds n to all elements of list l"
  (if (endp l)
    nil
    (cons (+ n (car l)) (scale (cdr l) n))))

;; Heres the accumulator-style(Tail recursive version)scale
;; scale*-acc: true-list Int true-list -> true-list
(defun scale*-acc (l n acc)
  (if (endp l)
    (rev acc)
    (scale*-acc (cdr l) n (cons (+ n (car l)) acc))))

;; scale*: true-list Int -> true-list
(defun scale* (l n)
  "Tail-recursive version of scale"
  (scale*-acc l n nil))
;7.(15 pts) Prove the faster accumulator-style scale gives the
; same answer as the original (slower) scale:
(equal (scale* L n) (scale L n)) 

;8(5pts) What inducton scheme does scale and scale*-acc give rise to?
;9(5pts) Apply the induction scheme of scale to 
(tlp (scale l n))
;to generate the proof obligations(base case and induction step). 
;Similarily Apply the 
;induction scheme of scale*-acc to 
(= (scale*-acc (app l1 l2) n l3)
   (app (app (rev l3) (scale l1 n))
        (scale l2 n)))

                                     


;|# 


#|
This Part is optional for this homework, and not required, but since
I would like you to start playing with ACL2s, I am giving out this.
But if you submit this, you will get extra points.
Part 2(50 extra credit marks): Prove theorems using ACL2s.
Make sure that your session mode is "Intermediate" and that the line
mode is "enforced" for this homework. You have to modify the remaining file and
submit the modified file as per the instructions for homework
submissions. Make sure that ACL2s accepts every event in your
submission.

We start with some definitions

|#

;; tlp : All -> Bool
(defun tlp (x)
"Recognize true lists"
  (if (endp x)
    (equal x nil)
    (tlp (cdr x))))

;; app : tlp x tlp -> tlp
(defun app (x y)
  "append two lists"
  (if (endp x)
    y
    (cons (car x) (app (cdr x) y))))

;; rev : tlp -> tlp
(defun rev (x)
  "Reverse a list"
  (if (endp x)
      nil
    (app (rev (cdr x)) (list (car x)))))

;; rev*-acc : tlp x tlp -> tlp
;; Tail-recursive version of rev (auxiliary function)
(defun rev*-acc (x acc)
  (if (endp x)
    acc
    (rev*-acc (cdr x) (cons (car x) acc))))

;; rev*: tlp -> tlp
(defun rev* (x)
  "Tail-recursive version of rev"
  (rev*-acc x nil))

;; scale: LoInt Int -> LoInt
(defun scale (l n)
  "adds n to all elements of list l"
  (if (endp l)
    nil
    (cons (+ n (car l)) (scale (cdr l) n))))

;; scale*-acc: LoInt Int LoInt -> LoInt
;; Tail recursive version of scale (auxiliary function)
(defun scale*-acc (l n acc)
  (if (endp l)
    (rev acc)
    (scale*-acc (cdr l) n (cons (+ n (car l)) acc))))

;; scale*: LoInt Int -> LoInt
(defun scale* (l n)
  "Tail-recursive version of scale"
  (scale*-acc l n nil))

(defun fact (n)
  "compute factorial of n"
  (if (zp n)
      1
    (* n (fact (- n 1)))))

;Consider the accumulator style version of fact
(defun fact*-acc(n acc)
 "accumulate the partial answer(fact) in acc and return it"
 (if (zp n)
     acc
   (fact*-acc (- n 1) (* n acc))))

(defun fact* (n)
 "compute factorial of n using a acc-style helper function"
  (fact*-acc n 1))

;; remove-all: All tlp -> tlp
(defun remove-all (a X)
  "removes all occurrences of a from X"
  (cond ((endp X) nil)
        ((equal a (car X)) (remove-all a (cdr X)))
        (t (cons (car X) (remove-all a (cdr X))))))

;; remove-once: All tlp -> tlp
(defun remove-once (a X)
  "removes the first occurrence of a from X"
  (cond ((endp X) nil)
        ((equal a (car X)) (cdr X))
        (t (cons (car X) (remove-once a (cdr X))))))

;; remove-multiple: tlp tlp -> tlp
(defun remove-multiple (x y)
  "removes all elements in x from y"
  (if (endp x)
    y
    (remove-multiple (cdr x) (remove-all (car x) y))))

;; perm: tlp tlp -> boolean
(defun perm (x y)
  "returns true if x is a permutation of y, i.e. they contain the same
elements in a different order (same number of occurrences for each)"
  (if (endp x)
      (endp y)
    (and (in (car x) y)
         (perm (cdr x) (remove-once (car x) y)))))

#|

All of the following conjectures are theorems. You have to figure out
how to steer ACL2s so that it discovers a proof.

In this homework, we use ACL2s in "intermediate" mode which provides
more automation compared to "recursion and induction" you used in the
lab assignment. In order to
complete it, you will have to prove lemmas (intermediate
theorems). You may use intermediate theorems we have already proved in
class and/or previous homeworks. How do you know which intermediate
theorems are needed? Look at the checkpoint ACL2s prints and see what
lemma it is missing. That is: what lemma would allow ACL2 to make
progress? Use the proof tree view! (See the ACL2s documentation if you
don't know what the proof tree view is.) I will also upload some
advice on how to come up with lemmas while looking at the ACL2 proof
tree view(checkpoints).

|#

#|

Part A(6pts): Proofs about tail-recursive functions

Recall that in order to prove that a tail-recursive function is
related to the regular recursive version, you have to come up with the
appropriate generalization and provide it as a lemma.

|#

(defthm rev*-rev
  (equal (rev* a)
         (rev a)))

(defthm scale*-scale
  (equal (scale* l n)
         (scale l n)))

(defthm fact*-fact
  (equal (fact* n)
         (fact n)))

#|

Part B(24 pts): More Proofs

Prove(Submit in ACL2) the following theorems. In case you cannot prove a theorem but
need it to proceed, replace "defthm" with "defaxiom" to provide it as
an axiom that ACL2s can use.
Hints: You might need to prove as lemmas that perm is reflexive and
transitive. Also notice that to prove anything about a function, you
need to prove a similar property about the functions it uses in its body.
|#
;1 (3pts)
(defthm contains-perm
  (implies (and (in a X)
                (perm X Y))
           (in a Y)))
;2 (6pts)
(defthm remove-all-element-remove-multiple
  (perm (remove-all a (remove-multiple X Y))
        (remove-multiple (cons a X) Y)))
;3 (3pts)
(defthm perm-rem-once
  (implies (perm X Y)
           (perm (remove-once a X)
                 (remove-once a Y))))

;(EXTRA PROBLEM added for PRACTICE)
(defthm remove-all-perm
  (implies (perm X Y)
           (perm (remove-all a X)
                 (remove-all a Y))))
;4 (6pts)
(defthm perm-rev
  (perm (rev x) x))

;5 (6pts)
(defthm perm-app
  (perm (app x y)
        (app y x)))

;6 (20pts)
;Prove all the practice questions of Part 1 in ACL2s.