#|
CS 2800 Homework 10 - Fall 2017


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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
 Inductive Proofs:
 - For all proofs below, solutions must be in the format described in class and
   in the notes. This includes:
     * Explicitly identifying an induction scheme and the function that gives
       rise to it.
     * Labeling general context (C1, C2....) and derived context.
     * Providing justifications for each piece of derived context.
     * Explicitly identifying axioms and theorems used
     * The if axioms and theorem substitutions are not required. You can use
       any other shortcuts previously identified.
     * PL can be given as justification for any propositional logic rules with the
      exceptions of Modus Ponens (MP) and Modus Tollens (MT)
     * Hocus Pocus (HP) is not permissible justification.
     * All arithmetic rules can be justified by writing "Arithmetic".
     
Previous homeworks (such as HW05) identify these requirements in more detail.

|#

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

Technical instructions:

- open this file in ACL2s as hw10.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.

- when done, save your file and submit it as hw10.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!

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
Instructions for programming problems:

For each function definition, you must provide both contracts and a body.

You must also ALWAYS supply your own tests (unless otherwise noted). 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.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; PART I: Warm up Proofs 
;; 

#|
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 in (a X) 
  :input-contract (listp X)
  :output-contract (booleanp (in a X))
  (cond ((endp X) nil)
        ((equal a (first X)) t)
        (t (in a (rest X)))))

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 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 -> Boolean
;; (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)
      nil
      (and (in (first l1) l2)
           (perm (rest l1) (del (first l1) l2))))))



;; Assume by "Def of lor" that each element is a rational
;; and a lor is (cons rational lor) | nil
;; A similar claim can be made about a lon
(defdata lor (listof rational))
(defdata lon (listof nat))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 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 sorted)
(defunc orderedp (l)
  :input-contract (lorp l)
  :output-contract (booleanp (orderedp l))
  (if (or (endp l)(endp (rest l)))
    t
    (and (<= (first l) (second l)) (orderedp (rest l)))))

