#|
CS 2800 Homework 4 - Spring 2013

For this homework, you will be using the BEGINNER mode in ACL2s.

Instructions for using this file:

- open this file in ACL2s as hw04.lisp

- set the session mode to "Beginner"

- insert your solutions into this file where indicated (for instance as
"..."). This includes contracts, the body of the function, and test cases.
Make sure you provide as many test cases as required (in addition to the
ones already provided, of course).

- do not comment in or comment out any existing function definitions from
this file. Also, do not change the order of any function definitions,
whether provided by us or defined by you.

- make sure the entire file is admitted by ACL2s in Beginner mode. This means:
  * 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.
  * all check= tests must be satisfied. If any of the provided tests fail,
    your function definition is wrong, and the file will not be admitted.
    If any of your own tests fail, it may be your function is wrong, but
    it may also be that your check= specification is incorrect.

  Sometimes it may take a while for your function to be admitted. Be
  patient: rest assured that, if your function is correct, the process will
  succeed. If you don't get a success message after 2-3 mins (depending on
  your hardware), then probably your definition is too complicated or
  wrong.

- save the file with your additions and turn it in. To do that, check out
the directory at

  svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/04/<groupname>

  where groupname is the name of the group as it was emailed to you. Your
  username and password remain as before.

  Place your file hw04.lisp in this directory, add it, and commit. Do NOT
  submit the session file (ending in .a2s).

Finally, add an ASCII text file "comments.txt" into the same directory
where you put hw04.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.

- for non-programming problems, include solutions as comments. We will use
F and T to represent false and true, and the following character
combinations to represent the Boolean connectives:

  NOT        ~

  AND        /\
  OR         \/

  IMPLIES    =>

  EQUIVALENT =
  XOR        <>

  The binding powers of these connectives are as in class: they are listed
  in the above table from highest to lowest. Within one group (no blank line),
  the binding power is the same.

|#

#| 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1. Classification 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For each of the following formulas, determine if they are valid,
satisfiable, unsatisfiable, or falsifiable. These labels can overlap (e.g.
a formula can be both satisfiable and valid), so indicate ALL of the four
characterizations that apply. You can use a truth table or a simplification
argument. For satisfiable or falsifiable formulas, you can also give
assignments that show satisfiability or falsifiability.

a) (p /\ q ) \/ r = (p /\ r) \/ q

b) (p => q) /\ (r=>s) /\ (p\/r) => (q\/s) 

c)  ~q /\ (p=>q) => q

d) ~p /\ (p => q) => ~q

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 2. Word problems 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The problems below consist of some assumptions followed by a conclusion.
Formalize and analyze the statements using propositional logic, as follows:
assign propositional variables to the atomic facts in the statements,
formalize the entire statement into a propositional logic formula, and then
determine whether the conclusion follows from the assumptions.

For example, suppose you were asked to formalize and analyze:

Mitt likes Jane if and only if Jane likes Mitt.
Jane likes Bill.
Therefore, Mitt does not like Jane.

Here's the kind of answer we expect. (Note that we have used "mnemonic"
[easy to remember] propositional variables to denote the facts in the
sentences. Do not use T or F as variables: these are reserved for true and
false, respectively.) :

Let mj denote "Mitt likes Jane"; let jm denote "Jane likes Mitt"; let jb
denote "Jane likes Bill". The first sentence can then be formalized as
mj = jm.  The second sentence is jb. The third sentence contains
the claim we are to analyze, which can be formalized as
(mj = jm) /\ jb => ~mj .

This is not a valid claim. A truth table shows that the claim is violated
by the assignment mj = jm = jb = T.

Problems: 

a) If Natasha is a spy, then exactly one of following holds: Natasha works
for USA or Natasha works for USSR. Natasha is a spy. Therefore, Natasha
works for USSR and Natasha works for USA.

b) If Arthur pulled a sword from stone, then Arthur is King. Arthur is
King. Therefore, Arthur pulled a sword from stone.

c) Tom takes the advanced course in Logic only if CS2800 is interesting.
Tom gets a good grade in CS2800 and Tom takes the advanced course in Logic.
Therefore, CS 2800 is interesting.

d) Find a non-CS and non-math book of your choice, such as a novel, a
history article, or a newspaper article on current affairs. Pick two
sentences whose formalization requires at least 3 and at most 6 variables.
Formalize the sentences and classify them as above. You can pick the two
sentences from two different books if you want. (Since you are quoting
these sentences from a book, remember to cite the source, i.e. the exact
book reference with page numbers!)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 3. Decision Procedures
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Given is a decision procedure UNSAT(h) that returns T if h is
unsatisfiable, F otherwise. Show how to construct a decision procedure for
satisfiability, one for falsifiability, and one for validity. Each of your
procedures should only involve UNSAT and elementary operations such as
tests, or negating answers. You are not allowed to build truth tables,
simplify input formulas, etc.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 4. Normal Forms
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Recall: a formula is in Conjunctive Normal Form (CNF) if it is a
conjunction of disjunctions of literals. Analogously, we defined
Disjunctive Normal Form (DNF) in the lecture.

Convert the following formulas to the normal form specified. You do not
have to show the intermediate steps, but state how you did it (e.g. via
truth table, via simplification, etc).

a) DNF for (x \/ ~y) /\ (y \/ ~z) => (~y => z)

 
b) CNF for (x => (y => z)) = (y => ~x)

c) DNF for (a \/ b) /\ (( a /\ c) \/ (a /\ b) \/ (a /\ ~c)  \/ b)

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Programming
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 
;; The goal of this exercise is to define an adder: a circuit that performs addition.
;; We begin by introducing a few binary operations.

