#|

CS 2800 Homework 12 - 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.
|#

#|
Induction, Programming, and Tail Recursion Proofs

This assignment is designed to serve as a review and prepare you
for exam 2. Thus, although this is done in groups, you should perhaps do
this by yourself and then merge with your group-mates.

How you approach a proof is not necessarily obvious and even your TAs and
instructors have to try a proof multiple ways. It's fine to try the wrong 
IS at first and then adjust. If you can figure out what inductive assumptions
and stopping conditions you need for a proof before starting, that's even better.
The point being: a false start to your proof doesn't imply (via MP) that you
don't understand the topic but practice reduces the number of false starts.
This assignment will hopefully give you that practice.

|#


#|
***************
THEME: I Love the End of Term
The end is fast approaching and although many of you might be concerned about 
the exam, I've regularly pointed out a key difference from the first half
of the semester: you can make your own problems.  The fact we can come up
with properties related to a function, we can write tail recursive versions of a function
and the fact we may need to prove a function is admissible (and thus terminates)
means that any single function can spawn a slew of questions touching on all aspects
of the course. Give it a try on your own......

....or let's do that now. Take the functions ssort (for selection sort) and weave.
We will keep revisiting these functions throughout the homework.  First, let's define
them and the functions necessary to use them.

Note that I'm denoting all questions with
##.............. so you don't accidentally overlook one (you can do a 
search).

Also note that many questions are "EXTRA" meaning they are worth no points and won't be 
graded.  These are for you to potentially get more practice.  The homework would be painfully
long if we required you to prove all the questions.  Hence keep an eye out for what is optional
and what is not.

***************
|#


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; del: Any x List -> List
;; (del e l) takes an element e and a list l
;; and removes the FIRST occurence 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))))))
;; Ignore
(sig del (all (listof :b)) => (listof :b))

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


(defdata lor (listof rational))
(defdata lon (listof nat))

;; min-l: LOR (non-empty -> Rational
;; (min-l l) returns the smallest element in l.
(defunc min-l (l)
  :input-contract (and (lorp l)(consp l))
  :output-contract (rationalp (min-l l))
  (if (endp (rest l))
    (first l)
    (let ((min (min-l (rest l))))
        (if (< min (first l)) min (first l)))))


;;Keep to help ssort go in AFTER you add your lemmata from part A.
;; This is purely optional.
(defthm phi_del_lorp (implies (lorp l)(lorp (del e l))))



;; ssort: LOR -> LOR
;; (ssort l) sorts list l using the selection sort algorithm
;; This involves repeatedly finding the smallest element in the list
;; and putting it at the front of the list (or sublist)
(defunc ssort (l)
  :input-contract (lorp l)
  :output-contract (lorp (ssort l))
  (if (endp l)
    l
    (let ((min (min-l l)))
      (cons min (ssort (del min l))))))

;; weave: list x List -> list
;; (weave x y) takes two lists and interweaves
;; them so the resultant list alternates between
;; an element from x and an element from y.
(defunc weave (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (weave x y))
  (cond ((endp x) y)
        ((endp y) x)
        (t (cons (first x) 
                 (cons (first y)
                       (weave (rest x)(rest y)))))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Section A: Admissibility, Measure Functions and Induction Schemes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
First, let's review the conditions necessary for a function to be admitted in
ACL2s (I'm paraphrasing below):
1) The function f is a new function symbol
2) The input variables are distinct variable symbols
3) The body of the function is a well formed term, possibly using a recursive
call to f and mentioning no variables freely (ie only the input variables)
4) The function is terminating
5) IC=>OC is a theorem
6) The body contract holds under the assumption that the IC holds (ie there
isn't a body contract violation if the input contract is true)


OK.  Now onto the questions. Note that I'm denoting all questions with
##.............. so you don't accidentally overlook one (you can do a 
search).

For each function fn below (f1...f5), determine if the function fn is admissible:

If fn is admissible: 
   1) provide a measure function mn that can be used to prove it terminates
   2) Write the proof obligations for fn using mn that can show it terminates.
   3) Convince yourself that the function terminates (no need for a formal proof)
   4) Write the induction scheme that fn gives rise to.

If fn is NOT admissible, 
   1) Give your justification as to why (conditions 1-6 above).
      a) If the problem is syntactic (admissibility conditions 1-3) then tell us what
         part of the function has a problem.
      b) If the issue is with conditions 4-6, then give an input that will illustrate
         the violation.
   2) Give the (invalid) induction scheme that fn gives rise to.
|#

#|
A1.

(defunc f1 (x y z)
  :input-contract (and (natp x) (natp y) (listp z))
  :output-contract (natp (f1 x y z))
  (cond ((< x 10) (* x y))
        ((<= (len z) y) (* (len z) y))
        ((> x (len z)) (+ x (f1 x y (rest z))))
        (t (f1 (- x 10) y z))))
    
##..............
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
SOLUTION
Admissible.
(defunc m1 (x y z)
  :input-contract (and (natp x) (natp y) (listp z))
  :output-contract (natp (m1 x y z))
  (+ (len z) x))
  
Proof Obligations to show termination:
1) (natp x) /\ (natp y) /\ (listp z) /\ ~(< x 10) 
        /\ ~(<= (len z) y) /\ (> x (len z)) 
    => ((m1 x y z) > (m1 x y (rest z)))
2) (natp x) /\ (natp y) /\ (listp z) /\ ~(< x 10) 
        /\ ~(<= (len z) y) /\ ~(> x (len z))
    => ((m1 x y z) > (m1 (- x 10) y z))

