blob: 545a8351fc5d88cf5dba63ca4e6a43147c6702d3 (
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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
{-# OPTIONS --without-K --safe #-}
open import Algebra.Bundles using (CommutativeMonoid)
open import Level using (0ℓ)
module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
import Algebra.Properties.CommutativeMonoid.Sum as Sum
import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise
import Relation.Binary.PropositionalEquality as ≡
open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt)
open import Data.Nat using (ℕ; _+_; suc)
open import Data.Product using (_,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Setoid using (∣_∣)
open import Data.Sum using (inj₁; inj₂)
open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel; Setoid; IsEquivalence)
open CommutativeMonoid A renaming (Carrier to Value)
open Func
open Sum A using (sum)
open Pointwise setoid using (≋-setoid; ≋-isEquivalence)
opaque
Values : ℕ → Setoid 0ℓ 0ℓ
Values = ≋-setoid
module _ {n : ℕ} where
opaque
unfolding Values
merge : ∣ Values n ∣ → Value
merge = sum
_⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣
xs ⊕ ys = zipWith _∙_ xs ys
<ε> : ∣ Values n ∣
<ε> = replicate n ε
head : ∣ Values (suc n) ∣ → Value
head xs = xs zero
tail : ∣ Values (suc n) ∣ → ∣ Values n ∣
tail xs = xs ∘ suc
module ≋ = Setoid (Values n)
_≋_ : Rel ∣ Values n ∣ 0ℓ
_≋_ = ≋._≈_
infix 4 _≋_
opaque
unfolding Values
open Setoid
≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n))
≋-isEquiv = ≋-isEquivalence
module _ {n : ℕ} where
opaque
unfolding _⊕_
⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v
⊕-cong x≋y u≋v i = ∙-cong (x≋y i) (u≋v i)
⊕-assoc : (x y z : ≋.Carrier {n}) → (x ⊕ y) ⊕ z ≋ x ⊕ (y ⊕ z)
⊕-assoc x y z i = assoc (x i) (y i) (z i)
⊕-identityˡ : (x : ≋.Carrier {n}) → <ε> ⊕ x ≋ x
⊕-identityˡ x i = identityˡ (x i)
⊕-identityʳ : (x : ≋.Carrier {n}) → x ⊕ <ε> ≋ x
⊕-identityʳ x i = identityʳ (x i)
⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x
⊕-comm x y i = comm (x i) (y i)
open CommutativeMonoid
Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ
Valuesₘ n .Carrier = ∣ Values n ∣
Valuesₘ n ._≈_ = _≋_
Valuesₘ n ._∙_ = _⊕_
Valuesₘ n .ε = <ε>
Valuesₘ n .isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = ≋-isEquiv n
; ∙-cong = ⊕-cong
}
; assoc = ⊕-assoc
}
; identity = ⊕-identityˡ , ⊕-identityʳ
}
; comm = ⊕-comm
}
opaque
unfolding Values
[] : ∣ Values 0 ∣
[] = Vec.[]
[]-unique : (xs ys : ∣ Values 0 ∣) → xs ≋ ys
[]-unique xs ys ()
module _ {n m : ℕ} where
opaque
unfolding Values
_++_ : ∣ Values n ∣ → ∣ Values m ∣ → ∣ Values (n + m) ∣
_++_ = Vec._++_
infixr 5 _++_
++-cong
: (xs xs′ : ∣ Values n ∣)
{ys ys′ : ∣ Values m ∣}
→ xs ≋ xs′
→ ys ≋ ys′
→ xs ++ ys ≋ xs′ ++ ys′
++-cong xs xs′ xs≋xs′ ys≋ys′ i with splitAt n i
... | inj₁ i = xs≋xs′ i
... | inj₂ i = ys≋ys′ i
splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m
to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_)
cong splitₛ v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_)
++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m)
to ++ₛ (xs , ys) = xs ++ ys
cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
|