(defdata PropOp (oneof 'and 'or 'xor))

; A propositional expression is either an atom (represented as a symbol)
; or (Op PropEx PropEx). Ignore the :type-lemmas directive in the data
; definition below.

(defdata PropEx (oneof symbol (list PropOp PropEx PropEx))
  :type-lemmas t)

(defdata listPropEx (listof PropEx))

; A bitvector is a list of of propositional atoms.
(defdata bv (listof symbol))

; A binding is a pair of the form (symbol,t) or (symbol,nil),
; which, intuitively, assigns t or nil to the atomic proposition
; specified by the symbol.
; (Note that t and nil are also symbols. To avoid confusion do not use
; them as propositional atoms.)

(defdata binding (list symbol boolean))

; an assignment is a list of bindings
(defdata assgn (listof binding))

; A value is the result of evaluating a propositional expression given the
; binding of the symbols that appear in the expression. If the
; assignment does not provide a binding of a symbol in the expression,
; its value is defined to be 'unbound.

(defdata value (oneof boolean 'unbound))

(defdata valuelist (listof value))

; 1.
; nodupsp : bv -> booleanp

; (nodupsp l) takes list of symbols as input and returns false if any
; symbol occurs more than once; else it returns true.
(defunc nodupsp (l)
  :input-contract (bvp l)
  :output-contract ...

...)

; 2.
; get-symbol-list : assgn -> list of symbols

; (get-symbol-list e) takes an assignment as input and returns the
; list of symbols that it binds, i.e. that are assigned values.
(defunc get-symbol-list (e)
  :input-contract ...
  :output-contract ...

...)

; 3.
; nodupbindingp : assgn -> boolean

; (nodupbindingp e) takes an assignment as input and returns true if
; there are no duplicate bindings for any symbol.
(defunc nodupbindingp (e)
  :input-contract ...
  :output-contract ...

...)

; 4.
; lookup-assgn : symbol x assgn -> value 

; (lookup-assgn a e) finds the value that the symbol a is bound to in the
; assgn e. If there exists no binding in the assignment then return
; 'unbound.
(defunc lookup-assgn (a e)
  :input-contract (and (symbolp a) (assgnp e) (nodupbindingp e))
  :output-contract ...

...)

; 5.
; vxor : value x value -> value 

; (vxor a b) is an extension of the known xor function. If the inputs
; are boolean it returns xor(a,b). In case any of the input is
; 'unbound then it returns 'unbound
(defunc vxor (a b)
  :input-contract (and (valuep a) (valuep b))
  :output-contract ...

)

; 6.
; vand : value x value -> value 

; (vand a b) is an extension of the known and function. If the inputs
; are boolean it returns a /\ b. In case any of the input is 'unbound
; then it returns 'unbound
(defunc vand (a b)
  :input-contract (and (valuep a) (valuep b))
  :output-contract ...

...)

; 7.
; vor : value x value -> value 

; (vor a b) is an extension of the known or function. If the inputs are
; boolean it returns a \/ b. In case any of the input is 'unbound then
; it returns 'unbound
(defunc vor (a b)
  :input-contract (and (valuep a) (valuep b))
  :output-contract ...

...)

; Please do not comment or delete the following. These theorems are
; required to admit some of the function definitions.

;  Begin
(defthm consp-propexp1
 (implies (and (PropExp s)
               (not (symbolp s)))
          (consp s))
 :rule-classes (:forward-chaining))

(defthm consp-propexp2
 (implies (and (PropExp s)
               (not (symbolp s)))
          (consp (rest s)))
 :rule-classes (:type-prescription))

(defthm consp-propexp3
 (implies (and (PropExp s)
               (not (symbolp s)))
          (consp (rest (rest s))))
 :rule-classes (:type-prescription))
; End

; 8. 
; evaluate-expr : PropEx x assgn -> value

; (evaluate-expr s e) takes a propositional expression s and an
; assignment e. The assignment tells the value a symbol appearing in
; the expression is bound to. Then it utilizes the propositional
; operations defined above to evaluate the expression.

; Write at least 5 checks. Cover the case when the assignment does not
; provide a binding of a symbol appearing in the expression.

; NOTE : It may take a little while (up to a minute or two depending on
; the machine) to admit the definition. Please be patient.
(defunc evaluate-expr (s e)
  :input-contract ...
  :output-contract ...

...)

(check= (evaluate-expr 'x '((x t))) t)
(check= (evaluate-expr 'x nil) 'unbound)
(check= (evaluate-expr '(and x y) '((x t) (y t))) t)
(check= (evaluate-expr '(and x y) '((x t) (y t))) t)

; 9.
; evaluate-exprlist : listPropEx x assgn -> valuelist

; (evaluate-exprlist ls e) inputs a list of propositional expressions
; ls, and assignment e such that e has no duplicate bindings. It
; evaluates each expression in ls and returns a list of values that
; each expression evaluates to.

; Write at least 5 checks. 
(defunc evaluate-exprlist (ls e)
  :input-contract (and (listPropExp ls) (assgnp e) (nodupbindingp e))
  :output-contract (valuelistp (evaluate-exprlist ls e))
  (if (endp ls)
    nil
    (cons (evaluate-expr (first ls) e)
          (evaluate-exprlist (rest ls) e))))

(check= (evaluate-exprlist '((or x y) (and x y)) '((x t) (y t))) '(t t))
(check= (evaluate-exprlist '((xor x y) (and x y)) '((x t) (y t))) '(nil t))

; 10.
; Define FA-sum : symbol x symbol x PropEx --> PropEx

; FA-sum function implements the "sum" of the full-adder. It takes two
; atomic propositions, a and b, and PropEx c (PropEx for carry
; in). It returns the PropEx representing the sum component of the
; full-adder.

; In this and the following functions, the carry c is a PropEx, rather than
; a variable, as these functions will be later used to get a propositional
; expression for adding two bitvectors.

(defunc FA-sum (a b c)
  :input-contract  (and (symbolp a) (symbolp b) (PropExp c))
  :output-contract ...
  
  ...)

; The above function generates a propositional expression. We will
; provide bindings to the symbols and use evaluate-expr in order to
; test it. For example
(check= (evaluate-expr (FA-sum 'a 'b '(and x y)) '((a nil) (b t) (x t))) 'unbound)
(check= (evaluate-expr (FA-sum 'a 'b 'c) '((a nil) (b nil) (c nil))) nil)
(check= (evaluate-expr (FA-sum 'a 'b 'c) '((a nil) (b t) (c nil))) t)
; Now assume that c is symbol, and write the other 6 possible test cases for FA-sum

; 11.
; Define FA-carry : symbol x symbol x PropEx --> PropEx

; FA-carry function implements the "carry" of the full-adder. It takes two
; atomic propositions, a and b, and PropEx c (PropEx for carry
; in). It returns the PropEx representing the carry component of the
; full-adder.
(defunc FA-carry (a b c)
  :input-contract (and (symbolp a) (symbolp b) (PropExp c))
  :output-contract ...

...)

(check= (evaluate-expr (FA-carry 'a 'b 'c) '((a nil) (b nil) (c nil))) nil)
(check= (evaluate-expr (FA-carry 'a 'b 'c) '((a t) (b t) (c nil))) t)
(check= (evaluate-expr (FA-carry 'a 'b '(and x y)) '((a nil) (b t) (x t) (y nil))) nil)

; Now assume that c is symbol, and write the other 6 possible test cases for FA-carry
(check= (evaluate-expr (FA-carry 'a 'b 'c) ...)

; 12.
; Define FA : symbol x symbol x PropEx --> ListPropEx

; FA function implements the "sum" and "carry" of the full-adder. It
; takes two atomic propositions, a and b, and PropEx c (PropEx for
; carry in). It returns the listPropEx of two elements. The first
; element is the "sum" component of the full-adder. The second element
; of the list is the "carry" component of the full-adder.
(defunc FA (a b c)
  :input-contract (and (symbolp a) (symbolp b) (PropExp c))
  :output-contract ...

...)
(check= (evaluate-exprlist (FA 'a 'b '(and x y)) '((a nil) (b t) (x t) (y nil))) '(t nil))
(check= (evaluate-exprlist (FA 'a 'b 'c) '((a nil) (b t) (c nil))) '( t nil))
(check= (evaluate-exprlist (FA 'a 'b 'c) '((a t) (b t) (c nil))) '(nil t))

; Write all the possible test cases for one bit FA (assume c is a symbol)

; Please do not comment or delete the following. These theorems are
; required to admit some of the function definitions.

;  Begin
(defthm len-equal-consp
  (implies (and (bvp bv1)
                (bvp bv2)
                (equal (len bv1) (len bv2))
                (consp bv1))
           (consp bv2)))

; End

; 13.
; Define ripcarry-in: bitvector x bitvector x PropEx -> listPropEx

; Given are two equal-length bitvectors and a PropEx representing an
; expression for a carry bit. This function computes a list of
; PropEx's.  The ith element represents the function that computes the
; ith bit of the sum of the given bitvectors. The input is assumed to
; be given such that the least significant bit comes first, most
; significant bit last. The output should be in the same order. 

(defunc ripcarry-in (bv1 bv2 carry)
  :input-contract (and (PropExp carry) ...)
  :output-contract ...

...)

; We reserve the two symbols 'false and 'true for constants. Further, we
; will assume that we always have the following bindings for them in any
; assignment that we create:
; ('false nil) and ('true t)

; 14.
; Define ripcarry: bitvector x bitvector -> (list PropEx)

; Given are two equal-length bitvectors. This function computes a list
; of PropEx's. The ith element represents the function that computes
; the ith bit of the sum of the given bitvectors. The initial carry is
; assumed to be 0, represented by the constant function 'false.
(defunc ripcarry (bv1 bv2)
  :input-contract ...
  :output-contract ...
  
  ...)

; Write 5 checks for a 2 bit adder. Use the evaluate-exprlist and an
; assignment for the symbols as above. Remember to assign 'false to
; nil and 'true to t in the assignments

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

#|

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

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

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.

|#