Wednesday 6/10 - EXERCISES W6 - Structural Induction - ANSWERS

Preparation

Lectures: Monday, week 6.

Read: Notes on Structural Induction (pdf). Nothing in the book.

Exercises

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 to use in the exercises:

  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

Hint: You need the length/++ property from the lecture notes as a lemma.

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

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

Hint: You need the property in exercise 1. as a lemma.

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

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

Hint: You don't need induction, just case split.

(5.) Prove that, for all lists xs:

  take (length xs) xs = xs

You may assume that length ys ≥ 0 for all lists ys. (If you wish to prove this too, go ahead! :-)

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)

To do this, you need to prove and use a helper lemma, namely the following: For all natural numbers x, y :: Nat:

  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)

Hint: You need to use a helper lemma about rev and ++, check the lecture notes.

(11.) Prove that, for all lists xs:

  flatten (spine xs) = xs

Starred Exercises

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

and the following helper function:

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

Can you prove that, for all lists xs:

  ordered (sort xs)

? In other words, the sort function actually produces a sorted list?

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

  ordered xs  ==>  ordered (insert x xs)

Prove this first.

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?