#|

CS 2800 Homework 6 - Fall 2019

This homework is done in groups: instructions as per homework 02.
In particular:

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

 * YOU MUST LIST THE NAMES OF ALL GROUP MEMBERS SUBMITTING THIS HOMEWORK:

Names of ALL group members: ...




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

Technical and programming instructions: as per previous homeworks,
but change file names appropriately.

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

  NOT     ~

  AND     /\ or & or *
  OR      \/ or | or +

  IMPLIES => or ->

  EQUIV   <=>
  XOR     ><  or XOR

|#

#|
Part I: Boolean formulas
|#

#|
6.1.

(a)
Simplify the Boolean formula
      ((p & q) + (r => ~q)) => (p XOR r)
That is, provide an equivalent, but simpler (shorter) formula.
Simplify as much as you can. You may use equational reasoning
for your simplification, or you may use the truth table method.
In both cases, show your work (i.e., either the equational proof,
or the truth table).
ANSWER:
|#
"
...
"
#|
(b)
Write as an ACL2s theorem the fact that the above formula
is equivalent to the simplified formula you provided:
|#
;; ANSWER:
(thm ...
             
#|
6.1. continued

(c)
Put the above formula in DNF: make your DNF as simple as possible:
ANSWER:
|#
"
...
"
#|
(d)
Put the above formula in CNF: make your CNF as simple as possible
(do not use Tseytin's method, do not introduce extra variables):
ANSWER:
|#
"
...
"
#|
(e)
Write as two ACL2s theorems the fact that your DNF and CNF are
equivalent to the original formula:
|#
;; ANSWER:
(thm ...

(thm ...



#|
6.2.

Answer the same questions (a),(b),(c),(d),(e) as in 6.1, for the
formula:
        ((x1 XOR x2) => (x3 XOR x4)) & x1 & x3
(a)
ANSWER:
|#
"
...
"
#|
(b)
|#
;; ANSWER:
(thm ...

#|
(c) DNF:
|#
"
...
"
...


#|
Part II: Substitutions
|#

#|
6.3. 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. The substitution ((x a) (y b) (x c))
is not legal because x appears twice. But ((x a) (y a)) is legal.

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
attempt to evaluate what you get after applying the substitution.

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

(The two line format E |
                     S
makes it easier to distinguish between E, the expression on
which we apply the substitution, and S, the substitution applied
to E.)

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

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. 

(let ((x 1)) (+ x y)) | ((y x))

Replace the "..."'s below with your answers.
|#
"
6.3.1. (g f 'f f) |
       ((f (list a b)) (g f))
       ANSWER:
	...

6.3.2. (+ (* x y) (- w z)) |
       ((y (list x)) (x (list y)) (w z) (z w))
       ANSWER:
	...

6.3.3. (let ((x 3)) (f (g x y) (h y x))) |
       ((f g) (h f) (x (f (g y x))) (y x))
       ANSWER:
	...

6.3.4. (f g 'h) |
       ((g (list a b)) ('h g))
       ANSWER:
	...

6.3.5. (f (f (natp (cons x y)) (natp '(cons x y))) (- a b)) |
       ((a 43) (b (* c d)) (y (cons x z)) (x x))
       ANSWER:
	...
"


#|
Part III: Equational reasoning

EQUATIONAL REASONING INSTRUCTIONS

Use the same proof format as we used in lectures, slides, and lab 06.
See instructions of lab 06 for more details on how proofs should look like.

As help, you may use the proof checker: http://checker.atwalter.com/.
We will not require you to check your proofs on the proof checker
before submitting them. But feel free to do so for your own benefit.
You will not get extra points for using the proof checker. You will not
lose points for not using either.

The proof checker is software still under development. As such, it
contains bugs, its error reporting leaves a lot to be desired, etc.
If you find using the proof checker is a source of more frustration
than help, then don't use it. Once you get the hang of it, it can
be helpful.

Feedback about the proof checker, bug reports, etc., are welcome!

Also note that the proof checker server might overload if you all
try to submit your requests at the same time. Again, the proof
checker is provided only for your convenience. If you do use it, 
and it checks that your proof is OK, please write a comment in your
problem submission like "Proof checked by the proof checker",
so that we know.

Important note: if your proof passes the proof checker, it does not
necessarily mean that it's correct! We will assess your proof
independently of whether it passes or does not pass the proof checker.
|#


;; Consider the function prefix defined below:
(definec prefix (l :tl n :nat) :tl
  (cond
   ((equal n 0) nil)
   ((endp l) nil)
   (t (cons (first l) (prefix (rest l) (- n 1))))))

#|
We want to prove a bunch of properties about prefix.
For each of the properties listed below:
(a) State whether the property requires contract completion and
if so complete the contracts as necessary.
(b) State whether the property (after any necessary contract
completions) is true. If you claim it is not true, provide a
counter example.
(c) If you stated in (b) that your property is true, prove it
using the proof format as described above.

In your proofs you may use any of theorems that we proved in
class, or that you proved previously in this homework.

Hint: several proofs below become much easier if you use 
previously proven theorems in this homework.

You may also introduce new lemmas that you may want to use
in your proofs. If you do introduce a lemma, you must prove it!

End each of your proofs with "QED" as shown below.
|#


#|
6.4.
(implies (and (tlp l) (equal n 0))
         (equal (prefix l n) nil))
;; ANSWER:
(a) ...
(b) ...
(c)
Claim 64:
...

Context:
...

Goal: ...

Proof:
...

QED
|#


#|
6.5.
(implies (and (natp n) (equal l nil))
         (equal (prefix l n) nil))
;; ANSWER:
(a) ...
(b) ...
(c)
Claim 65:
...

...

...

QED
|#


#|
6.6.
(implies (and (tlp l) (not (endp l)))
         (equal (first l) (first (prefix l n))))
;; ANSWER:
...
|#


#|
6.7.
(implies (and (tlp l) (not (endp l)) (> n 0))
         (equal (first (prefix l n)) (first l)))
;; ANSWER:
...
|#


#|
6.8.
(implies (and (tlp l) (not (endp l)) (> n 0))
         (consp (prefix l n)))
;; ANSWER:
...
|#



#|
For the next problems, assume that function "in" is
defined as follows:

(definec in (a :all X :tl) :bool
  (and (consp X)
       (or (equal a (first X))
           (in a (rest X)))))
|#


#|
6.9.
(implies (and (tlp l) (not (endp l)) (> n 0))
         (in (first l) (prefix l n)))
;; ANSWER:
...
|#


#|
For the next problems, we define llen:
|#

(definec llen (x :tl) :nat
  (if (endp x)
      0
    (+ 1 (llen (cdr x)))))

#|
6.10.
(implies (and (tlp l) (equal n 0))
         (equal (llen (prefix l n)) 0))
;; ANSWER:
...
|#


#|
6.11.
We would like to prove that the length of (prefix l n) is equal to n,
assuming n is within bounds. But we don't yet have the machinery to
be able to do that. It is instructive for you to try to prove it, and
see what happens. This will help you better appreciate the power of
induction later on.

For now, we can try to prove this claim instead:
(implies (and (tlp l) (consp l) (equal n (llen l))
              (implies (and (tlp l) (consp l) (tlp (rest l))
                            (natp n) (> n 0))
                       (equal (llen (prefix (rest l) (- n 1))) (- n 1))))
         (equal (llen (prefix l n)) n))

Hint: This proof becomes easier with the help of a lemma.

;; ANSWER:
...
|#




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;  Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
Each we'll take a short survey to monitor homework difficulty and to solicit feedback.

This survey is anonymous. We don't collect names, emails, etc. Each student responds individually. 
If you answer all mandatory questions, you get 5 points for this homework set. 
You report who among your team answered the survey in your homework answers, and we trust you 
that you reported this truthfully. 

Please fill out the following form (one response per team member):

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

Report here who in your team filled the form:

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>
...
...
...
|#