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

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

• The case-split m>n and m<=n does not look too useful to me, at a first glance. Prove the equations for xs=[], which is trivial. Then, assume that they work on xs for all pairs (n,m) where either n<N, m<=M or n<=N, m<M, and prove they must also work on x:xs with the pair (N,M). (Check that this is a well-founded ordering) – chi Apr 3 '17 at 14:11
• Perhaps you could include the definition of take and drop, for those of us not versed in Haskell. – Yuval Filmus Apr 3 '17 at 16:03
• @Yuval Filmus very good point thanks, I'll update the question – futtetennista Apr 3 '17 at 16:16

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.

• Thanks a bunch! Yeah the other law is trivial once you set up a handy inductive hypothesis. The ones I was originally using were completely bogus and didn't bring me anywhere. One clarification on your solution: you're using induction on n in the base case and on n and the list in the inductive step. I thought proofs should use inductions on the same (set of) variables (in this case taking [] wouldn't have made any difference but I'm more interested in the general case). – futtetennista Apr 3 '17 at 19:11
• I don't understand your question. My proof is by induction on n. The base case and the inductive step comprise the inductive proof. They're two parts of the puzzle. You're correct that there is a part missing, which I will now add. – Yuval Filmus Apr 3 '17 at 19:30
• Yeah apologies, just re-read my question and I did a bad job at explaining myself. Anyway with the addition of the missing case for [] now everything makes sense to me. Thanks again. – futtetennista Apr 3 '17 at 20:09