#|

CS 2800 Homework 11 - Fall 2019

This homework is done in groups: instructions as per homework 02.
In particular:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

 * YOU MUST LIST THE NAMES OF ALL GROUP MEMBERS SUBMITTING THIS HOMEWORK:

Names of ALL group members: ...




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Technical and programming instructions: as per previous homeworks,
but change file names appropriately.

Additional instructions: 

This homework is about formal proofs.

When we ask you to prove something, we ask for a formal proof using
any of the methods studied in class: equational reasoning, induction, etc.
If you use induction, you must clearly state that you are using induction,
and also identify clearly which induction scheme you are using!

If you need lemmas, identify them and prove them, also using formal proofs.

|#


;; we first define some well-known functions:
(definec aapp (x :tl y :tl) :tl
  (if (endp x)
      y
    (cons (car x) (aapp (cdr x) y))))

(definec rrev (x :tl) :tl
  (if (endp x)
    nil
    (aapp (rrev (rest x)) (list (first x)))))

;; we then define some well-known lemmas about
;; these functions. feel free to use these lemmas
;; in your proofs. you don't have to show proofs
;; of the lemmas below in your homework answers.
;; BUT YOU MUST BE ABLE TO PROVE ALL THESE LEMMAS
;; YOURSELF IF REQUESTED (e.g., in an exam).
(defthm aapp-associative
  (implies (and (tlp x) (tlp y) (tlp z))
           (equal (aapp (aapp x y) z)
                  (aapp x (aapp y z)))))

(defthm aapp-nil
  (implies (tlp x)
           (equal (aapp x nil)
                  x)))

(defthm aapp-len
  (implies (and (tlp x) (tlp y))
           (equal (len (aapp x y))
                  (+ (len x) (len y)))))

(defthm rrev-rrev
  (implies (tlp x)
           (equal (rrev (rrev x)) x)))

(defthm len-rrev
  (implies (tlp x)
           (equal (len (rrev x)) 
                  (len x))))

;; We then define the following data types:
(defdata lvar (listof var))

;; these lemmas specialize the output contracts of
;; aapp and rrev to lvar's: they say that if these
;; functions take as input lvar's, they return lvar's:
(defthm aapp-lvar
  (implies (and (lvarp x) (lvarp y))
           (lvarp (aapp x y))))

(defthm rrev-lvar
  (implies (lvarp l) (lvarp (rrev l))))


(defdata vbpair (cons var boolean))
(defdata assignment (listof vbpair))

(check= (assignmentp '((x . t) (y . nil))) t)

(defdata loa (listof assignment))

;; these lemmas specialize the output contracts of
;; aapp and rrev to loa's: they say that if these
;; functions take as input loa's, they return loa's:
(defthm aapp-loa
  (implies (and (loap x) (loap y))
           (loap (aapp x y))))

(defthm rrev-loa
  (implies (loap l) (loap (rrev l))))

;; we define these two functions below.
;; make sure you understand what they are doing.
;; hint: they are similar to a previous homework.
(definec add (x :var b :boolean l :loa) :loa
  (let ((p (cons x b)))
    (if (endp l)
      nil
      (cons (cons p (first l)) (add x b (rest l))))))

(definec f (l :lvar) :loa
  (if (endp l) (list nil)
    (let
      ((rl (f (rest l)))
       (x (first l)))
      (aapp (add x t rl)
            (add x nil rl)))))

;; check the outputs of these calls to make sure you understand them:
(f nil)
(f '(x))
(f '(x y))

;; the power of 2 function:
(definec pow2 (n :nat) :nat
  (if (= n 0) 1
    (* 2 (pow2 (- n 1)))))

#|
11.1.
Prove formally the claim below:

Claim 1: (lvarp l) => (len (f l)) = (pow2 (len l))

Here and in the rest of this homework, we require formal proofs.
You can use without proof any of the lemmas above, 
and any lemma we proved in class.
If you use a lemma that we proved in class, state which lemma!

You can introduce new lemmas as you need: if you do that, you
must prove all these lemmas.

If you use induction, specify clearly which induction scheme
you are using (function, variables).
|#

#|
; ANSWER:
...
|#




#|
11.2.
The function "add" above is not tail-recursive.
Define a new function, called "addt", which is the
tail-recursive version of add: addt uses an accumulator.
|#

; ANSWER:
(definec addt (x :var b :boolean l :loa acc :loa) :loa
  ...)



#|
11.3.
Define a new function, called "add*", which calls addt
with the appropriate arguments, so that add* is equivalent
to the original "add" function. That is, the following
claim must be a theorem (you will be asked to prove it later):

Claim add-add*: 
  (implies (and (varp x) (booleanp b) (loap l))
           (equal (add* x b l)
                  (add x b l)))
|#

; ANSWER:
(definec add* (x :var b :boolean l :loa) :loa
  ...)



#|
11.4.
Identify the lemma "add-addt" that relates add and addt,
as per the tail-recursive reasoning recipe:

;; ANSWER:
(defthm add-addt
  (implies ...
           ...))
|#




#|
11.5.
Prove formally the lemma add-addt that you formulated in 11.4.
Prove formally this lemma using the tail-recursive reasoning recipe:

;; ANSWER:
...
|#




#|
11.6.
Prove formally the Claim add-add* defined earlier in 11.3:

;; ANSWER:
...
|#




#|
11.7.
The function "f" above is not tail-recursive.
Define a new function, called "ft", which is the
tail-recursive version of f: ft uses an accumulator.
|#
;; ANSWER:
(definec ft (l :lvar acc :loa) :loa
  ...)



#|
11.8.
Define a new function, called "f*", which calls ft
with the appropriate arguments, so that f* is equivalent
to the original "f" function. That is, the following
claim must be a theorem (do not try to prove it):

Claim f-f*: (lvarp l) => (f* l) = (f l)
|#
;; ANSWER:
(definec f* (l :lvar) :loa
  ...)



#|
11.9. 
Prove formally the following claim:

Claim len-f*
  (implies (lvarp l)
           (equal (len (f* l))
                  (pow2 (len l))))
|#

#|
; ANSWER:
...
|#



#|
11.10.
We will not require that you prove that f and f*
are equivalent.
Instead, we will ask you to identify the lemma
f-ft that relates f and ft (this is like in the
tail-recursion reasoning recipe). You don't have
to prove that lemma f-ft, you just have to state
it formally (you don't have to prove it using ACL2s
either).

Note that in order to state the lemma f-ft you may
have to introduce new functions! These must be
admissible ACL2s functions.

;; ANSWER:
...
|#



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;  Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
Each we'll take a short survey to monitor homework difficulty and to solicit feedback.

This survey is anonymous. We don't collect names, emails, etc. Each student responds individually. 
If you answer all mandatory questions, you get 5 points for this homework set. 
You report who among your team answered the survey in your homework answers, and we trust you 
that you reported this truthfully. 

Please fill out the following form (one response per team member):

https://docs.google.com/forms/d/e/1FAIpQLScLuFHusJNaX0cLducQCApffnPHkZFMNtdJKK-G1wN1YszyNA/viewform?usp=sf_link

Report here who in your team filled the form:

The following team members filled out the feedback survey provided by
the link above (replace the ...'s with the names of the team members
who filled out the questionnaire).

<Firstname> <LastName>
...
...
...
|#