#|

CS 2800 Homework 9 - 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 hwk09.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 NOT need to use ACL2s. However, you could
use the Eclipse/ACL2s text editor to write up your solution and
you may want to use ACL2s to help you check your answers.

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

|#


#|

	mergesort (continued from last homework)

We will be doing more proofs about mergesort.

We require formal proofs, in the sense that we defined in class
and also used for instance in homework 8.

You may want to first do a fast/pro proof, to identify any lemmas
that you might need, and to also identify the induction scheme
that you will need. But you still have to do the formal proof
after the fast/pro proof.

You will also need to prove any lemmas that you introduce.
We require formal definitions and formal proofs of all lemmas too.

As usual, feel free to use shorthand notation, such as & for and, 
=> for implies, ~ for not, etc.

|#


(set-defunc-termination-strictp nil)
(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)

(defdata intlist (listof integer))

; mrg takes two lists and merges them in order
(definec mrg (x :intlist y :intlist) :intlist
  (cond
   ((endp x) y)
   ((endp y) x)
   ((< (car x) (car y)) (cons (car x) (mrg (cdr x) y)))
   (t (cons (car y) (mrg x (cdr y))))))

; a pair of lists, used in splitting a list into two parts:
(defdata intlistpair (cons intlist intlist))

(definec split-aux (x :intlist n :nat) :intlistpair
  (cond
   ((endp x) '(nil . nil))
   ((equal n 0) (cons nil x))
   (t (let*
        ((p (split-aux (cdr x) (- n 1)))
         (x1 (car p))
         (x2 (cdr p)))
        (cons (cons (car x) x1) x2)))))

; takes a list and splits it roughly in the middle
(definec listsplit (x :intlist) :intlistpair
  (cond
   ((endp x) '(nil . nil))
   ((endp (cdr x)) (cons x nil))
   ((evenp (len x)) (split-aux x (/ (len x) 2)))
   (t (split-aux x (/ (+ (len x) 1) 2)))))

(definec mergesort (x :intlist) :intlist
  (cond
   ((endp x) nil)
   ((endp (cdr x)) x)
   (t (let*
        ((p (listsplit x))
         (x1 (car p))
         (x2 (cdr p)))
        (mrg (mergesort x1) (mergesort x2))))))

#|
1: Prove lemma L1:

L1: (intlistp x) & (natp n) & (n <= (len x))
        => (len (car (split-aux x n))) = n

Note: this is a modified (and stronger) version of the L1 given in HWK08.
It turns that some of the assumptions used there are not needed. Prove this
version.
|#

; answer:

...


#|
2: Prove lemma L2:

L2: (intlistp x) & (natp n) & (n <= (len x))
        => (len (cdr (split-aux x n))) = (len x) - n

|#

; answer:

...


#|
Next, we want to prove that the result of mergesort is ordered.
Recall the definition of ordered:
|#

(definec ordered (L :intlist) :bool
  (or (endp L)
      (endp (cdr L))
      (and (<= (car L) (second L))
           (ordered (cdr L)))))



#|
3. Prove the theorem T:

T: (intlistp x) => (ordered (mergesort x))

|#

; answer:

...



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 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/1FAIpQLScuSizMAwYcWK8c-k1Audesnj0b9S9KQkaJWgm--pRo2BBWJQ/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>
---------------------------------------------
...

|#