Induction Scheme for f1:
1) ~((natp x) /\ (natp y) /\ (listp z)) => phi
2) (natp x) /\ (natp y) /\ (listp z) /\ (< x 10) => phi
3) (natp x) /\ (natp y) /\ (listp z) /\ ~(< x 10) /\ (<= (len z) y) => phi
4) (natp x) /\ (natp y) /\ (listp z) /\ ~(< x 10) /\ ~(<= (len z) y) /\ (> x (len z)) 
   /\ phi|((z (rest z))) => phi
5) (natp x) /\ (natp y) /\ (listp z) /\ ~(< x 10) /\ ~(<= (len z) y) 
   /\ ~(> x (len z)) /\ phi|((x (x-10))) => phi

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

|#

#|
;; Remember, induction schemes rely on converting a function to an equivalent
;; cond statement (at least if you want to use the design pattern for creating an IS
;; given in the notes)

(defunc f2 (x y)
  :input-contract (and (integerp x)(integerp y))
  :output-contract (integerp (f2 x y))
  (if (natp x)
    y
    (if (natp y)
      (if (<= (unary-- x) y)
        (f2 (+ x 1) y)
        (f2 x (- y 1)))
      x)))

##..............
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
SOLUTION
Admissible
(defunc m2 (x y)
  :input-contract (and (integerp x)(integerp y))
  :output-contract (natp (m2 x y))
       (let ((res (if (<= (- x) y) (- x) y)))
         (if (< res 0) 0 res)))
         
Another approach (since x is negative and can increase and y is positive):
(defunc m2b (x y)
  :input-contract (and (integerp x)(integerp y))
  :output-contract (natp (m2b x y))
  (abs (+ (abs x) y)))

Measure Function Proof Obligations
1) (integerp x) /\ (integerp y) /\ ~(natp x) /\ (natp y) /\ ((unary-- x) <= y)
=> ((m2 x y) > (m2 (+ x 1) y))
2) (integerp x) /\ (integerp y) /\ ~(natp x) /\ ~(natp y) 
    /\ ~((unary-- x) <= y) => ((m2 x y) > (m2 x (- y 1)))

Induction Scheme for f2:
1) ~((integerp x) /\ (integerp y)) => phi
2) (integerp x) /\ (integerp y) /\ (natp x) => phi
3) (integerp x) /\ (integerp y) /\ ~(natp x) /\ (natp y) /\ ((unary-- x) <= y)
 /\ phi|((x (+ x 1))) => phi
4) (integerp x) /\ (integerp y) /\ ~(natp x) /\ ~(natp y) /\ ~((unary-- x) <= y)
 /\ phi|((y (- y 1))) => phi 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
|#

;; No need to consider the admissibility of evenp.  Just f3
(defunc evenp (i)
  :input-contract (integerp i)
  :output-contract (booleanp (evenp i))
  (integerp (/ i 2)))

#|
A3.
(defunc f3 (x)
  :input-contract (lorp x)
  :output-contract (natp (f3 x))
  (cond ((< (len x) 5) (f3 (cons 10 (app x x))))
        ((evenp (len x))  (f3 (cons (* 2 (first x)) x)))
        (t (+ (len x) (first x)))))

##..............
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
SOLUTION  (not graded)
Not admissible due to output contract violation.
(f3 (list 1/2 0 0 0 0)) returns 11/2 which breaks the output contract (requirement 5)
1) ~(lorp x) => phi
2) (lorp x) /\ (< (len x) 5) /\ phi|((x (cons 10 (app x x)))) => phi
3) (lorp x) /\ ~(< (len x) 5) /\ (evenp (len x)) 
   /\ phi|((x (cons (* 2 (first x)) x))) => phi
4) (lorp x) /\ ~(< (len x) 5) /\ ~(evenp x) => phi
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

|#

#|
A4. 
(defunc weave (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (weave x y))
  (cond ((endp x) y)
        ((endp y) x)
        (t (cons (first x) 
                 (cons (first y)
                       (weave (rest x)(rest y)))))))

(Yes, we realize that weave is admissible. Give a measure, measure obligations 
and induction scheme just the same)
##..............
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
SOLUTION
Admissible
(defunc mweave (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (mweave x y))
  (len x))
         

Measure Function Proof Obligations
1) (listp x) /\ (listp y) /\ ~(endp x) /\ ~(endp y) 
=> ((mweave x y)= (len x) > (len (rest x)) = (mweave (rest x) (rest y)))

Induction Scheme for weave:
1) ~((listp x) /\ (listp y)) => phi
2) (listp x) /\ (listp y) /\ (endp x) => phi
3) (listp x) /\ (listp y) /\ ~(endp x) /\ (endp y) => phi
4) (listp x) /\ (listp y) /\ ~(endp x) /\ ~(endp y) 
/\ phi|((x (rest x))(y (rest y))) => phi 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

|#

#|
A5.
(defunc f5 (l1 l2)
  :input-contract (and (lorp l1) (lonp l2))
  :output-contract (listp (f5 l1 l2))
  (cond ((endp l1) (list 1 2))
        ((endp l2) (f5 (cons 5 l1) (list 5)))
        ((>= (len l2) (len l1)) (f5 l2 (list l1)))
        (t (f5 (rest l1) (rest l2)))))

##..............
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
SOLUTION:
Condition 4 fails: The function does not terminate.
(f5 '(1) '(1))
will be
(f5 '(1) '((1)))
and then
(f5 '((1)) '((1)))

The length of both lists stays at 1.

THere are a million other ways this may not terminate.  The function is terrible.

