#|

CS 2800 Homework 6 - 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 hwk06.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.



EQUATIONAL REASONING INSTRUCTIONS

The questions on equational reasoning ask for equational proofs about
ACL2s programs. These equational proofs must be in the format presented
in the lectures (slides, e.g., examples 5, 6, 7, etc) and in the lecture
notes.

You may use the equational reasoning proof checker presented in the labs:
http://checker.atwalter.com/. 
Please do the labs, go to the labs, and familiarize yourself with
the proof checker. If you encounter problems which
you think might be due to the proof checker having bugs (which is
certainly possible) please let us know by posting on piazza.

We will not require you to check your proofs on the proof checker
before submitting them. But feel free to do so. You will not get
extra points for using the proof checker. You will not lose points
if you don't use it (as long as your proofs are correct).

Please note that the proof checker is a new tool that we are releasing 
for the first time, so it might have bugs and usage limitations 
(that we would like to know about, so feedback is welcome!).

Also note that the proof checker server might overload if you all
try to submit your requests at the last minute. Again, the proof
checker is provided for your convenience but you are not required
to use it. If you do use it, and it checks your proofs OK, please
write a comment in your homework submission saying something like
"Proof checked by the proof checker" so that we know.

|#

#|

Consider the following functions:

|#

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

(definec in (a :all l :tl) :bool
  (if (endp l)
      nil
    (or (equal a (car l)) (in a (cdr l)))))
    
(defunc aapp (x y)
  :input-contract (and (tlp x) (tlp y))
  :output-contract (tlp (aapp x y))
  (if (endp x)
      y
    (cons (car x) (aapp (cdr x) y))))

(definec rrev (x :tl) :tl
  (if (endp x)
    nil
    (aapp (rrev (cdr x)) (list (car x)))))

#|
Provide proofs for each of the following claims about 
these functions. 
|#

#|
Claim 1:
(implies (endp x)
         (implies (>= (llen y)  0)
                  (>= (llen (aapp x y)) (llen x))))

                  
...

QED
|#


#|
Claim 2:
(implies (endp x)
         (>= (llen (aapp x y)) (llen x)))


...

QED
|#



#|
Claim 3:
(implies (consp x)
        (implies (>= (llen (aapp (cdr x) y)) (llen (cdr x)))
                  (>= (llen (aapp x y)) (llen x))))


...

QED
|#


#|
Claim 4:
(implies (in x l2)
         (implies (consp l1)
                  (implies (implies (in x l2) 
                                    (in x (cons (car l1) (aapp (cdr l1) l2))))
                           (in x (aapp l1 l2)))))

...

QED
|#


#|
Claim 5:
(implies (in x l)
         (implies (endp l)
                  (in x (rrev l))))


...

QED
|#


#|

For Claim 6, you are free to use the following two lemmas:
(see the lab to see what is the way to appeal to a lemma in the proof
checker)

|#

; lemmas:
(defthm in-aapp-1
  (implies (and (tlp l1)
                (tlp l2)
		(in x l1))
           (in x (aapp l1 l2))))

(defthm in-aapp-2
  (implies (and (tlp l1)
                (tlp l2)
		(in x l2))
           (in x (aapp l1 l2))))

#|
Claim 6:
(implies (in x l)
	 (implies (consp l)
		  (implies (not (equal x (car l)))
                           (implies (implies (and (tlp (cdr l)) (in x (cdr l)))
                                             (in x (rrev (cdr l))))
			            (in x (rrev l))))))


...

QED
|#

#|

For Claim 7, you are free to use the following lemma:
(do not use the lemmas available for Claim 6; just use Lemma in-aapp
below)

|#

; lemma:
(defthm in-aapp
  (implies (and (tlp l1)
                (tlp l2))
           (equal (in x (aapp l1 l2))
                  (or (in x l1) (in x l2)))))


#|
Claim 7:
(implies (in x l)
	 (implies (consp l)
		  (implies (not (equal x (car l)))
                           (implies (implies (and (tlp (cdr l)) (in x (cdr l)))
                                             (in x (rrev (cdr l))))
			            (in x (rrev l))))))


...

QED
|#

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

|#