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)