Skip to content

Instantly share code, notes, and snippets.

@khibino

khibino/Monoid.agda

Created October 18, 2023 10:34
Show Gist options
  • Save khibino/e42d20d7302bb9605d3e036d91611a18 to your computer and use it in GitHub Desktop.
Save khibino/e42d20d7302bb9605d3e036d91611a18 to your computer and use it in GitHub Desktop.
Download ZIP
Monoid Sum
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment