# CS 154 Homework 3: 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:

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)

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)

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)

#