Structural induction in Haskell (take n . map f) xs = (map f . take n) xs

How to show that for every function f and for every finite List xs following holds: (take n . map f) xs = (map f . take n) xs

take :: Int -> [a] -> [a]
take 0 _ = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = f x : map f xs

(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f(g x)

Show for every step the used argument. How I actually start on such problems and whats the way to prove it generally. Would appreciate some help to get into this easier.

looked into my script but couldnt really grasp it

I will follow the examples in Thinking Functionally by Richard Bird (Cambridge University Press, 2015, pp. 113 - 115).

We have seen that every finite list is either the empty list [] or of the form x:xs where xs is a finite list. Hence, to prove that P(xs) holds for all finite lists xs, we can prove:

1. P([]) holds;
2. For all x and for all finite lists xs, that P(x:xs) holds assuming P(xs) does. [emphasis mine]

The assumption mentioned in point two will be very important and referenced as "{induction}" in the proof.

First, let's lay out the equations for map and take with the references to be used in the proof.

map :: (a -> b) -> [a] -> [b]
map f [] = []                      -- {map.1}
map f (x:xs) = f x : map f xs      -- {map.2}

take :: Int -> [a] -> [a]
take n [] = []                     -- {take.1}
take 0 xs = []                     -- {take.2}
take n (x:xs) = x : take (n-1) xs  -- {take.3}

Proof:

We want to prove P(xs) holds for all finite lists xs where our property, P, is (take n . map f) xs == (map f . take n) xs.

Case []

(take n . map f) []               (map f . take n) []
= {map.1}                         = {take.1}
take n []                         map f []
= {take.1}                        = {map.1}
[]                                []

P([]) holds.

Case x:xs

(take n . map f) (x:xs)           (map f . take n) (x:xs)
= {map.2}                         = {take.3}
take n (f x : map f xs)           map f (x : take (n-1) xs)
= {take.3}                        = {map.2}
f x : (take (n-1) (map f xs))     f x : (map f (take (n-1) xs))
= {composition}                   = {composition}
f x : ((take (n-1) . map f) xs)   f x : ((map f . take (n-1)) xs)
                                  = {induction}
                                  f x : ((take (n-1) . map f) xs)

P(x:xs) holds.

Q.E.D.

In my opinion, the tricky part is the "{induction}" step. It is based on the very equivalence we are trying to prove. This is based on the assumption that P(xs) holds, as in point two in the quotation from Thinking Functionally above.

All I can offer here is the advice that you convince yourself of the legitimacy of the assumption. In "Case []" we show that P holds for an empty list, which is nevertheless an instance of xs. In "Case (x:xs)" we show that the first item in the list is the same for both sides, therefore we, in effect, know that P holds for [x] as well -- another instance of xs. Having shown that P holds for [] and [x], the assumption is sound. Then proceeding to another item in the list can be intuited as simply reiterating what has already been established. At least this is how I understand it.