#|
CS 2800 Homework 10 - Summer 2018


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

If your group does not already exist:

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

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

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.
   If you fail to follow these instructions, it costs us time and
   it will cost you points, so please read carefully.


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

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

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

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

|#

#|
------------------------------------
REASONING ABOUT TAIL-RECURSIVE FUNCTIONS

You can freely use the definitional and function contract theorems of
the functions we provide below or that we have covered in class. You
can also freely use any theorems we proved in class and in the lecture
notes.

Make sure you identify what induction scheme you are using.  For
example, suppose you were proving that app is associative:

(listp x) ^ (listp y) ^ (listp z) =>
(app (app x y) z) = (app x (app y z))

At the beggining of the proof you should say:

Proof by induction using (listp x).

You will be asked to define tail recursive versions of given
functions, using accumulators. This involves two function
definitions. 

For example, to define a tail recursive version of rev, we first
define rev-tl. rev-tl is recursive and has an extra argument, the
accumulator. Second, we define rev*, a non-recursive function that
calls rev-tl with the accumulater appropriately initialized and which
satisfies the theorem that rev* = rev, ie, :

(listp x) => (rev* x) = (rev x)

|#

;; Tail-recursive version of rev (auxiliary function)
(defunc rev-tl (x acc)
  :input-contract (and (listp x) (listp acc))
  :output-contract (listp (rev-tl x acc))
  (if (endp x)
      acc
    (rev-tl (rest x) (cons (first x) acc))))

;; Non-recursive version of rev that uses rev-tl
(defunc rev* (x)
  :input-contract (listp x) 
  :output-contract (listp (rev* x))
  (rev-tl x nil))

#|

You will also be asked to prove that the tail recursive version of a
function is equal to the original function.  For our
example, the theorem is

(implies (listp x)
         (equal (rev* x)
                (rev x)))

To do that you have to come up with lemmas; in particular you have to
come up with the right generalizations. If you choose to use ACL2s to
help you figure out the proofs, here is how you would do that:
|#

; This is the lemma we need
(defthm revt-rev
  (implies (and (listp x)
                (listp acc))
           (equal (rev-tl x acc)
                  (app (rev x) acc))))

; With the lemma above, the main theorem follows
(defthm rev*-rev
  (implies (listp a)
           (equal (rev* a)
                  (rev a))))

; The proofs were given in class.



#|
=====================================
Q1. In this example, we will see how to speed up numeric functions.

Consider the following Fibinacci-like function. Notice it takes a long time to admit
because it takes a long time to run (so testing takes a long time).
NOTE: going to labs will be extremely useful for this function.  We'll be
covering the fib-t proof

|#
:program
(defunc f1 (p)
  :input-contract (posp p)
  :output-contract (posp (f1 p))
  (if (<= p 2)
      (+ p 2)
    (+ (f1 (- p 1))
       (f1 (- p 2)))))

#|
Q1a

Think about why f1 takes long. Consider

(f1 6) = (f1 5) + (f1 4)
       = (f1 4) + (f1 3) + (f1 3) + (f1 2)
       = (f1 3) + (f1 2) + (f1 2) + (f1 1) + (f1 2) + (f1 1)
Notice that (f1 2) was computed multiple times, as was (f1 1). 
This leads to an exponential number of calls to f1.

We can do better.

Define f1-t, a function that takes multiple arguments and can be used
to compute f1 quickly. f1-t should only lead to a linear (in n) number
of recursive calls.

Note that you can have as many arguments to f1-t as you like.

|#
(defunc f1-t (p a b)
  :input-contract (and (posp p) (posp a) (posp b))
  :output-contract (posp (f1-t p a b))
  (cond ((equal p 1) 3)
        ((equal p 2) b)
;#......#

#|

Q1b

Define f1*, a non-recursive function that has the same signature as f1
and uses f1-t to efficiently compute f1. f1* should be equal to f1.

|#
#......#
#|
Q1c

Prove a theorem of this form

(implies ...
         (equal (f1-t ...)
                ... (f1 n) ....))
                
HOWEVER, we gave this to students last term and even I couldn't figure it out (at
least not with people looking at me).  Thus let me remind you of something:

(defunc fib (n)
  :input-contract (natp n)
  :output-contract (natp (fib n))
  (if (<= n 1)
    n
    (+ (fib (- n 1))
       (fib (- n 2)))))
       
Fill out the following table:

(f1-t p a b)  |  p  | (ft p) | a  |  b  | (fib (- p 1))
--------------------------------------------------------
47            |  7  |  47    | 3  |  4  |  8
47            |  6  |  29    | 4  |  7  |  5
47            |  5  |        |    |     |  3
47            |  4  |        |    |     |  2
47            |  3  |        |    |     |  1
47            |  2  |        |    |     |  1
47            |  1  |        |    |     |  0
#......#


Furthermore, let me point out that (f1-t p a b) = (f1 p) + (a-3)______ + (b-4)_________
Essentially you are looking for a pattern to calculate the missing
term to match f1-t and ft.  F1-t always returns  the same value while
f1 changes based on a fib-like pattern.

#......#


Prove that (f1* p) = (f1 p) using your lemma.
#......#

NO POINTS BONUS QUESTION:  Prove the lemma involving f1-t that you defined above
....the basic arithmetic got  too hairy for me so I can't ask you to do it but 
it's still a nice exercise.
#......#
|#

#|
Q1e

If your definition of f* is correct and efficient, then the following
test should pass instantaniously......and if your answer doesn't match, check on piazza.
It's not like I can confirm my answer is correct

|#

(check=
 (f1* 500)
 504437965285332091151961460776886639946151838089152805116856792315125770984413464788131304805242011086876)

(check= (f1* 6) 29)
(check= (f1* 1) 3)
(check= (f1* 2) 4)
(test? (implies (and (posp p)(< p 30)) (equal (f1 p) (f1* p))))
#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2.  Let's revisit a problem from the sample exam.  You've been given functions 
how-many-t and how-many* such that how-many = how-many*
|#
(defunc how-many (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many e l))
  (if (endp l)
    0
    (+ (if (equal e (first l)) 1 0)
       (how-many e (rest l)))))

;; how-many-t: All x List x Nat -> Nat
;; The tail recursive helper function for how-many*
;; where acc keeps a tally of the number of instances of
;; found so far in the list l.
(defunc how-many-t (e l acc)
  :input-contract (and (listp l) (natp acc))
  :output-contract (natp (how-many-t e l acc))
  (if (endp l)
    acc
    (how-many-t e (rest l) (+ (if (equal e (first l)) 1 0) acc))))

;; how-many*: All x List -> Nat
(defunc how-many* (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many* e l))
  (how-many-t e l 0))

#|
The goal is to prove the following conjecture:

phi : (listp l) => (how-many* e l) = (how-many e l)

That is, we want to show that the two functions compute the same result on
all inputs. We will prove this in several steps.

(a) Formulate a lemma that relates how-many-t to how-many, by filling in the ... below:

phi_1 : (listp l) /\ (natp acc) => (how-many-t e l acc) =  ... (how-many e l) ...
#......#

(b) Prove phi_1. Use the induction scheme how-many-t gives rise to. Note
that how-many-t has an if nested inside other functions. You can rewrite
it, using cond, before extracting an induction scheme if you want to use
the I.S. generating pattern from the the notes (it may help).
#......#

(c) Using only equational reasoning (no induction!), prove the main
conjecture phi from above. Using phi_1 (which you just proved) this should
be very simple.
phi : (listp l) => (how-many* e l) = (how-many e l)

#......#
|#


#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2. Filtering Data
Consider the following defdata and the function get-integers that uses it:
We're going to selectively filter out all elements in a list that aren't integers
|#
(defdata integerlist (listof integer))

(defunc get-integers (l)
  :input-contract (listp l)
  :output-contract (integerlistp (get-integers l))
  (cond ((endp l)         nil)
        ((integerp (first l)) (cons (first l) (get-integers (rest l))))
        (t                (get-integers (rest l)))))

(check= (get-integers '(b "23" lk ())) ())
(check= (get-integers '(h "ter" -1 aw 9)) '(-1 9))
(check= (get-integers '("qw" "brc" aw (1 2 3) 89 rt -1)) '(89 -1))

;(a) Write the function get-integers-t, which is a tail-recursive version of
;get-integers with an accumulator:

;; get-integers-t: listp x integerlist -> integerlist
;; get-integers-t takes a list and removes all elements
;; in the list that are not integers (this includes sub-lists of integers)
;; acc is an accumulator that collects integers to return.
(defunc get-integers-t (l acc)
  ;;......................) ;;Obviously write your own tests too
  #......#
  
;; Here is get-integers*, a non-recursive function that calls
;; get-integers-t and suitably initializes l and acc :
(defunc get-integers* (l)
  :input-contract (listp l)
  :output-contract (integerlistp (get-integers* l))
  (rev (get-integers-t l ())))

#|
(c) Identify a lemma that relates get-integers-t to get-integers. Remember
that this is a generalization step, i.e., all arguments to get-integers-t
are variables (no constants). The RHS should include acc.
....................
#......#

(d) Assuming that lemma in (c) is true and using ONLY equational reasoning,
prove the main theorem:

  (listp l) => (get-integers* l) = (get-integers l)

If you need any "lemmas", note them down as "debt", to be proved later. This should
include any theorems that we've already proven (you won't need to prove these but you
still need to list them)
....................
#......#

(e) Prove the lemma in (c). Use the induction scheme of get-integers-t. In
doing so, you can use the following lemma for free (i.e., you don't need to
prove it).

L3: (integerp e) /\ (integerlistp l) => (integerlistp (cons e l))

Again, if you need another lemma, note it as "dept"

#......#

(f) List here any lemmas that you used in parts c and d. If any of them are "new", you need
to prove them. (Hint: all lemmas in my solution have appeared in class/notes
before but your proof my differ)
#......#

|#

#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3. Max Depth
Consider a btree data structure that we want to calculate the maximum depth for.  
We will do this in 2 parts:
1) Write the tail recursive functions t-maxdepth-t and t-maxdepth*
   - If you all find this too difficult I can supply t-maxdepth-t
     It is NOT what I want you spending all your time on.  You time
     should be spent on the proof.
2) Prove t-maxdepth* = t-maxdepth
|#
; A binary tree structure where each node has a numeric value
; Notice the tree does not have to be in order.
(defdata btree (oneof nil (list rational btree btree)))

;; An empty tree has no child nodes and no value.
(defunc t-emptyp (btree)
  :input-contract (btreep btree)
  :output-contract (booleanp (t-emptyp btree))
  (equal btree nil))

(check= (t-emptyp '(2 nil nil)) nil)
(check= (t-emptyp nil) t)
(check= (t-emptyp '(3 (4 nil nil) (4 (3 nil nil) (2 nil nil)))) nil)

(defunc max (x y)
  :input-contract (and (natp x)(natp y))
  :output-contract (natp (max x y))
  (if (< x y) y x))

;; Proof for non-empty trees.  Used to help ACL2s reason.
(defthm t_secondne (implies (and (btreep btree)(not (t-emptyp btree)))
                            (btreep (second btree))))
(defthm t_thirdne (implies (and (btreep btree)(not (t-emptyp btree)))
                             (btreep (third btree))))

(defconst *tTest* '(3 (4 (5 (6 nil nil) (7 nil (8 nil nil))) 
                         (4 (3 nil nil) (2 nil nil))) 
                      (5 nil nil)))

(defunc t-maxdepth (btree)
  :input-contract (btreep btree)
  :output-contract (natp (t-maxdepth btree))
  (if (t-emptyp btree)
    0
    (let ((sdepth (+ 1 (t-maxdepth (second btree))))
          (tdepth (+ 1 (t-maxdepth (third btree)))))
      (if (< sdepth tdepth)
        tdepth
        sdepth))))


(check= (t-maxdepth *tTest*) 5)
(check= (t-maxdepth (list 4 nil *tTest*)) 6)
(test? (implies (btreep tree)(equal (t-maxdepth (list 4 nil tree))(+ (t-maxdepth tree) 1)))) 

; Program mode is fine if you need that.
#......#

#|
Now prove t-maxdepth = t-maxdepth*.  You will need a lemma and you will have
to prove that lemma
#......#

|#
(t-maxdepth-t nil 8 24)
(t-maxdepth nil)
;; You can test  your lemma with test? if that makes your life easier.
#......#

#| EXTRA PRACTICE ???
If you want additional practice problems, try writing tail recursive functions
for the following functions and then prove they are equivalent to the original
   - min-l
   - delete
   - merge
In fact, for many functions that aren't already tail recursive, you can write a tail
recursive version and then prove the equivalence. You can generate your own problems.
   
|#