#|
CS 2800 Homework 8 - Summer 2018


This homework is to be done in a group of 2-3 students. 

If your group does not already exist:

 * One group member will create a group in BlackBoard
 
 * Other group members then join the group
 
 Submitting:
 
 * Homework is submitted by one group member. Therefore make sure the person
   submitting actually does so. In previous terms when everyone needed
   to submit we regularly had one person forget but the other submissions
   meant the team did not get a zero. Now if you forget, your team gets 0.
   - It wouldn't be a bad idea for group members to send confirmation 
     emails to each other to reduce anxiety.

 * Submit the homework file (this file) on Blackboard.  Do not rename 
   this file.  There will be a 10 point penalty for this.

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

Names of ALL group members: FirstName1 LastName1, FirstName2 LastName2, ...

Note: There will be a 10 pt penalty if your names do not follow 
this format.

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
For this homework you may want to use ACL2s to help you.

Technical instructions:

- open this file in ACL2s as hw08.lisp

- make sure you are in BEGINNER 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 #.....#)

- only add to the file. Do not remove or comment out anything pre-existing
  unless asked to.

- 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.
  
 - Since many of the question are in comment blocks, I'm using the unique tag
 #.....# to identify areas where you need to add your solutions.

- when done, save your file and submit it as hw08.lisp

- avoid submitting the session file (which shows your interaction with the
  theorem prover). This is not part of your solution. Only submit the lisp
  file!

|#
#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Measure Functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
A measure function m for function f satisfies the 
following conditions (as discussed in class and in lectures):
1. m has the same arguments and the same input contract as f.
2. m's output contract is (natp (m ...))
3. m is admissible.
4. On every recursive call of f, given the input contract and 
   the conditions that lead to that call, m applied to the arguments in
   the call is less than m applied to the original inputs.
   
Thus when you are asked to prove termination using a measure function, you
need to
a) Write the function (if not provided) which satisfies points 1-3
b) Write proof obligations corresponding to recursive calls in f
c) Prove the proof obligations using equational reasoning or using an approach
   we specify
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Induction Proofs 

We will be looking at inductive proofs (in various forms) for the remainder 
of the term. If you want an example of an inductive proof, look at our proof 
for Gauss' Trick.
phi_sumn: (implies (natp n) (equal (sumn n)(fsumn n)) 
where sumn is the slow way to sum numbers from 0 to n while fsumn is 
n * (n+1) / 2.

We broke that proof into 3 parts based on the induction scheme of nind

phi_sumn1: ~(natp n) => phi_sumn
phi_sumn2: (natp n) /\ (equal n 0) => phi_sumn
phi_sumn3: (natp n) /\ (not (equal n 0)) /\ phi_sumn|((n (- n 1))) => phi_sumn

Notice that phi_sumn1 is the "bad data" or ~IC case which we ignored when doing
equational reasoning.
            
You'll also notice that since the parts imply phi_sumn
you should swap in the ENTIRE phi_sumn conjecture and use
exportation to get your context. Exportation means we just get 
a sequence of ands which imply (sumn n) = (fsumn n) for each of the 
conjectures. For example, phi_sumn2 is 
(natp n) /\ (equal n 0) => ((natp n) => (equal (sumn n)(fsumn n)))
or
(natp n) /\ (equal n 0) /\ (natp n) => (equal (sumn n)(fsumn n))) 

I will use the term proof obligations to refer to conjectures used to prove a
particular conjecture (eg "=> phi_sumn") while the induction scheme can be applied
to any inductive proof (eg "=> phi" where phi is not specified).

For each induction scheme conjecture we add the conditions that 
lead to a particular branch. We also assume that the 
conjecture holds for the next recursive call when a recursive call (or calls) occurs. 
Thus we substitutethe arguments of the recursive call into the original conjecture.

For inductive proofs you will always be expected to write proof obligations
or induction schemes, clearly label where these came from, and then prove
the various parts.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|#

;;==========================================
; Section 1: Induction schemes
;;==========================================


#|

Below you are given the proof obligations generated by
induction schemes. Your job is to: 
1) define functions, using defunc, that give rise to these induction schemes. 
phi|(...) denotes phi under substitution ... . 

