Discrete Mathematics for Computer Scientists -- Exercises Week 6 - Structural InductionDIT980, HT 2015
Home | Schedule | Assignments | Exercises | Exam | AboutFire | Forum | TimeEdit | Links | 2014
Exercises Week 6 - Structural Induction

Book: -. Lecture: Friday, week 5 (lecture notes).

Some answers are available.

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!)


Basic Exercise

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


More Exercises

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
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: n=k+1, k ≥ 2.

Let us assume we have a boring country with k 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 (=k+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?