# Lab: List Induction Practice

**Problem #1: Warm-Up**

1. Claim (Length of Tails): for all lists l, (length (tails l)) ≡ (+ 1 (length l)).
l cn be empty and non-empty and we can do case analysis for both cases. The empty case should be straight-forward but in the non-empty case, we will have to proceed with an induction hypothesis.

2. Proof. Let l be a list. We proceed by induction on l.

~~~Racket~~~
* l = null

Evaluating the left-hand side,

--> (length (tails l))
--> (length (tails '()))
--> (length '('()))
--> (+ 1 (length tail))
--> (+ 1 0)
--> 1

Evaluating the right-hand side, we get the same value i.e. 1

--> (+ 1 (length l))
-->* (+ 1 0)
--> 1
~~~
* l is not equal to null. Also, t is cdr of l and h is car of l

Inductive Hypothesis: (length (tails t)) ≡ (+ 1 (length t)).

Solving the left-hand side,

--> (length (tails l))
--> (length (cons l (tails t)))
-->* (+ 1 (length (tails t)))
-->(+ 1 (+ 1 (length t)))

Solving the right-hand side,

--> (+ 1 (length l))
--> (+ 1 (+ 1(length t)))

~~~
Our induction hypothesis allows us to conclude:
-->(+ 1 (+ 1 (length t))) = (+ 1 (+ 1 (length t)))
Hence, proving our claim:
(length (tails l)) ≡ (+ 1 (length l)).

**Problem 2: A World Apart**
(i)
l cn be empty and non-empty and we can do case analysis for both cases. The empty case should be straight-forward but in the non-empty case, we will have to proceed with an induction hypothesis.

(ii) Claim: (sum (inc l)) ≡ (+ (length l) (sum l))

Proof.

* For when l is null,

Evaluating right hand side,
~~~Racket~~~
-->(sum (inc l))
--> (sum '())
--> 0

~~~
Evaluating left hand side,
~~~Racket~~~
--> (+ (length l) (sum l))
--> (+ 0 (sum l))
--> (+ 0 0)
--> 0
~~~
Hence for null case, both are equal.

* For when l is not null, we perform induction on l:
~~~Racket~~~
Inductive Hypothesis: (sum (inc tail)) ≡ (+ (length tail) (sum tail))
~~~
Here head is car of l and tail is cdr of l.
Solving left-hand side,
~~~Racket~~~
--> (sum (inc l))
--> (sum cons (+ 1 head) (inc tail))
-->* (+ (sum (+ 1 head)) (sum (inc tail) ))
--> (+ 1 head (sum (inc tail)))
--> (+ 1 head (+ (length tail) (sum tail)))
~~~

Solving right-hand side,
~~~Racket~~~
--> (+ (length l) (sum l))
--> (+ (+ 1 (length tail)) (+ head (sum tail)))
--> (+ 1 head (+ (length tail) (sum tail)))
~~~

Our induction hypothesis allows us to conclude:
(+ 1 head (+ (length tail) (sum tail))) = (+ 1 head (+ (length tail) (sum tail)))
Hence, proving the claim:
(sum (inc l)) ≡ (+ (length l) (sum l))

**Problem 3: Building Up Facts**

~~~Racket

1-
(define (snoc l v)
(append l (list v)))

2-
(define (reverse list in)
(match in
['() list]
[(cons h t) (snoc (reverse list t) h)]))

(define (rev out)
(reverse '() out))
~~~

3-
~~~
Claim (Snoc Length): for all lists l and values v, (length (snoc l v)) ≡ (+ 1 (length l)).

proof:

let l be a list and v a value

l = empty

lhs:
(length (snoc l v))

-->(length (snoc '() v))

(append l (list v)))
-->(length (append'() (list v)))
-->(length '(v))
--> 1

rhs:

(+ 1 (length l))
--> (+1 (length '()))
--> (+1 0)
--> 1

non-empty l

lhs:

(length (snoc l v))
-->(length (append l (list v)))
-->(+ (length l) (length '(v)))
-->(+ (length l) 1)

~~~

rhs:
`(+ 1 (length l)).`

Thus, lhs is equivalent to the rhs as it evaluates to the same expression.

4.

~~~

(define (snoc l v)
(append l (list v)))

(define (reverse list in)
(match in
['() list]
[(cons h t) (snoc (reverse list t) h)]))

(define (rev out)
(reverse '() out))

Claim (Rev Length): for all lists l, (length (rev l)) ≡ (length l).

proof:

let l be any list

l= empty

lhs:

(length (rev l))
--> (length (rev '()))
--> (length (reverse '() '()))
--> (length ('()))
--> 0

rhs:

--> (length l).
--> (length '())
--> 0

cases where l is not empty

lhs:
(length (rev l))
(length (reverse '() l))
--> (length (snoc (reverse l t) h))
--> (length (append (reverse l t) (list h)))
-->(+ 1 (length (reverse l t) ))
--> (+ 1 (length (snoc (reverse t t') h')))
--> (+ 1(Length (append (reverse t t') (list h'))))
-->(+ 1 1 (length (reverse t t')))
--> (+ 1 1 (length (reverse t t')))

--> IH: (length (rev t)) ≡ (length t).
--> IH: (Lentgh (reverse '() t)) ≡ (length t).
--> IH: (Length (snoc (reverse t t') h')) ≡ (length t).
--> IH: (Length (append (reverse t t') (list h')) ≡ (length t).
--> IH: (+ 1 (length (reverse t t'))) ≡ (length t).

Gievn our IH, we can proceed as following:

--> (+ 1 (length t))

rhs:

--> (length l)
--> (+1 (length t))

Since rhs is equal to left-hand side, the claim is proven.

~~~