Lab6

Proving the proof obligations from the lecture slides

Given definition of (++):

We want to prove:

xs ++ [] = xs                (po.1)
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Proof of po.1

• Base:

  • We want to prove [] ++ [] = []

• Induction step:

  • We want to prove (x:xs) ++ [] = (x:xs)

  • our assumption is: xs ++ [] = xs = (IH0

Proving base:

LHS:

[] + [] = []            by (++.1)

RHS:

[]

RHS = LHS

Induction:

LHS

(x:xs) ++ []
= x:(xs ++ [])                 by (++.2)
= x:(xs)                       by (IH)
= (x:xs)

RHS

(x:xs)

RHS = LHS

Proof of (po.2)

• Base:

  • We want to prove [] ++ (ys ++ zs) = ([] ++ ys) ++zs

• Induction step:

  • We want to prove (x:xs)++ (ys ++ zs) = ((x:xs)++ ys) ++zs

  • our assumption is: xs ++ (ys ++ zs) = (xs ++ ys) ++zs

Proving base:

LHS:

 [] ++ (ys ++ zs) 
= (ys ++zs)               by ++.1

RHS:

([] ++ ys) ++zs
= (ys ++ zs)            by ++.1

RHS = LHS

Induction:

LHS

(x:xs) ++ (ys ++ zs)
= x:(xs ++ (ys ++ zs)) by ++.2
= x:((xs++ys) + zs)     by IH
= (x:(xs ++ ys)) ++ zs   by ++.2 (in the reverse direction)

RHS

((x:xs) ++ ys) ++ zs
= (x:(xs ++ ys))        by ++.2

RHS = LHS

Textbook exercises

9.10

Show for all finite xs and defined n that:

Take n xs ++ drop n xs = xs

• take n applied to xs returns the prefix of xs of length n

• drop skips the first n elements are returns the remainder

• Base:

  • We want to prove that Take n [] ++ drop n [] = []

• Induction step:

  • We want to prove Take n (x:xs) ++ drop n (x:xs) = (x:xs)

  • our assumption is: xs ++ (ys ++ zs) = (xs ++ ys) ++zs

Proving the base case:

RHS:

Take n [] ++ drop n []
= [] ++ drop n []       = by the property take _ [] = []
= [] ++ []               = by the property drop _ [] = []
= []

LHS:

[]

LHS = RHS

Proving the second base case:

RHS:

Take 0 xs ++ drop 0 xs
= [] ++ xs           by property 2 from both things
= xs

LHS:

xs

LHS = RHS

Induction:

LHS

Take n (x:xs) ++ drop n (x:xs)
x : take (n-1) xs

RHS

(x:xs)

RHS = LHS