2) For each function you write, also write a measure function that could
be used to prove your function works (you can do those proofs for practice
but they aren't required here)

For these functions (f1-f5) you do not need to provide
tests (i.e., no check= forms are required). It is also
a good idea to make these functions as simple as possible.

Example
1. (not (integerp x)) => phi
2. (and (integerp x) (equal x 0)) => phi
3. (and (integerp x) (not (equal x 0))(> x 0))) phi|((x (- x 1))))  => phi
4. (and (integerp x) (not (equal x 0))(not (> x 0)) phi|((x (+ x 1))))  => phi


;;(defunc f0 (x)
  :input-contract (integerp x)
  :output-contract t
  (cond ((equal x 0)  x)
        ((> x 0)      (f1 (- x 1)))
        (t            (f1 (+ x 1)))))

NOTE: The induction scheme below has been slightly simplified to avoid
the expression being too unruly (eg for obligation 3 you would see 
(not (equal x 1)))

f1)
1. (not (posp x)) => phi
2. (and (posp x) (equal x 1)) => phi
3. (and (posp x) (equal x 2)) => phi
4. (and (posp x) (equal x 3)) => phi
5. (and (posp x) (not (equal x 1)) (not (equal x 2))
(not (equal x 3)) phi|((x (- x 3))))  => phi

|#

;#.....#


