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)