#|

CS 2800 Homework 10 - 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 and induction.

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.


Example:

Consider the following function:

(defunc f (x y)
  :input-contract (and (tlp 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))))

A measure function for f is the following:
(definec m (x :tl y :nat) :nat
  (+ (len x) y))

QUESTION: Prove that the measure function m decreases on
every recursive call of f.
  
ANSWER:

For the first recursive call in f, the proof obligation 
for proving that the measure function decreases is:

(implies (and (tlp x)
              (natp y)
              (endp x)
              (not (equal y 0)))
         (< (m x (- y 1))
            (m x y)))

Context:
C1. (tlp x)
C2. (natp y)
C3. (endp x)
C4. y != 0

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

QED


For the second recursive call in f, the proof obligation
for proving that the measure function decreases is:

(implies (and (tlp x)
              (natp y)
              (not (endp x)))
         (< (m (rest x) y)
            (m x y)))

Context:
C1. (tlp x)
C2. (natp y)
C3. (not (endp x))

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

QED


QUESTION: Prove the contract theorem of f, which is:

T: (implies (and (tlp x)
                 (natp y))
            (natp (f x y)))

ANSWER:

We will prove T by induction, using the induction scheme 
that f gives rise to. Our proof obligations are:

1. (not (and (tlp x) (natp y))) => T
2. (and (tlp x) (natp y) (endp x) (equal y 0)) => T
3. (and (tlp x) (natp y) (endp x) (not (equal y 0)) T|((y (- y 1))))
   => T
4. (and (tlp x) (natp y) (not (endp x)) T|((x (rest x))))
   => T

Proof obligation 1:
Context:
C1. (not (and (tlp x) (natp y)))
C2. (and (tlp x) (natp y))

Derived Context:
D1. nil { C1, C2 }

QED

Proof obligation 2:
Context:
C1. (tlp x)
C2. (natp y)
C3. (endp x)
C4. (equal y 0)

Goal: (natp (f x y))

Proof:
(natp (f x y))
= { def f, C3, C4 }
(natp 0)
= { arithmetic }
t

QED

Proof obligation 3:
Context:
C1. (tlp x) 
C2. (natp y) 
C3. (endp x) 
C4. (not (equal y 0)) 
C5. (tlp x) & (natp (- y 1)) => (natp (f x (- y 1)))

Derived Context:
D1. (natp (- y 1)) { C2, C4, arithmetic }
D2. (natp (f x (- y 1))) { C5, C1, D1, MP }

Goal: (natp (f x y))

Proof:
(natp (f x y))
= { def f, C3, C4 }
(natp (+ 1 (f x (- y 1))))
= { D2, arithmetic }
t

QED

Proof obligation 4:
Context:
C1. (tlp x) 
C2. (natp y) 
C3. (not (endp x)) 
C4. (tlp (rest x)) & (natp y) => (natp (f (rest x) y))

Derived Context:
D1. (tlp (rest x)) { C1, C3 }
D2. (natp (f (rest x) y)) { C4, D1, C2, MP }

Goal: (natp (f x y))

Proof:
(natp (f x y))
= { def f, C3 }
(natp (+ 1 (f (rest x) y)))
= { D2, arithmetic }
t

QED
|#



;; We define the following data types:

(defdata UnaryOp '~)
(defdata BinaryOp (enum (list '& '+)))
(defdata Formula (oneof boolean
                        (list UnaryOp Formula)
                        (list Formula BinaryOp Formula)))

;; We define the following function:
(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))))))

#|
10.1. Suppose you want to prove some claim Phi using the induction
scheme generated by (eval-formula f). What are your proof obligations?
List all of them below:

; ANSWER:
PO1: ...

PO2: ...

...
|#


#|
10.2. Define the induction scheme (proof obligations) generated by
the following function:

(definec app?-t2 (x :tl y :tl acc :tl) :tl
  (if (endp x)
      (if (endp y)
          acc
        (app?-t2 x (rest y) (cons (first y) acc)))
    (app?-t2 (rest x) y (cons (first x) acc))))

; ANSWER:
PO1: ...

...
|#


#|
10.3. Define the induction scheme (proof obligations) generated by
the following function:

