Thursday 14 February 2008

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 []))