#|

CS 2800 Homework 2 - Spring 2013

Student names:  TODO: PUT YOUR NAMES HERE

For this homework, you will need to use ACL2s. You should have installed it
by now on your machine, and know the basics of using it. Make sure you have
the latest version (we occasionally need to make some changes to
accommodate circumstances in the class).

You will be using the Bare Bones mode in ACL2s, which has only a minimal
number of built-in functionality, allowing you to practice defining many
basic functions without any clashes.

Instructions for using this file:

- open this file in ACL2s as hw2.lisp

- set the session mode to "Bare Bones" (very important!)

- insert your solutions into this file where indicated (for instance as "...")

- do not remove or comment out any function definitions from this file,
such as booleanp below. These are not defined in bare bones mode; if you
remove them your file will not be accepted by ACL2s.

- make sure the entire file is accepted by ACL2s in Bare Bones mode. In
particular, there must be no "..." in the code. If you don't finish some
problems, comment them out. The same is true for any English text that you
may add. This file already contains many comments, so you can see what the
syntax is.

- turn in, via svn, the file hw2.lisp with your additions.

Use "commit" frequently, say after every session with your partner, even if
you only have partial solutions. This gives us feedback on how much time
these problems take for you.

Finally, add an ASCII text file "comments.txt" into the same directory
where you put hw2.lisp, with the following contents:

(i)  a summary of how much time you spent on this homework, and how you
     split up the work between the team members.

(ii) any feedback on the homework you may have, such as errors in it,
     sources of misunderstanding, general difficulty, did you learn
     something, etc.

|#

;DONT DELETE. defining a custom test? for hwk 2 only.

