Tutorial - Induction

Dealing with structures not numbers now

To rpove a property P(xs) holds for all finite lists, we must prove:

1. Base case: Prove P([])

2. Induction step: prove (P(x:xs) on the assumption that P(xs)

1.

• If both lists are empty, its trivial

Given:

sum [] = 0 —s1

sum (x:xs) = x + sum xs — s2

[ ]++ zs = zs — ++1

(w:ws) ++ zs = w:(ws ++ za) == (++2)

Question: Prove sum (xs ++ ys) = sum xs + sum ys

We want to prove two goals of the induction process

(1). For base case, we have to prove:

• sum ([] ++ ys) = sum [] + sum ys

(2) For induction step, we have to prove:

• sum ((x:xs) ++ ys) = sum (x:xs) + sum (ys) on the assumption that

• sum (xs ++ ys) = sum xs + sum ys is true (the Inductive hypothesis)

Base:

LHS:

• sum ([] ++ ys)

• = sum (ys) By rule ++1

RHS:

• sum [] + sum ys = 0 + sum ys by (s1)

• = sum ys by calculus

LHS = RHS

Inductive Case:

LHS: sum ((x:xs) ++ ys)

• = sum (x(xs ++ ys)) by ++2

• = x +sum (xs ++ ys) by s2

RHS: sum (x:xs) + sum (ys)

• = x + sum xs + sum ys by s2

• = x + sum (xs ++ ys) by Inductive Hypothesis

LHS = RHS

Question2: Prove xs ++ [] = xs

Base:

LHS: [] ++ []

• = [] by ++1

RHS: []

LHS = RHS

Given:

sum [] = 0 —s1

sum (x:xs) = x + sum xs — s2

[ ]++ zs = zs — ++1

(w:ws) ++ zs = w:(ws ++ za) == (++2)

Inductive Step

• Assume xs ++ [] = xs

LHS: (x:xs) ++ []

• x:(xs ++ []) by ++2

• (x:xs) by IH

RHS: (x:xs)

LHS = RHS