#|

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

MEASURE FUNCTIONS

In the previous homework we asked you to argue about termination
informally, in English. In this homework we ask you to provide
measure functions. More specifically, for each function given below
you have to answer the following questions:

(a) Does the function terminate? YES/NO

(b) If you answered YES in (a), provide a valid measure function:
This has to be an ACL2s admissible function (valid ACL2s code).

(c) If you answered YES in (a), provide all the proof obligations
that the measure function you provided in (b) decreases at every
recursive call. You do not have to manually prove these obligations.
You only have to state them, formally, in ACL2s format. But they
have to be correct (we will check that they are theorems). Feel
free to state them as ACL2s thm or test? statements, but this is
not required.
Make sure you don't forget the contract completion of your proof
obligations, as well as all the assumptions leading to the case
of the recursive call that you are considering.

Example:

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

ANSWERS:
(a) The function rrev terminates.

(b) A measure function for rrev is:
|#
(definec m (x :tl) :nat
 (len x))
#|
(c) rrev contains a single recursive call, so there is only
one proof obligation that m decreases on each recursive call.
That proof obligation is:

PO1:
(implies (and (tlp x) (not (endp x)))
         (< (m (rest x)) (m x)))
|#
(thm
(implies (and (tlp x) (not (endp x)))
         (< (m (rest x)) (m x)))
)


#|
9.1. Answer questions (a),(b),(c) above for the function:
|#
(definec f1 (x :nat) :rational
  (/ x 2))
#|
ANSWER:
(a) ...
(b)
Measure function:
|#
(definec m1 ...
#|
(c)
f1 has no recursive calls, so there are no proof obligations
that m1 is decreasing.
|#



; these definitions are given, you don't have to prove anything about them:
(defdata UnaryOp '~)
(defdata BinaryOp (enum (list '& '+)))
(defdata Formula (oneof boolean
                        (list UnaryOp Formula)
                        (list Formula BinaryOp Formula)))

#|
9.2. Answer questions (a),(b),(c) above for the function
eval-formula given below.
Hint: the predefined function len won't work for this example (why?).
We have seen another predefined function in class that you can use.
Note that if you define a recursive measure function m you have to
prove that m terminates too! Meaning you have to create a new measure
function mm for m. If mm itself is recursive, you have to create a
measure function mmm for mm, and so on. You don't need to do any of
that to solve this problem.
|#

(definec eval-formula (f :Formula) :bool
  (cond ((booleanp f) f)
        ((UnaryOpp (car f)) (not (eval-formula (second f))))
        ((equal (second f) '&) (and (eval-formula (first f))
                                    (eval-formula (third f))))
        (t (or (eval-formula (first f))
               (eval-formula (third f))))))
#|
ANSWERS:
(a) ...
(b) 
|#
(definec m2 ...

...

#|
9.3. Answer questions (a),(b),(c) above for the function:
|#
(definec list-contains-only-numbers (l :tl) :bool
  (if (endp l) t
    (and (rationalp (first l))
         (list-contains-only-numbers (rest l)))))
#|
ANSWERS:
...
|#
...



#|
9.4. Answer questions (a),(b),(c) above for the function:
|#
(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)))))
#|
ANSWERS:
...
|#
...



#|
9.5. Answer questions (a),(b),(c) above for the function:
|#
(definec list-insert-v2 (l :tl i :nat a :all) :tl
  (cond
   ((> i (len l)) nil)
   ((equal i 0) (cons a l))
   ((endp l) nil)
   (t (cons (first l) (list-insert-v2 (rest l) (- i 1) a)))))
#|
ANSWERS:
...
|#
...

 

#|
9.6. Answer questions (a),(b),(c) above for the function:
|#
(definec f2 (x :tl y :nat) :nat
  (if (endp x)
    (if (equal y 0) 
      0
      (+ 1 (f2 x (- y 1))))
    (+ 1 (f2 (rest x) y))))
#|
ANSWERS:
...
|#
...



#|
9.7. Answer questions (a),(b),(c) above for the function:
|#
(definec f97 (n :nat) :tl
  (cond
   ((< n 100) (cons n (f97 (+ n 1))))
   (t (list n))))
#|
ANSWERS:
...
|#
...



#|
9.8. Answer questions (a),(b),(c) above for the function:
|#
(definec f98 (n :integer) :nat
  (cond
    ((< n 0) (f98 (* n -1)))
    ((equal n 0) 0)
    (t (+ 1 (f98 (- n 1))))))
#|
ANSWERS:
...
|#
...



#|
9.9. Answer questions (a),(b),(c) above for the function:
|#
(definec f99 (x :nat y :nat) :nat
  (cond
    ((and (equal x 0) (equal y 0)) 0)
    ((< x y) (+ 1 (f99 y x)))
    (t (+ 2 (f99 (- x 1) y)))))
#|
ANSWERS:
...
|#
...




#|
9.10. Answer questions (a),(b),(c) above for the function:
|#
(definec f910 (m :integer x :rational) :rational
  (cond
   ((= m 0) x)
   ((< m 0) (f910 (- (* -1 m) 1) (/ x 2)))
   (t (f910 (+ (* -1 m) 1) (/ x 3)))))
#|
ANSWERS:
...
|#
...


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;  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/1FAIpQLSdf5GNUS_fMv730PxXi5uf-W_G7HKkVrAmCBEb2oIdKXzgbhQ/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>
...
...
...
|#