David Tran’s blog

Just prove one, maybe later back to prove others.

Prove: For all finite nonnegative m and n such that n >= m:
drop m . take n = take (n - m) . drop m

(a) base step: m = 0
(drop 0 . take n) xs = drop 0 (take n xs) = take n xs
(take (n-0) . drop 0) xs = take n (drop 0 xs) = take n xs
==> Proven.

(b) induction hypothesis: Assume that (drop m . take n) xs = (take (n-m) . drop m) xs

(drop (m+1) . take n) xs
= drop (m+1) (take n xs)
= drop (1+m) (take n xs) -- commutative of (+)
= (drop 1 . drop m) (take n xs)) -- property of drop m . drop n = drop (m+n)
= drop 1 ( drop m (take n xs))
= drop 1 ((drop m . take n) xs)
= drop 1 ((take (n-m) . drop m) xs) -- induction hypothesis assumption
= drop 1 (take (n-m) (drop m xs))
= (drop 1 . take (n-m)) (drop m xs)
= (take (n-m-1) . drop 1) (drop m xs) -- property of take m . drop n = drop n . take (m+n)
= take (n-(m+1)) (drop 1 (drop m xs))
= take (n-(m+1)) ((drop 1 . drop m) xs)
= take (n-(m+1)) (drop(1+m) xs) -- property of drop m . drop n = drop (m+n)
= (take (n-(m+1)) . drop (m+1)) xs -- commutative of (+)
==> Proven.

This entry was posted on Saturday, June 16th, 2007 at 5:10 pm and is filed under Haskell - SOE. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.