$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/11/02

### 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

Labels: ,