(check= (orderedp '(-1 -1/2 0 4 9/2)) t)
(check= (orderedp '(-1 -1/2 0 4 7/2)) nil)
(check= (orderedp nil) t)


(defthm phi_applen (implies (and (listp l1) (listp l2))
                            (equal (len (app l1 l2))
                                   (+ (len l1)(len l2)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; merge: lor x lor -> lor
;; (merge l1 l2) takes two lists of rationals l1 and l2
;; that are PRESUMED to be already in sorted order and 
;; generates a new list with all elements from l1 and l2 
;; still in order. We do this by comparing the first of 
;; l1 and l2 and cons-ing the smallest of the two
;; onto the results of a recursive call with the 
;; rest of one list and the other list.
;; Thus the lists can be merged in O(n) time.
(defunc merge (l1 l2)
  :input-contract (and (lorp l1)(lorp l2))
  :output-contract (lorp (merge l1 l2))
  (cond ((endp l1)   l2)
        ((endp l2)   l1)
        ((< (first l1)(first l2))  
         (cons (first l1)(merge (rest l1) l2)))
        (t                          
         (cons (first l2)(merge l1 (rest l2))))))

(test? (implies (and (lorp l1)(lorp l2)(sortedp l1)(sortedp l2))
                (sortedp (merge l1 l2))))

(test? (implies (and (lorp l1)(lorp l2))
                (equal (+ (len l1)(len l2))
                       (len (merge l1 l2)))))

(check= (merge '(1 3 5 7) '(2 4 6 8)) '(1 2 3 4 5 6 7 8))
(check= (merge '(1 2 3 4) '(5 6 7 8)) '(1 2 3 4 5 6 7 8))

#|
Prove the following conjecture -                  
phi_mergeordered: (implies (and (lorp l1)(lorp l2)(orderedp l1)(orderedp l2))
                        (orderedp (merge l1 l2)))

What Induction Scheme should you use? Provide the proof obligations
..........
;; =======================SOLUTION START
IS for merge is necessary since we shrink either l1 or l2.
1. (not (and (lorp l1)(lorp l2))) => phi
2. (and (lorp l1)(lorp l2)(endp l1) => phi
3. (and (lorp l1)(lorp l2)(not (endp l1))(endp l2) => phi
4. (and (lorp l1)(lorp l2)(not (endp l1))(not (endp l2))
(<= (first l1)(first l2))(phi|((l1 (rest l1)))  => phi
5. (and (lorp l1)(lorp l2)(not (endp l1))(not (endp l2))
(> (first l1)(first l2))(phi|((l2 (rest l2)))  => phi
NOTE: Instead of (> (first l1)(first l2)), (not ((<= (first l1)(first l2)))) is
also correct. I just did the basic arithmetic equivalence when writing the obligations.

Case 1:
C1. (not (and (lorp l1)(lorp l2)))
C2. (lorp l1) /\ (lorp l2)
----------
C3. nil
Thus the conjecture is true in this case.

Case 2: 
C1. (lorp l1)
C2. (lorp l2)
C3. (endp l1)
C4. (ordered l1)
C5. (ordered l2)

(orderedp (merge l1 l2))
= {def merge, C3}
(orderedp l2)
= {C5}
t

Case 3: 
C1. (lorp l1)
C2. (lorp l2)
C3. (not (endp l1))
C4. (endp l2)
C5. (orderedp l1)
C6. (orderedp l2)

(orderedp (merge l1 l2))
= {def merge, C4}
(orderedp l1)
= {C5}
t

Case 4:
C1. (lorp l1)
C2. (lorp l2)
C3. (not (endp l1))
C4. (not (endp l2))
C5. (<= (first l1)(first l2))
C6. (orderedp l1)
C7. (orderedp l2)
C8. (implies (and (lorp (rest l1))(lorp l2)(orderedp (rest l1))(orderedp l2))
             (orderedp (merge (rest l1) l2)))
--------------------
C9. (lorp (rest l1) {C1, C3}
C10. (orderedp (rest l1)) {Def orderedp, C1, C3, PL}
C11. (orderedp (merge (rest l1) l2))) {C8, C10, C9, C2, C7, MP}

(orderedp (merge l1 l2))
= {def merge, C3, C4, C5}
(orderedp (cons (first l1)(merge (rest l1) l2)))
= {def orderedp, consp axiom}
(and (<= (first l1) (first (merge (rest l1) l2)))
     (orderedp (merge (rest l1) l2)))
= {C11, PL}
(<= (first l1)(first (merge (rest l1) l2)))
= {C2, C9, PL, Def merge, first-rest axioms}
(or (<= (first l1) (first l2))
    (<= (first l1) (second l1)))
= {Def orderedp, C5, C6, PL}
t

Case 5:
C1. (lorp l1)
C2. (lorp l2)
C3. (not (endp l1))
C4. (not (endp l2))
C5. (> (first l1)(first l2))
C6. (orderedp l1)
C7. (orderedp l2)
C8. (implies (and (lorp l1)(lorp (rest l2))(orderedp (rest l2)(orderedp l1))
                        (orderedp (merge l1 (rest l2)))))
--------------------
C9. (lorp (rest l2) {C2, C4}
C10. (orderedp (rest l2)) {Def orderedp, C7, C2, C4, PL}
C11. (orderedp (merge l1 (rest l2)))) {C8, C10, C9, C1, C6, MP}

(orderedp (merge l1 l2))
= {def merge, C3, C4, C5}
(orderedp (cons (first l2)(merge l1 (rest l2))))
= {def orderedp, consp axiom}
(and (<= (first l2) (first (merge l1 (rest l2))))
     (orderedp (merge (rest l1) l2)))
= {C11, PL}
(<= (first l2)(first (merge l1 (rest l2)))
= {C1, PL, Def merge, first-rest axioms}
(or (<= (first l2) (first l1))
    (<= (first l2) (second l2)))
= {Def orderedp, C5, C6, PL}
t
=======================SOLUTION END
|#
;; A quick demonstration that ACL2s can do the proof above.
(defthm phi_merge_isort (implies (and (lorp l1)(lorp l2)
                                      (orderedp l1)(orderedp l2))
                                 (orderedp (merge l1 l2))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 2: isort II: The Revenge 
;; Last week we started work on the merge sort algorithm
;; proving that it not only terminates but it's equivalent
;; to isort.....by giving you a HUGE assumption about 
;; merging isort.
;; We will prove this conjecture
;;
;; Once again, this is going to be deceptively complex 
;;
;; You will need to use induction and some induction schemes are also 
;; easier to use than others.  
;; My stategy for choosing an I.S. is:
;; 1) Choose the simplest I.S. that changes variables like your functions will
;;    -> As a first pass, I always look at nind and listp in case they work.
;; 2) Make sure there are no variables in the I.S. that are not in the conjecture
;; 3) Choose an I.S. that provides useful context in your proof.
;; 4) Try to have your base cases in the I.S. match the recursive base cases.
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(merge '(0 1 2) '(0 2 3))
(merge '(0 1 2) '(0 2 3))

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



;;============================================
;; TEMPORARY DETOUR:  the proofs regarding isort
;; yet again.  you can use these theorems in your proof
;;============================================

(defunc insert (e l)
  :input-contract (and (rationalp e) (lorp l))
  :output-contract (lorp (insert e l))
  (cond ((endp l) (list e))
        ((<= e (first l)) (cons e l))
        (t (cons (first l) (insert e (rest l))))))

(defunc isort (l) 
  :input-contract (lorp l)
  :output-contract (lorp (isort l))
  (if (endp l)
    l
    (insert (first l) (isort (rest l)))))

(defthm insert-orderedp
  (implies (and (lorp l)
                (orderedp l)
                (rationalp e))
           (orderedp (insert e l))))

(defthm orderedp-isort
  (implies (and (lorp l) (orderedp l))
           (equal (isort l) 
                  l)))

(defthm phi_isort-orderedp
  (implies (lorp l)
           (orderedp (isort l))))

(defthm phi_insert_del
  (implies (and (lorp l)(rationalp r))
           (equal (del r (insert r l)) l)))

(defthm phi_insert_in
  (implies (and (lorp l)(rationalp r))
           (in r (insert r l))))

(defthm phi_insert_perm
  (implies (and (lorp l1)(lorp l2)(rationalp r)
                (perm l1 l2))
           (perm (cons r l1) (insert r l2))))
                

(defthm phi_isort-perm
  (implies (lorp l)
           (perm l (isort l))))

;; Now that we know (isort l) is a permutation
;; of l AND is ordered, we can make the following claim
;; (you do not have to prove any of the above)
(defthm phi_isort_sorted
  (implies (lorp l)
           (sortedp l (isort l))))

;;===================================SOLUTION START
#|
Lemma
Prove phi_merge_comm:
  (implies (and (lorp x)(lorp y)
                (orderedp x)(orderedp y))
           (equal (merge x y) (merge y x)))
============================SOLUTION START           
Proof using the induction scheme of merge
1) ~((lorp x)/\(lorp y)) => phi_merge_comm
2) (lorp x)/\(lorp y)/\(endp x) => phi_merge_comm
3) (lorp x)/\(lorp y)/\~(endp x) /\(endp y) 
    => phi_merge_comm
4) (lorp x)/\(lorp y)/\~(endp x)/\~(endp y)
  /\((first x) < (first y)) 
  /\ phi_merge_comm|((x (rest x))) => phi_merge_comm
5) (lorp x)/\(lorp y)/\~(endp x)/\~(endp y)
  /\((first x) >= (first y)) 
  /\ phi_merge_comm|((y (rest y))) => phi_merge_comm

Obligation 1:
C1.  ~((lorp x)/\(lorp y))
C2.  ((lorp x)/\(lorp y))
--------------
C3 nil {C1, C2, PL}
nil=> x is true, thus obligation 1 is true

Oblication 2:
C1. (lorp x)
C2. (lorp y)
C3. (endp x)
(merge x y)
= {Def merge, C3}
y
= {Def merge, C3 (if y is nil then still true}
(merge y x)

Oblication 3:
C1. (lorp x)
C2. (lorp y)
C3. (endp y)
C4. ~(endp x)

(merge x y)
= {Def merge, C3, C4}
y
= {Def merge, C3, C4}
(merge y x)


Obligation 4:
C1. (lorp x)
C2. (lorp y)
C3. ~(endp x)
C4. ~(endp y)
C5. (orderedp x)
C6. (orderedp y)
C7. ((first x) < (first y))
C8. (lorp (rest x)) /\(lorp y)/\(orderedp (rest x))
  /\(orderedp y) => ((merge (rest x) y) = (merge y (rest x)))
----------
C9. (lorp (rest x)) {C1, C3, def lorp}
C10. (orderedp (rest x)) {C5, C3, def orderedp}
C11. ((merge (rest x) y) = (merge y (rest x)))
   {C10, C9, C2, C6, C8, MP}

(merge x y)
= {C3, C4, C7, def merge}
(cons (first x)(merge (rest x) y))
= {C11}
(cons (first x)(merge y (rest x)))
= {def merge, C7,first-rest axioms}
(merge y x)


Obligation 5:
C1. (lorp x)
C2. (lorp y)
C3. ~(endp x)
C4. ~(endp y)
C5. (orderedp x)
C6. (orderedp y)
C7. ((first x) >= (first y))
C8. (lorp x) /\(lorp (rest y))/\(orderedp x)
  /\(orderedp (rest y)) => ((merge x (rest y)) = (merge (rest y) x))
----------
C9. (lorp (rest y)) {C2, C4, def lorp}
C10. (orderedp (rest y)) {C6, C4, def orderedp}
C11. ((merge x (rest y)) = (merge (rest y) x))
   {C10, C9, C3, C5, C8, MP}

(merge x y)
= {C3, C4, C7, def merge}
(cons (first y)(merge x (rest y)))
= {C11}
(cons (first y)(merge (rest y) x))
= {def merge, C7,first-rest axioms}
(merge y x)
|#
;;================================SOLUTION END


;;================================SOLUTION START

#|
Lemma 2        
PROVE 
(defthm phi_merge_insert 
  (implies (and (rationalp e)(lorp l1)(lorp l2)
                (orderedp l1)(orderedp l2))
           (equal (insert e (merge l1 l2))
                  (merge (insert e l1) l2))))
                  
This is assuming that (first l1) < (first l2) when 
both lists are non-empty. L1 and L2 can be re-arranged 
via phi_merge_comm Thus (or (endp l1)(endp l2)(< (first l1)(first l2))))
can be added to context if required.
GRADERS: be generous regarding this assumption about l1 and L2's order.


Proof Phi-merge_insert using the induction scheme for
insert
1) ~((rationalp e)/\(lorp l1)) => phi_merge_insert
2) (rationalp e)/\(lorp l1)/\ (endp l1) => phi_merge_insert
3) (rationalp e)/\(lorp l1)/\ ~(endp l1)
   /\(e <= (first l1)) => phi_merge_insert
4) (rationalp e)/\(lorp l1)/\ ~(endp l1)
   /\ (e > (first l1)) /\ phi_merge_insert|((l1 (rest l1))) 
      => phi_merge_insert
      
Obligation 1:
C1. ~((rationalp e)/\(lorp l1))
C2. ((rationalp e)/\(lorp l1))
----------------
C3. nil {C1, C2}

Obligation 2:
C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. (endp l1)
C5. (orderedp l1)
C6. (orderedp l2)

LHS
(insert e (merge l1 l2))
= {Def merge, C4}
(insert e l2)

RHS
(merge (insert e l1) l2)
= {def insert, C4}
(merge (cons e nil) l2)
= {L3}
(insert e l2)

GIVEN: L3
(rationalp e) /\ (lorp l2)/\(orderedp l2)
    => (merge (list e) l2) = (insert e l2)

Obligation 3 (with added context (:
C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. ~(endp l1)
C5. (e < (first l1))
C6. (or (endp l1)(endp l2)(< (first l1)(first l2)))
-----------------
C7. (or (endp l2)(< (first l1)(first l2))) {C4, PL}

Case 1: 
C8. (endp l2)
LHS
(insert e (merge l1 l2))
= {Def merge, C4, C5, C8}
(insert e l1)

RHS
(merge (insert e l1) l2)
= {def merge, C8}
(insert e l1)

Case 2: 
C8. (first l1) < (first l2)
LHS
(insert e (merge l1 l2))
= {Def merge, C4, C8}
(insert e (cons (first l1)(merge (rest l1) l2)))
= {Def insert, C5}
(cons e (cons (first l1)(merge (rest l1) l2)))

RHS
(merge (insert e l1) l2)
= {def insert, C8}
(merge (cons e l1) l2)
= {C8, C5, def merge}
(cons e (cons (first l1)(merge (rest l1) l2)))

LHS=RHS


Obligation 4:
C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. ~(endp l1)
C5. (e >= (first l1))
C6. (implies (and (rationalp e)(lorp (rest l1))(lorp l2)
                (orderedp (rest l1))(orderedp l2))
           (equal (insert e (merge (rest l1) l2))
                  (merge (insert e (rest l1)) l2)))
C7. (orderedp l1)
C8. (orderedp l2)
C9. (or (endp l1)(endp l2)(< (first l1)(first l2)))
-----------------
C10. (orderedp (rest l1)) {C7, C2, C4, Def endp}
C11. (lorp (rest l1)) {C2, C4, Def endp, def lorp}
C12. (equal (insert e (merge (rest l1) l2))
                  (merge (insert e (rest l1)) l2))
     {C6, C10, C8, C11, C1, C3, MP}
C13 (or (endp l2)(< (first l1)(first l2))) {C9, C4, PL}



Case 1: l2 is not empty
C14. (not (endp l2))
C15. (first l1) < (first l2) {c13, C14, PL}

(insert e (merge l1 l2))
= {Def merge, C14, C15}
(insert e (cons (first l1)(merge (rest l1) l2)))
= {Def insert, C5}
(cons (first l1) (insert e (merge (rest l1) l2)))
= {C12}
(cons (first l1) (merge (insert e (rest l1)) l2))
= {Def merge, C15}
(merge (cons (first l1)(insert e (rest l1))) l2)
= {Def insert, C5}
(merge (insert e l1) l2)

Case 2: 
C14. (endp l2)

(insert e (merge l1 l2)
= {Def merge, C14, C4}
(insert e l1)
= {Def merge, c14}
(merge (insert e l1) l2)

-------------------------------------------------
Dustin's Solution (in case any of you used the induction
scheme merge gives rise to:
PROVE:
(defthm phi_merge_insert 
  (implies (and (rationalp e)(lorp l1)(lorp l2)
                (orderedp l1)(orderedp l2))
           (equal (insert e (merge l1 l2))
                  (merge (insert e l1) l2))))
GIVEN: L3
(rationalp e) /\ (lorp l2)/\(orderedp l2)
    => (merge (list e) l2) = (insert e l2)

IS merge
1. ~(and (lorp l1)(lorp l2)) => phi
2. (and (lorp l1)(lorp l2) (endp l1)) => phi
3. (and (lorp l1)(lorp l2) ~(endp l1) (endp l2)) => phi
4. (and (lorp l1)(lorp l2) ~(endp l1) ~(endp l2) (< (first l1)(first l2))
        phi | ((l1 (rest l1)))) => phi
5. (and (lorp l1)(lorp l2) ~(endp l1) ~(endp l2) ~(< (first l1)(first l2))
        phi | ((l2 (rest l2)))) => phi

Obligation 1.

C1. ~(and (lorp l1)(lorp l2))
C2. (rationalp e)
C3. (lorp l1)
C4. (lorp l2)
C5. (orderedp l1)
C6. (orderedp l2)
-------------------
nil {C1, C3, C4}


Obligation 2.

C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. (orderedp l1)
C5. (orderedp l2)
C6. (endp l1)
-------------------

Proof:
LHS
(insert e (merge l1 l2))
= {def merge, C6}
(insert e l2)

RHS
(merge (insert e l1) l2))
= {def insert, C6}
(merge (cons e nil) l2)
= {L3, C1, C3, C5, MP}
(insert e l2)
LHS = RHS


Obligation 3.

C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. (orderedp l1)
C5. (orderedp l2)
C6. ~(endp l1)
C7. (endp l2)
-------------------

Proof:
(insert e (merge l1 l2))
= {def merge, C7}
(insert e l1)
= {def merge, C7}
(merge (insert e l1) l2))
LHS = RHS


Obligation 4.

C1. (rationalp e)
C2. (lorp l1)
C3. (lorp l2)
C4. (orderedp l1)
C5. (orderedp l2)
C6. ~(endp l1)
C7. ~(endp l2)
C8. (< (first l1)(first l2))
C9. (implies (and (rationalp e)(lorp (rest l1))(lorp l2)
                (orderedp (rest l1)) (orderedp l2))
           (equal (insert e (merge (rest l1) l2))
                  (merge (insert e (rest l1)) l2)))
--------------------------------------------------
C10. (lorp (rest l1)) {C2, C6, def lorp}
C11. (orderedp (rest l1)) {C2, C4, C6, L4, MP}
C12. (equal (insert e (merge (rest l1) l2))
            (merge (insert e (rest l1)) l2)) {C9, C1, C10, C3, C11, C5, MP}


Case (<= e (first l1)):

Additional Context:
C13. (<= e (first l1))
-----------------------
C14. (< e (first l2)) {C8, C13, arithmetic}

Proof:
(insert e (merge l1 l2))
= {def merge, C6, C7, C8}
(insert e (cons (first l1) (merge (rest l1) l2)))
= {def insert, C13}
(cons e (cons (first l1) (merge (rest l1) l2)))
= {def merge, C6, C7, C8}
(cons e (merge l1 l2))
= {def merge, C14, C7}
(merge (cons e l1) l2)
= {def insert, C13}
(merge (insert e l1) l2)
RHS = LHS

Case ~(<= e (first l1)):

Additional Context:
C13. (> e (first l1))

Proof:
(insert e (merge l1 l2))
= {def merge, C6, C7, C8}
(insert e (cons (first l1) (merge (rest l1) l2)))
= {def insert, C13}
(cons (first l1) (insert e (merge (rest l1) l2)))
= {C12}
(cons (first l1) (merge (insert e (rest l1)) l2))
= {def merge, C6, C7, C8}
(merge (cons (first l1) (insert e (rest l1))) l2)
= {def insert, C13}
(merge (insert e l1) l2)
LHS = RHS

Obligation 5…. (should be similar to the above)


|#
;;================================SOLUTION END

#|
Prove phi_merge_isort:
  (implies (and (lorp x)(lorp y))
           (equal (isort (merge x y)) 
                  (merge (isort x) (isort y)))))
......we are going to pretend the original conjecture
we assumed last week involved (isort (merge x y)) rather than
the original (isort (app x y)). You can prove
(isort (merge x y)) = (isort (app x y)) for extra
practice (but this isn't as simple as it seems)

So before you go diving into your proof, think about
things that should be true about merge:

- If lists x and y are ordered, what happens if you switch
from (merge x y) to (merge y x) ?

- What happens when you insert an element into a ordered 
merged list? What happens if  you insert the element
in x (which is ordered) and then merge? 
  * Let's assume that  (first x) < (first y) provided 
    lists x and y are non-empty just to make your lives easier 
    You can just add it to your lemma's context rather than 
    the conjecture itself.  If you really want to show off 
    your math skills, you can do the proof without this assumption.
    By the way, why can I order these lists any way I want and make
    that assumption?

Feedback from Dustin: Do NOT try to prove the associativity of merge.
The proof is horrible.  The above questions should guide you to a 
reasonable solution that you can finish before you graduate.

You can also assume the following is true (and can prove it
for extra practice):
L3:
(rationalp e) /\ (lorp l2)
    => (merge (list e) l2) = (insert e l2)
......................
=================================SOLUTION START
Using the induction scheme for merge
1) ~((lorp x)/\(lorp y)) => phi_merge_isort
2) (lorp x)/\(lorp y)/\(endp x) => phi_merge_isort
3) (lorp x)/\(lorp y)/\~(endp x) /\(endp y) 
    => phi_merge_isort
4) (lorp x)/\(lorp y)/\~(endp x)/\~(endp y)
  /\((first x) < (first y)) 
  /\ phi_merge_isort|((x (rest x))) => phi_merge_isort
5) (lorp x)/\(lorp y)/\~(endp x)/\~(endp y)
  /\((first x) >= (first y)) 
  /\ phi_merge_isort|((y (rest y))) => phi_merge_isort

Obligation 1:
C1. ~((lorp x)/\(lorp y))
C2. ((lorp x)/\(lorp y))
------------
C3. nil {C1, C2}

Obligation 2:
C1. (lorp x)
C2. (lorp y)
C3. (endp x)

(isort (merge x y)) 
= {Def merge, C3}
(isort y)
= {Def merge, C3}
(merge x (isort y))
= {Def isort, C3}
(merge (isort x)(isort y))

Obligation 3:
C1. (lorp x)
C2. (lorp y)
C3. ~(endp x)
C4. (endp y)

(isort (merge x y)) 
= {def merge, C4, C3}
(isort x)
= {Def merge, C4, C3, Def isort, consp axiom....(isort x) isn't empty}
(merge (isort x) y)
= {Def isort, C4}
(merge (isort x)(isort y))

Obligation 4:
C1. (lorp x)
C2. (lorp y)
C3. ~(endp x)
C4. ~(endp y)
C5. ((first x) < (first y))
C6. phi_merge_isort|((x (rest x)))
C7. (orderedp x)
C8. (orderedp y)
------------
C9. (lorp (rest x)) {def endp, def lorp, C3}
C10. (isort (merge (rest x) y)) = (merge (isort (rest x)) (isort y))
    {C1, C9, C6, MP}
C11. (orderedp (rest x)) {C7, Def orderedp, C3}

(isort (merge x y))
= {Def merge, C3, C4, C5, def isort}
(insert (first x) (isort (merge (rest x) y)))
= {C10}
(insert (first x)(merge (isort (rest x))(isort y)))
= {phi_merge_insert, phi_isort_ordered (twice), C11, C8, C2, C9, MP....this MP can be left off}
(merge (insert (first x) (isort (rest x)))(isort y))
= {Def isort}
(merge (isort x)(isort y))

Obligation 5:
C1. (lorp x)
C2. (lorp y)
C3. ~(endp x)
C4. ~(endp y)
C5. ((first x) >= (first y))
C6. phi_merge_isort|((y (rest y)))
C7. (orderedp x)
C8. (orderedp y)
------------
C9. (lorp (rest y)) {def endp, def lorp, C4}
C10. (isort (merge x (rest y))) = (merge (isort x) (isort (rest y)))
    {C1, C9, C6, MP}
C11. (orderedp (rest y)) {C8, Def orderedp, C4}

(isort (merge x y))
= {Def merge, C3, C4, C5, def isort}
(insert (first y) (isort (merge x (rest y))))
= {C10}
(insert (first y)(merge (isort x)(isort (rest y))))
= {phi_merge_comm, phi_isort_ordered (twice), C1, C9}
(insert (first y)(merge (isort (rest y)) (isort x)))
= {phi_merge_insert, phi_isort_ordered (twice), C11, C7, C2, C9, MP....this MP can be left off}
(merge (insert (first y) (isort (rest y)))(isort x))
= {Def isort, first rest axioms}
(merge (isort y)(isort x))
{phi_merge_comm, phi_isort_ordered (twice), C1, C2}
(merge (isort x)(isort y))
===================================SOLUTION END
|#



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SECTION III: Revisiting Mistakes
;; So if you couldn't tell, I don't actually
;; enjoy making mistakes but they're extremely useful
;; to help us learn.  In a previous homework, I asked
;; you to prove a conjecture but since there was a
;; counter example, many of you were able to get points
;; without a proof.  Well I can't let that happen.
;; I've improved my factoring functions so you can
;; see what the function could have looked like 
;; if I made a different design decision.....and while
;; we're at it, let's do an inductive proof using
;; these new function (the actual reason we are revisiting
;; the function)

 ;; gpos for potential positive integers greater than 1. 
(defdata gpos (range integer (2 <= _)))
;; Ignore
(defthm phi_shrink_factor (implies (and (gposp n)(gposp f)(posp (/ n f)))
                                   (< (/ n f) n)))
(defdata log (listof gpos))


(defunc factors-help (n f)
  :input-contract (and (gposp n)(gposp f))
  :output-contract (logp (factors-help n f))
  (if (<= n f)
    (list n)
    (if (gposp (/ n f)) 
      (cons f (factors-help (/ n f) f))
      (factors-help n (+ f 1)))))
  

;; factors : Factor -> log
;; returns a list containing all PRIME factors of n including (possibly) 
;; n and 1. 
(defunc factors (n)
    :input-contract (gposp n)
    :output-contract (logp (factors n))
    (factors-help n 2))

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


(defunc mult-l (l)
  :input-contract (logp l)
  :output-contract (posp (mult-l l))
  (if (endp l)
    1
    (* (first l)(mult-l (rest l)))))

;; 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))
    (mult-l (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 (posp a)(posp b))
                (equal (gcd a b)(gcd b a))))

