# Lab: Assumptions in Proofs

## Problem 1: Narrowing down the possibilities

~~~racket
(define f1
(lambda (name)
(cond [(equal? name "Alice") 0] ; Point A
[(equal? name "Bob") 1] ; Point B
[(equal? name "Carol") 2] ; Point C
[(not (equal? name "Daniel")) 3] ; Point D
[(not (equal? name "Emily")) 4]))) ; Point E

(define f2
(lambda (x y)
(cond
[(>= y 1) 0] ; Point A
[(or (>= x 1)) 1] ; Point B
[(== x -1) 2] ; Point C
[(or (<= x -5) (>= y 3)) 3] ; Point D
[(== x 0) 4] ; Point E
[(== x y) 5]))) ; Point F
~~~

1. In f1 name is a string and in f2 x y are real numbers.

2. f1: Point A: When `(equal? name "Alice")== #t` then name is "Alice"
Point B: When `(equal? name "Bob")== #t` then name is "Bob"
Point C: When `(equal? name "Carol")== #t` then name is "Carol"
Point D: When `(not(equal? name "Daniel"))== #t` then name is not "Daniel" or the previously named strings above.
Point E: When `(not(equal? name "Emily"))== #t` then name has to be "Daniel"
f2: Point A: When `(>= y 1) == #t` then y is greater than or equal to 1.
Point B: When `(or (>= x 1)) == #t` then x is greater than or equal to 1 and y is less than 1.
Point C: When `(== x -1) == #t` then x is equal to -1 and y is less than 1.
Point D: When `(or (<= x -5) (>= y 3)) == #t` then x is less than or equal to -5 and y is less than 1.
Point E: When `(== x 0) == #t` then x is equal to 0 and y is less than 1.
Point F: When `(== x y) == #t` then x is equal to y and are between the values 1 and -5, but not 0 and -1.

3. f1 is exhaustive because when the guards are evaluated, every string will evaluate to true under one of the guards. f2 is not exhaustive because there are cases that won't evaluate to true: when x and y are not equal, x is between 1 and -5, y is less than 1, and x is not 0 and -1

## Problem 2: Capture
~~~racket
(define report
(lambda (hw-avg quiz1 quiz2 quiz3)
(cond [(and (> hw-avg 90) (> quiz1 90) (> quiz2 90) (> quiz3 90)) "excelling"]
[(and (> hw-avg 75) (<= quiz1 quiz2) (<= quiz2 quiz3)) "progressing"]
[(or (< hw-avg 60) (< quiz1 60) (< quiz2 60) (< quiz2 60)) "needs help"]
[else "just fine"])))
~~~
1. Preconditions:
`hw-avg` is a non-negative real numbers between 0 and 100.
`quiz 1` is a non-negative real numbers between 0 and 100.
`quiz 2` is a non-negative real numbers between 0 and 100.
`quiz 3` is a non-negative real numbers between 0 and 100.

2. `(report hw-avg quiz1 quiz2 quiz3)` will return `"just fine"` when all parameters are above 60 and below 90, and either `hw-avg` is below 75, or `quiz 1` is greater than `quiz 2`, or `quiz 2` is greater than `quiz 3`.

3. We don't think there would be any case in which the function will return an inappropriate string, given that the input satisfy the preconditions. In the case that the input doesn't satisfy the preconditions, the function will either return an error message (for string type input for example), or progress as usually, deceived by integer type input.