The IS for f5 would be:
1) (implies (not (and (lorp l1) (lonp l2))) phi)
2) (implies (and (lorp l1) (lonp l2) (endp l1)) phi)
3) (implies (and (lorp l1) (lonp l2) (not (endp l1)) (endp l2)
                 phi|((l1 (cons 5 l1)) (l2 (list 5)))) 
            phi)
4) (implies (and (lorp l1) (lonp l2) (not (endp l1)) (not (endp l2))
                 (> (len l2) (len l1)) phi|((l1 l2)(l2 (list l1))) 
            phi)
5) (implies (and (lorp l1) (lonp l2) (not (endp l1)) (not (endp l2))
                 (not (> (len l2) (len l1))) phi|((l1 (rest l1)) (l2 (rest l2)))) 
            phi)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
|#
#|
A6.  Finally, prove that ssort should be admissible
by proving it terminates....and make sure the other 
admissibility conditions pass

(defunc ssort (l)
  :input-contract (lorp l)
  :output-contract (lorp (ssort l))
  (if (endp l)
    l
    (let ((min (min-l l)))
      (cons min (ssort (del min l))))))


....and as you might imagine based on HW10, this will
require lemmata. 
1) Write the measure function and  termination 
proof obligations.  Find what you need to prove.
2) Generalize the lemma so you know what happens
when something IN a list is DELeted from a list. What
happens to the size of the list?
3) How do you know (min-l l) is IN the list?....wait.
That sounds like a lemma too. See L3.
4) Finally, pull it all together to prove that the 
value of the measure function decreases with each 
recursive call (thus ssort terminates).  Your lemma 
will have something involving (del (min-l l) l))
The proof doesn't require induction provided you use
L3 (below) and 2) above.

-----------------------------------
Hopefully Helpful Theorems
Let's make the proof easier....or less annoying at least.
You can use the following theorem without proving it:

L3: (lorp l) /\ (consp l) => (in (min-l l) l)

(This is hint 3) from the list above by the way)
-----------------------------------

##..............
;;=======================================SOLUTION START

(defunc mss(l)
  :input-contract (lorp l)
  :output-contract (natp (mss l))
  (len l))
Lemmata:


L2: (lisp l) /\ (in e l) => (< (len (del e l)) (len l))
  
L1: (lorp l) /\ (consp l) => (< (len (del (min-l l) l)) (len l))
  
Proving L2 using IS for del....or in.  The same I.S.
1) ~(listp l) => L2
2) (listp l) /\ (endp l) => L2
3) (listp l) /\ ~(endp l) 
   /\ (e =(first l)) => L2
4) (listp l) /\ ~(endp l) 
   ~(e =(first l)) /\ L2|((l (rest l))) => L2


Obligation 1
C1. ~(listp l)
C2. (listp l)
---------------
C3. nil {C1, C2,PL}
nil=> x is true.

Obligation 2
C1. (listp l)
C2. (endp l)
C3. (in e l)
-----------
C4. ~(end l) {Def in, C3, PL}
C5. nil {C4, C2, PL}
nil=> x is true.

Obligation 3
C1. (listp l)
C2. ~(endp l)
C3. (in e l)
C4. (e = (first l))
-------------

