Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment