; ****************** BEGIN INITIALIZATION FOR ACL2s MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%") (value :invisible))
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%") (value :invisible))
(include-book "acl2s/base-theory" :dir :system :ttags :all)


#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "custom" :dir :acl2s-modes :ttags :all)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s mode.") (value :invisible))

;Settings common to all ACL2s modes
(acl2s-common-settings)
;(acl2::xdoc acl2s::defunc) ;; 3 seconds is too much time to spare -- commenting out [2015-02-01 Sun]

(acl2::xdoc acl2s::defunc) ; almost 3 seconds

; Non-events:
;(set-guard-checking :none)

(acl2::in-package "ACL2S")

; ******************* END INITIALIZATION FOR ACL2s MODE ******************* ;
;$ACL2s-SMode$;ACL2s
#|

CS 2800 Homework 11 - Summer 2018

This homework is to be done by INDIVIDUALLY and is designed to be done
under exam conditions.

 * The main section of the homework is designed to be taken under exam conditions
   and over a 2 hour period.  As such it would be a great idea for you to solve the
   problems using pen and paper and THEN type your answers in this file later
   Extra work but you want to feel comfortable taking the exam with a pen/pencil to
   match test conditions (look up State Dependent Learning if you want to know why).
 * Obviously I didn't time the duration of this homework.  The time required is an estimate.
   Don't panic if you take 2 hours and 10 minutes to complete.  Don't relax if it takes you
   40 minutes either. :)
 * The extra questions at the end of the exam are there for extra practice.  They aren't
   worth points but a 2 hour exam didn't seem like it gave sufficient practice for a review.

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

 |#

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

For each function fn below (f1...f4), 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
      but good practice later)
   4) Write the induction scheme that fn gives rise to.

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

#|
A1.

(defunc f1 (x y flag)
  :input-contract (and (listp x) (listp y) (booleanp flag))
  :output-contract (listp (f1 x y flag))
  (cond ((and flag (endp x)) y)
        ((and (not flag) (endp y)) x)
        (flag  (cons (first x)(f1 (rest x) y flag)))
        (t   (f1 (cons (first y) x) (rest y) flag))))
        
##..............


|#

#|
(defunc f2 (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (f2 x y))
  (cond ((equal (len x)(len y)) (app x y))
        ((< (len x)(len y))  (cons (first y)(f2 x (rest y))))
        (t  (f2 x (app y (list x))))))
##..............

|#


#|
A3.
;; Assume f3a is admissible....we will see it again soon.
(defunc f3a (l flag)
  :input-contract (and (listp l)(booleanp flag))
  :output-contract (listp (f3a l flag))
  (cond ((endp l) l)
        (flag (f3a (rest l) (not flag)))
        (t    (cons (first l)(f3a (rest l)(not flag))))))

;; You can prove this for practice
(defthm phi_f3a (implies (and (listp l)(consp l))(< (len (f3a l)) (len l))))

(defunc f3 (x)
  :input-contract (listp x)
  :output-contract (listp (f3 x))
  (cond ((endp x) x)
        ((endp (rest x)) x)
        (t (app (f3 (f3a x t))
                (f3 (f3a x nil))))))

##.............. JUST f3
|#



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

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

|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;
SECTION 2: half-list
Look at f3a.....it should actually be called half-list since it removes half the elements
from the list.  The flag changes which half of the elements are removed.
|#
(defunc half-list (l flag)
  :input-contract (and (listp l)(booleanp flag))
  :output-contract (listp (half-list l flag))
  (cond ((endp l) l)
        (flag (half-list (rest l) (not flag)))
        (t    (cons (first l)(half-list (rest l)(not flag))))))
#|
If you look carefully, however, you may notice that
phi_half_perm
(listp l)/\(booleanp flag) => (perm l (app (half-list l flag)(half-list l (not flag))))

OK. Time to prove this.

Identify the Induction Scheme you will use and the function that gives rise to it.

#......#


Now "prove" phi_half_perm.  You can ignore non-recursive proof obligations (hence the quotes
around the word prove).

You can use any theorems that we've discussed in the past or assumed
in homeworks.....and since I can't catch you doing it, you can look at previous homeworks.
This will help  you build your "cheat sheet"

#......#


OPTIONAL FOR NO MARKS (this question only)
If you want even MORE practice, take the function weave which we discussed in class:
(defunc weave (l1 l2)
  :input-contract (and (listp l1)(listp l2))
  :output-contract (listp (weave l1 l2))
  (cond ((endp l1) l2)
        ((endp l2) l1)
        (t (cons (first l1)(cons (first l2)(weave (rest l1)(rest l2)))))))
        
Prove (listp l) => (equal l (weave (half-list l nil)(half-list l t)))
|#


#|
;;;;;;;;;;;;;;;;;;;;;;;;;
SECTION 3: half-list*
NOTE: I'm worried that this question might be a bit too easy for an exam.
Thus do not be shocked if the exam question is a bit harder.
|#

  
;Define half-list-t
;half-list-t: list x boolean x list -> list
;(half-list-t l flag acc) removes elements in l if flag
; is true, otherwise it keeps the elements. 
;#......#


; half-list* should be equivalent to half-list. Write a function 
; half-list-t that is tail recursive and has an accumulator.
(defunc half-list* (l flag)
  :input-contract (and (listp l)(booleanp flag))
  :output-contract (listp (half-list* l flag))
  (half-list-t l flag nil))


(test? (implies (and (listp l)(booleanp flag)) 
                (equal (half-list l flag)
                       (half-list* l flag)))) 

#|
  Write a lemma relating half-list-t, it's accumulator and half-list? This lemma should
  contain no constants and 
  #......#

  
  Prove (listp l) /\ (booleanp flag) => (half-list* l flag) = (half-list l flag)
  #......#

  
  Now prove the lemma
  #......#










#|
***************
---------EVERYTHING BELOW HERE IS OPTIONAL------------

EXTRA PRACTICE QUESTION (no marks)

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


|#

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

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


|#

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

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


|#

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


|#

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

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

|#
#|
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, 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)
-----------------------------------

##..............
|#


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

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

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

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


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

|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 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:

##..............
|#

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

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


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

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


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

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

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

 #|
 b) Now prove that weave* = weave. You should do all the steps we outlined
 in our tail recursive proof recipe.
 ##..............
 |#
 
 #|
 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
 ##.......................

 |#
 

#| Good luck on the exam everyone. |#