---
# System prepended metadata

title: 'Lab 9: List Induction Practice'

---

# Lab 9: List Induction Practice

## Problem 1: Warm-Up

### 1. Proof Sketch
- We know `l` is an arbitrary list.
- `l` can be either empty or non-empty, and `l` can contain inner lists (a list of lists). 
    - In function `tails`, lists are being `cons`ed to more lists, making a list of lists. Therefore, the length of said list would be the number of lists inside of it.
- Now, we would analyze the case of `l` being empty, and prove the equivalence between both sides for this case. 
    - For function `length`, the empty case would return `0`.
    - For function `tails`, the empty case would return a list containing one empty list. 
- For the non-empty list case, we would evaluate as usual until we cannot proceed further and then use the induction hypothesis to prove equivalence.
    - For function `length`, the non-empty case would return `(+ 1 (length tail))`.
    - For function `tails`, the non-empty case would return `(cons l (tails tail))`.

### 2. Formal Proof
**Claim**: For all lists `l`, `(length (tails l))` ≡ `(+ 1 (length l))`.

_Proof_. Let `l` be an arbitrary list. We prove this claim by induction on `l`. 

Either `l` is empty or non-empty.
- **`l` is empty**. 

    The left-hand side, `(length (tails '()))`, evaluates as follows:
    ```racket
         (length (tails '()))
    -->* (length '('()))
    -->* (+ 1 (length '()))
    -->* (+ 1 0)
    -->  1
    ```
    The right-hand side, `(+ 1 (length '()))`, evaluates as follows:
    ``` racket
         (+ 1 (length '()))
    -->* (+ 1 0)
    -->  1
    ```

- **`l` is non-empty**: Let `tail` be the tail of `l`. We assume our induction hypothesis:
    
    **Induction Hypothesis**: `(length (tails tail))` ≡ `(+ 1 (length tail))`.

    We must prove:
    **Goal**: `(length (tails l))` ≡ `(+ 1 (length l))`.

    The left-hand side, `(length (tails l))`, evaluates as follows:
    ```racket
         (length (tails l))
    -->* (length (cons l (tails tail)))
    ```
    `(cons l (tails tail))` is a list with `l` as the head and `(tails tail)` as the tail. Then we have:
    ```racket
    -->* (+ 1 (length (tails tail)))
    ```

    The right hand side, `(+ 1 (length l))`, evaluates as follows:
    ```racket
         (+ 1 (length l))
    -->* (+ 1 (+ 1 (length tail)))
    ```

    By our induction hypothesis: 
    `(+ 1 (length (tails tail)))` ≡ `(+ 1 (+ 1 (length tail)))`.
    
    `(+ 1 (+ 1 (length tail)))` ≡ `(+ 1 (+ 1 (length tail)))`.
    
    Therefore, the left-hand side steps to the value that the right-hand side steps to. 
    
□

## Problem 2: A World Apart
### 1. Proof Sketch
- We know that `l` is an arbitrary list.
- `l` can be either empty or non-empty. 
- Now, we would analyze the case of `l` being empty, and prove the equivalence between both sides for this case. 
    - For function `list-inc`, the empty case would return `'()`.
    - For function `sum`, the empty case would return `0`.
- For a non-empty list, we would evaluate both sides as usual until we cannot proceed any furhter. Then, we need to use the induction hypothesis to prove equivalence.
    - For function `list-inc`, the non-empty case would return `(cons (+ 1 head) (list-inc tail))`, essentially adding `1` to every element in `l`.
    - For function `sum`, the non-empty case would return `(+ head (sum tail))`. 

### 2. Formal Proof
**Claim**: For any list of numbers `l`, `(sum (list-inc l))` ≡ `(+ (length l) (sum l))`.

_Proof_. Let `l` be an arbitrary list. We prove this claim by induction on `l`.

Because `l` is a list, `l` is either empty or non-empty. 
- **l is empty**. 

    The left-hand side, `(sum (list-inc '()))`, evaluates as follows:
    ```racket
         (sum (list-inc '()))
    -->* (sum '())
    -->* 0
    ```
    
    The right-hand side, `(+ (length '()) (sum '()))`, evaluates as follows:
    ```racket
         (+ (length '()) (sum '()))
    -->* (+ 0 (sum '()))
    -->* (+ 0 0)
    -->  0
    ```
    
