← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Algebra.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra.agda
3
3
-- (packed in records together with sets, operations, etc.)
4
4
------------------------------------------------------------------------
5
5
 
 
6
{-# OPTIONS --universe-polymorphism #-}
 
7
 
6
8
module Algebra where
7
9
 
8
10
open import Relation.Binary
9
11
open import Algebra.FunctionProperties
10
12
open import Algebra.Structures
11
 
open import Data.Function
 
13
open import Function
12
14
open import Level
13
15
 
14
16
------------------------------------------------------------------------
15
17
-- Semigroups, (commutative) monoids and (abelian) groups
16
18
 
17
 
record Semigroup : Set₁ where
 
19
record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
18
20
  infixl 7 _∙_
19
21
  infix  4 _≈_
20
22
  field
21
 
    Carrier     : Set
22
 
    _≈_         : Rel Carrier zero
 
23
    Carrier     : Set c
 
24
    _≈_         : Rel Carrier ℓ
23
25
    _∙_         : Op₂ Carrier
24
26
    isSemigroup : IsSemigroup _≈_ _∙_
25
27
 
30
32
 
31
33
-- A raw monoid is a monoid without any laws.
32
34
 
33
 
record RawMonoid : Set₁ where
 
35
record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
34
36
  infixl 7 _∙_
35
37
  infix  4 _≈_
36
38
  field
37
 
    Carrier : Set
38
 
    _≈_     : Rel Carrier zero
 
39
    Carrier : Set c
 
40
    _≈_     : Rel Carrier ℓ
39
41
    _∙_     : Op₂ Carrier
40
42
    ε       : Carrier
41
43
 
42
 
record Monoid : Set₁ where
 
44
record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
43
45
  infixl 7 _∙_
44
46
  infix  4 _≈_
45
47
  field
46
 
    Carrier  : Set
47
 
    _≈_      : Rel Carrier zero
 
48
    Carrier  : Set c
 
49
    _≈_      : Rel Carrier ℓ
48
50
    _∙_      : Op₂ Carrier
49
51
    ε        : Carrier
50
52
    isMonoid : IsMonoid _≈_ _∙_ ε
51
53
 
52
54
  open IsMonoid isMonoid public
53
55
 
54
 
  semigroup : Semigroup
 
56
  semigroup : Semigroup _ _
55
57
  semigroup = record { isSemigroup = isSemigroup }
56
58
 
57
59
  open Semigroup semigroup public using (setoid)
58
60
 
59
 
  rawMonoid : RawMonoid
 
61
  rawMonoid : RawMonoid _ _
60
62
  rawMonoid = record
61
63
    { _≈_ = _≈_
62
64
    ; _∙_ = _∙_
63
65
    ; ε   = ε
64
66
    }
65
67
 
66
 
record CommutativeMonoid : Set₁ where
 
68
record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
67
69
  infixl 7 _∙_
68
70
  infix  4 _≈_
69
71
  field
70
 
    Carrier             : Set
71
 
    _≈_                 : Rel Carrier zero
 
72
    Carrier             : Set c
 
73
    _≈_                 : Rel Carrier ℓ
72
74
    _∙_                 : Op₂ Carrier
73
75
    ε                   : Carrier
74
76
    isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
75
77
 
76
78
  open IsCommutativeMonoid isCommutativeMonoid public
77
79
 
78
 
  monoid : Monoid
 
80
  monoid : Monoid _ _
79
81
  monoid = record { isMonoid = isMonoid }
80
82
 
81
83
  open Monoid monoid public using (setoid; semigroup; rawMonoid)
82
84
 
83
 
record Group : Set₁ where
 
85
record Group c ℓ : Set (suc (c ⊔ ℓ)) where
84
86
  infix  8 _⁻¹
85
87
  infixl 7 _∙_
86
88
  infix  4 _≈_
87
89
  field
88
 
    Carrier : Set
89
 
    _≈_     : Rel Carrier zero
 
90
    Carrier : Set c
 
91
    _≈_     : Rel Carrier ℓ
90
92
    _∙_     : Op₂ Carrier
91
93
    ε       : Carrier
92
94
    _⁻¹     : Op₁ Carrier
94
96
 
95
97
  open IsGroup isGroup public
96
98
 
97
 
  monoid : Monoid
 
99
  monoid : Monoid _ _
98
100
  monoid = record { isMonoid = isMonoid }
99
101
 
100
102
  open Monoid monoid public using (setoid; semigroup; rawMonoid)
101
103
 
102
 
record AbelianGroup : Set₁ where
 
104
record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
103
105
  infix  8 _⁻¹
104
106
  infixl 7 _∙_
105
107
  infix  4 _≈_
106
108
  field
107
 
    Carrier        : Set
108
 
    _≈_            : Rel Carrier zero
 
109
    Carrier        : Set c
 
110
    _≈_            : Rel Carrier ℓ
109
111
    _∙_            : Op₂ Carrier
110
112
    ε              : Carrier
111
113
    _⁻¹            : Op₁ Carrier
113
115
 
114
116
  open IsAbelianGroup isAbelianGroup public
115
117
 
116
 
  group : Group
 
118
  group : Group _ _
117
119
  group = record { isGroup = isGroup }
118
120
 
119
121
  open Group group public using (setoid; semigroup; monoid; rawMonoid)
120
122
 
121
 
  commutativeMonoid : CommutativeMonoid
 
123
  commutativeMonoid : CommutativeMonoid _ _
122
124
  commutativeMonoid =
123
125
    record { isCommutativeMonoid = isCommutativeMonoid }
124
126
 
125
127
------------------------------------------------------------------------
126
128
-- Various kinds of semirings
127
129
 
128
 
record NearSemiring : Set₁ where
 
130
record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
129
131
  infixl 7 _*_
130
132
  infixl 6 _+_
131
133
  infix  4 _≈_
132
134
  field
133
 
    Carrier        : Set
134
 
    _≈_            : Rel Carrier zero
 
135
    Carrier        : Set c
 
136
    _≈_            : Rel Carrier ℓ
135
137
    _+_            : Op₂ Carrier
136
138
    _*_            : Op₂ Carrier
137
139
    0#             : Carrier
139
141
 
140
142
  open IsNearSemiring isNearSemiring public
141
143
 
142
 
  +-monoid : Monoid
 
144
  +-monoid : Monoid _ _
143
145
  +-monoid = record { isMonoid = +-isMonoid }
144
146
 
145
147
  open Monoid +-monoid public
147
149
         renaming ( semigroup to +-semigroup
148
150
                  ; rawMonoid to +-rawMonoid)
149
151
 
150
 
  *-semigroup : Semigroup
 
152
  *-semigroup : Semigroup _ _
151
153
  *-semigroup = record { isSemigroup = *-isSemigroup }
152
154
 
153
 
record SemiringWithoutOne : Set₁ where
 
155
record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
154
156
  infixl 7 _*_
155
157
  infixl 6 _+_
156
158
  infix  4 _≈_
157
159
  field
158
 
    Carrier              : Set
159
 
    _≈_                  : Rel Carrier zero
 
160
    Carrier              : Set c
 
161
    _≈_                  : Rel Carrier ℓ
160
162
    _+_                  : Op₂ Carrier
161
163
    _*_                  : Op₂ Carrier
162
164
    0#                   : Carrier
164
166
 
165
167
  open IsSemiringWithoutOne isSemiringWithoutOne public
166
168
 
167
 
  nearSemiring : NearSemiring
 
169
  nearSemiring : NearSemiring _ _
168
170
  nearSemiring = record { isNearSemiring = isNearSemiring }
169
171
 
170
172
  open NearSemiring nearSemiring public
173
175
               ; *-semigroup
174
176
               )
