= Solution
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 $0\leq n\leq\mathrm{len}$. 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.
Back to article page
