PIH - ch13 - Reasoning about programs

PIH - ch13 - Reasoning about programs - exercises

by @ardumont on 04 Jun 2013

At last, the last chapter exercises.

Overlapping patterns

Give an example of a function from the standard library in appendix A that is defined using overlapping patterns.

Example using overlapping patterns:

null :: [a] -> Bool
null [] = True
null (_ : _) = False

Proof by induction

Show that add n (Succ m) = Succ (add n m), by induction on n.

Recall the definition:

data Nat = Zero | Succ Nat

add :: Nat -> Nat -> Nat
add Zero m = m                  -- (1)
add (Succ n) m = Succ (add n m) -- (2)

To prove by induction on n the asked properties, we'll begin by the base case:

add Zero (Succ m) = Succ m            -- by definition of (1)
                  = Succ (add Zero m) -- (2)

Ok, the base case is sound.

Now, we can focus on the inductive case:

add (Succ n) (Succ m) = Succ (add n (Succ m)) -- using the induction hypothesis
                      = Succ (Succ (add n m))
                      = Succ (add (Succ n) m)

So the property holds.

commutativity

Using this property, together with add n Zero = n, show that addition is commutative, add n m = add m n, by induction on n.

Again, base case first:

add Zero m = m
           = add m Zero -- property of add in the previous exercise.

ok.

Now, inductive case:

add (Succ n) m = Succ (add n m) -- by hypothesis
               = Succ (add m n)
               = add m (Succ n) -- using property add n (Succ m) = Succ (add n m)

The property holds.

The base case is ok and the inductive case holds the property. So by induction, the hypothesis is sound, add is commutative.

all true

Using the following definition for the library function that decides if all elements of a list satisfy a predicate:

all p [] = True

all p (x : xs) = p x && all p xs

Complete the proof of the correctness of replicate by showing that it produces a list with identical elements, all (= x) (replicate n x)=, by induction on n ≥ 0.

Hint: show that the property is always True.

Recall replicate's definition:

replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x:replicate (n-1) x

base case:

all (== x) (replicate 0 x) = all (== x) [] -- by definition of replicate
                           = True          -- by definition of all

ok.

Inductive case:

all (== x) (replicate (n+1) x) = all (== x) (x:replicate n x)             -- by definition of all
                               = ((== x) x) && all (== x) (replicate n x)
                               = True && all (== x) (replicate n x)       -- by hypothesis
                               = True

ok.

Checks

Using the definition

[] ++ ys = ys (1)

(x:xs) ++ ys = x:(xs ++ ys) (2)

verify the following two properties, by induction on xs:

xs ++ [] = xs

xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Hint: the proofs are similar to those for the add function.

base case:

[] ++ [] = []                       -- using 1)

[] ++ (ys ++ zs) = ys ++ zs         -- using 1)
                 = ([] ++ ys) ++ zs

Inductive case:

(x:xs) ++ [] = x:(xs ++ []) -- using induction hypothesis
             = (x:xs)

(x:xs) ++ (ys ++ zs) = x:(xs ++ (ys ++ zs)) -- induction hypothesis
                     = x:((xs ++ ys) ++ zs
                     = (x:(xs ++ ys) ++ zs
                     = ((x:xs) ++ ys) ++ zs

ok.

Proof on map and composition of functions

Using the definitions

map f [] = []

map f (x : xs) = f x : map f xs

(f . g) x = f (g x)

show that map f (map g xs) = map (f . g) xs, by induction on xs.

base case:

map f (map g []) = map f []       -- by definition of map
                 = []             -- by definition of map
                 = map (f . g) []

inductive case:

map f (map g (x:xs)) = map f ((g x):(map g xs))    -- by definition of map
                     = f (g x):(map f (map g xs))  -- by hypothesis
                     = f (g x):(map (f . g) xs)    -- by definition of (f . g)
                     = (f . g) x):(map (f . g) xs) -- by definition of map
                     = map (f . g) (x:xs)

ok.

take'n drop

Using the definition for ++ given above, together with:

take 0 _ = []

take _ [] = []

take n (x:xs) = x:take (n-1) xs

drop 0 xs = xs

drop _ [] = []

drop n (_:xs) = drop (n-1) xs

show that take n xs ++ drop n xs = xs , by simultaneous induction on the integer n ≥ 0 and the list xs.

Hint: there are three cases, one for each pattern of arguments in the definitions of take and drop.

base cases:

take 0 xs ++ drop 0 xs = [] ++ [] -- by definition of take and drop
                       = []       -- this is true for all xs, including []

take n [] ++ drop n [] = [] ++ []
                       = []

inductive cases:

take (n+1) (x:xs) ++ drop (n+1) (x:xs) = (x:take n xs) ++ (drop n xs)   -- by definition of take and drop
                                       = x:((take n xs) ++ (drop n xs)) -- by induction hypothesis
                                       = (x:xs)

ok.

Tree

Given the type declaration data Tree = Leaf Int | Node Tree Tree, show that the number of leaves in such a tree is always one greater than the number of nodes, by induction on trees.

Hint: start by defining functions that count the number of leaves and nodes in a tree.

First the definitions:

leaves :: Tree -> Int
leaves (Leaf _) = 1
leaves (Node l r) = leaves l + leaves r

*C12> leaves (Node (Node (Leaf 0) (Node (Leaf 1) (Leaf 2))) (Leaf 3))
4

nodes :: Tree -> Int
nodes (Leaf _) = 0
nodes (Node l r) = 1 + nodes l + nodes r

*C12> nodes (Node (Node (Leaf 0) (Node (Leaf 1) (Leaf 2))) (Leaf 3))
3

Now, we must prove that the relation between the number of nodes and leaves is the following: (leaves t) - (nodes t) = 1

Beginning with base case:

leaves (Leaf x) - nodes (Leaf x) = 1 - 0 -- following the definitions
                                 = 1

ok.

Inductive case:

leaves (Node l r) - nodes (Node l r) = (leaves l + leaves r) - (1 + nodes l + nodes r)
                                     = (leaves l - nodes l) + (leaves r - nodes r) - 1 -- by induction hypothesis
                                     = 1 + 1 - 1
                                     = 1

ok.

comp

Given the equation comp' e c = comp e ++ c, show how to construct the recursive definition for comp', by induction on e.

Recall the definition of expression:

data Expr = Val Int | Add Expr Expr

eval :: Expr -> Int
eval (Val x)   = x
eval (Add x y) = eval x + eval y

type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD deriving (Show)

exec :: Code -> Stack -> Stack
exec [] s             = s
exec (PUSH x:c) s     = exec c (x:s)
exec (ADD:c) (x:y:xs) = exec c (x+y:xs)

-- *C12> exec [PUSH 1,PUSH 2,ADD] []
-- [3]
-- *C12> exec [PUSH 10,PUSH 11,PUSH 12,ADD,ADD] []
-- [33]

comp :: Expr -> Code
comp (Val x)   = [PUSH x]
comp (Add l r) = (comp l) ++ (comp r) ++ [ADD]

Now the construction.

base case:

comp' (Val x) c = comp (Val x) ++ c
                = [PUSH x] ++ c
                = (PUSH x:c)

inductive case:

comp' (Add l r) c = comp (Add l r) ++ c
                  = (comp l) ++ (comp r) ++ [ADD] ++ c
                  = comp l ++ (comp r ++ (ADD:c))
                  = comp l ++ (comp' r (ADD:c))
                  = comp' l (comp' r (ADD:c))

We obtain the definition of comp':

comp' (Val x) c = (PUSH x:c)
comp' (Add l r) c = comp' l (comp' r (ADD:c))