; *************** END INITIALIZATION FOR INTERMEDIATE MODE **************** ;
;$ACL2s-SMode$;Intermediate
#|
CS2800 Homework 4 - 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

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

You should turn in a .lisp file (this one, but renamed just before
submitting to turnitin as .txt!) for which all the forms are
accepted by ACL2; thus, please delete or comment out any parts you haven't
completed by turn-in time.
|#



; Part A(40pts):  Not theorems   (Rubric: each question 5pts)
; Each of the following propositions is *not* a theorem.  Use CHECK= and LET
; to demonstrate a counterexample for each proposition.
;  This demonstrates each is not a theorem.
;
; Example problem:
;   (or (> x 5)
;       (< x 5))
; solution:
;   (check=
;    (let ((x 5))
;      (or (> x 5)
;          (< x 5)))
;    nil)
;which basically says the above formula(proposition) is false under the
; assignment x:=5, therefore x:=5 is a counterexample.
;use the following definition of app and rev.
;true-list  true-list -> true-list (intended contract)
;but of course, you can call app outside its contract,
;since ACL2 is total.
(defun app (x y)
"append x and y"
 (if (endp x)
    y
    (cons (car x)
          (app (cdr x) y))))

;true-list -> true-list
;remember you can call rev, outside its contract.
(defun rev (x)
"reverses x"
  (if (endp x)
    nil
    (app (rev (cdr x))
         (list (car x)))))
 
;[A1]
 (check= 
  (let ((x (/ 15 2)))
        (or (>= x 8)
            (<= x 7)))
        nil)

;[A2]
 (check=
  (let ((x 15) (y -6))
    (implies (and (integerp x)
                  (integerp y))
             (integerp (/ x y))))
  nil)


;[A3]
 (check=
  (let ((x (cons 1 2)))
    (implies (consp x)
             (true-listp x)))
  nil)

;[A4]
 (check=
  (let ((x 23))
    (implies (endp x)
         (equal x nil)))
  nil)

;[A5]
 (check= 
  (let ((x nil) (y nil)) 
    (<= (len (cons x (rev y))) (len (rev (app y x)))))
  nil)

;[A6]
  (check= 
  (let ((x nil)) 
    (implies (natp (len x))
             (consp x)))
  nil)

;[A7]
  (check= 
  (let ((x '(1 2)) (y 5))
    (implies (true-listp x)
             (true-listp (append x y))))
  nil)

;[A8]
  (check=
  (let ((x 1) (y nil))
    (equal x (car (app x y))))
  nil)


; Part B(30 pts):  Simple theorems  (Rubric: Each question 5pts)
; Each of the following statements can be written as an ACL2 theorem that ACL2
; can prove automatically. So formalize the given statements in ACL2 Logic.
; Example problem:
;   Every natural number is an integer.
; Solution:
;   (thm (implies (natp x)
;                 (integerp x)))

;[B1]
; The CDR of a CONS of any ACL2 object and y is equal to y.
(thm (equal (cdr (cons x y)) y))

;[B2]
; Every rational number is not a cons.
(thm (implies (rationalp x)
              (not (consp x))))

;[B3]
; Every integer is either less than 9, equal to 9, or greater than 9.
(thm (or (< x 9)
         (= x 9)
         (> x 9)))



;[B4] (yes, this is silly, but true)
; Every integer that is greater than 5 and less than 4 is a string. 
(thm (implies (and (integerp x)
                   (> x 5)
                   (< x 4))
              (stringp x)))

;[B5]
; The length of consing a value onto any list is one plus the length of
; the original list.  (Use LEN for finding length.)
(thm (equal (len (cons x L))
            (+ 1 (len L))))


;[B6]
; APP of x and every true-list is a true-list. 
(thm (implies (true-listp y)
              (true-listp (app x y))))



; Part C(30pts):  Existential theorems
; Each of the following existential statements can be written as an ACL2
; theorem by providing witnesses, and if correct, ACL2 should prove each
; automatically(each thm should pass/succeed).
;
; Example problem:
;   For every value, there exists a true list containing only that one value.
; Solution:
   (thm (let ((y (list x)))
          (and (equal (car y) x)
               (equal (cdr y) nil))))
; or you can also formalize it without using let binding:
   (thm (and (equal (car (list x))
                    x)
             (equal (cdr (list x))
                    nil)))
; (list x) constructs witnesses to the existential.

;[C1] 10pts
; There exists an integer we can multiply any positive number to 
;get a negative number.
(thm (let ((x -1))
       (implies (posp y)
                (negp (* y x)))))

;[C2] 10pts
; For every integer i, there exists an integer (its additive inverse) that
; we can add to i to get zero. 
(thm (let ((x (- y)))
       (implies (integerp y)
                (and (integerp x)
                     (= (+ y x) 0)))))

;[C3] 10pts
;There exists a 3 element list that when reverses, returns itself.
(thm (let ((l (list x y x)))
       (equal (rev l)
              l)))



; Part D (Extra Credit 30pts):  Theories
; So far, we have been considering whether propositions are theorems in ACL2's
; "ground zero" theory, the theory you get when you start running ACL2.  Now
; let's consider *extending* that theory by defining a function.  Whether
; something is a theorem in the new theory can depend on how we define that
; function.

; ACL2 has the following function built-in, len, which counts the number of
; elements in a list.

;Suppose we add the following function definition:

;[D0]
    (defun count-integers (x)
       (if (endp x)
         0;changing nil to 0
         (if (integerp (car x))
           (+ 1 (count-integers (cdr x)))
           (count-integers (cdr x)))))

#| START COMMENT BLOCK
Without running ACL2s, answer [D1] to [D5], say "THEOREM", if you
think it is a theorem and say "NOT A THEOREM" if you think it is not a 
theorem and provide a counterexample. Answer [D1] to [D5] within these comments,
but [D6](outside the comment block)  should succeed in ACL2s.

;[D1] 5pts
 
(implies (true-listp x)
         (<= (count-integers x) (len x))

;[D2] 5pts

(<= (count-integers x) (len x))

;[D3] 5pts
(implies (consp x)
         (> (count-integers x) 0)

;[D4] 5pts
(implies (true-listp x)
         (integerp (count-integers x)))

;[D5] 5pts
(implies (integerp x)
         (equal (count-integers x)
                1))

|#; END COMMENT BLOCK
;When you have answered all of these, you can check if you are right or
;wrong, how do you do that, just like in the previous questions? 
;Just ask ACL2(Use thm to show proof and the let binding to show counterexample)!

;[D6] 5pts
;Now change the definition of count-integers(edit [D0]) in such a way, that [D4] is
;a theorem, i.e the following thm should succeed in ACL2s.
    
(thm (implies (true-listp x)
         (integerp (count-integers x))))#|ACL2s-ToDo-Line|#