Prove filter (all p) . cp = cp . map (filter p)

Question

In chapter 5th of Thinking Functionally with Haskell by Richard Bird, there's an equation:

filter (all p) . cp = cp . map (filter p)

I wonder how to prove it? (fusion law)?

I try to prove with fusion law. but how to prove the fusion law?

Answer 1

rewrite cp with foldr

cp = folder g [[]]
        where g xs xss = [x:ys|x<-xs,ys<-xss]

Assumption: (a) filter (all p) (cp xss) = cp (map (filter p) xs) = folder g [[]] (map (filter p) xs)

should prove equation (b) holds

(b)    filter (all p) (cp (xs:xss)) = cp (map (filter p) (xs:xss)) 

{# definition of map and cp #}
cp (map (filter p) (xs:xss)) = foldr g [[]] (map (filter p) (xs:xss))
{# definition of folder #}
g (filter p xs) (foldr g [[]] (map (filter p)) xss)

{# based on assumption (a)#) g (filter p xs) (filter (all p) (cp xss))

{# definition of g #}
[x:ys|x<-filter p xs, ys<-filter (all p) (cp xss)]
{# definition of filter 
[x:ys|x<-[x' <- xs,p x'], ys <- [ys' <- (cp xss), (all p) ys']]

{# condiontial cp means cp after filter #}

filter (all p) (cp (xs:xss))

In conclusion,
cp (map (filter p) (xs:xss)) = filter (all p) (cp (xs:xss))