# CS 154 Homework 2: Proof by induction

## Proving properties of programs

In this written homework we shift our focus from just programming to writing proofs about programs, following along with the material being presented lately in lecture. As with previous homeworks, this one will be self-graded with a session in lecture and some on-line example solutions. You can still ask for help in lecture or lab, or office hours, etc., of course. You should also consult the proof rules "handout" (online) for the kinds of steps you can take during the course of a proof.

The properties we are proving here are not especially surprising: in fact, they're fairly obvious on the face of it. The point is rather to gain some experience in doing proofs by induction (on natural numbers and lists), especially with respect to the tricky parts, namely variable names, scoping and substitution. Sometimes you might even need to work "backwards" with respect to the normal direction of evaluation, i.e., replace the right-hand side of a definition by the left-hand side. You may want to use cut-and-paste in order to get a "symmetric" part of the proof out quickly, but be careful! Try to give "reasonable" reasons for your steps and, don't worry for now about non-termination or infinite lists.

OK, for this assignment, see if you can prove each of the following:

1. `length (append as bs) = add (length as) (length bs)` (i.e., the length of appended lists is the sum of their individual lengths) using these definitions:
```data Nat = Zero | Succ Nat data List a = Nil | Cons a (List a) add Zero m = m add (Succ n) m = Succ (add n m) length Nil = Zero length (Cons x xs) = Succ (length xs) append Nil ys = ys append (Cons x xs) ys = Cons x (append xs ys)```

2. `map (f . g) = map f . map g` (mapping a composed function once is the same as successively mapping each function individually) using these definitions:
```data List a = Nil | Cons a (List a) map f Nil = Nil map f (Cons x xs) = Cons (f x) (map f xs) (f . g) x = f ( g x)```

3. `twice (take n) = take n` (for all natural numbers n, as defined below) using these definitions:
```data Nat = Zero | Succ Nat data List a = Nil | Cons a (List a) take (Succ n) (Cons x xs) = Cons x (take n xs) take (Succ n) Nil = Nil take Zero (Cons x xs) = Nil take n Nil = Nil twice f x = f (f x)```