# Lab: Assumptions in Proofs

**Problem 1: Narrowing Down the Possibilities**

1. The parameter name is a string.
The parameters x and y are integers.

2. For f1,
At Point A, we know that name is "Alice"
At POint B, we know name is "Bob"
At Point C, we know that name is "Carol"
At POint D, we know that name is not "Alice", "Bob", "Carol" but it can be anything but "Daniel".
At Point E, we know that name is "Daniel".
For f2,
At Point A, we know that y is greater than or equal to 1.
At Point B, we know that y is less than 1 and x is greater than or equal to 1.
At Point C, we know that y is less than 1 and x is equal to -1.
At Point D, we know that x is less than or equal to -5 and y is still less than 1.
At Point E, we know that x is equal to 0 and y is still less than 1.
At Point F, we know that x is less than -1 and greater than -5 and y is equal to x.

3. f1 is exhaustive since it covers all possible strings for name. However, f2 is not exhaustive since x and y can still be anywhere between -1 and -5.

**Problem 2: Capture**
1. All of the inputs have to be positive integers. They also must be less than 100.

2. All of the scores must be greater than 60. At least one of the scores must be less than 90. Either the homework is less than 75 or there is no improvment on at least one of the quizzes.

3.if a student's quiz scores were 45, 50, and 55, they would get progressing even though all of their quiz scores were below 60, and the program should have displayed "needs help."

**Problem 3: Looking Ahead**

1. Claim (Nil Is An Identity on the Left): for any list l, (append '() l) ≡ l.

Proof:

~~~Racket~~~

(append '() l) ≡ l
Evaluating the left-hand side:
--> append '() l)
--> (if (null? '())
l
(cons (car '()) (append (cdr '()) l)))
--> l

Hence, (append '() l) ≡ l
~~~

2. Claim (Append is Not Commutative): there exists lists l1 and l2 such that (append l1 l2) =/= (append l2 l1).

~~~Racket~~~

l1 = '(a)
l2 = '(b)

Left-hand side:

(append l1 l2)
--> (if (null? l1)
l2
(cons (car l1) (append (cdr l1) l2)))
--> (cons (car l1) (append (cdr l1) l2))
--> (cons (car l1) (append '() l2))
--> (cons '(a) (append '() l2))
--> (cons '(a) l2)
--> (cons '(a) '(b))
--> '(a b)

Right-hand side:

(append l2 l1)
--> (if (null? l2)
l1
(cons (car l2) (append (cdr l2) l1)))
--> (cons (car l2) (append (cdr l2) l1))
--> (cons (car l2) (append '() l1))
--> (cons '(b) (append '() l1))
--> (cons '(b) l1)
--> (cons '(b) '(a))
--> '(b a)

Since both don't give the same output, the claim holds that append is not commutative.

~~~

3. Claim (Nil Is An Identity on the Right): for any list l, (append l '()) ≡ l.

For an unknown list l, evaulating left-hand side:

~~~Racket~~~
--> (if (null? l)
'()
(cons (car l) (append (cdr l) '())))
--> (cons (car l) (append (cdr l) '()))
--> (cons (car l) cons (car (cdr l)) (append (cdr (cdr l)) '()))
--> (cons (car l) cons (car (cdr l)) (cons (car (cdr (cdr l))) (append (cdr (cdr (cdr l))) '())))

~~~

4. * In the left-identity claim, we instantly hit the base case and didn't go to the else statements. Hence, we were't stuck in an infinite loop and didn't have to repetitively take the cdr of l since it was l2.
* It is more difficult to prove because we never hit the base case and always go into the else statements. Hence, we were stuck in an infinite loop and had to repetitively take the cdr of l since it was l1.
* If we know the length of the list, we can know when the cdr of the list is equal to '() and we hit the base case. Once we hit the base case, the infinite loop breaks.