module List+ where open import Prelude open import Logic.Base open import Logic.Identity open import Logic.ChainReasoning data List⁺ (A : Set) : Set where [_]⁺ : A -> List⁺ A _::⁺_ : A -> List⁺ A -> List⁺ A infixr 50 _::⁺_ module ChainR = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans) open ChainR foldr⁺ : {A B : Set} -> (A -> B -> B) -> (A -> B) -> List⁺ A -> B foldr⁺ f g [ a ]⁺ = g a foldr⁺ f g (a ::⁺ x) = f a (foldr⁺ f g x) map⁺ : {A B : Set} -> (A -> B) -> List⁺ A -> List⁺ B map⁺ f = foldr⁺ (\a x -> f a ::⁺ x) ([_]⁺ ∘ f) _++⁺_ : {A : Set} -> List⁺ A -> List⁺ A -> List⁺ A x ++⁺ y = foldr⁺ _::⁺_ (\a -> a ::⁺ y) x concat⁺ : {A : Set} -> List⁺ (List⁺ A) -> List⁺ A concat⁺ = foldr⁺ _++⁺_ id foldr⁺-fusion : {A B C : Set} -> (h : B -> C) -> {f : A -> B -> B} -> {g : A -> C -> C} -> {k : A -> B} -> {l : A -> C} -> ((a : A) -> (b : B) -> h (f a b) ≡ g a (h b)) -> ((a : A) -> h (k a) ≡ l a) -> ∀ (\x -> h (foldr⁺ f k x) ≡ foldr⁺ g l x) foldr⁺-fusion h {f} {g} {k} {l} _ q [ a ]⁺ = q a foldr⁺-fusion h {f} {g} {k} {l} p q (a ::⁺ x) = chain> h (foldr⁺ f k (a ::⁺ x)) === h (f a (foldr⁺ f k x)) by refl === g a (h (foldr⁺ f k x)) by p a (foldr⁺ f k x) === g a (foldr⁺ g l x) by cong (g a) (foldr⁺-fusion h p q x) === foldr⁺ g l (a ::⁺ x) by refl foldr⁺-fusion' : {A B C : Set} -> (h : B -> C) -> {f : A -> B -> B} -> {g : A -> C -> C} -> {k : A -> B} -> ((a : A) -> (b : B) -> h (f a b) ≡ g a (h b)) -> ∀ (\x -> h (foldr⁺ f k x) ≡ foldr⁺ g (h ∘ k) x) foldr⁺-fusion' h {f} {g} {k} p x = foldr⁺-fusion h {f} {g} {k} {h ∘ k} p (\_ -> refl) x idIsFold⁺ : {A : Set} -> (x : List⁺ A) -> (x ≡ foldr⁺ _::⁺_ [_]⁺ x) idIsFold⁺ {_} [ a ]⁺ = refl idIsFold⁺ {_} (a ::⁺ x) = chain> (a ::⁺ x) === a ::⁺ foldr⁺ _::⁺_ [_]⁺ x by cong (_::⁺_ a) (idIsFold⁺ x) === foldr⁺ _::⁺_ [_]⁺ (a ::⁺ x) by refl 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) ([_]⁺ ∘ g ∘ f) x by foldr⁺-fusion' (map⁺ (g ∘ f)) (\_ _ -> refl) x === (map⁺ g ∘ foldr⁺ (\a y -> f a ::⁺ y) ([_]⁺ ∘ f)) x by sym (foldr⁺-fusion' (map⁺ g) (\_ _ -> refl) x) === (map⁺ g ∘ map⁺ f) x by refl 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⁺ _::⁺_ (\a -> a ::⁺ y) x) by refl === foldr⁺ (\a z -> f a ::⁺ z) (\a -> f a ::⁺ map⁺ f y) x by foldr⁺-fusion' (map⁺ f) (\_ _ -> refl) x === foldr⁺ (\a z -> f a ::⁺ z) ([_]⁺ ∘ f) x ++⁺ (map⁺ f y) by sym (foldr⁺-fusion' (\z -> z ++⁺ map⁺ f y) (\_ _ -> refl) x) === map⁺ f x ++⁺ map⁺ f y by refl 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) ([_]⁺ ∘ map⁺ f) xs) by refl === foldr⁺ (\x xs -> map⁺ f x ++⁺ xs) (map⁺ f) xs by foldr⁺-fusion' concat⁺ (\_ _ -> refl) xs === map⁺ f (concat⁺ xs) by sym (foldr⁺-fusion' (map⁺ f) (\z w -> map⁺-cat⁺ z) xs) foldr⁺-eq : {A B : Set} -> {f g : A -> B -> B} -> {h k : A -> B} -> (forall a -> forall b -> f a b ≡ g a b) -> (forall a -> h a ≡ k a) -> forall x -> foldr⁺ f h x ≡ foldr⁺ g k x foldr⁺-eq {A} {B} {f} {g} {h} {k} f≡g h≡k x = chain> foldr⁺ f h x === foldr⁺ f h (foldr⁺ _::⁺_ [_]⁺ x) by cong (foldr⁺ f h) (idIsFold⁺ x) === foldr⁺ g k x by foldr⁺-fusion (foldr⁺ f h) (\a x -> f≡g a (foldr⁺ f h x)) h≡k 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) ([_]⁺ ∘ f) x by refl === foldr⁺ (\a y -> g a ::⁺ y) ([_]⁺ ∘ g) x by foldr⁺-eq (\a y -> cong (\b -> b ::⁺ y) (f≡g a)) (\a -> cong [_]⁺ (f≡g a)) x === map⁺ g x by refl