#|

CS 2800 Homework 8 - 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 hwk08.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.

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

|#


#|

PROVING ADMISSIBILITY

Part I:

Prove that each function defined below is admissible.
We will simplify your task so that you only have to prove 
the following two things (in this order):

1. The function terminates. To do this, construct a measure function
   and prove that it decreases. The proof may involve equational
   reasoning, but it may also require lemmas that you have to prove by
   induction.

2. The contract theorem ic => oc (where ic is the input contract and 
   oc the output contract). For this proof, you can use the definitional
   axiom of the function (but not the contract theorem!). These
   proofs typically require induction.

Contrary to Homework 7, in this homework we require formal proofs
(using equational reasoning, induction, etc., as needed) and not
just intuitive explanations in English.

Unless clearly stated otherwise, when you prove that a function m is
a measure function for some function f, you need to prove a separate
proof obligation for EACH recursive call of f, as shown in class.

If you need lemmas, identify and prove them.

Here is an example.

(defunc f (x y)
  :input-contract (and (tlp x) (natp y))
  :output-contract (natp (f x y))
  (if (endp x)
    (if (equal y 0) 
      0
      (+ 1 (f x (- y 1))))
    (+ 1 (f (rest x) y))))

ANSWER:
A measure function for f is the following:
(definec m (x :tl y :nat) :nat
  (+ (len x) y))

For the first recursive call in f, the proof obligation 
for proving Condition 4 of measure functions is:

(implies (and (tlp x)
              (natp y)
              (endp x)
              (not (equal y 0)))
         (< (m x (- y 1))
            (m x y)))

Proof:
Context:
C1. (tlp x)
C2. (natp y)
C3. (endp x)
C4. y != 0

(m x (- y 1))
= { Def m, C3, Def len, Arithmetic }
(- y 1)
< { Arithmetic }
y
= { Def m, C3, Def len, Arithmetic }
(m x y)

For the second recursive call in f, the proof obligation
for proving Condition 4 of measure functions is:

(implies (and (tlp x)
              (natp y)
              (not (endp x)))
         (< (m (rest x) y)
            (m x y)))

Proof:
C1. (tlp x)
C2. (natp y)
C3. (not (endp x))

(m (rest x) y)
= { Def m, C3 }
(+ (len (rest x)) y)
< { Arithmetic, Decreasing len axiom }
(+ (len x) y)
= { Def m }
(m x y)

Hence f terminates, and m is a measure function for it.

It remains to prove the function contract theorem, which is:

T: (implies (and (tlp x)
                 (natp y))
            (natp (f x y)))

We will prove T by induction, using the induction scheme 
that f gives rise to. Our proof obligations are:

1. (not (and (tlp x) (natp y))) => T
2. (and (tlp x) (natp y) (endp x) (equal y 0)) => T
3. (and (tlp x) (natp y) (endp x) (not (equal y 0)) T|((y (- y 1))))
   => T
4. (and (tlp x) (natp y) (not (endp x)) T|((x (rest x))))
   => T

You have to prove all four proof obligations using equational
reasoning. These proofs are not shown here.

|#

(definec f1 (n :nat) :tl
  (if (>= n 100)
      (list n)
    (cons n (f1 (+ n 1)))))

; answer:
...

(definec f2 (n :integer) :nat
  (cond
    ((< n 0) (f2 (* n -1)))
    ((equal n 0) 0)
    (t (+ 1 (f2 (- n 1))))))

; answer:
...


(definec f3 (x :nat y :nat) :nat
  (cond
    ((and (equal x 0) (equal y 0)) 0)
    ((< x y) (+ 1 (f3 y x)))
    (t (+ 2 (f3 (- x 1) y)))))

; answer:
...




; A data definition for positive rationals
(defdata posrat (range rational (0 < _)))

(definec f4 (x :rational e :posrat) :posrat
  (cond
    ((and (< x e) (> x (* e -1))) e)
    ((< x 0) (+ (* x x) (f4 (+ x e) e)))
    (t (+ (* x x) (f4 (- x e) e)))))

; answer:
...



#|
Part II: mergesort

We will also implement the merge-sort function and prove its
admissibility.

We begin by the definitions below:
|#


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

(defdata intlist (listof integer))

(intlistp '(1 . 2))
(intlistp '(1 2))
(intlistp nil)


; 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))))))

(check= (mrg nil nil) nil)
(check= (mrg '(1 2 3) nil) '(1 2 3))
(check= (mrg nil '(-1 0 10)) '(-1 0 10))
(check= (mrg '(1 2 3) '(-1 0 10)) '(-1 0 1 2 3 10))
(check= (mrg '(1 2 3) '(-1 0 0 3 10)) '(-1 0 0 1 2 3 3 10))



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

(intlistpairp '(nil . nil))
(intlistpairp '((1 2 3) . (1 2 3)))
(intlistpairp (cons nil (list '(3))))
(cons nil (list '(3)))


(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)))))


(split-aux '(1 2 3) 2)
(split-aux '(2 3) 1)
(split-aux '(3) 0)
(split-aux '(1 2 3) 1)



; 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)))))


(check= (listsplit nil) '(() . ()))
(check= (listsplit '(1 2 3)) '((1 2) 3))
(check= (listsplit '(1 2 3 4)) '((1 2) 3 4))
(check= (listsplit '(1)) '((1)))
(check= (listsplit '(1)) '((1) . nil))


(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))))))


(check= (mergesort nil) nil)
(check= (mergesort '(-1)) '(-1))
(check= (mergesort '(38 27 43 3 9 72 10)) '(3 9 10 27 38 43 72))
(check= (mergesort '(6 5 3 1 8 7 2 4)) '(1 2 3 4 5 6 7 8))
(check= (mergesort '(9 6 5 3 1 8 7 2 4)) '(1 2 3 4 5 6 7 8 9))
(check= (mergesort '(6 5 3 1 8 7 2 4 -10)) '(-10 1 2 3 4 5 6 7 8))

#|

Prove that mergesort is admissible. In particular, prove
that it is terminating, by coming up with a measure function
for it and proving the admissibility of the measure function
and the fact that it is decreasing on recursive calls of
mergesort. Also prove the contract theorem (function contract)
of mergesort.

Feel free to use without proof the following lemmata:

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

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

|#

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

|#