#|
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:  Not theorems
; 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]
(or (>= x 8)
    (<= x 7))

;[A2]
(implies (and (integerp x)
              (integerp y))
         (integerp (/ x y)))


;[A3]
(implies (consp x)
         (true-listp x))

;[A4]
(implies (endp x)
         (equal x nil))

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

;[A6]
(implies (natp (len x))
         (consp x))

;[A7]
(implies (true-listp x)
         (true-listp (app x y)))

;[A8]
(equal x (car (app x y))) 


; Part B:  Simple theorems
; 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 ?)

;[B2]
; Every rational number is not a cons.
(thm ?)

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


;[B4] (yes, this is silly, but true)
; Every integer that is greater than 5 and less than 4 is a string. 
(thm ?)

;[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 ?)

;[B6]
; APP of x and every true-list is a true-list.  



; Part C:  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]
; There exists an integer we can multiply any positive number to 
;get a negative number.
(thm ?)

;[C2]
; For every integer i, there exists an integer (its additive inverse) that
; we can add to i to get zero. 
(thm ?)

;[C3]
;There exists a 3 element list that when reverses, returns itself.
(thm ?)



; Part D (Extra Credit):  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)
         nil
         (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]
 
(implies (true-listp x)
         (<= (count-integers x) (len x))

;[D2]

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

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

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

;[D5]
(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]
;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))))