CS 254 Lab 7: Proof by induction

Proving properties of programs

In this "lab" (more like written homework, but you can come to lab for help, and you should use a computer to type up your answers) we will move on to proofs, as in lecture. You should also consult the class handouts, which give some ideas about proof rules to use and an example 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. Note that you may sometimes 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. mult x (mult y z) = mult (mult x y) z

   (i.e., the associativity of multiplication) using these definitions:

   data Nat = Zero | Succ Nat
   
   mult  Zero    m = Zero
   mult (Succ n) m = plus m (mult n m)
   
   plus  Zero    m = m
   plus (Succ n) m = Succ (plus n m)

---

2. twice (take n) = take n

   (for all natural numbers n, as defined above, but note here we are using standard math notation for successor and zero)
   using these additional definitions:

   data [a] = [] | (:) a [a]  -- weird pseudo-definition of lists
   		
   take (n+1) (x:xs) = x : take n xs
   take (n+1) []     = []
   take 0    (x:xs)  = []
   take n     []     = []
   
   twice f x = f (f x)

---

3. length (filter p xs) <= length xs

   using these definitions in addition to that for lists above (note that this is an inequality, so here you may also use standard facts from math about "<="):

   length [] = 0
   length (x:xs) = 1 + length xs
   		
   filter p [] = []
   filter p (x:xs) = if p x then x:ys else ys
                     where ys = filter p xs

---