Proving laws of take and drop functions using structural induction on lists

Question

I'm trying to prove the following laws using structural induction on (finite) lists:

take m (drop n xs) = drop n (take (m + n) xs)
drop m (drop n xs) = drop (m + n) xs

for all m, n and every finite list xs (code snippets are in Haskell). I'm not sure how to tackle it though, more specifically: afaik when using induction on intervals, the first induction step is for m > n and the second for m ≤ n. Now in this case the law must also be valid for all finite lists, does that mean the proof involves prooving all the following?

• case m > n: [] and (x:xs), and in the latter m + n > length xs and m + n ≤ length xs

• case m ≤ n: [] and (x:xs), and in the latter m + n > length xs and m + n ≤ length xs

If yes I can update my question and show exactly where I'm stuck.

(Please don't post the entire solution, I'd just like to have some pointers. Thanks!)

UPDATE

If [] denotes the empty list and (x:xs) a list with at least one element (x is the head of the list and xs its tail), possible definitions of take and drop are:

take n [] = []
take 0 xs = []
take n (x:xs) = x : take (n - 1) xs

if n is greater than l, where l is the length of the input list, then take returns a list of length l

drop n [] = []
drop 0 xs = xs
drop n (x:xs) = drop (n - 1) xs

if n is greater than l, where l is the length of the input list, then drop returns the empty list

Answer 1

You can prove the second law by induction on n:

• Base case:

drop m (drop 0 xs) = drop m xs (definition of drop, base case)

= drop (m + 0) xs (since m + 0 = m)

• Inductive step:

We have to consider two cases: when the input list is empty, and when it's not empty. When it's empty, we have

drop m (drop n []) = drop m [] = [] = drop (m + n) [] (definition of drop, base case)

When the input list is not empty, we have

drop (m + n) (x:xs) = drop (m + n - 1) xs (definition of drop, inductive case)

= drop m (drop (n - 1) xs) (inductive hypothesis)

= drop m (drop n (x:xs)) (definition of drop, inductive case)

I imagine that the first law is not much more difficult. Try to prove it by induction on n, and if it doesn't work, try induction on m. One of them will probably work.