#|

CS 2800 Homework 7 - 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: 

When proving the claims below, you may use any of the propositional logic
proof rules that we established in class, to transform your claim _prior_ 
to proving it using our proof format. For example, you can use:
 - proof by cases
 - proof of disjunctive claims
 - proof of conjunctive claims
 - generalization
etc.

When you do this, preface your proof by saying something like:
"by the propositional logic rule ... our claim becomes ...".
If you use proof by cases, you may generate multiple proof
obligations. Then, instead of having just one claim to prove,
you may have two, or more. Number those newly generated claims
and state them clearly, then go ahead and prove each one of them
separately.

|#





#|
Assume that evenp and oddp are defined as follows:

(definec evenp (n :integer) :bool
  (integerp (/ n 2)))

(definec oddp (n :integer) :bool
  (not (evenp n)))
|#


#|
7.1.
Prove the following claim:

Claim 71:
(implies (natp n)
         (or (evenp n) (oddp n)))

;; ANSWER:
...
QED

|#


#|
7.2.
Can you generalize the claim that you proved in 7.1, and how?
You may either answer "no", or "yes". In the case of "yes",
provide the generalized claim and prove it.

;; ANSWER:
...
QED

|#


;; We define the following functions:

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

(definec aapp (x :tl y :tl) :tl
  (if (endp x) y
    (cons (first x) (aapp (rest x) y))))

(definec dup-list (x :tl) :tl
  (aapp x x))

"
We will assume in is defined as:

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

(definec del (a :all X :tl) :tl
  (cond ((endp X) nil)
        ((equal a (car X)) (del a (cdr X)))
        (t (cons (car X) (del a (cdr X))))))


;; We prove the following theorems about
;; these functions. We can use those
;; theorems as lemmas in our proofs!

(defthm llen-aapp
  (implies (and (tlp x) (tlp y))
           (equal (llen (aapp x y))
                  (+ (llen x) (llen y)))))

(defthm plus-twice
  (implies (rationalp x)
           (equal (+ x x) (* 2 x))))

(defthm even-double
  (implies (natp x)
           (evenp (* 2 x))))



#|
7.3.
Prove the following claim. If the claim requires
contract completion, complete it first. Show the
contract completion step explicitly.

Claim 73:
     (implies (consp x)
              (and (< 0 (llen (dup-list x)))
                   (evenp (llen (dup-list x)))))

;; ANSWER:
...
QED
|#


#|
7.4.
Prove the following claim. If the claim requires
contract completion, complete it first. Show the
contract completion step explicitly.

Claim 74:
(implies
 (and (tlp x)
      (tlp y)
      (endp x))
 (equal (llen (del a (aapp x y)))
        (+ (llen (del a x)) (llen (del a y)))))

;; ANSWER:
...
QED
|#


#|
7.5.
Prove the following claim. If the claim requires
contract completion, complete it first. Show the
contract completion and exportation step explicitly.

Claim 75:
(implies
 (tlp x)
 (implies
  (and (not (endp x))
       (equal a (car x))
       (implies (tlp (rest x))
                (implies
                 (tlp y)
                 (equal (llen (del a (aapp (rest x) y)))
                        (+ (llen (del a (rest x))) (llen (del a y)))))))
  (equal (llen (del a (aapp x y)))
         (+ (llen (del a x)) (llen (del a y))))))
;; ANSWER:
...
QED
|#


#|
7.6.
Prove the following claim. If the claim requires
contract completion, complete it first. Show the
contract completion and exportation step explicitly.

Claim 76:
(implies
 (tlp y)
 (implies (and (not (endp x))
               (not (equal a (car x)))
               (implies (and (tlp (rest x))
                             (tlp y))
                        (equal (llen (del a (aapp (rest x) y)))
                               (+ (llen (del a (rest x))) (llen (del a y))))))
          (equal (llen (del a (aapp x y)))
                 (+ (llen (del a x)) (llen (del a y))))))

;; ANSWER:
...
QED
|#


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;  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/1FAIpQLSe3aXMnKKtMkWNTUKTuSCYUxc52qlozaXM3f9urukE7gjDp1w/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>
...
...
...
|#