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) xsfor 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 xscase m  n: [] and (x:xs), and in the latter m + n > length xs and m + n  length xsIf 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!)UPDATEIf [] 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) xsif n is greater than l, where l is the length of the input list, then take returns a list of length ldrop n [] = []drop 0 xs = xsdrop n (x:xs) = drop (n - 1) xsif n is greater than l, where l is the length of the input list, then drop returns the empty list
Proving laws of take and drop functions using structural induction on lists
proof techniques;induction
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 havedrop m (drop n []) = drop m [] = [] = drop (m + n) [] (definition of drop, base case)When the input list is not empty, we havedrop (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.