#|
CSU290 Homework 6 - Fall 2008
You may work individually or in pairs on this assignment:

Student name 1:  TODO: PUT ONE NAME HERE
Student name 2:  PUT OTHER NAME HERE if you have a partner

This and all remaining homeworks using ACL2s should be completed in
*** Intermediate session mode. ***

You should turn in a .lisp file (this one!) for which all the forms are
accepted by ACL2; thus, please comment out any parts you haven't completed
by turn-in time.

In fact, this is divided into sections, and each section can be completely
independently of the previous sections by commenting them out.
|#


; Some definitions used in this homework:
(defun app (x y)
  (if (endp x)
    y
    (cons (car x) (app (cdr x) y))))

(defun rev (x)
  (if (endp x)
    nil
    (app (rev (cdr x))
         (cons (car x) nil))))

(defun mem (e l)
  (if (endp l)
    nil
    (if (equal e (car l))
      t
      (mem e (cdr l)))))


; Part A:  Find the lemmas.  Some of the following theorems will require other
; theorems (lemmas) to be proven first for ACL2 to prove them automatically.
; You should add DEFTHM events with a reasonable name and formulas that are as
; general as seems possible such that the given theorems are proven by ACL2.

;----------------------------------------------------------------------|#
; Section A1
;#| <- Remove semicolon at beginning to comment out this section. 


(defthm rev--integer-listp   ; DO NOT MODIFY!
  (implies (integer-listp x)
           (integer-listp (rev x))))


;----------------------------------------------------------------------|#
; Section A2
;#| <- Remove semicolon at beginning to comment out this section. 


(defthm len--rev          ; DO NOT MODIFY!
  (equal (len (rev x))
         (len x)))


;----------------------------------------------------------------------|#
; Section A3
;#| <- Remove semicolon at beginning to comment out this section. 


(defthm rev--true-listp   ; DO NOT MODIFY!
  (true-listp (rev x)))

(defthm app--nil          ; DO NOT MODIFY!
  (implies (true-listp x)
           (equal (app x nil)
                  x)))

(defthm rev--app          ; DO NOT MODIFY!
  (equal (rev (app x y))
         (app (rev y) (rev x))))

(defthm rev--rev          ; DO NOT MODIFY!
  (implies (true-listp x)
           (equal (rev (rev x))
                  x)))


;----------------------------------------------------------------------|#
; Section A4
;#| <- Remove semicolon at beginning to comment out this section. 


(defthm mem--rev          ; DO NOT MODIFY
  (equal (mem e (rev x))
         (mem e x)))


;----------------------------------------------------------------------|#
; Part B:  Generalization.  Follow the instructions below:
;
;#| <- Remove semicolon at beginning to comment out this section. 


; MAKEL-AC is an accumulator function for building lists with one value
; repeated some number of times:

(defun makel-ac (n val ac)
  (if (zp n)
    ac
    (makel-ac (- n 1) val (cons val ac))))

; We can define a more convenient front-end to that function: 

(defun makel (n val)
  (makel-ac n val nil))

; So that one creates lists with repeated elements:

(check= (makel 5 t) '(t t t t t))
(check= (makel 3 2) '(2 2 2))
(check= (makel 0 42) '())

; Let us define the same functionality in a more traditional way:

(defun makel-logic (n val)
  (if (zp n)
    nil
    (cons val (makel-logic (- n 1) val))))

; Now we want prove that makel and makel-logic are equivalent.  Theorem
; MAKEL=MAKEL-LOGIC (at the bottom) fails to prove because it is not general
; enough for the induction to work out.  Prove a generalization first so that
; ACL2 can prove this.  However, you will need this lemma to prove the
; generalization:

(defthm makel-ac=makel-logic--lemma
  (equal (app (makel-logic n val)
              (cons val l))
         (cons val
               (app (makel-logic n val)
                    l))))

; PROBLEM:  Find and prove the generalization of MAKEL=MAKEL-LOGIC that
; allows it to be proven automatically.  (Write a new DEFTHM here.)


(defthm makel=makel-logic    ; DO NOT MODIFY
  (equal (makel n val)
         (makel-logic n val)))

;----------------------------------------------------------------------|#