(definec app?-t3 (x :tl y :tl acc :tl) :tl
  (cond ((and (endp x) (endp y)) acc)
        ((endp x) (app?-t3 x (rest y) (cons (first y) acc)))
        ((endp y) (app?-t3 (rest x) y (cons (first x) acc)))
        (t (app?-t3 x nil (app?-t3 nil y acc)))))

; ANSWER:
...
|#


;; Consider these two function definitions:
(definec f97 (n :nat) :tl
  (cond
   ((< n 100) (cons n (f97 (+ n 1))))
   (t (list n))))

(definec m7 (n :nat) :nat
  (if (>= n 100) 0 (- 100 n)))

#|
10.4. Prove the following theorem:
|#
(thm (implies (and (natp n) (< n 100))
              (< (m7 (+ n 1)) (m7 n))))

#|
; ANSWER:
...
|#



#|
10.5. Prove the contract theorem of f97, that is, prove:

T1: (natp n) => (tlp (f97 n))
|#

#|
; ANSWER:
...
|#



;; Consider these two function definitions:
(definec f98 (n :integer) :nat
  (cond
    ((< n 0) (f98 (* n -1)))
    ((equal n 0) 0)
    (t (+ 1 (f98 (- n 1))))))

(definec m98 (n :integer) :nat
  (cond
    ((< n 0) (+ 1 (* n -1)))
    (t n)))

#|
10.6. Prove the following two theorems:
|#
(thm (implies (and (integerp n) (< n 0))
              (< (m98 (* n -1)) (m98 n))))

(thm (implies (and (integerp n) (not (< n 0)) (not (equal n 0)))
              (< (m98 (- n 1)) (m98 n))))
#|
; ANSWER:
...
|#


#|
10.7. Prove the contract theorem of f98, that is, prove:

T2: (integerp n) => (natp (f2 n))
|#

#|
; ANSWER:
...
|#



;; Consider these two function definitions:

(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)))))

(definec m910 (m :integer x :rational) :nat
  (declare (ignorable x))
  (cond
   ((= m 0) 0)
   ((< m 0) (* -1 m))
   (t m)))

#|
10.8. Prove the following two theorems:
|#
(thm (implies (and (integerp m) (rationalp x) (< m 0))
              (< (m910 (- (* -1 m) 1) x) (m910 m x))))

(thm (implies (and (integerp m) (rationalp x) (> m 0))
              (< (m910 (+ (* -1 m) 1) x) (m910 m x))))

#|
; ANSWER:
...
|#




#|
10.9.
Consider the following "induction scheme":

PO1: (not (natp n)) => Phi
PO2: (natp n) & (equal n 0) => Phi
PO3: (natp n) & (not (equal n 0)) & Phi|((n (+ n 1))) => Phi

Prove that the above scheme is not valid, because it is unsound.
That is, prove that you can use the above scheme to prove False.

Hint: consider how we proved False using some non-terminating
functions a few lectures ago.

; ANSWER:

...
|#



;; consider the following definitions:

(defdata natlist (listof nat))

(definec non-decreasing (l :natlist) :bool
  (or (endp l)
      (endp (cdr l))
      (and (<= (first l) (second l))
           (non-decreasing (rest l)))))

(defunc insert-nd (X n)
  :input-contract (and (natlistp X) (non-decreasing X) (natp n))
  :output-contract (and (natlistp (insert-nd X n))
                        (non-decreasing (insert-nd X n)))
  (cond
   ((endp X) (list n))
   ((< (first X) n) (cons (first X) (insert-nd (rest X) n)))
   (t (cons n X))))

#|
10.10. 
Prove the following theorem:
|#

(thm (implies (and (natlistp X) (not (endp X)) (non-decreasing X))
              (non-decreasing (cdr X))))

#|
; ANSWER:
...
|#


#|
10.11. 
Prove the following theorem:
|#
(thm (implies (and (natp n) (natlistp X) (non-decreasing X))
              (equal (len (insert-nd X n))
                     (+ 1 (len X)))))


#|
; 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/1FAIpQLSdPK_mV3bFQw-rn6I2lWoinje9MD19KC2mQVfXER4Ay8Zrxmg/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>
...
...
...
|#