# 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.
□
Sign in with Wallet
Connect another wallet