The idea is that you should prepare these exercises at home, by yourself or with your group. If you have any questions, you can come to the exercise session and ask them to the assistants. (If you do not prepare in advance, there is little point in coming!)

Lectures: Friday, week 5.

Read: lecture notes. (Nothing in the book.)

Some answers are available.

Please read the lecture notes and make sure you understand most of the example proofs there.

Now please think about these.

I encourage you to type in the (Haskell) code of these functions, and play around with them. A good idea is to write QuickCheck properties that check these equations! If you do this, don't forget to specify the type on which you are testing your properties. When you test the properties of lists, use [Int]. Testing properties of trees, use Tree Int.

Some code:

  elem :: Eq a => a -> [a] -> Bool
  x `elem` []     = False
  x `elem` (y:ys) = x==y || (x `elem` ys)   

  (++) :: [a] -> [a] -> [a]
  []     ++ ys = ys
  (x:xs) ++ ys = x : (xs ++ ys)

  rev :: [a] -> [a]
  rev []     = []
  rev (x:xs) = rev xs ++ [x]

  length :: [a] -> Integer
  length []     = 0
  length (x:xs) = 1 + length xs

  take :: Integer -> [a] -> [a]
  take n _  | n <= 0 = []
  take n []          = []
  take n (x:xs)      = x : take (n-1) xs

1. Prove that, for all x and all lists xs, ys:

  x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys)

2. Prove that, for all lists xs:

  length (rev xs) = length xs

3. Prove that, for all x and all lists xs:

  x `elem` rev xs = x `elem` xs

4. Prove that, for all x and all lists xs:

  x `elem` xs  ==>  length xs > 0

5. Prove that, for all lists xs:

  take (length xs) xs = xs

Some more code. Here, we define the natural numbers, as they are defined primitively in basic mathematics.

  data Nat = Zero | Succ Nat
  
  even :: Nat -> Bool
  even Zero     = True
  even (Succ n) = not (even n)

  odd :: Nat -> Bool
  odd Zero     = False
  odd (Succ n) = not (odd n)
  
  plus :: Nat -> Nat -> Nat
  plus Zero     y = y
  plus (Succ x) y = Succ (plus x y)

6. Prove that, for all natural numbers x :: Nat:

  even x = not (odd x)

7. Prove that, for all natural numbers x :: Nat:

  plus x Zero = x

8. Prove that, for all natural numbers x :: Nat:

  even (plus x x)

  plus x (Succ y) = Succ (plus x y)

Some more code. Here, we define a datatype for trees. The flatten function takes a tree and produces a list of all the elements in the tree. The swap function works the same as in the lecture. The size function computes the number of nodes in a tree. The spine function creates a tree from a list, where all elements are put in the right "spine" of the tree.

  data Tree a = Empty | Node a (Tree a) (Tree a)

  flatten :: Tree a -> [a]
  flatten Empty        = []
  flatten (Node x p q) = flatten p ++ [x] ++ flatten q

  swap :: Tree a -> Tree a
  swap Empty        = Empty
  swap (Node x p q) = Node x (swap q) (swap p)

  size :: Tree a -> Integer
  size Empty        = 0
  size (Node _ p q) = 1 + size p + size q

  spine :: [a] -> Tree a
  spine []     = Empty
  spine (x:xs) = Node x Empty (spine xs)

9. Prove that, for all trees p:

  size p = length (flatten p)

10. Prove that, for all trees p:

  flatten (swap p) = rev (flatten p)

11. Prove that, for all lists xs:

  flatten (spine xs) = xs

These exercises are for students who are looking for a challenge.

1*. Consider the following program.

  sort :: [Integer] -> [Integer]
  sort []     = []
  sort (x:xs) = insert x (sort xs)

  insert :: Integer -> [Integer] -> [Integer]
  insert x []              = [x]
  insert x (y:ys) | x <= y = x : y : ys
                  | x > y  = y : insert x ys

  ordered :: [Integer] -> Bool
  ordered []       = True
  ordered [x]      = True
  ordered (x:y:xs) = x <= y && ordered (y:xs)

  ordered (sort xs)

You will need a helper lemma, that says that, for all x and all lists xs:

  ordered xs  ==>  ordered (insert x xs)

Hint: For the helper lemma, you need structural induction on xs, and in the step case you need to do a case split on if the tail of xs is empty or not.

After you prove the helper lemma, the original property (ordered (sort xs)) is easy.

2*. A few weeks ago we "proved" that all horses have the same color, by using a faulty induction proof.

Here is another inductive "proof", with another mistake! I would like you to catch this mistake.

We are going to introduce the concept of a "boring country". A boring country is a country where there exist no unique names. In other words, for every person who lives in a boring country, there exists another person who also lives there who has the same name. You are never the only one with your name!

To "prove": Everyone in a boring country has the same name. (This is obviously not true, can you find a counterexample?)

Proof: By simple induction on the number n of people in the boring country.

Base cases:

n=1: A country with only 1 person cannot be boring, so our statement is trivially true.

n=2: In a boring country with 2 persons, both have to have the same name.

Step case:

Let us assume we have a boring country with n people. The I.H. says that all people in that country must have the same name.

Now, we add one person X, getting a country with n+1 people. For the resulting country to be boring, there must be at least one other person Y that has the same name as X. But Y lives in the country with k people, where everyone has the same name as Y. So, everyone also has the same name as X.

Can you spot the mistake?