- **l is non-empty**. Let `head` and `tail` be the head and tail of `l`, respectively. We assume our induction hypothesis:

    **Induction Hypothesis**: `(sum (list-inc tail))` ≡ `(+ (length tail) (sum tail))`.
    
    We must prove:
    **Goal**: `(sum (list-inc l))` ≡ `(+ (length l) (sum l))`.

    The left-hand side, `(sum (list-inc l))`, evaluates as follows:
    ```racket
         (sum (list-inc l))
    -->* (sum (cons (+ 1 head) (list-inc tail)))
    ```
    `(cons (+ 1 head) (list-inc tail))` is a list with `(+ 1 head)` as the head and `(list-inc tail)` as the tail.
    ```racket
    -->* (+ (+ 1 head) (sum (list-inc tail)))
    -->* (+ 1 (+ head (sum (list-inc tail))))
    ```
    The final step of evaluation comes from the commutative property of addition: `(1 + x)` + `y` = `1` + `(x + y)`.
    
    The right-hand side, `(+ (length l) (sum l))`, evaluates as follows:
    ```racket
         (+ (length l) (sum l))
    -->* (+ (+ 1 (length tail)) (sum l))
    -->* (+ (+ 1 (length tail)) (+ head (sum tail)))
    -->* (+ 1 (+ (length tail) (+ head (sum tail))))
    -->* (+ 1 (+ head (+ (length tail) (sum tail))))
    ```
    The final two steps of evaluation come from the commutative property of addition: `(1 + x)` + `y` = `1` + `(x + y)`.
    
    By our induction hypothesis:
    `(+ 1 (+ head (sum (list-inc tail))))` ≡ `(+ 1 (+ head (+ (length tail) (sum tail))))`.
    
    `(+ 1 (+ head (+ (length tail) (sum tail))))` ≡ `(+ 1 (+ head (+ (length tail) (sum tail))))`.
    
    Therefore, the left-hand side steps to the value that the right-hand side steps to.
□
    

## Problem 3: Building Up Facts
1. `rev`:
```racket
(define rev
  (lambda (l)
    (match l
      ['() '()]
      [(cons head tail) (snoc (rev tail) head)])))
```
2. **Claim (Snoc Length)**: For all lists `l` and values `v`, `(length (snoc l v))` ≡ `(+ 1 (length l))`.

    _Proof_. Let `l` be an arbitrary list, and let `v` be an arbitrary value. We prove this claim by induction on `l`.

    Either `l` is empty or non-empty.
- **`l` is empty**. 

    The left-hand side, `(length (snoc '() v))` evaluates as follows:
    ```racket
         (length (snoc '() v))
    -->* (length (list v))
    -->  (length '(v))
    -->* (+ 1 (length '()))
    -->* (+ 1 0)
    -->  1
    ```
    
    The right-hand side, `(+ 1 (length '()))`, evaluates as follows:
    ```racket
         (+ 1 (length '()))
    -->* (+ 1 0)
    -->  1
    ```
    
- **`l` is nonempty**. Let `head` and `tail` be the head and tail of the list, respectively. We assume our induction hypothesis:

    **Induction Hypothesis**: `(length (snoc tail v))` ≡ `(+ 1 (length tail))`.

    We must prove:
    **Goal**: `(length (snoc l v))` ≡ `(+ 1 (length l))`.
    
    The left-hand side, `(length (snoc l v))`, evaluates as follows:
    ```racket
         (length (snoc l v))
    -->* (length (cons (car l) (snoc (cdr l) v)))
    -->* (length (cons head (snoc tail v)))
    ```
    `(cons head (snoc tail v))` is a list with `head` as the head and `(snoc tail v)` as the tail.
    ```racket
    -->* (+ 1 (length (snoc tail v)))
    ```
    
    The right-hand side, `(+ 1 (length l))`, evaluates as follows:
    ```racket
         (+ 1 (length l))
    -->* (+ 1 (+ 1 (length tail)))
    ```

    By our induction hypothesis: 
    `(+ 1 (length (snoc tail v)))` ≡ `(+ 1 (+ 1 (length tail)))`.
    
    `(+ 1 (+ 1 (length tail)))` ≡ `(+ 1 (+ 1 (length tail)))`
    
    Therefore, the left-hand side steps to the same value that the right-hand side steps to.
    
□


3. **Claim (Rev Length)**: For all lists `l`, `(length (rev l))` ≡ `(length l)`.

    _Proof_. Let `l` be an arbitrary list. We prove this claim by induction on `l`. 
    
    Either `l` is empty or non-empty.
- **`l` is empty**. 

    The left-hand side evaluates as follows:
    ```racket
         (length (rev '()))
    -->* (length '())
    -->* 0
    ```

    The right-hand side evaluates as follows:
    ```racket
         (length '())
    -->* 0
    ```
    
- **`l` is non-empty**. Let `head` and `tail` be the head tail of the list, respectively. We assume our induction hypothesis:

    **Induction Hypothesis**: `(length (rev tail))` ≡ `(length tail)`.

    We must prove:
    **Goal**: `(length (rev l))` ≡ `(length l)`.
    
     The left-hand side evaluates as follows:
    ```racket
         (length (rev l))
    -->* (length (snoc (rev tail) head))
    -->* (+ 1 (length (rev tail)))
    ```
    The last step of the evaluation was derived using the Snoc Length property: `(length (snoc l v))` ≡ `(+ 1 (length l))`.

    The right-hand side evaluates as follows:
    ```racket
          (length l)
    -->*  (+ 1 (length tail))
    ```
    
    By our induction hypothesis: 
    `(+ 1 (length (rev tail)))` ≡ `(+ 1 (length tail))`.
    
    `(+ 1 (length tail))` ≡ `(+ 1 (length tail))`.
    
    Therefore, the left-hand side steps to the same value that the right-hand side steps to.
    
□