## Problem 3: Looking Ahead
~~~racket
(define append
(lambda (l1 l2)
(if (null? l1)
l2
(cons (car l1) (append (cdr l1) l2)))))
~~~
**Claim 1** (Nil Is An Identity on the Left): for any list`l`, `(append '() l)` ≡ `l`
*Proof*: Evaluating the left hand side: for `l` is any list:
~~~racket
-->(append `() l)
-->(if (null? `()) l (cons (car `()) (append (cdr `()) l)))
-->(if #t l (cons (car `()) (append (cdr `()) l)))
-->l
-->l ≡ l
~~~
*Conclusion*: The Left hand side evaluates to `l` which is exactly equivelent to the right and therefore the claim holds.

**Claim 2** (Append is Not Commutative): there exists lists `l1` and `l2` such that `(append l1 l2)` ≡ `(append l2 l1)`.
*Proof*: Evaluating the left hand side and right hand side for `l1` and `l2` with different content.
`l1 = '(a b c)`
`l2 = '(x y z)`
* Evaluating the left hand side:
~~~racket
--> (append l1 l2)
--> (if (null? l1)
l2
(cons (car l1) (append (cdr l1) l2)))
--> (cons (car l1) (append cdr l1) l2)
--> (cons a (append '(b c) '(x y z)))
--> (cons a (if (null? '(b c))
'(x y z)
(cons (car '(b c)) (append (cdr '(b c)) '(x y z)))))
--> (cons a (cons b (if (null? '(c))
'(x y z)
(cons (car '(c)) (append (cdr '(c)) '(x y z))))))
--> (cons a (cons b (cons c (if (null? '())
'(x y z)
(cons (car '()) (append (cdr '()) '(x y z)))))))
--> (cons a (cons b (cons c '(x y z))))
--> (cons a (cons b '(c x y z)))
--> (cons a '(b c x y z))
--> '(a b c x y z)
~~~
* Evaluating the right hand side:
~~~racket
--> (append l2 l1)
--> (if (null? l2)
l1
(cons (car l2) (append (cdr l2) l1)))
--> (cons (car l2) (append cdr l2) l1)
--> (cons x (append '(y z) '(a b c)))
--> (cons x (if (null? '(y z))
'(a b c)
(cons (car '(y z)) (append (cdr '(y z)) '(a b c)))))
--> (cons x (cons y (if (null? '(z))
'(a b c)
(cons (car '(z)) (append (cdr '(z)) '(a b c))))))
--> (cons x (cons y (cons z (if (null? '())
'(a b c)
(cons (car '()) (append (cdr '()) '(a b c)))))))
--> (cons x (cons y (cons z '(a b c))))
--> (cons x (cons y '(z a b c)))
--> (cons x '(y z a b c))
--> '(x y z a b c)
~~~
*Conclusion*: Since `'(a b c x y z) =! '(x y z a b c)`, it is safe to conlude that there exists `l1`, `l2` such that `(append l1 l2) =! (append l2 l1)`.

**Claim 3** (Nil Is An Identity on the Right): for any list `l`, `(append l '())` ≡ `l`
*Proof*: Evaluating the left hand side for `l` is any list.
~~~racket
-->(append l '())
-->(if (null? l) '() (cons (car l) (append (cdr l) '())))
-->(cons (car l) (append (cdr l) '()))
-->(cons (car l ) (if (null? (cdr l)) '() (cons (car (cdr l) (append (cdr (cdr l)) '())))))
~~~
*Conclusion*: Since we are assuming `l` is any list we have no way to prove that this function will return an output since we don't know the length of the list.

**4:**
* *Why were you able to directly prove the left-identity claim?*
We were able to directly prove the left-identity claim because the first input was null `append` can evaluate it immediately. Here, `(null? '())` will evaluate to `#t`, `append` returns `l2` and terminates the loop.
* *Why is the right-identity claim more difficult to prove?*
Assuming `l` is an unspecified list, the right-identity claim is more difficult to prove because `append` will evaluate the list `l` first and `cons` elements of `l` and continuously loop itself with `(cdr l)` as input. Since `l` is not specified, its content and length is also unknown, meaning arbitrary evaluation could go on infinitely.
* *What information do you need in order to break the chain of infinite reason that you found in the previous proof?*
If we're given specified length or content, the chain of infinite reason will be broken. However, we're not sure if specifications will allow us to prove universal claim. Another option we have is that we can assume that the list is going to end at some point.