Monoid Sum

Monoid.agda

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

record Monoid (m : Set) : Set where
  infixl 6 _⊕_
  field
    _⊕_ : m → m → m

    associativity : ∀{a b c} → ((a ⊕ b) ⊕ c) ≡ (a ⊕ (b ⊕ c))

open Monoid {{...}}

data NList (m : Set) : Set where
  Sing : m → NList m
  Cons : m → NList m → NList m

infixr 5 _++_
_++_ : ∀ {m} → NList m → NList m → NList m
Sing x ++ ys = Cons x ys
Cons x xs ++ ys = Cons x (xs ++ ys)

data Bin (m : Set) : Set where
  Leaf : m → Bin m
  Plus : Bin m → Bin m → Bin m

bin2nlist : ∀ {m} → Bin m → NList m
bin2nlist (Leaf m) = Sing m
bin2nlist (Plus b₁ b₂) = bin2nlist b₁ ++ bin2nlist b₂

sumNList : ∀ {m}{{M : Monoid m}} → NList m → m
sumNList {_} (Sing m) = m
sumNList {m} (Cons x xs) = x ⊕ sumNList xs

sumBin : ∀ {m}{{M : Monoid m}} → Bin m → m
sumBin (Leaf m) = m
sumBin (Plus b₁ b₂) = sumBin b₁ ⊕ sumBin b₂

sum-dist : ∀{m} {{M : Monoid m}} → (xs ys : NList m) → sumNList (xs ++ ys) ≡ sumNList xs ⊕ sumNList ys
sum-dist {_} (Sing x) ys = refl
sum-dist {m} (Cons x xs) ys rewrite associativity {m} {x} {sumNList xs} {sumNList ys} =
  cong (_⊕_ x) (sum-dist xs ys)

sum-universal : ∀{m} {{M : Monoid m}} → (b : Bin m) → sumNList (bin2nlist b) ≡ sumBin b
sum-universal {m} (Leaf x) = refl
sum-universal {m} (Plus b₁ b₂)
  rewrite sum-dist (bin2nlist b₁) (bin2nlist b₂)
  rewrite sum-universal b₁
  rewrite sum-universal b₂  = refl