← Back to branch summary

~ubuntu-branches/ubuntu/maverick/agda-stdlib/maverick

« back to all changes in this revision

Viewing changes to src/Algebra/Structures.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Structures.agda
 
1
------------------------------------------------------------------------
 
2
-- Some algebraic structures (not packed up with sets, operations,
 
3
-- etc.)
 
4
------------------------------------------------------------------------
 
5
 
 
6
open import Relation.Binary
 
7
 
 
8
module Algebra.Structures where
 
9
 
 
10
import Algebra.FunctionProperties as FunctionProperties
 
11
open FunctionProperties using (Op₁; Op₂)
 
12
import Relation.Binary.EqReasoning as EqR
 
13
open import Data.Function
 
14
open import Data.Product
 
15
import Level as L
 
16
 
 
17
------------------------------------------------------------------------
 
18
-- One binary operation
 
19
 
 
20
record IsSemigroup {A} (≈ : Rel A L.zero) (∙ : Op₂ A) : Set where
 
21
  open FunctionProperties ≈
 
22
  field
 
23
    isEquivalence : IsEquivalence ≈
 
24
    assoc         : Associative ∙
 
25
    ∙-cong        : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
 
26
 
 
27
  open IsEquivalence isEquivalence public
 
28
 
 
29
record IsMonoid {A} (≈ : Rel A L.zero) (∙ : Op₂ A) (ε : A) : Set where
 
30
  open FunctionProperties ≈
 
31
  field
 
32
    isSemigroup : IsSemigroup ≈ ∙
 
33
    identity    : Identity ε ∙
 
34
 
 
35
  open IsSemigroup isSemigroup public
 
36
 
 
37
record IsCommutativeMonoid {A} (≈ : Rel A L.zero)
 
38
                               (∙ : Op₂ A) (ε : A) : Set where
 
39
  open FunctionProperties ≈
 
40
  field
 
41
    isMonoid : IsMonoid ≈ ∙ ε
 
42
    comm     : Commutative ∙
 
43
 
 
44
  open IsMonoid isMonoid public
 
45
 
 
46
record IsGroup {A} (≈ : Rel A L.zero)
 