(acl2::defmacro implies (a b) 
  `(acl2::implies ,a ,b))

(acl2::defmacro test? (x)
  `(acl2::test? ,x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part 1: Booleans
;
; Built in to Bare Bones mode are the Boolean constants t and nil (for true
; and false) and the functions if and equal.
; 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; recall the definition of booleanp
(defunc booleanp (x)
  :input-contract t
  :output-contract (booleanp (booleanp x))
  (if (equal x t)
      t
    (equal x nil)))

; and the definition of and
(defunc and (a b)
  :input-contract (if (booleanp a) (booleanp b) nil)
  :output-contract (booleanp (and a b))
  (if a b nil))

; Define
; or: Boolean x Boolean -> Boolean 
; 
; (or a b) is t if a is t or b is t, and nil otherwise.
; 
; Replace ... below with the definition
;
; Make sure that you satisfy the tests and add two more of your
; own tests

(defunc or (a b)
  :input-contract (and (booleanp a) (booleanp b))
  :output-contract (booleanp (or a b))
  ...)

(check= (or t   nil) t)
(check= (or nil nil) nil)



; What happens if you evaluate (or 1 nil)? Try it.
; Fill in the ...'s below with what ACL2s reports.

#|

...


|#


; When ACL2s reports a "guard" violation, as it did when you
; tried evaluating (or 1 nil), that means that we violated the
; contract of a function.


; Does (or a b) always return t? 
; Check it using test? with: (test? (equal (or a b) t))


; Fill in the ...'s below with 3 contract violations and 
; 3 failed examples and 3 examples where the test passed (witnesses) 
; (Copy and paste from ACL2s output)

#|

...






|#

; test? provides you with automated testing feature.
; Unlike check=, you can use free variables in your 
; conjecture (i.e the expression you are checking to be true or false)
; For example, it will provide you with examples in which the
; conjecture (or a b) is not t and examples in which 
; (or a b) is t. Just as you got a guard violation
; when evaluating (or 1 nil), test? also prints out contract
; violations whenever it tests bad inputs. Think about
; how you could fix this problem? Use 'implies' and 
; 'and' to modify the conjecture, so that a and b are assumed 
; to be booleans and so that ACL2s does not print violations.
; Try evaluating the following in the session editor:
#|
(test?  (implies (and (booleanp a)
                      (booleanp b))
            (equal (or a b) t)))
       
|#
; Notice that when we test conjectures, we have to test them in a
; way that satisfies the contracts for the functions used. For
; example, in the above conjecture, we use the 'or' function,
; which has a contract stating that its arguments are
; Booleans. Hence, the test? has a hypothesis stating that the
; arguments to or satisfy booleanp.

; There are no more contract violations, but you still get a counterexample,
; because (or nil nil) is nil, which in ACL2 stands for falsity.


; Define
; aand: Boolean x Boolean x Boolean -> Boolean
; 
; (aand a b c) is t if a is t and b is t and c is t, and nil otherwise.
;
; Define aand using and.
;
; Replace ... below with the definition
;
; Add two of your own tests

(defunc aand (a b c)
  :input-contract (and (and (booleanp a) (booleanp b)) (booleanp c))
  :output-contract (booleanp (aand a b c))
  ...)

(check= (aand t   nil t  ) nil)
(check= (aand t t t) t)

; Provide an example of an expression containing an 'if' and an 'and' whose
; evaluation leads to a contract violation.

#|
...
|#

; Define
; not: Boolean -> Boolean 
; 
; (not a) is nil if a is t, and t otherwise.
; 
; Replace ... below with the definition
;
; Add one of your own tests

(defunc not (a)
  :input-contract (booleanp a) 
  :output-contract (booleanp (not a))
  ...)

(check= (not t)   nil)


; Define
; follows-from: Boolean x Boolean -> Boolean 
; 
; (follows-from a b) is nil if a is nil and b is t, and t otherwise.
; 
; Replace ... below with the definition
;
; Make sure that you satisfy the tests and add two more of your
; own tests

(defunc follows-from (a b)
  :input-contract (and (booleanp a) (booleanp b))
  :output-contract (booleanp (follows-from a b))
  ...)

(check= (follows-from t   t)   t)
(check= (follows-from nil nil) t)



; Define
; iff: Boolean x Boolean -> Boolean 
; 
; (iff a b) is t if a and b are both t or both nil, and nil otherwise.
; 
; Replace ... below with the definition
;
; Make sure that you satisfy the tests and add two more of your
; own tests

(defunc iff (a b)
  :input-contract (and (booleanp a) (booleanp b))
  :output-contract (booleanp (iff a b))
  ...)

(check= (iff t   t)   t)
(check= (iff nil nil) t)




; Provide an example of an expression containing an equal whose
; evaluation does not lead to a contract violation, but when we
; replace the equal with an iff, evaluation does lead to a contract
; violation.


#|

...

|#

; Can you provide an example of an expression containing a iff
; whose evaluation does not lead to a contract violation, but
; when we replace the iff with an equal, evaluation leads to a
; contract violation? If so, provide an example. If not, explain.


#|

...


|#



; Confirm that 'iff' (pronounced if and only if) is functionally
; equivalent to 'equal' if its arguments are boolean, using test?.
; (If you defined iff correctly the following will not give error)
; The following confirms that under the constraints that a and b 
; are boolean, 'iff' and 'equal' give same results.


(test? (implies (and (booleanp a) 
                     (booleanp b))
                (equal (iff a b)
                       (equal a b))))

; Define
; nor: Boolean x Boolean -> Boolean
; 
; (nor a b) is t if a and b are both nil, and nil otherwise.
; 
; Replace ... below with the definition
;
; Make sure that you satisfy the tests and add two more of your
; own tests

(defunc nor (a b)
  :input-contract (and (booleanp a) (booleanp b))
  :output-contract (booleanp (nor a b))
  ...)

(check= (nor t   t)   nil)
(check= (nor nil nil) t)


; NOR - the universal base
; You can write all boolean functions in terms of nor.
; Fill in the following ... (if you are successfull, you will not see any counterexamples)
; The first is done for you as an e.g.

(test? (implies (and (booleanp a)
                     (booleanp b))
                (iff (follows-from a b)
                     (nor nil (nor a (nor nil b))))))

(test? (implies (booleanp a)
                (iff (not a)
                     ...))) ; Using just the nor function

(test? (implies (and (booleanp a)
                     (booleanp b))
                (iff (or a b)
                     ))) ; Using just the nor function

(test? (implies (and (booleanp a)
                     (booleanp b))
                (iff (and a b)
                     ))) ; Using just the nor function


; Define
; minority : Boolean x Boolean x Boolean -> Boolean

; (minority a b c) is t if at most 1 of a,b,c is t, and nil otherwise.
; 
; Replace ... below with the definition and add the contracts
; (you'll have to add contracts from now on in this homework).
;
; Make sure that you satisfy the tests and add two more of your
; own tests

(defunc minority (a b c)
...


)

(check= (minority t nil t)   nil)
(check= (minority nil t   nil) t)

; if you have no mistakes in your minority function, the following test? should pass
(test? (implies (aand (booleanp a) 
                      (booleanp b)
                      (booleanp c))
                (follows-from (minority a b c) (nor a b))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part 2: Numbers
;
; ACL2 numbers includes integers and rationals
; 
; The built-in functions are:
;   + * unary-- unary-/ < numerator denominator rationalp integerp
; If you are not sure what these functions do, try them out.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Define
; <= : Rational x Rational -> Boolean
; 
; (<= a b) is t if a <= b, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc <= (a b)
...


)



; Define
; > : Rational x Rational -> Boolean
; 
; (> a b) is t if a > b, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc > (a b)
...

)


; Define
; <> : Rational x Rational x Rational -> Boolean
; 
; (<> a b c) is t if a < b > c, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least five tests

(defunc <> (a b c)
...


)

(check= (<> 1/4 1/2 1/3) t)


; Define
; pos-rationalp: All -> Boolean
; 
; (pos-rationalp a) is t if a is a positive rational, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc pos-rationalp (a)
...



)


; Define
; natp: All -> Boolean
; 
; (natp a) is t if a is a natural number, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc natp (a)
...



)


; Define
; *+: Rational x Rational x Rational -> Rational
; 
; (*+ a b c) returns a * b + c

; This is sometimes called fused multiple-add and is an important operation
; in matrix calculations. Many architectures have direct hardware support for
; this operation.
; 
; Replace ... below with the definition
;
; Make sure that you write at least five tests

(defunc *+ (a b c)
...

)



; Define
; /: Rational x Rational-{0} -> Rational
; 
; (/ a b) returns a/b; note that b has to be non-0.
; Think carefully about the input contract.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc / (a b)
...


)

