blob: 2ba0a0ec3e74a71654b300b7ea72e4edb4a3206c (
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
|
{-# OPTIONS --without-K --safe #-}
{-# OPTIONS --hidden-argument-puns #-}
module Data.Opaque.Multiset where
import Data.List as L
open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; prep)
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 Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Setoid.Unit using (⊤ₛ)
open import Function using (_⟶ₛ_; Func; _⟨$⟩_)
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
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
|
