#|

CS 2800 Homework 8 - 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 the definitional principle and admissibility.

DEFINITIONAL PRINCIPLE & ADMISSIBILITY

For each function definition below, answer whether it is admissible,
i.e., whether it satisfies all the rules of the definitional principle.

If you claim admissibility, BRIEFLY

1. Explain in English why the body contracts hold.
2. Explain in English why the contract theorem holds.
3. Explain in English why the function terminates.

If you claim non-admissibility, identify a rule in the Definitional Principle
that is violated.

If you blame one of the purely syntactic rules (variable names,
non-well-formed body etc), explain the violation in English.

If you blame one of the semantic rules (body contract, contract theorem or
termination), you must provide an input that satisfies the input contract, but
causes a violation in the body or violates the output contract or causes
non-termination. That is, you must provide a counterexample.

Remember that the rules are not independent: if you claim the function does
not terminate, you must provide an input on which the function runs forever
*without* causing a body contract violation: a body contract violation is
not a counterexample to termination. Similarly, if you claim the function
fails the contract theorem, you must provide an input on which it
terminates and produces a value, which then violates the output contract.

Your explanations should be brief but clear. We are not looking for a page
of text per question but we also want to clearly see that you understand
the function and if/what is wrong with it.

We are also not looking for formal proofs (like the equational proofs)
at this point. In the next homework, we will prove termination formally.
Here, we are just looking for informal arguments (English).

Note that there is a difference between a function being admissible,
as per the definitional principle, and ACL2s automatically proving
that it is admissible.  There are many functions that are admissible,
but ACL2s will not admit them without help from the user. Conversely,
it is possible that ACL2s has bugs, so it is possible that it erroneously
proves admissibility in some cases. The point is that you cannot justify
admissibility by saying "I entered the function definition into ACL2s
and it was admitted". You are welcome to try these functions on ACL2s,
but you cannot just report what ACL2s reports. You have to provide
your own arguments for or against admissibility, as per instructions 
above.

Example:

(definec llen (x :tl) :nat
  (if (endp x) 0
    (+ 1 (llen (rest x)))))

ANSWER:
Admissible.
- Body contracts: x is a tl by input contract, so it satisfies ic of endp;
                (rest x) is a tl assuming x is a tl;
                llen returns a nat so ic of + is satisfied.
- Contract theorem: both 0 and the result of + are nats, since 1 is nat
                        and the recursive call to llen returns a nat
- Termination: terminates when list is empty, and the length of the list
                decreases on every recursive call, so list eventually becomes
                empty.


|#

#|
8.1.

(definec f1 (x :nat) :rational
  (/ x 2))

; ANSWER:
...
|#


#|
8.2.

(definec division (x :rational y :rational) :rational
  (/ x y))

; ANSWER:
...
|#


#|
8.3.

(definec list-contains-only-numbers (l :tl) :bool
  (if (endp l) t
    (and (rationalp (first l))
         (list-contains-only-numbers (rest l)))))

; ANSWER:
...
|#




#|
8.4.

(defunc add-number-to-list-v3 (l x)
  :input-contract (and (tlp l) (rationalp x) (list-contains-only-numbers l))
  :output-contract (and (tlp (add-number-to-list-v3 l x))
                        (equal (len l) (len (add-number-to-list-v3 l x))))
  (cond
   ((endp l) nil)
   ((rationalp (first l)) (cons (+ (first l) x) (add-number-to-list-v3 (rest l) x)))
   (t (cons (first l) (add-number-to-list-v3 (rest l) x)))))

; ANSWER:
...
|#


#|
8.5.

(definec in (a :all X :tl) :bool
  (and (consp X)
       (or (equal a (first X))
           (in a (rest X)))))

; ANSWER:
...
|#

;; this function is given, and is admissible:
(definec aapp (x :tl y :tl) :tl
  (if (endp x)
    y
    (cons (first x) (aapp (rest x) y))))


#|
8.6.

(definec f2 (X :tl) :tl
  (if (endp X) ()
    (aapp (f2 (rest X)) (first X))))

; ANSWER:
...
|#


#|
8.7.

(definec f3 (X :tl) :tl
  (if (consp X)
    (aapp (f3 (cdr X)) (list (car X)))
    nil))

; ANSWER:
...
|#

;; this function is given, and is admissible:
(definec llen (x :tl) :nat
  (if (endp x)
    0
    (+ 1 (llen (rest x)))))


#|
8.8.

(definec list-insert-v1 (l :tl i :nat a :all) :tl
  (cond
   ((> i (llen l)) nil)
   ((equal i 0) (cons a l))
   (t (cons (first l) (list-insert-v1 (rest l) (- i 1) a)))))

; ANSWER:
...
|#

#|
8.9.

(definec list-insert-v2 (l :tl i :nat a :all) :tl
  (cond
   ((> i (llen l)) nil)
   ((equal i 0) (cons a l))
   ((endp l) nil)
   (t (cons (first l) (list-insert-v2 (rest l) (- i 1) a)))))


; ANSWER:
...
|#

; these definitions are given, you don't have to prove anything about them:
(defconst *not* '~)
(defconst *and* '&)
(defconst *or* '+)
(defconst *implies* '=>)
(defconst *iff* '<=>)
(defconst *xor* '><)

(defdata UnaryOp *not*)
(defdata BinaryOp (enum (list *and* *or* *implies* *iff* *xor*)))
(defdata Formula (oneof boolean
                        var
                        (list UnaryOp Formula)
                        (list Formula BinaryOp Formula)))

(defdata lvar (listof var))
(defdata lform (listof Formula))
(defdata lstring (listof string))

#|
8.10.

(definec formula-vars-aux (f :Formula) :lvar
  (cond
   ((booleanp f) nil)
   ((varp f) (list f))
   ((UnaryOpp (first f)) (formula-vars-aux (second f)))
   (t (app (formula-vars-aux (first f)) (formula-vars-aux (third f))))))


; ANSWER:
...
|#


#|
8.11.

(definec g (x :nat y :rational) :rational
  (if (> x y)
   0
   (/ (* g x) (+ y 1))))

; ANSWER:
...
|#


#|
8.12.

(definec h (x :nat y :nat z :nat) :nat
  (cond
   ((and (equal x 0) (equal y 0) (equal z 0)) 0)
   ((and (<= x y) (<= x z)) (h (- x 1) (- y 1) (- z 1)))
   ((and (<= y x) (<= y z)) (h (- x 1) (- y 1) (- z 1)))
   ((and (<= z x) (<= z y)) (h (- x 1) (- y 1) (- z 1)))
   (t 0))
  )

; ANSWER:
...
|#


#|
8.13.

(definec foo (l :tl) :tl
  (cond
   ((equal (len l) 0) nil)
   ((equal (len l) 1) (foo (list (cons (first l) 1))))
   (t (cons (cons (first l) 1) (foo (rest l))))))

; ANSWER:
...
|#


#|
8.14.

(definec bar (n :nat) :nat
  (cond
   ((equal n 0) 0)
   ((evenp n) (bar (/ n 2)))
   (t (bar (+ n 1)))))

; 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/1FAIpQLSfeyU-RPCTekUYjCSjQR1GHblfbb09tWbmXoD1sRu1lrpdBYA/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>
...
...
...
|#