47
                   (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set where
 
48
  open FunctionProperties ≈
 
49
  infixl 7 _-_
 
50
  field
 
51
    isMonoid  : IsMonoid ≈ _∙_ ε
 
52
    inverse   : Inverse ε _⁻¹ _∙_
 
53
    ⁻¹-cong   : _⁻¹ Preserves ≈ ⟶ ≈
 
54
 
 
55
  open IsMonoid isMonoid public
 
56
 
 
57
  _-_ : Op₂ A
 
58
  x - y = x ∙ (y ⁻¹)
 
59
 
 
60
record IsAbelianGroup {A} (≈ : Rel A L.zero)
 
61
                          (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set where
 
62
  open FunctionProperties ≈
 
63
  field
 
64
    isGroup : IsGroup ≈ ∙ ε ⁻¹
 
65
    comm    : Commutative ∙
 
66
 
 
67
  open IsGroup isGroup public
 
68
 
 
69
  isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε
 
70
  isCommutativeMonoid = record
 
71
    { isMonoid = isMonoid
 
72
    ; comm     = comm
 
73
    }
 
74
 
 
75
------------------------------------------------------------------------
 
76
-- Two binary operations
 
77
 
 
78
record IsNearSemiring {A} (≈ : Rel A L.zero)
 
79
                          (+ * : Op₂ A) (0# : A) : Set where
 
80
  open FunctionProperties ≈
 
81
  field
 
82
    +-isMonoid    : IsMonoid ≈ + 0#
 
83
    *-isSemigroup : IsSemigroup ≈ *
 
84
    distribʳ      : * DistributesOverʳ +
 
85
    zeroˡ         : LeftZero 0# *
 
86
 
 
87
  open IsMonoid +-isMonoid public
 
88
         renaming ( assoc       to +-assoc
 
89
                  ; ∙-cong      to +-cong
 
90
                  ; isSemigroup to +-isSemigroup
 
91
                  ; identity    to +-identity
 
92
                  )
 
93
 
 
94
  open IsSemigroup *-isSemigroup public
 
95
         using ()
 
96
         renaming ( assoc    to *-assoc
 
97
                  ; ∙-cong   to *-cong
 
98
                  )
 
99
 
 
100
record IsSemiringWithoutOne {A} (≈ : Rel A L.zero)
 
101
                                (+ * : Op₂ A) (0# : A) : Set where
 
102
  open FunctionProperties ≈
 
103
  field
 
104
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
 
105
    *-isSemigroup         : IsSemigroup ≈ *
 
106
    distrib               : * DistributesOver +
 
107
    zero                  : Zero 0# *
 
108
 
 
109
  open IsCommutativeMonoid +-isCommutativeMonoid public
 
110
         renaming ( assoc       to +-assoc
 
111
                  ; ∙-cong      to +-cong
 
112
                  ; isSemigroup to +-isSemigroup
 
113
                  ; identity    to +-identity
 
114
                  ; isMonoid    to +-isMonoid
 
115
                  ; comm        to +-comm
 
116
                  )
 
117
 
 
118
  open IsSemigroup *-isSemigroup public
 
119
         using ()
 
120
         renaming ( assoc       to *-assoc
 
121
                  ; ∙-cong      to *-cong
 
122
                  )
 
123
 
 
124
  isNearSemiring : IsNearSemiring ≈ + * 0#
 
125
  isNearSemiring = record
 
126
    { +-isMonoid    = +-isMonoid
 
127
    ; *-isSemigroup = *-isSemigroup
 
128
    ; distribʳ      = proj₂ distrib
 
129
    ; zeroˡ         = proj₁ zero
 
130
    }
 
131
 
 
132
record IsSemiringWithoutAnnihilatingZero
 
133
         {A} (≈ : Rel A L.zero) (+ * : Op₂ A) (0# 1# : A) : Set where
 
134
  open FunctionProperties ≈
 
135
  field
 
136
    -- Note that these structures do have an additive unit, but this
 
137
    -- unit does not necessarily annihilate multiplication.
 
138
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
 
139
    *-isMonoid            : IsMonoid ≈ * 1#
 
140
    distrib               : * DistributesOver +
 
141
 
 
142
  open IsCommutativeMonoid +-isCommutativeMonoid public
 
143
         renaming ( assoc       to +-assoc
 
144
                  ; ∙-cong      to +-cong
 
145
                  ; isSemigroup to +-isSemigroup
 
146
                  ; identity    to +-identity
 
147
                  ; isMonoid    to +-isMonoid
 
148
                  ; comm        to +-comm
 
149
                  )
 
150
 
 
151
  open IsMonoid *-isMonoid public
 
152
         using ()
 
153
         renaming ( assoc       to *-assoc
 
154
                  ; ∙-cong      to *-cong
 
155
                  ; isSemigroup to *-isSemigroup
 
156
                  ; identity    to *-identity
 
157
                  )
 
158
 
 
159
record IsSemiring {A} (≈ : Rel A L.zero)
 
160
                      (+ * : Op₂ A) (0# 1# : A) : Set where
 
161
  open FunctionProperties ≈
 
162
  field
 
163
    isSemiringWithoutAnnihilatingZero :
 
164
      IsSemiringWithoutAnnihilatingZero ≈ + * 0# 1#
 
165
    zero : Zero 0# *
 
166
 
 
167
  open IsSemiringWithoutAnnihilatingZero
 
168
         isSemiringWithoutAnnihilatingZero public
 
169
 
 
170
  isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
 
171
  isSemiringWithoutOne = record
 
172
    { +-isCommutativeMonoid = +-isCommutativeMonoid
 
173
    ; *-isSemigroup         = *-isSemigroup
 
174
    ; distrib               = distrib
 
175
    ; zero                  = zero
 
176
    }
 
177
 
 
178
  open IsSemiringWithoutOne isSemiringWithoutOne public
 
179
         using (isNearSemiring)
 
180
 
 
181
record IsCommutativeSemiringWithoutOne
 
182
         {A} (≈ : Rel A L.zero) (+ * : Op₂ A) (0# : A) : Set where
 
183
  open FunctionProperties ≈
 
184
  field
 
185
    isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
 
186
    *-comm               : Commutative *
 
187
 
 
188
  open IsSemiringWithoutOne isSemiringWithoutOne public
 
189
 
 
190
record IsCommutativeSemiring
 
191
         {A} (≈ : Rel A L.zero) (+ * : Op₂ A) (0# 1# : A) : Set where
 
192
  open FunctionProperties ≈
 
193
  field
 
194
    isSemiring : IsSemiring ≈ + * 0# 1#
 
195
    *-comm     : Commutative *
 
196
 
 
197
  open IsSemiring isSemiring public
 
198
 
 
199
  *-isCommutativeMonoid : IsCommutativeMonoid ≈ * 1#
 
200
  *-isCommutativeMonoid = record
 
201
      { isMonoid = *-isMonoid
 
202
      ; comm     = *-comm
 
203
      }
 
204
 
 
205
  isCommutativeSemiringWithoutOne :
 
206
    IsCommutativeSemiringWithoutOne ≈ + * 0#
 
207
  isCommutativeSemiringWithoutOne = record
 
208
    { isSemiringWithoutOne = isSemiringWithoutOne
 
209
    ; *-comm               = *-comm
 
210
    }
 
211
 
 
212
record IsRing {A} (≈ : Rel A L.zero)
 
213
              (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set where
 
214
  open FunctionProperties ≈
 
215
  field
 
216
    +-isAbelianGroup : IsAbelianGroup ≈ _+_ 0# -_
 
217
    *-isMonoid       : IsMonoid ≈ _*_ 1#
 
218
    distrib          : _*_ DistributesOver _+_
 
219
 
 
220
  open IsAbelianGroup +-isAbelianGroup public
 
221
         renaming ( assoc               to +-assoc
 
222
                  ; ∙-cong              to +-cong
 
223
                  ; isSemigroup         to +-isSemigroup
 
224
                  ; identity            to +-identity
 
225
                  ; isMonoid            to +-isMonoid
 
226
                  ; inverse             to -‿inverse
 
227
                  ; ⁻¹-cong             to -‿cong
 
228
                  ; isGroup             to +-isGroup
 
229
                  ; comm                to +-comm
 
230
                  ; isCommutativeMonoid to +-isCommutativeMonoid
 
231
                  )
 
232
 
 
233
  open IsMonoid *-isMonoid public
 
234
         using ()
 
235
         renaming ( assoc       to *-assoc
 
236
                  ; ∙-cong      to *-cong
 
237
                  ; isSemigroup to *-isSemigroup
 
238
                  ; identity    to *-identity
 
239
                  )
 
240
 
 
241
  zero : Zero 0# _*_
 
242
  zero = (zeroˡ , zeroʳ)
 
243
    where
 
244
    open EqR (record { isEquivalence = isEquivalence })
 
245
 
 
246
    zeroˡ : LeftZero 0# _*_
 
247
    zeroˡ x = begin
 
248
        0# * x                              ≈⟨ sym $ proj₂ +-identity _ ⟩
 
249
       (0# * x) +            0#             ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
 
250
       (0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym $ +-assoc _ _ _ ⟩
 
251
      ((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
 
252
             ((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _ ⟨ *-cong ⟩ refl)
 
253
                                                 ⟨ +-cong ⟩
 
254
                                               refl ⟩
 
255
                    (0# * x) + - (0# * x)   ≈⟨ proj₂ -‿inverse _ ⟩
 
256
                             0#             ∎
 
257
 
 
258
    zeroʳ : RightZero 0# _*_
 
259
    zeroʳ x = begin
 
260
      x * 0#                              ≈⟨ sym $ proj₂ +-identity _ ⟩
 
261
      (x * 0#) + 0#                       ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
 
262
      (x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym $ +-assoc _ _ _ ⟩
 
263
      ((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
 
264
      (x * (0# + 0#)) + - (x * 0#)        ≈⟨ (refl ⟨ *-cong ⟩ proj₂ +-identity _)
 
265
                                               ⟨ +-cong ⟩
 
266
                                             refl ⟩
 
267
      (x * 0#) + - (x * 0#)               ≈⟨ proj₂ -‿inverse _ ⟩
 
268
      0#                                  ∎
 
269
 
 
270
  isSemiringWithoutAnnihilatingZero
 
271
    : IsSemiringWithoutAnnihilatingZero ≈ _+_ _*_ 0# 1#
 
272
  isSemiringWithoutAnnihilatingZero = record
 
273
    { +-isCommutativeMonoid = +-isCommutativeMonoid
 
274
    ; *-isMonoid            = *-isMonoid
 
275
    ; distrib               = distrib
 
276
    }
 
277
 
 
278
  isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
 
279
  isSemiring = record
 
280
    { isSemiringWithoutAnnihilatingZero =
 
281
        isSemiringWithoutAnnihilatingZero
 
282
    ; zero = zero
 
283
    }
 
284
 
 
285
  open IsSemiring isSemiring public
 
286
         using (isNearSemiring; isSemiringWithoutOne)
 
287
 
 
288
record IsCommutativeRing {A}
 
289
         (≈ : Rel A L.zero)
 
290
         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set where
 
291
  open FunctionProperties ≈
 
292
  field
 
293
    isRing : IsRing ≈ + * - 0# 1#
 
294
    *-comm : Commutative *
 
295
 
 
296
  open IsRing isRing public
 
297
 
 
298
  isCommutativeSemiring : IsCommutativeSemiring ≈ + * 0# 1#
 
299
  isCommutativeSemiring = record
 
300
    { isSemiring = isSemiring
 
301
    ; *-comm     = *-comm
 
302
    }
 
303
 
 
304
  open IsCommutativeSemiring isCommutativeSemiring public
 
305
         using (isCommutativeSemiringWithoutOne)
 
306
 
 
307
record IsLattice {A} (≈ : Rel A L.zero) (∨ ∧ : Op₂ A) : Set where
 
308
  open FunctionProperties ≈
 
309
  field
 
310
    isEquivalence : IsEquivalence ≈
 
311
    ∨-comm        : Commutative ∨
 
312
    ∨-assoc       : Associative ∨
 
313
    ∨-cong        : ∨ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
 
314
    ∧-comm        : Commutative ∧
 
315
    ∧-assoc       : Associative ∧
 
316
    ∧-cong        : ∧ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
 
317
    absorptive    : Absorptive ∨ ∧
 
318
 
 
319
  open IsEquivalence isEquivalence public
 
320
 
 
321
record IsDistributiveLattice {A} (≈ : Rel A L.zero)
 
322
                                 (∨ ∧ : Op₂ A) : Set where
 
323
  open FunctionProperties ≈
 
324
  field
 
325
    isLattice    : IsLattice ≈ ∨ ∧
 
326
    ∨-∧-distribʳ : ∨ DistributesOverʳ ∧
 
327
 
 
328
  open IsLattice isLattice public
 
329
 
 
330
record IsBooleanAlgebra {A}
 
331
         (≈ : Rel A L.zero)
 
332
         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set where
 
333
  open FunctionProperties ≈
 
334
  field
 
335
    isDistributiveLattice : IsDistributiveLattice ≈ ∨ ∧
 
336
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
 
337
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
 
338
    ¬-cong                : ¬ Preserves ≈ ⟶ ≈
 
339
 
 
340
  open IsDistributiveLattice isDistributiveLattice public