;; Just a theorem in case you want ACL2s to do the proof
;; (you cna ignore this)
(defthm phi_cp_intersect 
  (implies (and (gposp a)(gposp b))
           (equal (coprime a b) 
                  (endp (intersect (factors a) 
                                   (factors b))))))

#|
PROVE (optional....you still need to prove phi_prime_factorize)
Once more with feeling: prove phi_gcd_cp.  
This ONE CONJECTURE is not graded
It doesn't require induction. This is just for those
of you that like finishing what you start.

phi_gcd_cp: (implies (and (gposp a)(gposp b))
                     (equal (coprime a b)(equal (gcd a b) 1)))
                     
However, you can't take your mult-l for granted and assume
"arithmetic" explains why non-empty lists of factors must return a value
> 1.

......................
=====================================SOLUTION START
L1: (logp l) /\ ~(endp l) => (gposp (mult-l l))

C1. (logp l)
C2. ~(endp l)
-----------
C3. (posp (mult-l (rest l))) {C2, C1, contract axiom mult-l}
C4. (gposp (first l)) {C2, c1, Def logp}

(gposp (mult-l l))
= {Def mult-l, C2}
(gposp (* (first l) (mult-l (rest l))))
= {C4, C3, Arithmetic, Def factor}
t

Case 1: a and b have no factors in common
C1. (gposp a)
C2. (gposp b)
C3. (endp (intersect (factors a) (factors b)))

(coprime a b) = ((gcd a b) = 1)
= {Def coprime, def gcd}
(endp (intersect (factors a) (factors b))) 
   = (1 = (mult-l (intersect (factors a)(factors b)))
= {C3, def mult-l}
  t = (1=1)

Case 2: a and b have no factors in common
C1. (gposp a)
C2. (gposp b)
C3. ~(endp (intersect (factors a) (factors b)))
-----------
C4. (gposp (mult-l (intersect (factors a)(factors b)))) {C3, L1}

(coprime a b) = ((gcd a b) = 1)
= {Def coprime, def gcd}
(endp (intersect (factors a) (factors b))) 
   = (1 = (mult-l (intersect (factors a)(factors b)))
= {C3, def mult-l, C4}
  nil = nil
  
  ================================SOLUTION END
|#

#|    
Prove phi_prime_factorize:  
(implies (gposp a)(equal a (mult-l (factors a))))
.............
===========================SOLUTION START
Need a Lemma:
L1: (implies (and (gposp a)(gposp f))(equal a (mult-l (factors-help a f))))
Prove using the induction scheme for factors-help
1) ~((gposp a)/\(gposp f)) => L1
2) (gposp a)/\(gposp f)/\(<= a f)) => L1
3) (gposp a)/\(gposp f)/\(> a f)/\(gposp (/ n f))/\ L1|((a (/ a f)))  => L1
4) (gposp a)/\(gposp f)/\(> a f)/\ ~(gposp (/ n f)) /\ L1|((f (+ f 1)))  => L1

