#|
CSU290 Homework 3 - 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 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 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--a case in which it
; equals nil.  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)

;[A1]
(or (>= x 6)
    (<= x 5))

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

;[A3]
(implies (and (integerp x)
              (integerp y))
         (not (integerp (/ x y))))

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

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

;[A6]
(implies (equal (car x) nil)
         (atom x))

;[A7](see definition of BINARY-APPEND)
(true-listp (append x y))

;[A8]
(atom (nth i l))

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

;[A10] (see ACL2 documentation on UNION-EQUAL)
(equal (len (union-equal x y))
       (+ (len x) (len y)))



; Part B:  Simple theorems
; Each of the following statements can be written as an ACL2 theorem that ACL2
; can prove automatically.
; Example problem:
;   Every natural number is an integer.
; solution:
;   (thm (implies (natp x)
;                 (integerp x)))

;[B1]
; Everything is either a cons or an atom.
(thm ?)

;[B2]
; Four times five equals twenty.
(thm ?)

;[B3]
; The CAR of a CONS of x and y is equal to x.
(thm ?)

;[B4]
; Every string is not a cons.
(thm ?)

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

;[B6]
; x plus y is equal to y plus x
(thm ?)

;[B7]
; If we know
;  x + y < z
;  y + z < x
; then
;  y < 0
(thm ?)

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

;[B9]
; LEN always returns a natural number
(thm ?)

;[B10]
; The length of consing a value onto some list is one plus the length of
; the original list.  (Use LEN for finding length.)
(thm ?)



; 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.
;
; Example problem:
;   For every value, there is a true list containing only that one value.
; solution:
;   (thm (let ((y (list x)))
;          (and (equal (car y) x)
;               (equal (cdr y) nil))))
; or:
;   (thm (and (equal (car (list x))
;                    x)
;             (equal (cdr (list x))
;                    nil)))
;
; ((list x) constructs witnesses to the existential.)

;[C1]
; There is an integer we can multiply by 3 to get 18.
(thm ?)

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

;[C3]
; For every rational r, there is a *positive* integer that we can multiply r
; by to get an integer.  (Hint: we have studied a function that returns
; exactly the positive integer we want.)
(thm ?)



; Part D:  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.

; The following definition passes tests within the intended domain, but the
; subsequent proposition, (true-listp (rev x)), is not a theorem given this
; definition.  Modify the function definition so that the proposition is a
; theorem (ACL2 should prove it easily) and all the tests still pass.
; (Note that the proposition concerns all possible inputs to the function--
; including those outside the intended domain.)

; REV: true-list -> true-list
; Returns the reverse of the given list.
(defun rev (x)
  (if (endp x)
    x
    (append (rev (cdr x)) (list (car x)))))

;**** DO NOT MODIFY ANYTHING BELOW HERE! ****
(check= (rev '(1 2 3)) '(3 2 1))
(check= (rev '(a b)) '(b a))
(check= (rev '("hi")) '("hi"))
(check= (rev '()) '())

(thm (true-listp (rev x)))