Write u = take n xs, v = drop n xs, and len = length xs. Part (c) gives xs = u ++ v; part (d) gives length v = len-n because . Use the finite-list laws take (length v) (v ++ w) = v, length (reverse v) = length v, and reverse (reverse v) = v. Then equational reasoning gives
reverse (take (len-n) (reverse xs))
= reverse (take (length v) (reverse (u ++ v)))
= reverse (take (length (reverse v)) (reverse v ++ reverse u))
= reverse (reverse v)
= v
= drop n xs
The first and second steps use the decomposition and the length equation; the third uses reversal of a concatenation; the fourth uses the stated take law. This is an algebraic proof using established laws, rather than a new induction proof.

Articles by others on the same topic (0)

There are currently no matching articles.