Obligation 1:
C1. ~((gposp a)/\(gposp f))
C2. ((gposp a)/\(gposp f))
------------
C3. nil
nil=> x is true

Obligation 2:
C1. (gposp a)
C2. (gposp f)
c3. (<= a f)

(mult-l (factors-help a f))
= {def factors-help, C1, C2, C3}
(mult-l (cons a nil))
= {Def mult-l, consp axiom, first-rest axiom, def. endp}
(* a 1)
= {Arithmetic}
a

Obligation 3:
C1. (gposp a)
C2. (gposp f)
c3. (> a f)
C4. (gposp (/ a f))
C5. (implies (and (gposp (/ a f))(gposp f))(equal (/ a f) (mult-l (factors-help (/ a f) f))))
------------
C6. (equal (/ a f) (mult-l (factors-help (/ a f) f))) {C5, C4, C2, MP}


(mult-l (factors-help a f))
= {def factors-help, C1, C2, C3, C4}
(mult-l (cons f (factors-help (/ a f) f)))
= {Def mult-l, consp axiom, first-rest axioms}
(* f (mult-l (factors-help (/ a f) f)))
= {C6}
(* f (/ a f))
= {Arithmetic}
a

Obligation 4:
C1. (gposp a)
C2. (gposp f)
c3. (> a f)
C4. ~(gposp (/ a f))
C5. (implies (and (gposp a)(gposp (+ f 1)))(equal a (mult-l (factors-help a (+ f 1)))))
------------
C6. (gposp (+ f 1)) {Def factor, C2}
C7. (equal a (mult-l (factors-help a (+ f 1)))) {C6, C1, C5, MP}

(mult-l (factors-help a f))
= {def factors-help, C1, C2, C3, C4}
(mult-l (factors-help a (+ f 1)))
= {C7}
a

Prove phi_prime_factorize:
C1. (gposp a)

(mult-l (factors a))
= {Def factors, C1}
(mult-l (factors-help a 2))
= {L1, C1}
a

===========================SOLUTION END
|#            
   
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|

I would like to get more feedback from you. Here are a couple questions 
to monitor how the course is progressing.  This should be brief. 

Please fill out the following form.

https://goo.gl/forms/Dhd69pk19amvQCcj2

As before, 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, 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.  

5 points will be awarded to each team member for filling out the 
questionnaire.

The following team members filled out the feedback survey provided by 
the link above:
---------------------------------------------
<firstname> <LastName>
<firstname> <LastName>

|#