Proof that scanl can be written as foldr?

Hello, I'm trying to solve the exercise 4.6.5 of Bird's "Introduction to functional programming using Haskell". Let me quote: "Prove that scanl f e can be written as a foldr, if f is associative with unit e. Can scanl f e be written as a foldl without any assumptions on f and e?" So far reasoning by myself and googling a bit I reached to the following scanl definition using foldl (without any assumptions afaik): scanl f e = foldl (\xs next -> xs ++ [f (last xs) next]) [e] Furthermore, previously on the same chapter, it says that: scanl f e = foldr g [e] where g x xs = e : map (f x) xs Using this definition, I tried proving it by induction, but since I got stuck, I tried seeing if I could find some way to use the first duality theorem (with the foldl definition), or fusion, but to no avail. The induction proof I wrote is the following: scanl f e = foldr g [e] where g y ys = e : map (f y) ys By the principle of extensionality, this is equivalent to: scanl f e xs = foldr g [e] xs where g y ys = e : map (f y) ys We prove this equality by induction on xs. Case([]). For the left-hand side we reason scanl f e [] = {scanl.1} [e] For the right-hand side foldr g [e] [] = {foldr.1} [e] Case(x:xs). For the left-hand side we reason scanl f e (x:xs) = {scanl.2} e : scanl f (f e x) xs = {f has unit e} e : scanl f x xs = {induction hypothesis} e : foldr g [x] xs For the right-hand side foldr g [e] (x:xs) = {foldr.2} g x (foldr g [e] xs) = {definition of g} e : map (f x) (foldr g [e] xs) = {definition of map} e : foldr ((:) . (f x)) [] (foldr g [e] xs) I'm not even sure the last step is useful, but I thought maybe I could combine both foldrs into a single one (that's why I thought about the fusion law). Anyway, any help or pointer that can lead me in the right direction is very much appreciated. Thanks in advance.
participants (1)
-
Cristian Ontivero