(check= (/ 23 46) 1/2)

; Define
; div3p: All -> Boolean
; 
; (div3p a) is t if a is an integer divisible by 3, otherwise it is nil.
; 
; Replace ... below with the definition
;
; Make sure that you write at least three tests

(defunc div3p (a)
...



)




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Evaluates to <?>
;
; For each of these, try to predict what the left-hand-side of the equality
; will evaluate to and then replace the ... with the correct value--in the
; canonical form ACL2 prints when passed that expression in the
; read-eval-print loop.  For example:
;
;   (check= (/ 3 2) ...)
;
; should become
;
;   (check= (/ 3 2) 3/2)
;
; which is accepted by ACL2 after moving the line past it.  (The arguments
; to CHECK= must be equal for ACL2 to accept the check.)  What you fill in
; should be an atom, rewritten if the left hand side is already an atom.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(check= (/ 18 7)                      ...)
(check= (/ 49 7)                     ...)
(check= (* 45 10/11)                 ...)
(check= 64/32                        ...)
(check= -0/3                         ...)
(check= (numerator 42/7)             ...)
(check= (denominator (/ 108 12))     ...)

; Numbers: predicates (these are t or nil)

(check= (<= 12 (/ 24 2))      ...)
(check= (<> 1 2 2)          ...)

(check= (integerp 0)          ...)
(check= (pos-rationalp 0)         ...)

(check= (integerp  73/3)      ...)
(check= (rationalp 73/3)      ...)
(check= (rationalp 84/3)      ...)
(check= (integerp  84/3)      ...)
(check= (integerp (/ 108 9))   ...)
(check= (pos-rationalp (/ 108 9))  ...)

(check= (integerp -1)         ...)
(check= (rationalp -1)        ...)
(check= (integerp (/ -7 41))  ...)
(check= (pos-rationalp (/ -7 41)) ...)

(check= (pos-rationalp 0)              ...)
(check= (div3p 0)             ...)
(check= (div3p -72/4)         ...)
(check= (natp 83/3)           ...)
(check= (natp 0)           ...)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

Please fill out the following feedback form, not as a team, but each team
member individually:

https://docs.google.com/spreadsheet/viewform?formkey=dDltQWVfSUQ2UFk3OWZheDRIbzgxT3c6MA


Confirm here whom of the team members filled out the form:

Name 1 ...
Name 2 ...
(Name 3 ...)

Everyone who filled out the form gets credit worth 1 quiz.

The form is anonymous, to encourage you to write what you think about this
class. (If you want to stay anonymous, do not reveal your name on the
feedback form.) On the other hand, we must rely on your honesty in stating
whether you filled out the form or not, and in NOT filling out the form
several times (why would you do that??). We do not want to find
discrepancies in the number of entries on the form, and the number of
people claiming to have filled out the form.

|#