(< (len (del e l)) (len l))
= {Def. del, C4, C2}
(< (len (rest l)) (len l)
= {Decreasing len axiom}
t


Obligation 4
C1. (listp l)
C2. ~(endp l)
C3. (in e l)
C4. ~(e = (first l))
C5. (lisp (rest l)) /\ (in e (rest l)) => (< (len (del e (rest l))) (len (rest l)))
-------------
C6. (lisp (rest l)) {C2, C1, Def endp, def listp}
C7. (in e (rest l)) {C3, C4, Deft in, C2, PL}
C8. (< (len (del e (rest l))) (len (rest l))) {C5, C6, C7, MP}

(< (len (del e l)) (len l))
= {Def. del, C4, C2, Def len}
(< (len (cons (first l)(del e (rest l)) (+ 1 (len (rest l)))
= {Def len, consp axiom, arithmetic}
(< (len (del e (rest l))) (len (rest l)))
= {C8}
t

Prove L1: (lorp l) /\ (consp l) => (< (len (del (min-l l) l)) (len l))
I don't need an induction scheme.  Pure ER
C1. (lorp l)
C2. (consp l)
----------
C3. (in (min-l l) l) {L3, MP, C1, C2}

(< (len (del (min-l l) l)) (len l)) 
= {C3, C1, L2, MP}
t


Prove: (lorp l)/\ ~(endp l) => ((mss l) > (mss (del (min-l l) l)))
C1. (lorp l
C2. ~(endp l)
-----------
C3. (consp l) {C2, C1, Def endp}

(mss l)
= {Def mss}
(len l)
> {L1, C3, C1, MP}
(len (del (min-l l) l))
= {Def mss}
(mss (del (min-l l) l))
==================================SOLUTION END
|#


#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Section B: IN
 Next, let's do some proofs involving the function in
 and weave.

---------------------------------------------
Hopefully Helpful Theorems
You may assume the following theorems (or prove them
if you want the practice):

Phi_permReflect: (listp l) => (perm l l)

Assumption A1. (listp x) /\ (listp y)/\(listp z) /\ (in e y) =>
               (perm (cons e z) (app x y) = (perm z (app x (del e y)))

....in other words, even if e exists in list x, you can delete e from y
(provided it's in y) to see if z is a permutation of x and y minus element e.

---------------------------------------------

B1. Prove (listp x)/\ (listp y) => 
           (in e (app x y)) = ((in e x) \/ (in e y))

##..............
============================SOLUTION START
Using the induction scheme for in
1) ~(listp x) => phi_inapp
2) (listp x) /\ (endp x) => phi_inapp
3) (listp x) /\ ~(endp x) /\ (equal (first x e)) => phi_inapp
4) (listp x) /\ ~(endp x) /\ ~(equal (first x e)) 
   /\ phi_inapp|((x (rest x))) => phi_inapp



Obligation 1
C1. ~(listp x)
C2. (listp x)
---------------
C3. nil {C1, C2,PL}
nil=> phi is true.

Obligation 2
C1. (listp x)
C2. (endp x)
C3. (listp y)

(in e (app x y))
= {Def app, C2}
(in e y)
= {PL}
(nil \/ (in e y))
= {Def in, C2}
(in e x) \/ (in e y)

Obligation 3
C1. (listp x)
C2. (listp y)
C3. ~(endp x)
C4. (e = (first x))
-------------
(in e (app x y))
= {Def in, Def app, C2, first-rest axioms, C4}
t


Obligation 4
C1. (listp x)
C2. (listp y)
C3. ~(endp x)
C4. ~(e = (first x))
C5. (lisp (rest x)) /\ (listp y) 
=> ((in e (app (rest x) y))= (in e (rest x)) \/ (in e y))
-------------
C6. (lisp (rest l)) {C3, C1, Def endp, def listp}
C7. ((in e (app (rest x) y)) 
    = (in e (rest x)) \/ (in e y)) {C5, C6, C2, MP}

(in e (app x y))
= {Def app, C3}
(in e (cons (first x)(app (rest x) y)))
= {Def in, C4, C3}
(in e (app (rest x) y))
= {C7}
(in e (rest x)) \/ (in e y)
= {Def in, C4}
(in e (cons (first x)(rest x))) \/ (in e y)
= {First-rest axioms}
(in e x) \/ (in e y)

============================SOLUTION END

EXTRA QUESTION (no points and purely optional): B1 can be used to prove the following
B1b: (listp x)/\(listp y) => ((in e (app x y)) = (in e x) \/ (in e y))

How can you use B1 to prove this? and what other conjectures do you need 
to prove to get the equality (or iff)?  Prove B1b for extra practice.  
You can write B1b and the related theorems on your cheat sheet for 
the exam if you want.

##..............


B2. Prove (listp x)/\ (listp y) => 
           (in e (weave x y)) = ((in e x) \/ (in e y))

##..............

============================SOLUTION START

Using I.S. for weave
1) ~((listp x)/\ (listp y)) => B2
2) (listp x)/\ (listp y)/\(endp x) => B2
3) (listp x)/\ (listp y)/\~(endp x) /\(endp y) => B2
4) (listp x)/\ (listp y)/\~(endp x) /\~(endp y)
   /\ [(listp (rest x))/\ (listp (rest y)) => 
           ((in e (weave (rest x) (rest y))) 
           = ((in e (rest x)) \/ (in e (rest x))))]=> B2

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

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

(in e (weave x y))
= {Def weave, C3}
(in e y)
= {PL, DEf in, C3}
(in e x) \/ (in e y)

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

(in e (weave x y))
= {Def weave, C3, C4}
(in e x)
= {PL, Def in, C3, C4}
(in e x)\/(in e y)

Obligation 4:
C1. (listp x)
C2. (listp y)
C3. ~(endp y)
C4. ~(endp x)
C5. [(listp (rest x))/\ (listp (rest y)) => 
           ((in e (weave (rest x) (rest y))) 
           = ((in e (rest x)) \/ (in e (rest x))))]
---------------------------
C6. (listp (rest x)) {C1, C4, Def endp}
C7. (listp (rest y)) {C2, C3, Def endp}
C8. ((in e (weave (rest x) (rest y))) 
     = ((in e (rest x)) \/ (in e (rest y))))
    {C5, C6, C7, MP}

(in e (weave x y))
= {Def weave, C3, C4}
(in e (cons (first x)(cons (first y)(weave (rest x)(rest y)))))
= {Def in, PL}
(equal e (first x))\/(equal e (first y))
   \/(in e (weave (rest x)(rest y)))
= {C8}
(equal e (first x))\/(equal e (first y))
   \/(in e (rest x))\/(in e (rest y))
= {PL}
(equal e (first x))\/(in e (rest x))
\/(equal e (first y)) \/(in e (rest y))
= {Def in, PL, C3, C4}
(in e x) \/ (in e y)

QED
============================SOLUTION END

EXTRA (no points): prove 
Phi_permWA: (listp x)/\(listp y) =>(perm (weave x y)(app x y)) 
using the induction scheme for weave.
##..............

