blob: 99501d6b300df3b2bfb743dc9b6ca04739a6540a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
{-# OPTIONS --without-K --safe #-}
{-# OPTIONS --hidden-argument-puns #-}
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 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 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 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)
open Func
private
variable
a c ℓ : Level
A B : Set a
Aₛ Bₛ : Setoid c ℓ
opaque
Multiset : Set a → Set a
Multiset = L.List
[] : Multiset A
[] = L.[]
_∷_ : A → Multiset A → Multiset A
_∷_ = L._∷_
map : (A → B) → Multiset A → Multiset B
map = L.map
_++_ : Multiset A → Multiset A → Multiset A
_++_ = L._++_
Multisetₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ)
Multisetₛ = ↭-setoid
[]ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Multisetₛ {c} {ℓ} Aₛ
[]ₛ {Aₛ} = Const ⊤ₛ (Multisetₛ Aₛ) []
∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ
∷ₛ .to = uncurry′ _∷_
∷ₛ .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)
mapₛ {Aₛ} {Bₛ} f .cong xs≈ys = map⁺ Aₛ Bₛ (cong f) xs≈ys
++ₛ : Multisetₛ Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ
++ₛ .to = uncurry′ _++_
++ₛ {Aₛ} .cong = uncurry′ (++⁺ Aₛ)
++ₛ-comm
: (open Setoid (Multisetₛ Aₛ))
→ (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
|
