FP2

Problems 3 - Sample Outline Solutions

(warning, there may be some spurious symbols or layout errors produced in

transcription to html)

Theorem && is assoc.

i.e. "x,y,z.(x&&y)&&z = x&&(y&&z)

Proof by case (on x)

True case show (True &&y) &&z = True && (y&& z).

lhs: y&&z by &&.0

rhs: y&&z by &&.0

False case Show (False &&y) &&z = False && (y&&z)

lhs: False &&z by &&.1

= False by &&.1

rhs: False by &&.1

Theorem && is comm. i.e. "x,y.(x&&y) = (y&&x)

Proof by case (on x)

True Case Show True &&y = y&&True

lhs: y by &&.0

rhs: y by &&.2

Theorem: "finite xs. sumlist1 xs = sumlist2 xs.

Proof by Induction on xs.

Base Case. Show sumlist1 [ ] = sumlist 2 [ ].

lhs. sumlist1 [ ] = 0 by sumlist1.0

rhs. sumlist2 [ ] = foldr + 0 [ ] by sumlist2.0

= 0 by foldr.0

Ind. Case Assume sumlist1xs = sumlist2 xs.

Show sumlist1 x:xs = sunlist2 x:xs

Lhs: sumlist1 x:xs = x + sunmlist1 xs by sumlist1.0

= x + sumlist2 xs by ass.

Rhs: sumlist2 x:xs = foldr + 0 (x:xs) by sumlist2.0

= x + (foldr + 0 xs) by foldr.1

= x + sumlist2 xs by sumlist2.0

(note: prefix Þinfix +)

Theorem "finite xs. double1 xs = double2 xs

Proof by Induction on xs

Base Case Show double1 [ ] = double2 [ ].

Lhs double1 [ ] = [ ] by double1.0

Rhs double2 [ ] = map (2*) [ ] by double2.0

= [ ] by map.1

Ind. Case Assume double1 xs = double2 xs

Prove double x:xs = double2 x:xs

Lhs double1 x:xs = (2*x) : double1 xs by double1.1

= (2*x) : double2 x by ass.

Rhs double2 x:xs = map (2*) x:xs

= (2+) x : map (2*) xs by map.1

= 2*x : map (2*) xs by (2*)

= 2*x : double 2 xs by double2.0

Theorem "xs. revl xs = rev2 (xs, [ ]) .

Proof by Induction on xs.

Base Case show

rev1 [ ] = rev2 ( [ ], [ ]).

Lhs. revl [ ] = [ ] by rev1.0

Rhs. rev2 ([ ], [ ]) = [ ] by rev2.0

Ind. Case Assume revl xs = rev2(xs, [ ]).

Show revl x:xs = rev2 (x:xs,[])

lhs. rev1 x:xs = rev1 xs ++ [x] by rev1.0

= rev2(xs,[]) ++ [x] by ass.

rhs. rev2 (x:xs,[]) = rev2(xs,[x]) by rev2.1

= rev2(xs,[])++[x] by rev2.2