============================SOLUTION START
1) ~((listp x)/\ (listp y)) => Phi_permWA
2) (listp x)/\ (listp y)/\(endp x) => Phi_permWA
3) (listp x)/\ (listp y)/\~(endp x) /\(endp y) => Phi_permWA
4) (listp x)/\ (listp y)/\~(endp x) /\~(endp y)
   /\ [(listp (rest x))/\ (listp (rest y)) => 
           ((perm (weave (rest x) (rest y))(app (rest x)(rest y)))) 
=> Phi_permWA

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

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

(perm (weave x y)(app x y))
= {Def weave, Def app, C3}
(perm y y)
= {Phi_permReflect}
t

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

(perm (weave x y)(app x y))
= {Def weave, phi_appnil, C4}
(perm x x)
= {Phi_permReflect}
t

Obligation 4:
C1. (listp x)
C2.(listp y)
C3.~(endp x) 
C4. ~(endp y)
C5. (listp (rest x))/\ (listp (rest y)) => 
           ((perm (weave (rest x) (rest y))(app (rest x)(rest y)))) 
-------------------
C6. (listp (rest x)) {C1, C4, Def endp}
C7. (listp (rest y)) {C2, C3, Def endp}
C8. (perm (weave (rest x)(rest y))(app (rest x)(rest y))) {C6, C7, C5, MP}
C9. (in (first y) y) {Def in, C4}

(perm (weave x y)(app x y))
= {Def weave, C3, c4}
(perm (cons (first x) (cons (first y)(weave (rest x)(rest y))))
      (app (x y)))
= {Def perm, first-rest axiom, C3, Def in}
(perm (cons (first y)(weave (rest x)(rest y)))
      (app (del (first x)(app x y))))
= {Def del, Def app, C3}
(perm (cons (first y)(weave (rest x)(rest y)))
      (app (app (rest x) y)))
= {Def perm, first-rest axiom, C4, Def in, }
(perm (weave (rest x)(rest y))(del (first y) (app (rest x) y)))
= {A1, C9}
(perm (weave (rest x)(rest y))(app (rest x)(rest y)))
= {C5}
t
============================SOLUTION END
|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Section C: Tail Recursion I
Let's revisit some functions from the sample exam.
|#

;; add-to-all: nat x LON -> LON
;; (add-to-all n l) takes a natural number n and
;; a list of natural numbers l and adds n to each element of l:
(defunc add-to-all (n l)
  :input-contract (and (natp n) (lonp l))
  :output-contract (lonp (add-to-all n l))
  (if (endp l)
    ()
    (cons (+ (first l) n) (add-to-all n (rest l)))))

(check= (add-to-all 1 '(1 2 3)) '(2 3 4))

;; find: All x List -> LON
;; (find x l) returns the indexes of each occurence of
;; x in list l.  Thus the returned value is a list of natural numbers
(defunc find (x l)
  :input-contract (listp l)
  :output-contract (lonp (find x l))
  (cond ((endp l) ())
        ((equal (first l) x) (cons 0 (add-to-all 1 (find x (rest l)))))
        (t                           (add-to-all 1 (find x (rest l))))))

(check= (find 1 '(1 2 3 2 1)) '(0 4)) ; find counting starts from 0


#|
a)  Now define a tail-recursive version find-t of find.

Hint: the tail-recursive function find-t walks through the input list
from left to right. Suppose you see an occurrence of x. In order to know
what its index is in the *original* list, you have to keep track of the
number of elements already processed. Function find-t should thus have
an extra argument, say c, for that purpose:

##..............

|#
;;========================SOLUTION START
(defunc find-t (x l c acc)
  :input-contract (and (listp l) (natp c) (lonp acc))
  :output-contract (lonp (find-t x l c acc))
  (cond ((endp l) acc)
        ((equal (first l) x) (find-t x (rest l) (+ c 1) (cons c acc)))
        (t                   (find-t x (rest l) (+ c 1)         acc))))
;;=========================SOLUTION END
#|
(c) We define below a non-recursive function find* that uses find-t to
compute the same value as find. Note that we need to initialize both c 
and acc properly.
|#
##..............
;;========================SOLUTION START
(defunc find* (x l)
  :input-contract (listp l)
  :output-contract (lonp (find x l))
  (rev (find-t x l 0 ())))

(check= (find* 1 '(1 2 3 2 1)) '(0 4))
;;========================SOLUTION END
#|
(d) Write a lemma that relates find-t and find.

Hint: this requires some thought. Evaluate find-t on some examples to
figure out what it should be. The lemma will involve several functions other
than find-t and find. Remember add-to-all. There should be no
constants anywhere in your lemma.

HINT: Use test? to sanity-check your lemma.
##..............
;;========================SOLUTION START
phi: (listp l) /\ (natp c) /\ (lonp acc) => (find-t x l c acc) = (app (rev (add-to-all c (find x l))) acc)
;;========================SOLUTION END

(e) Assuming the lemma is true, prove that find* and find compute
the same function:

##..............

;;========================SOLUTION START
(listp l) => (find* x l) = (find x l)

  (find* x l)

= { def. find* }

  (rev (find-t x l 0 ()))

= { phi: ((c 0) (acc ())) }

  (rev (app (rev (add-to-all 0 (find x l))) ()))

= { lemma: (listp x) => (app x nil) = x }

  (rev (rev (add-to-all 0 (find x l)))

= { lemma: (listp x) => (rev (rev x)) = x }

  (add-to-all 0 (find x l))

= { lemma: (lonp l) => (add-to-all 0 l) = l }

  (find x l)
;;========================SOLUTION END

(f) Prove the lemma in (d).

In proving the lemma, you can assume the following:

(natp a) /\ (lonp l) => (lonp (cons a l)) (we typically say "Def of lon" but
it's OK to be more specific like this from time to time)

In addition, during the proof you will need several lemmas that we have
proven before, and some that are new.
***************
L2: (listp l) /\ (natp c) /\ (lonp acc) => (find-t x l c acc) = (app (rev (add-to-all  c (find x l))) acc)

L3: (natp c) /\ (natp i) /\ (listp l) => (cons c (add-to-all (+ c i) l)) = (add-to-all c (cons 0 (add-to-all i l)))

##..............
====================SOLUTION START
We use the IS from find-t
Obligation 1
C1. ~(listp l) /\ (natp c) /\ (lonp acc)
C2. (listp l) /\ (natp c) /\ (lonp acc)
----------
C3. nil

The (endp l) case  
Context:
C1. (listp l)
C2. (natp c)
C3. (lonp acc)
C4. (endp l)
Proof:
RHS
(app (rev (add-to-all  c (find x l))) acc)
={Def. find, C4, C2, C3}
(app (rev (add-to-all  c nil)) acc)
={Def. add-to-all, C2, C3}
(app (rev nil) acc)
={Def. rev, C3}
(app nil acc)
={ Def. app, C3}
acc
={Def find-t, C4, C1, C2, C3}
(find-t x l c acc)
RHS
QED

The first recursive case:

C1. (listp l)
C2. (natp c)
C3. (lonp acc)
C4. (not (endp l))
C5. (first l) = x
C6. phi|((l (rest l)) (c (+ c 1)) (acc (cons c acc)))
- - -
C7. (listp (rest l)) {C1, C4, Def. listp}
C8. (natp (+ c 1)) {C2}
C9. (lonp (cons c acc)) {C3, C2}
C10. (find-t x (rest l) (+ c 1) (cons c acc)) = (app (rev (add-to-all (+ c 1) (find x (rest l)))) (cons c acc)) {C7, C8, C9, C6, MP}

  (find-t x l c acc)

= { def. find-t, C4, C5 }

  (find-t x (rest l) (+ c 1) (cons c acc))

= { C10 }

  (app (rev (add-to-all (+ c 1) (find x (rest l)))) (cons c acc))

= { associativity app, after rewriting (cons c acc) = (app (list c) acc) }

  (app (app (rev (add-to-all (+ c 1) (find x (rest l)))) (list c)) acc)

= { lemma: (listp x) /\ (listp y) => (app (rev x) (rev y)) = (rev (app y x)) }

  (app (rev (app (list c) (add-to-all (+ c 1) (find x (rest l))))) acc)

= { def. app, axioms cons, list }

  (app (rev (cons c (add-to-all (+ c 1) (find x (rest l))))) acc)

= { lemma: (cons c (add-to-all (+ c i) l)) = (add-to-all c (cons 0 (add-to-all i l))) }

  (app (rev (add-to-all c (cons 0 (add-to-all 1 (find x (rest l)))))) acc)

= { def. find, C4, C5 }

  (app (rev (add-to-all c (find x l))) acc)
  
====================SOLUTION END

(g) Prove any new lemmas used in (f).
(if there are any)
##..............
 
|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Section D: Tail Recursion II: Revenge of Weave
 
 a) Remember weave?  I told you we would keep using the same
 function for these proofs. Write a tail recursive
 version of weave (weave-t) and a wrapper function weave*
 Keep in mind the order that (first x) and (first y) are being
 added to acc.
 
 (defunc weave (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (weave x y))
  (cond ((endp x) y)
        ((endp y) x)
        (t (cons (first x) 
                 (cons (first y)
                       (weave (rest x)(rest y)))))))
|#
##..............
;;======================SOLUTION START
 (defunc weave-t (x y acc)
  :input-contract (and (listp x)(listp y)(listp acc))
  :output-contract (listp (weave-t x y acc))
  (cond ((endp x) (app (rev acc) y))
        ((endp y) (app (rev acc) x))
        (t (weave-t (rest x)(rest y)
                    (cons (first y)
                          (cons (first x) acc))))))
 
 (defunc weave* (x y)
   :input-contract (and (listp x)(listp y))
   :output-contract (listp (weave* x y))
   (weave-t x y nil))
                                                         
;;======================SOLUTION END
 

 #|
 b) Now prove that weave* = weave. You should do all the steps we outlined
 in our tail recursive proof recipe.
 ##..............
 ====================SOLUTION START
 Lemma D1: (listp x)/\(listp y)/\(listp acc) => 
    [(weave-t x y acc) = (app (rev acc) (weave x y))]
 
 Prove weave* = weave
 C1. (listp x)
 C2. (listp y)

 (weave* x y)
 = {def weave}
 (weave-t x y nil)
 = {D1}
 (app (rev nil) (weave x y))
 = {Def endp, def rev}
 (app nil (weave x  y))
 = {Def endp, def app}
 (weave x y)
 
 Prove D1 using the Induction scheme for weave
1) ~((listp x)/\ (listp y)/\(listp acc)) => D1
2) (listp x)/\ (listp y)/\(listp acc)/\(endp x) => D1
3) (listp x)/\ (listp y)/\(listp acc)/\~(endp x) /\(endp y) => D1
4) (listp x)/\ (listp y)/\(listp acc)/\~(endp x) /\~(endp y)
   /\ [(listp (rest x))/\ (listp (rest y)
       /\ (listp (cons (first y)(cons (first x) acc)))) => 
           (weave-t (rest x) (rest y) (cons (first y)(cons (first x) acc)))
           = (app (rev (cons (first y)(cons (first x) acc))) (weave (rest x)(rest y))]=> D1
 
 
Obligation 1
C1. ~((listp x)/\ (listp y)/\(listp acc))
C2. ((listp x)/\ (listp y)/\(listp acc))
---------------
C3. nil {C1, C2,PL}
nil=> x is true.

Obligation 2
C1. ((listp x)
C2. (listp y)
C3. (listp acc)
C4. (endp x)

(app (rev acc)(weave x y))
= {Def weave, C4}
(app (rev acc) y)
= {Def weave-t, C4}
(weave-t x y acc)


Obligation 3
C1. ((listp x)
C2. (listp y)
C3. (listp acc)
C4. ~(endp x)
C5. (endp y)

(app (rev acc)(weave x y))
= {Def weave, C4, C5}
(app (rev acc) x)
= {Def weave-t, C4, C5}
(weave-t x y acc)

Obligation 4
C1. (listp x)
C2. (listp y)
C3. (listp acc)
C4. ~(endp x)
C5. ~(endp y)
C6. [(listp (rest x))/\ (listp (rest y)
     /\ (listp (cons (first y)(cons (first x) acc)))) => 
        (weave-t (rest x) (rest y) (cons (first y)(cons (first x) acc)))  
         = (app (rev (cons (first y)(cons (first x) acc))) (weave (rest x)(rest y))]
---------------
C7. (listp (rest x)){C4, C1, Def listp, def endp}
C8. (listp (rest y)){C5, C2, Def listp, def endp}
C9. (listp (cons (first y)(cons (first x) acc)))) {Def listp, C3}
C10. (weave-t (rest x) (rest y) (cons (first y)(cons (first x) acc))) 
         = (app (rev (cons (first y)(cons (first x) acc))) (weave (rest x)(rest y))
         {C7, C8, C9, C6, MP}

(app (rev acc) (weave x y))
= {C4, C5, Def weave}
(app (rev acc) (cons (first y)(cons (first x)(weave (rest x)(rest y)))))
= {Def app (twice), Def list}
(app (rev acc)(app (list (first y)(first x))(weave (rest x)(rest y))))
= {Assoc. app}
(app (app (rev acc) (list (first y)(first x)))(weave (rest x)(rest y)))
= {phi_app_rev}
(app (rev (app (rev (list (first y)(first x))) (rev (rev acc))))(weave (rest x)(rest y)))
= {Phi_rev_rev}
(app (rev (app (rev (list (first y)(first x))) acc))(weave (rest x)(rest y)))
= {def rev (twice), def list, def endp}
(app (rev (app (list (first x))(list (first y))) acc) (weave (rest x)(rest y)))
= {Def app (twice)}
(app (rev (cons (first x)(cons (first y) acc)))(weave (rest x)(rest y)))
= {C10}
(weave-t (rest x)(rest y)(cons (first y)(cons (first x) acc)))
= {Def weave-t, C4, C5}
(weave-t x y acc)
=========================SOLUTION END
 |#
 
 #|
 Extra Practice: Write a tail recursive version of isort
 (don't get fancy by calling max-l instead of min-l.  Just reverse
 the sorted list at the end)
 The solution won't be provided but it's still a good exercise
 ##.......................
 ;;================SOLUTION
 A solution is not given but I'm willing to supply it IF you submit 
 or show your solution first
 |#
 
 
#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
E. A Heap of Work (no points BUT abstract data types
can potentially appear on the exam. This tests the concept
at a greater difficulty than the exam)

Consider the binary heap data definition above.

A heap is a semi-ordered tree-based data structure such that the "top" or root node of 
a heap is the smallest element in the structure.  This is considered a min heap.  A max heap 
(not discussed here) has the largest value as the root node. A binary heap is a binary tree 
such that the value of the two children of any given node must be larger than the parent's 
value.  Hence a heap may look like this.
    3
 5     6
7 8   7 9

Calling pop on this heap gives the following
    5 
 7     6
  8   7 9

Popping again gives:
    6
 7     7
  8     9
  
Inserting the value 5 results in the following structure:
    6
 7     7
5 8     9

And then a series of operations which bubble the 5 up to the appropriate point
    5
 6     7
7 8     9

For more information on heaps see: https://en.wikipedia.org/wiki/Heap_(data_structure)

We will consider the following functions:
Insert: adds a value to the heap. The position of the value within the heap will vary
depending on the implementation
emptyp: Returns a boolean whether a heap is empty or not.
Pop: Remove the root node of the heap and adjust the heap accordingly.

E1.
What other basic functions should a heap have if implemented in ACL2s? Only write functions 
that cannot be created by a series of other basic functions.  

For example, function "heap-size" which returns the number of values in the heap 
would not be acceptable because it can be written  as a series of pop operations until 
the heap is empty.

* Give at least 2 "independent functions" that cannot be defined in terms of insert, emptyp,
or pop.
* You do not need to write the functions and your answers should be relatively simple but 
you need to clearly identify what the function does (like the the functions listed above).
* Feel free to implement the functions if you want to. Your answer will be a lot more 
obvious in such a case.
......................

|#

(defdata BinHeap
  (oneof nil
         (list rational BinHeap BinHeap)))

;; These functions can be difficult to admit so we will not
;; admit them in logic mode.  Your properties in G2 also don't need
;; to be proven as theorems.
:program

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; new-node: Rational x BinHeap x BinHeap -> BinHeap
;; (newnode v c1 c2) is a helper function
;; that makes a heap node with v as the value
;; and c1 and c2 as child nodes.
(defunc new-node (v c1 c2)
  :input-contract (and (rationalp v)(BinHeapp c1)(BinHeapp c2))
  :output-contract (BinHeapp (new-node v c1 c2))
  (list v c1 c2))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; emptyp: BinHeap -> Boolean
;; (emptyp h) takse a heap h and returns
;; true if it is empty (has no values)
(defunc emptyp (h)
  :input-contract (BinHeapp h)
  :output-contract (booleanp (emptyp h))
  (equal h nil))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; heap-size: BinHeap -> Nat
;; (heap-size h) takes a heap h and returns
;; the number of values in it. An empty heap
;; returns 0.
(defunc heap-size (h)
  :input-contract (BinHeapp h)
  :output-contract (natp (heap-size h))
  (if (emptyp h)
    0
    (+ 1 (+ (heap-size (second h))
            (heap-size (third h))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; balance: BinHeap -> BinHeap
;; (balance par) takes a "parent" heap node par 
;; and swaps parent and child values if a child
;; node value is less than the parent's value
;; This works under the assumption that before 
;; insertion the heap is well formed. Thus at MOST 
;; one child can have a smaller value than the parent node.
(defunc balance (par)
  :input-contract (BinHeapp par)
  :output-contract (BinHeapp (balance par))
  (if (emptyp par)  
    par
    (let ((c1 (second par))
          (c2 (third par)))
      (cond ((and (not (emptyp c1))(< (first c1)(first par)))
             (new-node (first c1) 
                       (new-node (first par)(second c1)(third c1))
                       c2))
            ((and (not (emptyp c2))(< (first c2)(first par)))
             (new-node (first c2)  c1
                       (new-node (first par)(second c2)(third c2))))
            (t  par)))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; insert: Rational x BinHeap -> BinHeap
;; (insert r h) inserts r at the shallowest
;; branch of the heap and then rebalances the heap
;; up to the root node to ensure the heap structure
;; maintained.
(defunc insert (r h)
  :input-contract (and (rationalp r)(BinHeapp h))
  :output-contract (BinHeapp (insert r h))
  (if (emptyp h)
    (list r nil nil)
    (let ((lDepth (heap-size (second h)))
          (rDepth (heap-size (third h))))
      (if (<= lDepth rDepth)
        (balance (new-node (first h) (insert r (second h)) (third h)))
        (balance (new-node (first h) (second h) (insert r (third h))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; pop: BinHeap -> BinHeap
;; (pop h) removes the root element of the heap 
;; (the min value in the heap),  fixes the structure
;; and then returns the revised heap.
(defunc pop (h)
  :input-contract (BinHeapp h)
  :output-contract (BinHeapp (pop h))
  (cond ((emptyp h)  h)
        ((and (emptyp (second h))(emptyp (third h))) nil)
        ((emptyp (second h)) (third h))
        ((emptyp (third h)) (second h))
        ((< (first (second h))(first (third h))) 
         (list (first (second h)) (pop (second h))(third h)))
        (t  (list (first (third h)) (second h)(pop (third h))))))

;; Valid-heapp and valid-node are not strictly needed for heap definitions but it can help
;; with your testing.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; valid-nodep: BinHeap -> Boolean
;; (valid-nodep h) checks if the value of h is less than
;; or equal to the value of any child nodes.
(defunc valid-nodep (h)
  :input-contract (BinHeapp h)
  :output-contract (booleanp (valid-nodep h))
  (cond ((emptyp h) t)
        ((and (emptyp (second h))(emptyp (third h))) t)
        ((emptyp (second h)) (<= (first h)(first (third h))))
        ((emptyp (third h))  (<= (first h)(first (second h))))
        (t (and (<= (first h)(first (second h)))
                (<= (first h)(first (third h)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; valid-heapp: All -> Boolean
;; (valid-heapp h) traverses a heap h to confirm that
;; all child node values are strictly greater than the 
;; parent node values. If h is not a heap than return nil.
(defunc valid-heapp (h)
  :input-contract t
  :output-contract (booleanp (valid-heapp h))
  (if (not (BinHeapp h))
    nil    
    (if (emptyp h)
      t
      (if (valid-nodep h)
        (and (valid-heapp (second h))
             (valid-heapp (third h)))
        nil))))
  
  (defconst *test-heap* (insert 6 (insert 1 (insert 4 (insert 2 nil)))))
  (check= (valid-heapp *test-heap*) t)
  (check= (valid-heapp (pop *test-heap*)) t)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; E1.
##.............. ADD OTHER FUNCTIONS
;;=======================SOLUTION START
 SOLUTION
(defunc new-heap()
  :input-contract t
  :output-contract (BinHeapp (new-heap))
  nil)


 (defunc peek(h)
 :input-contract (and (BinHeapp h)(not (emptyp h)))
 :output-contract (rationalp (peek h))
 (first h))
 ;;================SOLUTION END
#|
E2.
 Above you can see an implementation of insert, emptyp and pop. For anyone who has 
 implemented a heap before, you'll notice how inefficient this implementation is. 
 In a language like Java, an array can be used and the place to insert the next 
 value is relatively fast. This begs the question: what guarantees does any heap 
 implementation need?
 * Write at least 2 more properties of a min heap that all implementations
   MUST pass. You can include the functions you described in G1.
 * Properties should be independent. A way to show this is to change the implementation
   of the functions and observe only the one property is no longer satisfied. We did
   this for properties of stacks in the lecture.
 * Properties should be written as a ACL2s theorem definition OR as a test?. 
   -If you want to test your functions (if you implemented code for G1), you can write
   test? to test if your properties are likely correct.  
   - If you simply wrote a function description, write the theorem as a comment.
 * See Chapter 8 of the lecture notes for more information about abstract data types
   and independent properties.
   
|#

;; Here are a couple properties
(test? (implies (and (rationalp r)(BinHeapp h)(emptyp h)) 
                (emptyp (pop (insert r h)))))

##..............
;;-==============================SOLUTION START
(test? (implies (rationalp r) (emptyp (new-heap))))

(test? (implies (and (rationalp r) (BinHeapp h)(valid-heapp h)(not (emptyp h))(< r (peek h)))
                (equal r (peek (insert r h)))))

;; Not really independent but still a nice property
(test? (implies (and (rationalp r)(BinHeapp h)) 
                (>= (heap-size (insert r h))(heap-size h))))

(test? (implies (and (rationalp r1)(rationalp r2)
                     (BinHeapp h)(valid-heapp h))
                (<= (peek (insert r2 (insert r1 h)))
                    (peek (pop (insert r2 (insert r1 h)))))))

;; There are plenty of other properties.  I hope you were creative and came up with good ones.
;;================================SOLUTION END
#| Good luck on the exam everyone. |#