diff options
Diffstat (limited to 'Data/Opaque')
| -rw-r--r-- | Data/Opaque/Multiset.agda | 74 |
1 files changed, 69 insertions, 5 deletions
diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda index 2ba0a0e..99501d6 100644 --- a/Data/Opaque/Multiset.agda +++ b/Data/Opaque/Multiset.agda @@ -4,14 +4,20 @@ module Data.Opaque.Multiset where import Data.List as L +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Data.Opaque.List as List -open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; prep) +open import Algebra.Bundles using (CommutativeMonoid) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) +open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; ↭-refl) open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺; ++⁺; ++-comm) -open import Data.Product using (_,_) -open import Data.Product using (uncurry′) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.Product using (_,_; uncurry′) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) open import Data.Setoid.Unit using (⊤ₛ) -open import Function using (_⟶ₛ_; Func; _⟨$⟩_) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) open import Function.Construct.Constant using () renaming (function to Const) open import Level using (Level; _⊔_) open import Relation.Binary using (Setoid) @@ -50,7 +56,11 @@ opaque ∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ ∷ₛ .to = uncurry′ _∷_ - ∷ₛ .cong = uncurry′ prep + ∷ₛ .cong = uncurry′ ↭.prep + + [-]ₛ : Aₛ ⟶ₛ Multisetₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ {Aₛ} .cong y = ↭.prep y (↭-refl Aₛ) mapₛ : (Aₛ ⟶ₛ Bₛ) → Multisetₛ Aₛ ⟶ₛ Multisetₛ Bₛ mapₛ f .to = map (to f) @@ -65,3 +75,57 @@ opaque → (xs ys : Carrier) → ++ₛ ⟨$⟩ (xs , ys) ≈ ++ₛ ⟨$⟩ (ys , xs) ++ₛ-comm {Aₛ} xs ys = ++-comm Aₛ xs ys + +module _ (M : CommutativeMonoid c ℓ) where + + open CommutativeMonoid M renaming (setoid to Mₛ) + + opaque + unfolding Multiset List.fold-cong + fold : ∣ Multisetₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = List.fold monoid -- RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Multisetₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Multisetₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong (↭.refl x) = cong (List.foldₛ monoid) x + fold-cong (↭.prep x≈y xs↭ys) = ∙-cong x≈y (fold-cong xs↭ys) + fold-cong + {x₀ L.∷ x₁ L.∷ xs} + {y₀ L.∷ y₁ L.∷ ys} + (↭.swap x₀≈y₁ x₁≈y₀ xs↭ys) = trans + (sym (assoc x₀ x₁ (fold xs))) (trans + (∙-cong (trans (∙-cong x₀≈y₁ x₁≈y₀) (comm y₁ y₀)) (fold-cong xs↭ys)) + (assoc y₀ y₁ (fold ys))) + fold-cong {xs} {ys} (↭.trans xs↭zs zs↭ys) = trans (fold-cong xs↭zs) (fold-cong zs↭ys) + + foldₛ : Multisetₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Multisetₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo monoid id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : CommutativeMonoid c ℓ) where + + module M = CommutativeMonoid M + module N = CommutativeMonoid N + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Multisetₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ = List.fold-mapₛ M.monoid N.monoid |