---
# System prepended metadata

title: 'Lab: List Induction Practice'

---

# 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. 


~~~

