#|

CS 2800 Homework 7 - Summer 2018

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

This homework is to be done in a group of 2-3 students. It is designed
to give you practice with function admissibility and introduce you to
measure functions.

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.

For this homework you will NOT need to use ACL2s. However, you could
use the Eclipse/ACL2s text editor to write up your solution.

|#


#|

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Admissible or not?
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For each of the definitions below, check whether it is theoretically 
admissible, i.e. it satisfies all rules of the definitional principle. 
You can assume that Rule 1 is met: the symbol used in the defunc is a new 
function symbol in each case.

If you claim admissibility, BRIEFLY

1. Explain in English why the body contracts hold.
2. Explain in English why the contract theorem holds.
3. Suggest a measure function that can be used to show termination.
   (You DO NOT have to prove the measure function properties in this problem.)

Otherwise, identify a rule in the Definitional Principle that is violated.

If you blame one of the purely syntactic rules (variable names,
non-wellformed 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.

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.

I used the term "theoretically admissible" because for some functions below
you can demonstrate they are admissible but ACL2s won't actually admit it 
without a lot of extra guidance from you (this isn't your responsibility).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SECTION 1: Admissibility
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1.

(defunc f1 (n)
  :input-contract (natp n)
  :output-contract (rationalp (f1 n))
  (if (equal n 0)
    n
    (f1 (/ n 2))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2.

(defunc f2 (a b)
  :input-contract  (and (listp a) (listp b))
  :output-contract (posp (f2 a b))
  (cond ((or (endp a) (endp b)) 1)
        ((> (len a) (len b)) 
         (+ 1 (f2 (rest a) (cons (first a) b))))
        ((equal (len a) (len b)) 0)
        (t                
         (+ 1 (f2 (cons (first b) a)(rest b))))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3.

(defunc f3 (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (f3 x y))
  (cond ((< (len x) (len y)) (f3 (cons (first y) x) y))
        ((> (len x) (len y)) (f3 (rest x) y))
        (t   x)))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4.

(defunc f4 (x y)
  :input-contract (and (natp x) (posp y))
  :output-contract (posp (f4 x y))
  (cond ((equal y 1) y)
        ((equal x 0) x)
        ((< y x)     (f4 y x))
        (t           (f4 x (- y 1)))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
5.

(defunc f5 (y z)
  :input-contract (and (rationalp y) (rationalp z))
  :output-contract (rationalp (f5 y z))
  (cond ((<= y  0) z)
        ((> z 0) (f5 y (- z y)))
        (t z)))

Think about if any variables converge towards a value
and how much they are guaranteed to converge each recursive call.
Can you convert this amount to a natural?

................
    
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6.

(defunc f6 (x y)
  :input-contract (and (listp x)(natp y))
  :output-contract (natp (f6 x y))
  (cond ((equal y 0) (len x))
        ((endp x)    0)
        (t           (f6 (len x) (list y)))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
7.

(defunc f7 (i)
  :input-contract (integerp i)
  :output-contract (integerp (f7 i))
  (if (< i -5)
    i
    (- f7 (* i i))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
8.

(defunc f8 (x y)
  :input-contract (and (posp x) (integerp y))
  :output-contract (posp (f8 x y))
  (if (>= y x)
    (+ x y)
    (+ (* y y) (f8 (+ x 1) (+ y 2)))))

................
    
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
9.

(defunc f9 (i x j)
  :input-contract (and (posp i) (listp x) (posp i))
  :output-contract (posp (f9 i x j))
  (cond ((equal j 1) (+ (len x) j))
        ((equal i 1) (+ i j))
        (t           (f9 (- i 1) (cons (+ i j) x) (- j 1)))))
    
................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
10.

(defunc f10 (a b)
  :input-contract  (and (natp a) (posp b))
  :output-contract (posp (f10 a b))
  (cond ((or (equal a 0)(equal b 1)) 1)
        ((> a b) (f10 b a))
        (t (+ 1 (f10 a (- b 1))))))


................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
11.

(defunc f11 (x n)
  :input-contract (and (listp x) (integerp n))
  :output-contract (loip (f11 x n))
  (if (endp x)
    nil
    (if (< n 0) 
      (cons (first x) (f11 (rest x) (+ n 1))
      (f11 (cons n (rest x)) (- n 1)))))

................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
12.

; if you want to push ACL2s through these functions, put it in program mode here.
;:program
(defunc f12 (p i)
  :input-contract (and (posp p)(integerp i))
  :output-contract (posp (f12 p i))
  (cond ((equal p 1)   10)
        ((< p 9)       (- (f12 (- p 1) i) 1))
        ((> i p)       (f12 i (- p 2)))
        (t             (f12 (- p 1) i))))

      
 ................

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13.

(defunc f13 (p r)
  :input-contract (and (posp p)(rationalp r))
  :output-contract (posp (f13 p r))
  (cond ((equal p r) 10)
        ((< p r)  (+ (f13 (+ p (numerator r)) r) 1))
        (t  (f13 p (+ r 1)))
        
................
        
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
14.

(defunc f14 (x y)
  :input-contract (and (posp x) (posp y))
  :output-contract (integerp (f14 x y))
  (cond ((equal x y) 5)
        ((< x y)     (f14 y x))
        ((< x 1)     (f14 x y))
        (t           (- (f14 (- x 1) y) 3))))

................

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

15.

(defunc f15 (x y)
  :input-contract  (and (natp x) (natp y))
  :output-contract (posp (f15 x y))
  (cond ((equal x y)    1)
        ((> x y)        (f15 y x))
        (t              (f15 x (- y 2)))))


................

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

16.

(defunc f16 (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (listp (f16 x y))
  (cond ((endp x)     (list y))
        ((equal y 1)  (f16 x (len x)))
        (t            (f16 (rest x) (- y 1)))))
  
................
        
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

17.

(defunc  f17 (l)
  :input-contract (listp l)
  :output-contract (booleanp (f17 l))
  (cond ((endp l)  l)
        ((in e l)  t)
        (t         (cons (first l)(f17 (rest l))))))

................


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

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SECTION 2: DOES IT TERMINATE?
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; For each of the following functions, mention whether the function terminates 
;; or not. If it does, give a measure function for it AND write the proof obligations
;; needed to prove termination (here we are not asking  you to prove anything). 
;; Features of a valid measure function are described
;; in section 3 below and in the notes.
;; If it does not terminate, give a concrete input on which it fails.
;; Here is a function you can use to help you

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; abs: integer -> natural
;; (abs i) takes an integer value
;; and returns the absolute value
;; of that number (thus a natural number)
(defunc abs (i)
  :input-contract (integerp i)
  :output-contract (natp (abs i))
  (if (< i 0) (unary-- i)  i))
#|
;; EXAMPLE: for the function app the solution would be
(defunc m-app (x y)
  :input-contract (and (listp x)(listp y))
  :output-contract (listp (m-app x y))
  (len x))

;Proof Obligation
(listp x) /\ (listp y) /\ ~(endp x) 
   => (m-app x y) = (len x) > (len (rest x)) = (m-app (rest x) y)
|#

#|
(defunc f18 (r)
  :input-contract (rationalp r)
  :output-contract (integerp (f18 r))
  (if (equal r 0)
    14
    (+  (f18 (- (abs (numerator r)) 1)) 4)))


................
 
(defunc  f19 (x)
  :input-contract (integerp x)
  :output-contract (integerp (f19 x))
  (cond ((equal x 0) 1)
        ((> x 0) (* x (f19 (- x 1))))
        (t (* x (f19 (+ x 1))))))

................
  
(defunc  f20 (l i)
  :input-contract (and (listp l)(integerp i))
  :output-contract (natp (f20 l i))
  (if (< i 0) 
    (len l)
    (f20 l (- i (len l)))))

................
 
(defunc  f21 (l1 l2)
  :input-contract (and (listp l1)(listp l2))
  :output-contract (booleanp (f21 l1 l2))
  (cond ((endp l1)    t)
        ((endp l2)  (f21 (rest l1) l2))
        (t    (f21 (cons (first l2) l1) (rest l2)))))

................

(defunc f22 (n m)
  :input-contract (and (integerp n)(integerp m))
  :output-contract (integerp (f22 n m))
  (cond ((equal n m)                 1)
        ((< n m)  (f22 (+ n 1)(- m 1)))
        (t             (f22 (- n 1) m))))
        
................
|#  


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 3: Proving a Measure Function
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|

You can prove a function f terminates using a measure function m. 
This requires the following conditions are met:

Condition 1. m has the same arguments and the same input contract as f.
Condition 2. m's output contract is (natp (m ...))
Condition 3. m is admissible.
Condition 4. On every recursive call of f, given the input contract and 
   the conditions that lead to that call, m applied to the arguments in
   the call is less than m applied to the original inputs.

You should do this proof as shown in class (which is also the way we will
expect you to prove termination on exams):

- Write down the propositional logic formalization of Condition 4.
- Simplify the formula.
- Use equational reasoning to conclude the formula is valid.

Unless clearly stated otherwise, you need to follow these steps for EACH
recursive call separately.

Here is an example.

(defunc f (x y)
  :input-contract (and (listp x) (natp y))
  :output-contract (natp (f x y))
  (if (endp x)
    (if (equal y 0) 
      0
      (+ 1 (f x (- y 1))))
    (+ 1 (f (rest x) y))))

The measure is
(defunc m (x y)
  :input-contract (and (listp x) (natp y))
  :output-contract (natp (m x y))
  (+ (len x) y))


For the first recursive call in f, the propositional logic formalization 
for proving Condition 4 is:
(implies (and (listp x) (natp y) (endp x) (not (equal y 0)))
         (< (m x (- y 1)) (m x y)))

This can be rewritten as:
(implies (and (listp x) (natp y) (endp x) (> y 0))
         (< (m x (- y 1)) (m x y)))
         
Proof of Condition 4 for the first recursive call:
Context
C1. (listp x)
C2. (natp y)
C3. (endp x)
C4. (> y 0)

(m x (- y 1))
= { Def m, C3, Def len, Arithmetic }
(- y 1)
< { Arithmetic }
y
= { Def m, C3, Def. len, Arithmetic }
(m x y)

The propositional logic formalization for Proof of Condition 4 for the 
second recursive call:
(implies (and (listp x) (natp y)(not (endp x)))
         (< (m (rest x) y) (m x y)))

Proof:
C1. (listp x)
C2. (natp y)
C3. (not (endp x))

(m (rest x) y)
= { Def m, C3 }
(+ (len (rest x)) y)
< { Arithmetic, Decreasing len axiom }
(+ (len x) y)
= { Def m }
(m x y)

Hence f terminates, and m is a measure function for it.
QED


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

23. Prove f23 terminates:

(defunc f23 (x y c)
  :input-contract (and (natp x) (natp y) (natp c))
  :output-contract (integerp (f23 x y c))
  (cond ((and (>= x 1024) (>= y 1024)) c)
        ((< y 1024) (f23 x (+ y 1) (+ c 1)))
        (t          (f23 (+ x 1) 0 (+ c 1)))))
.....in case you are curious as to what this is, 
think about a 2D array
        
        
What is the measure function for f23?
Keep in mind that (if (> x 1024) 0 (- 1024 x))
will always be a nat AND if x is outside of a typical
the value is 0.
Also, what is the maximum number of recursive calls this
function can ever make?
............

What are the proof obligations?
.........

     
Now prove that m23 is a measure function for f23 using equational reasoning

..........


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
24. Prove f24 terminates (ungraded extra practice)
|#

(defunc f24 (l1 l2 flag)
  :input-contract (and (listp l1)(listp l2)(booleanp flag))
  :output-contract (listp (f24 l1 l2 flag))
  (cond ((and (endp l1) (not flag))  (f24 l1 l2 t))
        ((not flag) (f24 (rest l1) (cons (first l1) l2) flag))
        ((not (endp l2))             (f24 (cons (first l2) l1) (rest l2) flag))
        (t                           l1)))
#|
...............

Proof Obligations:

................

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|

Each week we will ask a couple questions to monitor how the course
is progressing.  This won't be as long as the HW05 survey. 

Please fill out the following form.

https://goo.gl/forms/pypK8LX4GlfQ1Ovs1

As before, feedback is anonymous and each team member should fill out
the form (only once per person).

After you fill out the form, write your name below in this file, not
on the questionnaire. We have no way of checking if you submitted the
file, but by writing your name below you are claiming that you did,
and we'll take your word for it.  

5 points will be awarded to each team member for filling out the 
questionnaire.  More importantly, if a course topic is confusing you, I can
address the issue without you having to worry that only you don't get the topic
(Note: it's almost never the the case that only 1 student is confused but I know
it can still be scary)

The following team members filled out the feedback survey provided by 
the link above:
---------------------------------------------
<firstname> <LastName>
<firstname> <LastName>

|#