Fold-Fusion Strikes Back

Since I'm determined not to touch Agda after I get up in order to prepare for the midterms, I'm currently reluctant to fall asleep XD. Below I proved some simple facts about fold in Agda, but I haven't written any practical examples yet.

First we define function composition. The operator precedence "30" is arbitrarily chosen, which luckily seems to work.

infixl 30 _○_

_○_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
(f ○ g) x = f (g x)

Now we prove the Fold-Fusion Theorem. (By chain reasoning, of course. XD)

foldr-fusion : {α β γ : Set} ->
                 {f : α -> β -> β} {e : β} {h : β -> γ} {g : α -> γ -> γ}->
                 ((x : α)(y : β) -> h (f x y) ≡ g x (h y)) ->
                 ∀ (\xs -> (h ○ (foldr f e)) xs ≡ foldr g (h e) xs)
foldr-fusion _ [] = refl
foldr-fusion {_}{_}{_} {f}{e}{h}{g} fuse (x :: xs) =
  chain> (h ○ foldr f e) (x :: xs)
     === h (foldr f e (x :: xs)) by refl
     === h (f x (foldr f e xs)) by cong h refl
     === g x (h (foldr f e xs)) by fuse x (foldr f e xs)
     === g x ((h ○ foldr f e) xs) by cong (g x) refl
     === g x (foldr g (h e) xs) by cong (g x) (foldr-fusion fuse xs)
     === foldr g (h e) (x :: xs) by refl

This is the first time I formally prove the Fold-Fusion Theorem. XD

Define the identity fold and prove that it is indeed an identity.

id-foldr : {A : Set} -> List A -> List A
id-foldr = foldr _::_ []

id-foldr-id : {A : Set}{xs : List A} -> id-foldr xs ≡ xs
id-foldr-id {_}{[]} = refl
id-foldr-id {_}{x :: xs} =
  chain> id-foldr (x :: xs)
     === foldr _::_ [] (x :: xs) by refl
     === x :: foldr _::_ [] xs by refl
     === x :: xs by cong (_::_ x) id-foldr-id

Then we prove that for any function f, f is the same as f ○ id-foldr.

compose-id : {A B : Set}(f : List A -> B)(xs : List A) ->
               f xs ≡ (f ○ id-foldr) xs
compose-id f xs =
  chain> f xs
     === f (id-foldr xs) by cong f (sym id-foldr-id)
     === (f ○ id-foldr) xs by refl

Finally we prove that map f is a fold by Fold-Fusion Theorem: first add an id-foldr to the right of map f and then apply fold-fusion.

map-as-foldr : {A B : Set}{f : A -> B}{xs : List A} ->
                map f xs ≡ foldr (\y ys -> f y :: ys) [] xs
map-as-foldr {A}{_}{f}{xs} =
  chain> map f xs
     === (map f ○ id-foldr) xs by compose-id (map f) xs
     === foldr (\y ys -> f y :: ys) [] xs by foldr-fusion fuse-cond xs
  where
    fuse-cond : (x : A)(xs : List A) ->
                  (map f) (x :: xs) ≡ (\y ys -> f y :: ys) x (map f xs)
    fuse-cond x xs = refl

--
Chain reasoning is marvelous! XD