#|
f2)
1. (not (and (listp x)(listp y))) => phi
2. (and (listp x)(listp y)(endp x)(endp y)) => phi
3. (and (listp x)(listp y)(endp x))(phi|((y (rest y))) => phi
4. (and (listp x)(listp y)(not (endp x))(endp y)(phi|((x (rest x))(y (cons (first x) y))) 
   => phi
|#
;#.....#


#|
f3)
1. (not (and (listp x)(natp y))) => phi
2. (and (listp x)(natp y)(endp x)(equal y 0)) => phi
3. (and (listp x)(natp y)(not (and (endp x)(equal y 0)))
        (endp x) phi|((y (- y 1)))) => phi
4. (and (listp x)(natp y)(not (and (endp x)(equal y 0)))(not (endp x))
        (equal y 0) phi|((x (rest x)))) => phi
5. (and (listp x)(natp y)(not (and (endp x)(equal y 0)))(not (endp x))
        (not (equal y 0))  phi|((x (rest x))(y (- y 1))) )
    => phi
|#

;#.....#


;; The following functions are not trivial to admit into ACL2s in logic
;; mode.  For f4 and f5, just convince yourself that the terminate and IC=>OC
:program


#|
f4)
1. (not (integerp x)) => phi
2. (and (integerp x) (< x -1)) => phi
4. (and (integerp x) (not (< x -1)) 
        phi|((x (- x 1))) phi|((x (- x 2)))  => phi

|#

;#.....#

#|
f5)
1. (not (and (listp x) (integerp y))) => phi
2. (and (listp x) (integerp y) (endp x) (equal y -1)) => phi
3. (and (listp x) (integerp y) (not (and (endp x) (equal y -1)))
        (endp x)(< y -1) phi|((y (+ y 1)))) => phi 
4. (and (listp x) (integerp y) (not (and (endp x) (equal y -1)))
        (not (and (endp x)(< y -1)))
        (endp x) (phi|((x (cons 1 x)) (y (- y 1))))) => phi 
5. (and (listp x) (integerp y) (not (and (endp x) (equal y -1)))
        (not (and (endp x)(< y -1)))
        (not (endp x)) (phi|((x (rest x))))) => phi 

Hint: phi|((a (rest a)) (b b)) is the same as 
      phi|((a (rest a))).  You can leave off variable parameters 
      that don't change.
|#

;#.....#

:logic
#|
==========================================
SECTION 2: Pre-defined Functions and Warm Up

We start with some familiar definitions just in case they
are useful. You will be asked to
define functions later on. Make sure to use defunc.
==========================================
(defunc listp (x)
  :input-contract t
  :output-contract (booleanp (listp x))
  (if (consp x)
      (listp (rest x))
    (equal x nil)))

(defunc app (a b) 
  :input-contract (and (listp a) (listp b))
  :output-contract (listp (app a b))
  (if (endp a)
      b
    (cons (first a) (app (rest a) b))))

(defunc rev (a) 
  :input-contract (listp a) 
  :output-contract (listp (rev a))
  (if (endp a)
      nil
    (app (rev (rest a)) (list (first a)))))

(defunc len (a) 
  :input-contract t 
  :output-contract (natp (len a))
  (if (atom a)
      0
    (+ 1 (len (rest a)))))
 
(defunc in (a X) 
  :input-contract (listp x)
  :output-contract (booleanp (in a X))
  (if (endp x)
      nil
    (or (equal a (first X))
        (in a (rest X)))))

|#

:logic
;; Assume by "Def of lor" that each element is a rational
;; and a lor is (cons rational lor) | nil
(defdata lor (listof rational))

(defthm phi_applen (implies (and (listp l1) (listp l2))
                            (equal (len (app l1 l2))
                                   (+ (len l1)(len l2)))))
#|
PROVE
Let's do a warm-up proof (NOT GRADED)

Prove phi_applen: (implies (and (listp l1) (listp l2))
                           (equal (len (app l1 l2))
                                  (+ (len l1)(len l2))))
Make sure you clearly identify the induction scheme you are
using and what function the IS is from.
#.....#

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; orderedp: lor -> boolean
;; (orderedp l) takes a list of rationals
;; and returns true if and only if the elements 
;; are in non-decreasing order (ie they are ordered)
(defunc orderedp (l)
  :input-contract (lorp l)
  :output-contract (booleanp (orderedp l))
  (or (endp l)
      (endp (rest l))
      (and (<= (first l) (second l))
           (orderedp (rest l)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; del: Any x List -> List
;; (del e l) takes an element e and a list l
;; and removes the FIRST occurance of e from l
;; If e is not in l then l is returned.
(defunc del (e l)
  :input-contract (listp l)
  :output-contract (listp (del e l))
  (if (endp l)
    l
    (if (equal e (first l))
      (rest l)
      (cons (first l) (del e (rest l))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; perm: List x List -> List
;; (perm l1 l2) takes two lists (l1 and l2) and
;; returns true if and only if l1 and l2 have
;; the same elements (and the same number of each)
;; Essentially, is l2 a reordering of l1.
(defunc perm (l1 l2)
  :input-contract (and (listp l1)(listp l2))
  :output-contract (booleanp (perm l1 l2))
  (if (equal l1 l2)
    t
    (if (endp l1)
      (endp l2)
      (and (in (first l1) l2)
           (perm (rest l1) (del (first l1) l2))))))


;;==========================================
; Section 3: Permutation "Fun"
;;==========================================
#|
As a general rule, proofs involving permutations seem simple
but are a royal pain to prove (if you don't believe me, ask someone
who took 2800 this past Spring. They did a lot of permutation proofs)
Let's start with something "simple".  Prove the following

phi_perm_appcons: (listp x)/\(listp y)=> (perm (app x (cons e y))(cons e (app x y)))

** You may assume (perm l l) is always true.
   (listp l) => (perm l l)
** You may also assume (perm x y)/\(perm y z) => (perm x z) is a theorem
   (listp x)/\ (listp y)/\(listp z) /\ (perm x y)/\ (perm y z)=> (perm x z)

#.....#

Now prove the following:
phi_perm_app: (listp x)/\(listp y) => (perm (app x y)(app y x))

#.....#




Finally, you may wonder why you had to prove these.  Let's do the following proof to see:
phi_perm_rev: (listp x) => (perm x (rev x))

#.....#

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; A BUNCH OF FUNCTIONS TO BE USED IN THE PROOFS BELOW
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defdata gpos (range integer (2 <= _)))
;; Ignore
(defthm phi_shrink_factor (implies (and (gposp n)(gposp f)(gposp (/ n f)))
                                   (< (/ n f) n)))
(defdata logp (listof gpos))

;; GIVEN:
;; factors-help : gpos x gpos -> Lop
;; returns a list containing all PRIME factors of n including (possibly) 
;; n and 1.
(defunc factors-help (n p)
  :input-contract (and (gposp n) (gposp p))
  :output-contract (logpp (factors-help n p))
  (cond ((> p n) nil)
        ((equal p n) (list n))
        ((gposp (/ n p)) (cons p (factors-help (/ n p) p)))
        (t              (factors-help n (+ p 1)))))


;; GIVEN
;; factors : Pos -> Lop
;; returns a list containing all PRIME factors of n including (possibly) 
;; n and 1. 
(defunc factors (n)
    :input-contract (gposp n)
    :output-contract (logpp (factors n))
    (let ((fh (factors-help n 2)))
      (if (endp fh) (list n) fh)))

;; Note the factors for 12 *could* be listed as 1 2 3 4 6 12 but
;; really 12 is uniquely represented as the product of non-decreasing 
;; prime numbers: 2*2*3.  Thus factors will return '(2 2 3)  
;; 13 is prime so it isn't decomposed into other
;; primes and '(13) is returned. 
;; If you get the same values but in a different order, feel free to 
;; change the tests.
(check= (factors 2)'(2))
(check= (factors 4)'(2 2))
(check= (factors 6)'(2 3))
(check= (factors 12)'(2 2 3))
(check= (factors 13)'(13))

;; GIVEN
;; Defined in previous functions. Removes
;; the first instance of an element in a list
(defunc delete (e l)
  :input-contract (listp l)
  :output-contract (listp (delete e l))
  (if (endp l)
    l
    (if (equal e (first l))
      (rest l)
      (cons (first l)(delete e (rest l))))))

;; Ignore
(sig delete (all (listof :b)) => (listof :b))

;; GIVEN
;; intersect: list x list -> list
;; (intersect l1 l2) returns a list containing every element 
;; that is in both lists l1 and l2.
(defunc intersect (l1 l2)
    :input-contract (and (listp l1) (listp l2))
    :output-contract (listp (intersect l1 l2))
    (cond ((endp l1) l1)
          ((in (first l1) l2) 
           (cons (first l1)
                 (intersect (rest l1) 
                            (delete (first l1) l2))))
          (t (intersect (rest l1) l2))))

;; GIVEN
;; coprime: pos x pos -> boolean
;; determines whether two positive integers a and b are coprime
(defunc coprime (a b)
    :input-contract (and (gposp a) (gposp b))
    :output-contract (booleanp (coprime a b))
    (endp (intersect (factors a) (factors b))))

;; this line is for ACL2s
(sig intersect ((listof :b) (listof :b)) => (listof :b))

;; GIVEN
;; prod-list: lop -> Pos
;; (prod-list lp) multiplies all values in list lp together
;; If the list is emtpy, return 1.
(defunc prod-list (lgp)
  :input-contract (logpp lgp)
  :output-contract (posp (prod-list lgp))
  (if (endp lgp)
    1
    (* (first lgp)(prod-list (rest lgp)))))

;; GIVEN
;; gcd: pos x pos -> pos
;; (gcd a b) determines the greatest common divisor for a and b.
;; Do you remember how to calculate that with prime factors?
(defunc gcd (a b)
    :input-contract (and (gposp a) (gposp b))
    :output-contract (posp (gcd a b))
    ;; SOLUTION
    (prod-list (intersect (factors a) (factors b))))

(check= (gcd 7 6) 1)
(check= (gcd 8 6) 2)
(check= (gcd 12 6) 6)
(check= (gcd 30 12) 6)
(check= (gcd 30 28) 2)
(check= (gcd 35 28) 7)
(test? (implies (and (gposp a)(gposp b))
                (equal (gcd a b)(gcd b a))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; sortedp: LOR x LOR -> Boolean
;; (sortedp origL sortL) takes the original list
;; and the theoretically sorted list (sortL)
;; and determines if sortL is a sorteding
;; of the original list.
(defunc sortedp (origL sortL )
  :input-contract (and (lorp origL)(lorp sortL))
  :output-contract (booleanp (sortedp origL sortL))
  (and (perm origL sortL)(orderedp sortL)))

;; less: rational x lor -> lor
;; (less x lst) makes a list of all elements in lst that
;; are less than x
(defunc less (x lst)
  :input-contract (and (rationalp x) (lorp lst))
  :output-contract (lorp (less x lst))
  (cond ((endp lst) ())
        ((< (first lst) x)
         (cons (first lst) (less x (rest lst))))
        (t (less x (rest lst)))))

;; not-less: rational x lor -> lor
;; (not-less x lst) makes a list of all elements in lst that
;; are not-less than x
(defunc not-less (x lst)
  :input-contract (and (rationalp x) (lorp lst))
  :output-contract (lorp (not-less x lst))
  (cond ((endp lst) ())
        ((< (first lst) x)
         (not-less x (rest lst)))
        (t (cons (first lst) (not-less x (rest lst))))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; qsort: LOR -> LOR
;; (qsort l)....or quicksort takes the original list of rationals l
;; and arranges the elements so the list is sorted.
;; It does this by taking the first element (pivot element)
;; and putting all elements < the pivot before it, and all
;; elements >= the pivot after the pivot. qsort is then
;; called on the < list and the >= list. Thus the list is eventually sorted
(defunc qsort (l)
  :input-contract (lorp l)
  :output-contract (lorp (qsort l))
  (if (endp l)  
    l
    (let ((less (less (first l) (rest l)))
          (gte (not-less (first l) (rest l))))
      (app (qsort less) (cons (first l) (qsort gte))))))

#|
;;============================================
;; SECTION 4: FACTORS.....AGAIN
Remember HW06?  I threw this random theorem at you:
Prove A1-old: (iff (in b (factors a)) (natp (/ a b)))
....well our assumption actually wasn't true.
It should have been 

      A1: (implies (in b (factors a)) (natp (/ a b)))

or we would need to prove b is a prime number.

Well I can't have such a glaring assumption.  Prove the revised A1.
However, try doing with with a straight equational reasoning proof.
You should get stuck and need a lemma since factors is not recursive.
- Figure out the lemma (L1) you need....it will look very similar to A1.
  Also notice that you may need to guard against the factor being checked (p)
  being greater than b.
- Assume L1 is true and finish the proof
Prove L1
- First, you should decide what induction scheme to use. What
  conditions would be useful to break your proof down into parts?
  (this function does not have to appear in A1).
- Explicitly write your induction scheme and the function it comes from
- Prove each of the proof obligations

#.....#


|#

;;============================================
;; SECTION 5: QSORT - Part 1 (part 2 in HW09)
;; Look at the functions less, not-less and qsort
;; We will prove these functions terminate other theorems
;; We will then revisit qsort for HW09 to finish off our proof that (sortedp (qsort l)) 
;; is true.

#|
Prove less terminates by giving a measure function and then prove the measure
function decreases with each recursive call.....we will assume not-less terminates
provided less terminates.
#.....#

Now prove qsort terminates.....notice that (less l) is not guaranteed
to be a shorter length list than l (it is but you would need to prove this
by finding an appropriate conjecture and proving the conjecture). Notice the length
of (less l), (not-less l) and l? 
If you have nearly identical conjectures for less and not-less, you only need to do 
the proof for one of these.

You can temporarily assume the following theorem
     T1. (lorp l) => ((len l) = (len (qsort l)))


#.....#


Let's not just assume T1. Prove it is true....you will need a lemma....again think about
how the length of l, (less r l) and (not-less r l) all relate.
I also know I stump a lot of students when I ask them to prove things about qsort without guiding them.
Following the questions below should lead you to how to solve the main proof.

Write the induction scheme for qsort....remember you get an inductive assumption for EACH recursive call

#.....#


Now prove T1.  If you need a lemma (L5), write it out BEFORE your main proof just so you can use it.
Assume your lemma is valid, finish the proof, and then prove the lemma.

#.....#

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SECTION 6: Bubble Sort (HUGE NO CREDIT CHALLENGE)
;; Check out this known slow sorting function.
;; I have to throw things into program mode to let it
;; be admitted. Show that you are smarter than a computer
;; Prove that the function terminates. 
;; How do you know bsort is getting closer to a sorted list?
;; You may need to write another function
;; Even if you get a rough outline of the proof, that would
;; be a great exercise to demonstrate to yourself that you 
;; know what you are doing, but it's well outside of the scope
;; of this already long assignment.
;; DO NOT DO THIS PROBLEM UNTIL YOU FINISH THE REST OF THE ASSIGNMENT
;; It really is worth no points.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

:program

(defunc bubble (l)
  :input-contract (lorp l)
  :output-contract (lorp (bubble l))
  (cond ((endp l) l)
        ((endp (rest l)) l)
        ((> (first l)(second l))(cons (second l)(bubble (cons (first l) (rest (rest l))))))
        (t (cons (first l)(bubble (rest l))))))

(defunc bsort (l)
  :input-contract (lorp l)
  :output-contract (lorp (bsort l))
  (if (orderedp l)
    l
    (bsort (bubble l))))
;; #.....#