; CSU290 Homework 4 - Fall 2008
; You must work in pairs on this assignment:
;
; Student name 1:  TODO: PUT ONE NAME HERE
; Student name 2:  TODO: PUT OTHER NAME HERE
;
; 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 text file
; (.txt or .lisp is OK.  .doc or .docx or .rtf is NOT)



; Given the following axioms:

; Consp-nil
(equal (consp nil)
       nil)

; Consp-cons
(equal (consp (cons a b))
       t)

; Car-cons
(equal (car (cons a b))
       a)

; Cdr-cons
(equal (cdr (cons a b))
       b)

; If-true
(implies x
         (equal (if x y z)
                y))

; If-false
(implies (not x)
         (equal (if x y z)
                z))

; Definition of true-listp
(equal (true-listp x)
       (if (endp x)
         (equal x nil)
         (true-listp (cdr x))))

; Definition of app
(equal (app x y)
       (if (endp x)
         y
         (cons (car x) (app (cdr x) y))))

; Definition of rev
(equal (rev x)
       (if (endp x)
         nil
         (app (rev (cdr x))
              (cons (car x) nil))))

; END of given axioms (but you may need other ACL2 built-in axioms)



; 1. Prove
(implies (and (endp x)
              (true-listp y))
         (true-listp (app x y)))


; 2. Prove
(implies (and (consp x)
              (true-listp (app (cdr x) y)))
         (true-listp (app x y)))





; Now for the rest of the assignment, you may assume without proof
; the following theorem/lemma:  (call it True-listp-app)
(implies (true-listp y)
         (true-listp (app x y)))



; 3. Prove
(implies (endp x)
         (true-listp (rev x)))


; 4. Prove
(implies (consp x)
         (true-listp (rev x)))


; 5. Use the previous two results to prove:  (call it True-listp-rev)
(true-listp (rev x))




; Now consider also having this definition:

; REV-APPEND: true-list true-list -> true-list
; returns a list with the elements of the first list in reverse order,
; followed by the elements of the second list.
(defun rev-append (x y)
  (if (endp x)
    y
    (rev-append (cdr x) (cons (car x) y))))

; which gives us the axiom
(equal (rev-append x y)
       (if (endp x)
         y
         (rev-append (cdr x) (cons (car x) y))))

; Also, you may assume without proof a result proved in class:
; (call it App-assoc)
(equal (app (app x y) z)
       (app x (app y z)))



; 6. Prove:
(implies (endp x)
         (equal (rev-append x y)
                (app (rev x) y)))



; 7. Prove:
(implies (and (consp x)
              (equal (app (rev (cdr x)) (cons (car x) y))
                     (rev-append (cdr x) (cons (car x) y))))
         (equal (rev-append x y)
                (app (rev x) y)))


; Now for the rest of the assignment, you may assume without proof
; the following theorem/lemma:  (call it Rev-append=App-rev)
(equal (rev-append x y)
       (app (rev x) y))


; 8. Prove: (Hint: Use case analysis on x, much like how you were guided in
; doing to prove (true-listp (rev x)).)
(equal (rev-append x nil)
       (rev x))