Proof of the foldl, foldr relation

-- This is a self contained development of the proof that
--  foldr f z (reverse xs) ≡ foldl (flip f) z xs

-- I use some definitions from
-- http://code.haskell.org/~dolio/agda-play/
-- Particularly Data.List and Relation.Equivality

module Folding where

flip : forall {A B C} -> (A -> B -> C) -> B -> A -> C
flip f b a = f a b


infix  20 _≡_
infixr 30 _≡→_
infixr 25 _lhs_ _rhs_

data _≡_ {a : Set} : a -> a -> Set where
  refl : forall {x} -> x ≡ x

≡sub : forall {a}{P : a -> Set}{x y : a} -> x ≡ y -> P x -> P y
≡sub refl Px = Px

≡symm : forall {a}{x y : a} -> x ≡ y -> y ≡ x
≡symm refl = refl

≡trans : forall {a}{x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
≡trans refl refl = refl

-- take and equation and apply a function to both sides
_≡→_ : forall {a b}{x y : a} -> x ≡ y -> (f : a -> b) -> f x ≡ f y
refl ≡→ _ = refl

-- rewrite on the left
_lhs_ : forall {a}{x y k : a} -> x ≡ k -> x ≡ y -> y ≡ k
E₁ lhs E₂ = ≡trans (≡symm E₂) E₁

-- rewrite on the right
_rhs_ : forall {a}{x y k : a} -> k ≡ x -> x ≡ y -> k ≡ y
E₁ rhs E₂ = ≡symm (≡symm E₁ lhs E₂)


infixr 50 _∷_ 
infixr 40 _++_

data [_] (a : Set) : Set where
  [] : [ a ]
  _∷_ : a -> [ a ] -> [ a ]


foldr : {a b : Set} -> (a -> b -> b) -> b -> [ a ] -> b
foldr _ z []       = z
foldr f z (a ∷ as) = f a (foldr f z as)

foldl : {a b : Set} -> (b -> a -> b) -> b -> [ a ] -> b
foldl _ z []       = z
foldl f z (a ∷ as) = foldl f (f z a) as

_++_ : forall {a} -> [ a ] -> [ a ] -> [ a ]
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

reverse : {A : Set} -> [ A ] -> [ A ]
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ (x ∷ [])


-- Some theorems about ++

-- [] is the right unit
++unit : forall {a} -> (x : [ a ]) -> x ++ [] ≡ x
++unit []       = refl
++unit (x ∷ xs) = ++unit xs ≡→ \s -> x ∷ s

-- Associative
++assoc : forall {a} -> (a b c : [ a ]) ->
   (a ++ b) ++ c ≡ a ++ (b ++ c)
++assoc {_} []       _ _ = refl
++assoc {_} (x ∷ xs) _ _ = ++assoc xs _ _ ≡→ \s -> x ∷ s

++reverse : forall {a} (x y : [ a ]) ->
   reverse y ++ reverse x ≡ reverse (x ++ y)
++reverse [] ys       = ++unit (reverse ys)
++reverse (x ∷ xs) ys = ++reverse xs ys
                        ≡→ (\s -> s ++ reverse (x ∷ []))
                        lhs ++assoc (reverse ys) _ _

++foldr : forall {a b} ->
          (f : a -> b -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldr f z (xs ++ ys) ≡ foldr f (foldr f z ys) xs
++foldr f z []       ys = refl
++foldr f z (x ∷ xs) ys = ++foldr f z xs ys ≡→ f x

-- This identity is not actually used but I leave it in for
-- the sake of completeness
++foldl : forall {a b} ->
          (f : b -> a -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldl f z (xs ++ ys) ≡ foldl f (foldl f z xs) ys
++foldl f z []       ys = refl
++foldl f z (x ∷ xs) ys = ++foldl f (f z x) xs ys


foldl^foldr : forall {a b} ->
              (f : a -> b -> b) -> (z : b) -> (xs : [ a ]) ->
   foldr f z (reverse xs) ≡ foldl (flip f) z xs
foldl^foldr f z []       = refl
foldl^foldr f z (x ∷ xs) = foldl^foldr f (f x z) xs
                           lhs ≡symm (++foldr f z
                                              (reverse xs)
                                              (x ∷ []))