175
177
 
176
 
  +-commutativeMonoid : CommutativeMonoid
 
178
  +-commutativeMonoid : CommutativeMonoid _ _
177
179
  +-commutativeMonoid =
178
180
    record { isCommutativeMonoid = +-isCommutativeMonoid }
179
181
 
180
 
record SemiringWithoutAnnihilatingZero : Set₁ where
 
182
record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
181
183
  infixl 7 _*_
182
184
  infixl 6 _+_
183
185
  infix  4 _≈_
184
186
  field
185
 
    Carrier                           : Set
186
 
    _≈_                               : Rel Carrier zero
 
187
    Carrier                           : Set c
 
188
    _≈_                               : Rel Carrier ℓ
187
189
    _+_                               : Op₂ Carrier
188
190
    _*_                               : Op₂ Carrier
189
191
    0#                                : Carrier
194
196
  open IsSemiringWithoutAnnihilatingZero
195
197
         isSemiringWithoutAnnihilatingZero public
196
198
 
197
 
  +-commutativeMonoid : CommutativeMonoid
 
199
  +-commutativeMonoid : CommutativeMonoid _ _
198
200
  +-commutativeMonoid =
199
201
    record { isCommutativeMonoid = +-isCommutativeMonoid }
200
202
 
205
207
                  ; monoid    to +-monoid
206
208
                  )
207
209
 
208
 
  *-monoid : Monoid
 
210
  *-monoid : Monoid _ _
209
211
  *-monoid = record { isMonoid = *-isMonoid }
210
212
 
211
213
  open Monoid *-monoid public
214
216
                  ; rawMonoid to *-rawMonoid
215
217
                  )
216
218
 
217
 
record Semiring : Set₁ where
 
219
record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
218
220
  infixl 7 _*_
219
221
  infixl 6 _+_
220
222
  infix  4 _≈_
221
223
  field
222
 
    Carrier    : Set
223
 
    _≈_        : Rel Carrier zero
 
224
    Carrier    : Set c
 
225
    _≈_        : Rel Carrier ℓ
224
226
    _+_        : Op₂ Carrier
225
227
    _*_        : Op₂ Carrier
226
228
    0#         : Carrier
229
231
 
230
232
  open IsSemiring isSemiring public
231
233
 
232
 
  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero
 
234
  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
233
235
  semiringWithoutAnnihilatingZero = record
234
236
    { isSemiringWithoutAnnihilatingZero =
235
237
        isSemiringWithoutAnnihilatingZero
243
245
               ; *-semigroup; *-rawMonoid; *-monoid
244
246
               )
245
247
 
246
 
  semiringWithoutOne : SemiringWithoutOne
 
248
  semiringWithoutOne : SemiringWithoutOne _ _
247
249
  semiringWithoutOne =
248
250
    record { isSemiringWithoutOne = isSemiringWithoutOne }
249
251
 
250
252
  open SemiringWithoutOne semiringWithoutOne public
251
253
         using (nearSemiring)
252
254
 
253
 
record CommutativeSemiringWithoutOne : Set₁ where
 
255
record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
254
256
  infixl 7 _*_
255
257
  infixl 6 _+_
256
258
  infix  4 _≈_
257
259
  field
258
 
    Carrier                         : Set
259
 
    _≈_                             : Rel Carrier zero
 
260
    Carrier                         : Set c
 
261
    _≈_                             : Rel Carrier ℓ
260
262
    _+_                             : Op₂ Carrier
261
263
    _*_                             : Op₂ Carrier
262
264
    0#                              : Carrier
266
268
  open IsCommutativeSemiringWithoutOne
267
269
         isCommutativeSemiringWithoutOne public
268
270
 
269
 
  semiringWithoutOne : SemiringWithoutOne
 
271
  semiringWithoutOne : SemiringWithoutOne _ _
270
272
  semiringWithoutOne =
271
273
    record { isSemiringWithoutOne = isSemiringWithoutOne }
272
274
 
278
280
               ; nearSemiring
279
281
               )
280
282
 
281
 
record CommutativeSemiring : Set₁ where
 
283
record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
282
284
  infixl 7 _*_
283
285
  infixl 6 _+_
284
286
  infix  4 _≈_
285
287
  field
286
 
    Carrier               : Set
287
 
    _≈_                   : Rel Carrier zero
 
288
    Carrier               : Set c
 
289
    _≈_                   : Rel Carrier ℓ
288
290
    _+_                   : Op₂ Carrier
289
291
    _*_                   : Op₂ Carrier
290
292
    0#                    : Carrier
293
295
 
294
296
  open IsCommutativeSemiring isCommutativeSemiring public
295
297
 
296
 
  semiring : Semiring
 
298
  semiring : Semiring _ _
297
299
  semiring = record { isSemiring = isSemiring }
298
300
 
299
301
  open Semiring semiring public
305
307
               ; semiringWithoutAnnihilatingZero
306
308
               )
307
309
 
308
 
  *-commutativeMonoid : CommutativeMonoid
 
310
  *-commutativeMonoid : CommutativeMonoid _ _
309
311
  *-commutativeMonoid =
310
312
    record { isCommutativeMonoid = *-isCommutativeMonoid }
311
313
 
312
 
  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne
 
314
  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
313
315
  commutativeSemiringWithoutOne = record
314
316
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
315
317
    }
319
321
 
320
322
-- A raw ring is a ring without any laws.
321
323
 
322
 
record RawRing : Set₁ where
 
324
record RawRing c : Set (suc c) where
323
325
  infix  8 -_
324
326
  infixl 7 _*_
325
327
  infixl 6 _+_
326
328
  field
327
 
    Carrier : Set
 
329
    Carrier : Set c
328
330
    _+_     : Op₂ Carrier
329
331
    _*_     : Op₂ Carrier
330
332
    -_      : Op₁ Carrier
331
333
    0#      : Carrier
332
334
    1#      : Carrier
333
335
 
334
 
record Ring : Set₁ where
 
336
record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
335
337
  infix  8 -_
336
338
  infixl 7 _*_
337
339
  infixl 6 _+_
338
340
  infix  4 _≈_
339
341
  field
340
 
    Carrier : Set
