## 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.Equivalitymodule Folding whereflip : forall {A B C} -> (A -> B -> C) -> B -> A -> Cflip f b a = f a binfix  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 yrefl ≡→ _ = refl-- rewrite on the left_lhs_ : forall {a}{x y k : a} -> x ≡ k -> x ≡ y -> y ≡ kE₁ lhs E₂ = ≡trans (≡symm E₂) E₁-- rewrite on the right_rhs_ : forall {a}{x y k : a} -> k ≡ x -> x ≡ y -> k ≡ yE₁ 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 ] -> bfoldr _ z []       = zfoldr f z (a ∷ as) = f a (foldr f z as)foldl : {a b : Set} -> (b -> a -> b) -> b -> [ a ] -> bfoldl _ z []       = zfoldl 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 ysfoldl^foldr : forall {a b} ->              (f : a -> b -> b) -> (z : b) -> (xs : [ a ]) ->   foldr f z (reverse xs) ≡ foldl (flip f) z xsfoldl^foldr f z []       = reflfoldl^foldr f z (x ∷ xs) = foldl^foldr f (f x z) xs                           lhs ≡symm (++foldr f z                                              (reverse xs)                                              (x ∷ []))`