; ****************** BEGIN INITIALIZATION FOR ACL2s MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);
(make-event
 (er-progn
  (set-deferred-ttag-notes t state)
  (value '(value-triple :invisible))))

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/base-theory" :dir :system :ttags :all)


#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/custom" :dir :system :ttags :all)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s mode.") (value :invisible))

;Settings common to all ACL2s modes
(acl2s-common-settings)
;(acl2::xdoc acl2s::defunc) ;; 3 seconds is too much time to spare -- commenting out [2015-02-01 Sun]

(acl2::xdoc acl2s::defunc) ; almost 3 seconds

; Non-events:
;(set-guard-checking :none)

(acl2::in-package "ACL2S")

; ******************* END INITIALIZATION FOR ACL2s MODE ******************* ;
;$ACL2s-SMode$;ACL2s
#|

CS 2800 Homework 5 - Spring 2019

This homework is done in groups. 

 * Groups should consist of 2-3 people.

 * One group member will create a group in BlackBoard. See the class Webpage for
   instructions on how to do that.
 
 * Other group members then join the group. 

 * Homework is submitted by only one person per group. Therefore make sure the
   person responsible for submitting actually does so. If that person forgets to
   submit, your team gets 0.

   - We recommend that groups email confirmation messages and submit early and
     often. 

 * Submit the homework file (this file) on Blackboard.  Do not rename 
   this file.  There will be a 10 point penalty for this.
   When done, save your file and submit it as hwk05.lisp.
   Make sure your Blackboard submission is valid ACL2s code. One way
   to check this is to download your submission from Blackboard after
   you've uploaded it, and check it using ACL2s.

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.  If you
   fail to follow these instructions, it costs us time and it will cost you
   points, so please read carefully.

The format should be: FirstName1 LastName1, FirstName2 LastName2, ...
For example:
Names of ALL group members: Frank Sinatra, Billy Holiday

There will be a 10 pt penalty if your names do not follow this format.

Replace "..." below with the names as explained above.

Names of ALL group members: ...

* Later in the term if you want to change groups, the person who created the
  group should stay in the group. Other people can leave and create other groups
  or change memberships.  See the class Webpage.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For this homework you will need to use ACL2s.

Technical instructions:

- Open this file in ACL2s.

- Make sure you are in ACL2s mode. This is essential! Note that you can
  only change the mode when the session is not running, so set the correct
  mode before starting the session.

- Insert your solutions into this file where indicated (usually as "...").
  Sometimes we require textual explanations (e.g., complexity analysis below)
  so just add your explanation inside the ACL2s comments.

- Only add to the file. Do not remove or comment out anything pre-existing.

- Make sure the entire file is accepted by ACL2s. In particular, there must
  be no "..." left in the code. If you don't finish all problems, comment
  the unfinished ones out. Comments should also be used for any English
  text that you may add. This file already contains many comments, so you
  can see what the syntax is. We will deduct points for files that are
  not accepted by ACL2s: we sometimes ask explicitly to insert your
  answer in the comments, when the answer is not to be accepted by ACL2s.
  When asked to insert your answer in the comments, do so.

- Do not submit the session file (which shows your interaction with the theorem
  prover). This is not part of your solution. Only submit the lisp file.

Instructions for programming problems:

For each function definition, you must provide both contracts and a body.

You must also ALWAYS supply your own tests. This is in addition to the
tests sometimes provided. Make sure you produce sufficiently many new test
cases. This means: cover at least the possible scenarios according to the
data definitions of the involved types. For example, a function taking two
lists should have at least 4 tests: all combinations of each list being
empty and non-empty.

Beyond that, the number of tests should reflect the difficulty of the
function. For very simple ones, the above coverage of the data definition
cases may be sufficient. For complex functions with numerical output, you
want to test whether it produces the correct output on a reasonable
number of inputs.

Use good judgment. For unreasonably few test cases we will deduct points.

We use the following ASCII character combinations to represent the Boolean
connectives:

  NOT     ~

  AND     /\ or &
  OR      \/ or +

  IMPLIES =>

  EQUIV   <=>
  XOR     ><  or XOR

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

|#

#|

PART I: Equational reasoning and simplifications

I.1.
Simplify each of the Boolean formulas below. That is, for
each formula f, find an equivalent formula g, such that
g is as simple as possible, meaning as short as possible.
Use "0" and "1" for the constant expressions "true" and "false".
You can use any of the "useful equalities" from Section 3.3
in the lecture notes. You can also use any auxialiary equalities
that you have proven previously (including in previous problems).

You don't have to state which rule you are using, but perform 
the simplification step by step.

Do NOT use truth tables to simplify. The point is to learn to
do simplifications without truth tables. Truth tables might work
for 2-3 variables, but beyond that they become unmanageable.

Example: p & (p & q) = (p & p) & q = p & q

I.1.1: (p => q) & p
answer: ...

I.1.2: (p => q) & q
answer: ...

I.1.3: (x => y) & (y => z) & (z => w) & (w => u) & x
answer: ...
          
I.1.4: (x => y) & (y => z) & (z => w) & (w => u) & ~u
answer: ...

I.1.5: (p XOR q) & p
answer: ...


|#


#|
I.2. Apply the substitutions

Below you are given a set of ACL2s terms and substitutions. Recall
that a substitution is a list of pairs, where the first element of
each pair is a variable and the second is an expression. Also,
variables can appear only once as a left element of a pair in any
substitution. For example, the substitution ((y (cons a b)) (x m))
maps y to (cons a b) and x to m. 

For each term/substitution pair below, show what you get when you
apply the substitution to the term. If the substitution is not
well-formed (it does not satisfy the definition of a substitution),
indicate why.  If the substituion is well-formed all you have to do 
is apply the substitution, so do not do anything else, e.g., do not
evaluate the expression you obtain after applying the substitution.

Example:
 (f (bar x y) 'f f)|
 ((x (list 3)) (bar zap) (y (cons 'l nil)) (f (+ 1 2)))

Answer:
 (f (bar (list 3) (cons 'l nil)) 'f (+ 1 2))

In class we wrote this as 

(f (bar x y) 'f f)|((x (list 3)) (bar zap) (y (cons 'l nil)) (f (+ 1 2)))

but the two line format will make it easier for you to read.  

Notice that we only substitute an occurrence of a symbol that
corresponds to a variable, which is why the occurrence of f in
function position (f ...) was not changed.  On the other hand the last
occurrence of in (f ... f) is a variable and was replaced by its
target in the substitution. Finally, 'f is *not* a variable. It is a
constant and it is not affected by any substitution. Replace
the "..."'s below with your answers.

I.2.1. (f 'f f)|
       ((f (list a b)))
       answer: ...

I.2.2. (goo goo 'goo)|
       ((goo (list a b)) ('goo goo))
       answer: ...
       
I.2.3. (cons (app x y) z)|
       ((y (list x)) (x (list y)) (y (list z)))
       answer: ...
   
I.2.4. (f (g x y) (h y x))|
       ((f g) (h f) (x (f (g y x))) (y x))
       answer: ...

I.2.5. (+ (+ (natp (cons x y)) (natp '(cons x y))) (- a b))|
       ((a 43) (b (* c d)) (y (cons x z)) (x x))
       answer: ...
       
I.2.6. (app x y)|
       ((x (list x)) (y (list y)))
       answer: ...
       
#|

|#
I.3. Find the substitutions

For each pair of ACL2 terms, give a substitution that instantiates the 
first to the second. If no substitution exists write "None".

Example:
  (app x y)
  (app (list a x) nil)

Answer:
  ((x (list a x)) (y nil))

I.3.1. (list x y)
       (app x y)
       answer: ...

I.3.2. (f y (cons x y))
       (f x y)
       answer: ...

I.3.3. (f x y)
       (f y (cons x y))
       answer: ...

I.3.4. (foo (+ (bar a b) (baz bar a)) (if if foo baz))
       (foo (+ (bar (if bar baz foo) (baz 'a 'b)) (baz bar (if bar baz foo))) (if foo bar foo))
       answer: ...

I.3.5. (foo (+ (bar a b) (baz 'a a)) (if a foo baz))
       (foo (+ (bar (if nil bar foo) (baz 'a 'b)) (baz bar (if bar baz foo))) (if foo bar foo))
       answer: ...

|#


#|
I.4. Equational proofs

Natural numbers can be defined "inductively" as follows:
- "zero" is a natural number
- if n is a natural number, then S(n) is a natural number,
  where "S" is a special constructor symbol ("S" for "successor").

Our defdata definitions below encode this idea:
|#

(defdata myzero nil)
(defdata mynat (oneof myzero (cons 'S mynat)))


; in this encoding, 0 is represented as nil
(mynatp nil)
; 1 is represented as '(S) = (cons 'S nil)
(mynatp '(S))
; 2 is represented as '(S S) = (cons 'S (cons 'S nil))
(mynatp '(S S))
; and so on (which number is the one below?)
(mynatp '(S S S S S S S S S S S S S))


#|
We can now redefine simple arithmetic operations on mynat.
This is addition:
|#

(definec myplus (x :mynat y :mynat) :mynat
  (if (myzerop x)
    y
    (cons 'S (myplus (cdr x) y))))

#|
We would like you to state some simple facts about addition
as theorems about mynats in ACL2s and have ACL2s prove them.
Then prove the same theorems "manually" using equational reasoning.
The theorems we want to prove are the following equalities:
0 + 0 = 0
0 + 1 = 1
1 + 0 = 1
1 + 1 = 2

In your equational proofs feel free to use the above
equalities about quote:
'(S) = (cons 'S nil)
'(S S) = (cons 'S (cons 'S nil))
and so on.

You can also use the facts
(myzerop nil) = t
(myzerop '(S)) = nil
(myzerop '(S S)) = nil
and so on.

You can also use previously proven equalities as lemmas,
but state them explicitly. For example, if A = B has been
already proven, write:
...
= {lemma A = B proven above}
...
in your proof.

For this problem you are NOT allowed to justify your
proof by simply claiming { Evaluation }.
The point is to do equational reasoning on simple examples.

Also, do NOT "jump" multiple steps. Write only one
in the = { ... } of each step. After a while, we will
allow ourselves to go faster, but for this homework,
we really want to go step by step.

To get you started, here's how we would answer for the
first equality, 0 + 0 = 0.
First we state it as a theorem about mynats in ACL2s:
|#
(thm (equal (myplus nil nil) nil))


#|
Now we prove it manually using equational reasoning:

(myplus nil nil)
= {definition of myplus}
  (if (myzerop nil)
    nil
    (cons 'S (myplus (cdr nil) nil)))
= {(myzerop nil) = t}
  (if t
    nil
    (cons 'S (myplus (cdr nil) nil)))
= {if axioms}
   nil
|#

#|
I.4.1. 
State as an ACL2s theorem about mynat numbers the 
equality 0+1 = 1, and then prove it also manually using
equational reasoning:
|#
;answer
(thm ...

#|
equational proof:
...
|#

#|
I.4.2. 
State as an ACL2s theorem about mynat numbers the 
equality 1+0 = 1, and then prove it also manually using
equational reasoning:
|#

;answer
(thm ...
#|
equational proof:
...
|#

#|
I.4.3. 
State as an ACL2s theorem about mynat numbers the 
equality 1+1 = 2, and then prove it also manually using
equational reasoning:
|#
;answer
(thm (...

#|
equational proof:
...
|#


#|
I.4.4. 
The above theorems are not very interesting: after
all, they operate on concrete numbers, 0, 1, 2, etc. So
they are really tests. We could just as well have evaluated
the function myplus on these concrete values, and verified
that we get the right result with check=.
Now we are going to state and prove a more interesting
theorem, which we cannot turn into a test.

Following the same outline as above, state as an ACL2s 
theorem about mynat numbers the equality 0+n = n, and then
prove it also manually using equational reasoning. Remember
to make sure that in the property you write in your thm
the contracts are satisfied: you must assume that n is
of type mynat.
|#
;answer
(thm ...
     
#|
equational proof:
...
|#

#|
I.4.5. 
We have proven 0+n = n, but what about n+0 = n?
Surely this should be very easy!, you might say.
Do we really have to do it? It's getting a bit
tedious and, frankly, a bit boring as well...

Try to do it, and you might be surprised.
Note that you cannot use something like
(myplus m n) = (myplus n m)
because this has not been proven!
(We know x+y = y+x from arithmetic, but here
we are reasoning about our newly defined
function myplus, not about standard +.)

So try to prove using equational reasoning
that (myplus n nil) = n, and write your
observations below:
|#
;answer
(thm ...
#|
equational proof attempt:
...
|#

#|
Practice: as a suggestion, look at all the
examples of equational reasoning in the slides
and in the lecture notes, and fill in any gaps.
For example, if a proof in the slides says
...
= {Def of aapp, C4}
...
redo that proof by expanding all the steps that
are omitted, e.g.:
...
= {Def of aapp}
...
= {...}
...
=  {C4}
...
Do NOT submit any answers here. They will not
be graded, and they won't count. This is for
your own practice.
|#

#| 

PART II: improving our SAT solver

   Recall the rudimentary SAT Solver that we built in the
   last homework. That SAT Solver is not very informative:
   it only returns a yes/no answer, depending on whether
   the input formula is satisfiable or not. But if the
   formula is satisfiable, we want to know how. We want
   a "witness" assignment, that is, an assignment that
   makes the formula true. We will now extend our SAT
   solver so that it also returns such an assignment,
   in case the formula is true.
   
   First, we recall some of the definitions from the
   previous homework which will be used here also:
|#

(defdata UnaryOp '~)
(defdata BinOp (enum '(& + => <=> ><)))
(defdata PropEx (oneof boolean 
                       var
                       (list UnaryOp PropEx)
                       (list PropEx Binop PropEx)))

; here's some examples of valid and invalid formulas:
(check= (PropExp '(x & y)) t)
(check= (PropExp '((~ x) & y)) t)
(check= (PropExp '((~ x) <=> (y >< z))) t)
(check= (PropExp '(~x)) nil)
(check= (PropExp '(~ x)) t)


(definec is-in-list (l :tl x :all) :bool
  (and (consp l)
       (or (equal x (first l))
           (is-in-list (rest l) x))))

(check= (is-in-list '(1 2 3) 0) nil)
(check= (is-in-list '(1 2 3) 1) t)

(definec list-union (l1 :tl l2 :tl) :tl
  (cond
   ((endp l1) l2)
   ((is-in-list l2 (first l1)) (list-union (rest l1) l2))
   (t (list-union (rest l1) (cons (first l1) l2)))))

(check= (list-union '(1 2 3) '(2 3 4)) '(1 2 3 4))
(check= (list-union '(1 2 3 7) '(1 2 3 3)) '(7 1 2 3 3))

(defdata lov (listof var))


:program


(definec set-of-vars (f :PropEx) :lov
  (cond
   ((booleanp f) nil)
   ((varp f) (list f))
   ((UnaryOpp (first f)) (set-of-vars (second f)))
   (t (list-union (set-of-vars (first f)) (set-of-vars (third f))))))

(check= (set-of-vars '((~ t) + t)) nil)
(check= (set-of-vars '(x & y)) '(x y))
(check= (set-of-vars '(~ (x & (y & z)))) '(x y z))
(check= (set-of-vars '(x & x)) '(x))


(defunc eval-varfree-formula (f)
  :input-contract (and (PropExp f) (endp (set-of-vars f)))
  :output-contract (booleanp (eval-varfree-formula f))
  (cond
   ((booleanp f) f)
   ((UnaryOpp (first f))
    (not (eval-varfree-formula (second f)))) ; the only unary op is ~
   (t (let* ((op (second f))
             (f1 (first f))
             (f2 (third f))
             (ef1 (eval-varfree-formula f1))
             (ef2 (eval-varfree-formula f2)))
        (cond
         ((equal op '&) (and ef1 ef2))
         ((equal op '+) (or ef1 ef2))
         ((equal op '=>) (implies ef1 ef2))
         ((equal op '<=>) (iff ef1 ef2))
         ((equal op '><) (xor ef1 ef2)))))))

(check= (eval-varfree-formula '((~ t) + t)) t)
(check= (eval-varfree-formula '(t & t)) t)
(check= (eval-varfree-formula '(~ (t & (t & t)))) nil)


(definec sbst (f :PropEx x :var v :boolean) :PropEx
  (cond
   ((booleanp f) f)
   ((varp f) (if (equal f x) v f))
   ((UnaryOpp (first f))
    (list '~ (sbst (second f) x v))) ; the only unary op is ~
   (t (list (sbst (first f) x v) (second f) (sbst (third f) x v)))))

(check= (sbst '(~ (x & (y & z))) 'x t) '(~ (t & (y & z))))
(check= (sbst '(~ (x & (y & x))) 'x t) '(~ (t & (y & t))))
(check= (sbst '(~ (x & (y & z))) 'w t) '(~ (x & (y & z))))

#|
II.1.

Now, define a data type "assignment" which represents an
assignment as a list of pairs (var, boolean).
|#

; answer
(defdata assignment ...


(check= (assignmentp '((x . t) (y . nil))) t)

#|
II.2.

Next, define a data type which represents the return value that we
really want from a SAT solver: a pair (v . a) where v is t or nil
depending on whether the formula is SAT (satisfiable) or UNSAT
(unsatisfiable), and a is an assignment. 
If the formula is UNSAT then a can be empty.
If the formula is SAT then we want a to be a satisfying assignment,
i.e., an assignment that makes the formula true.
|#

; answer
(defdata satreturn ...

(check= (satreturnp '(nil . ())) t)
(check= (satreturnp '(t . ((x . t) (y . nil)))) t)

#|
II.3.
Now define a new version of sat? which takes as
input a formula f and returns a satreturn, that is, a pair (v . a),
such that: either f is SAT, and then v must be t and a must be an
assignment satisfying f; or f is UNSAT, and then v must be nil
and a must also be nil (in the UNSAT case a could be anything,
but we prefer homogeneous answers). 
|#

; answer

(definec sat? (f :PropEx) :satreturn
   ...

(check= (or
         (equal (sat? '(x & y)) '(t . ((x . t) (y . t))))
         (equal (sat? '(x & y)) '(t . ((y . t) (x . t))))) t)


#|
II.4.

We have written our new SAT solver that returns assignments, and we
have tested it on a few examples, and it seems to be working fine.
That's great, but we want to test it a bit more thoroughly, using
test? (property-based testing).

In order to do this, we first need a function "asgn" which takes
a formula f and an assignment a, and returns a new formula g
obtained from f by substituting the propositional variables of
f by their truth values in a. 

Hint: asgn can use the sbst function defined earlier.
|#

; answer

(definec asgn (f :propex a :assignment) :propex
  ...
  
(check= (asgn '(x & y) '((x . nil) (y . t))) '(nil & t))


#|
II.5.

Now let's write a few property-based tests about our SAT solver.

One reasonable property to expect is:

"If our SAT solver claims that a formula f is true, and returns
satisfying assignment a for f, then the formula obtained by
applying a to f (i.e., the formula returned y (asgn f a)) is
variable-free, meaning that it has no propositional variables."

|#

; answer:
(test? ...
       
#|
II.6.

Another reasonable property to expect is:

"If our SAT solver claims that a formula f is true, and returns
satisfying assignment a for f, then the formula g obtained by
applying a to f (i.e., the formula returned y (asgn f a))
evaluates to true."

|#

; answer:
(test? ...



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part III: Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|

Each week we will ask a few questions to monitor how the course is
progressing and to solicit suggestions for improvement.

Please fill out the following form.

https://docs.google.com/forms/d/e/1FAIpQLSeh5IX3KdltzkYuI9FGu3psEa21lVj67e3XBHUZvpWdQejKvA/viewform?usp=sf_link

Feedback is anonymous and each team member should fill out
the form (only once per person).

After you fill out the form, write your name below in this file, but
not on the questionnaire. We have no way of checking if you submitted
the file, but by writing your name below you are claiming that you
did, and we'll take your word for it.

The questionnaire is worth 5 points (hence the rest of the homework
problems are worth 95 points). 

The following team members filled out the feedback survey provided by
the link above (replace the ...'s with the names of the team members
who filled out the questionnaire).

<Firstname> <LastName>
---------------------------------------------
...

|#