fold-fusion.agda

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- definition of List
data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

-- "fold", or "reduce" in python
fold : ∀ {A B : Set} → (A → B → B) → B → List A → B
fold f e []       = e
fold f e (x ∷ xs) = f x (fold f e xs)

-- The Fold-Fusion Theorem:
--  let      h (f x y) = g x (h y)
--  then     h · foldr f e = foldr g (h e)
fold-fusion : ∀ {A B C}
    → (f : A → B → B)
    → (g : A → C → C)
    → (h : B → C)
    → (∀ {x y} → h (f x y) ≡ g x (h y))
    → (e : B)
    → (xs : List A)
    → h (fold f e xs) ≡ fold g (h e) xs
fold-fusion f g h prf e []       = refl         -- base case
fold-fusion f g h prf e (x ∷ xs) =              -- inductive step
    begin
        h (fold f e (x ∷ xs))
    ≡⟨ refl ⟩   -- by definition of fold
        h (f x (fold f e xs))
    ≡⟨ prf ⟩    -- by prf
        g x (h (fold f e xs))
    ≡⟨ cong (g x) (fold-fusion f g h prf e xs) ⟩
        g x (fold g (h e) xs)
    ≡⟨ refl ⟩
        fold g (h e) (x ∷ xs)
    ∎