module ListProperties where

open import Prelude
open import Logic.Base
open import Logic.Identity
open import Logic.ChainReasoning

open import Data.List

module ChainR = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)
open ChainR


foldr-fusion : {A B C : Set} ->  
  (h : B -> C) -> {f : A -> B -> B} -> {g : A -> C -> C} -> {z : B} -> 
   ((a : A) -> (b : B) -> h (f a b) ≡ g a (h b)) ->
      ∀ (\x -> h (foldr f z x) ≡ foldr g (h z) x)
foldr-fusion h {f} {g} {z} _ [] = refl
foldr-fusion h {f} {g} {z} p (a :: x) =
   chain> h (foldr f z (a :: x))  
      === h (f a (foldr f z x))   by refl 
      === g a (h (foldr f z x))   by p a (foldr f z x)
      === g a (foldr g (h z) x)   by cong (g a) (foldr-fusion h p x) 
      === foldr g (h z) (a :: x)  by refl


idIsFold : {A : Set} -> (x : List A) ->
              (x ≡ foldr _::_ [] x)
idIsFold {_} [] = refl
idIsFold {_} (a :: x) = 
   chain> (a :: x)
      === a :: foldr _::_ [] x    by cong (_::_ a) (idIsFold x)
      === foldr _::_ [] (a :: x)  by refl

++IsFold : {A : Set} -> (x : List A) -> {y : List A} -> 
             x ++ y ≡ (foldr _::_ y x)
++IsFold {A} x {y} = 
   chain> x ++ y
      === (foldr _::_ [] x) ++ y  by cong (\x -> x ++ y) (idIsFold x)
      === foldr _::_ ([] ++ y) x  by foldr-fusion (\x -> x ++ y) (\_ _ -> refl) x
      === foldr _::_ y x          by refl

mapIsFold : {A B : Set} -> {f : A -> B} ->
             (x : List A) -> map f x ≡ foldr (\a y -> f a :: y) [] x
mapIsFold {A} {B} {f} x =
   chain> map f x
      === map f (foldr _::_ [] x)        by cong (map f) (idIsFold x) 
      === foldr (\a y -> f a :: y) [] x  by foldr-fusion (map f) (\_ _ -> refl) x


map-cat : {A B : Set} -> {f : A -> B} -> (x : List A) -> {y : List A} ->
      map f (x ++ y) ≡ (map f x ++ map f y)
map-cat {A} {B} {f} x {y} = 
  chain> map f (x ++ y) 
     === map f (foldr _::_ y x)                     by cong (map f) (++IsFold x)
     === foldr (\a z -> f a :: z) (map f y) x       by foldr-fusion (map f) (\_ _ -> refl) x
     === foldr (\a z -> f a :: z) [] x ++ (map f y) by sym (foldr-fusion (\z -> z ++ map f y) (\_ _ -> refl) x)
     === map f x ++ map f y                         by cong (\z -> z ++ map f y) (sym (mapIsFold x))

concat : {A : Set} -> List (List A) -> List A 
concat = foldr _++_ []

concat-map : {A B : Set} -> {f : A -> B} -> 
         ∀ (\xs -> concat (map (map f) xs) ≡ map f (concat xs))
concat-map {A} {B} {f} xs = 
  chain> concat (map (map f) xs) 
     === concat (foldr (\x ys -> map f x :: ys) [] xs) by cong concat (mapIsFold xs)
     === foldr (\x xs -> map f x ++ xs) [] xs          by foldr-fusion concat (\_ _ -> refl) xs
     === map f (concat xs)                           
           by sym (foldr-fusion (map f) (\z w -> map-cat z) xs)

map-compose : {A B C : Set} -> {g : B -> C} -> {f : A -> B} -> 
                (x : List A) -> (map (g ∘ f) x ≡ (map g ∘ map f) x)
map-compose {A} {B} {C} {g} {f} x = 
   chain> map (g ∘ f) x
      === map (g ∘ f) (foldr _::_ [] x)
             by cong (map (g ∘ f)) (idIsFold x) 
      === foldr (\a y -> g (f a) :: y) [] x
             by foldr-fusion (map (g ∘ f)) (\_ _ -> refl) x
      === (map g ∘ foldr (\a y -> f a :: y) []) x 
             by sym (foldr-fusion (map g) (\_ _ -> refl) x)
      === (map g ∘ map f) x
             by cong (map g) (sym (mapIsFold x)) 


foldr-eq : {A B : Set} -> {f g : A -> B -> B} -> {e : B} ->
             (forall a -> forall b -> f a b ≡ g a b) ->
               forall x -> foldr f e x ≡ foldr g e x
foldr-eq {A} {B} {f} {g} {e} f≡g x =
   chain> foldr f e x 
      === foldr f e (foldr _::_ [] x)  by cong (foldr f e) (idIsFold x)
      === foldr g e x                  by foldr-fusion (foldr f e) (\a x -> f≡g a (foldr f e x)) x

map-eq : {A B : Set} -> {f g : A -> B} ->
           (forall a -> f a ≡ g a) -> forall x -> map f x ≡ map g x
map-eq {A} {B} {f} {g} f≡g x = 
    chain> map f x
       === foldr (\a y -> f a :: y) [] x  by mapIsFold x
       === foldr (\a y -> g a :: y) [] x  by foldr-eq (\a y -> cong (\b -> b :: y) (f≡g a)) x
       === map g x                        by sym (mapIsFold x)