341
 
    _≈_     : Rel Carrier zero
 
342
    Carrier : Set c
 
343
    _≈_     : Rel Carrier ℓ
342
344
    _+_     : Op₂ Carrier
343
345
    _*_     : Op₂ Carrier
344
346
    -_      : Op₁ Carrier
348
350
 
349
351
  open IsRing isRing public
350
352
 
351
 
  +-abelianGroup : AbelianGroup
 
353
  +-abelianGroup : AbelianGroup _ _
352
354
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
353
355
 
354
 
  semiring : Semiring
 
356
  semiring : Semiring _ _
355
357
  semiring = record { isSemiring = isSemiring }
356
358
 
357
359
  open Semiring semiring public
366
368
  open AbelianGroup +-abelianGroup public
367
369
         using () renaming (group to +-group)
368
370
 
369
 
  rawRing : RawRing
 
371
  rawRing : RawRing _
370
372
  rawRing = record
371
373
    { _+_ = _+_
372
374
    ; _*_ = _*_
375
377
    ; 1#  = 1#
376
378
    }
377
379
 
378
 
record CommutativeRing : Set₁ where
 
380
record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
379
381
  infix  8 -_
380
382
  infixl 7 _*_
381
383
  infixl 6 _+_
382
384
  infix  4 _≈_
383
385
  field
384
 
    Carrier           : Set
385
 
    _≈_               : Rel Carrier zero
 
386
    Carrier           : Set c
 
387
    _≈_               : Rel Carrier ℓ
386
388
    _+_               : Op₂ Carrier
387
389
    _*_               : Op₂ Carrier
388
390
    -_                : Op₁ Carrier
392
394
 
393
395
  open IsCommutativeRing isCommutativeRing public
394
396
 
395
 
  ring : Ring
 
397
  ring : Ring _ _
396
398
  ring = record { isRing = isRing }
397
399
 
398
 
  commutativeSemiring : CommutativeSemiring
 
400
  commutativeSemiring : CommutativeSemiring _ _
399
401
  commutativeSemiring =
400
402
    record { isCommutativeSemiring = isCommutativeSemiring }
401
403
 
412
414
------------------------------------------------------------------------
413
415
-- (Distributive) lattices and boolean algebras
414
416
 
415
 
record Lattice : Set₁ where
 
417
record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
416
418
  infixr 7 _∧_
417
419
  infixr 6 _∨_
418
420
  infix  4 _≈_
419
421
  field
420
 
    Carrier   : Set
421
 
    _≈_       : Rel Carrier zero
 
422
    Carrier   : Set c
 
423
    _≈_       : Rel Carrier ℓ
422
424
    _∨_       : Op₂ Carrier
423
425
    _∧_       : Op₂ Carrier
424
426
    isLattice : IsLattice _≈_ _∨_ _∧_
428
430
  setoid : Setoid _ _
429
431
  setoid = record { isEquivalence = isEquivalence }
430
432
 
431
 
record DistributiveLattice : Set₁ where
 
433
record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
432
434
  infixr 7 _∧_
433
435
  infixr 6 _∨_
434
436
  infix  4 _≈_
435
437
  field
436
 
    Carrier               : Set
437
 
    _≈_                   : Rel Carrier zero
 
438
    Carrier               : Set c
 
439
    _≈_                   : Rel Carrier ℓ
438
440
    _∨_                   : Op₂ Carrier
439
441
    _∧_                   : Op₂ Carrier
440
442
    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
441
443
 
442
444
  open IsDistributiveLattice isDistributiveLattice public
443
445
 
444
 
  lattice : Lattice
 
446
  lattice : Lattice _ _
445
447
  lattice = record { isLattice = isLattice }
446
448
 
447
449
  open Lattice lattice public using (setoid)
448
450
 
449
 
record BooleanAlgebra : Set₁ where
 
451
record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
450
452
  infix  8 ¬_
451
453
  infixr 7 _∧_
452
454
  infixr 6 _∨_
453
455
  infix  4 _≈_
454
456
  field
455
 
    Carrier          : Set
456
 
    _≈_              : Rel Carrier zero
 
457
    Carrier          : Set c
 
458
    _≈_              : Rel Carrier ℓ
457
459
    _∨_              : Op₂ Carrier
458
460
    _∧_              : Op₂ Carrier
459
461
    ¬_               : Op₁ Carrier
463
465
 
464
466
  open IsBooleanAlgebra isBooleanAlgebra public
465
467
 
466
 
  distributiveLattice : DistributiveLattice
 
468
  distributiveLattice : DistributiveLattice _ _
467
469
  distributiveLattice =
468
470
    record { isDistributiveLattice = isDistributiveLattice }
469
471