← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Algebra/FunctionProperties.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/FunctionProperties.agda
2
2
-- Properties of functions, such as associativity and commutativity
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
-- These properties can (for instance) be used to define algebraic
6
8
-- structures.
7
9
 
11
13
-- The properties are specified using the following relation as
12
14
-- "equality".
13
15
 
14
 
module Algebra.FunctionProperties {A} (_≈_ : Rel A zero) where
 
16
module Algebra.FunctionProperties
 
17
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
15
18
 
16
19
open import Data.Product
17
20
 
23
26
------------------------------------------------------------------------
24
27
-- Properties of operations
25
28
 
26
 
Associative : Op₂ A → Set
 
29
Associative : Op₂ A → Set _
27
30
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
28
31
 
29
 
Commutative : Op₂ A → Set
 
32
Commutative : Op₂ A → Set _
30
33
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
31
34
 
32
 
LeftIdentity : A → Op₂ A → Set
 
35
LeftIdentity : A → Op₂ A → Set _
33
36
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x
34
37
 
35
 
RightIdentity : A → Op₂ A → Set
 
38
RightIdentity : A → Op₂ A → Set _
36
39
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x
37
40
 
38
 
Identity : A → Op₂ A → Set
 
41
Identity : A → Op₂ A → Set _
39
42
Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙
40
43
 
41
 
LeftZero : A → Op₂ A → Set
 
44
LeftZero : A → Op₂ A → Set _
42
45
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z
43
46
 
44
 
RightZero : A → Op₂ A → Set
 
47
RightZero : A → Op₂ A → Set _
45
48
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
46
49
 
47
 
Zero : A → Op₂ A → Set
 
50
Zero : A → Op₂ A → Set _
48
51
Zero z ∙ = LeftZero z ∙ × RightZero z ∙
49
52
 
50
 
LeftInverse : A → Op₁ A → Op₂ A → Set
 
53
LeftInverse : A → Op₁ A → Op₂ A → Set _
51
54
LeftInverse e _⁻¹ _∙_ = ∀ x → (x ⁻¹ ∙ x) ≈ e
52
55
 
53
 
RightInverse : A → Op₁ A → Op₂ A → Set
 
56
RightInverse : A → Op₁ A → Op₂ A → Set _
54
57
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e
55
58
 
56
 
Inverse : A → Op₁ A → Op₂ A → Set
 
59
Inverse : A → Op₁ A → Op₂ A → Set _
57
60
Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙
58
61
 
59
 
_DistributesOverˡ_ : Op₂ A → Op₂ A → Set
 
62
_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
60
63
_*_ DistributesOverˡ _+_ =
61
64
  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
62
65
 
63
 
_DistributesOverʳ_ : Op₂ A → Op₂ A → Set
 
66
_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
64
67
_*_ DistributesOverʳ _+_ =
65
68
  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
66
69
 
67
 
_DistributesOver_ : Op₂ A → Op₂ A → Set
 
70
_DistributesOver_ : Op₂ A → Op₂ A → Set _
68
71
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
69
72
 
70
 
_IdempotentOn_ : Op₂ A → A → Set
 
73
_IdempotentOn_ : Op₂ A → A → Set _
71
74
_∙_ IdempotentOn x = (x ∙ x) ≈ x
72
75
 
73
 
Idempotent : Op₂ A → Set
 
76
Idempotent : Op₂ A → Set _
74
77
Idempotent ∙ = ∀ x → ∙ IdempotentOn x
75
78
 
76
 
IdempotentFun : Op₁ A → Set
 
79
IdempotentFun : Op₁ A → Set _
77
80
IdempotentFun f = ∀ x → f (f x) ≈ f x
78
81
 
79
 
_Absorbs_ : Op₂ A → Op₂ A → Set
 
82
_Absorbs_ : Op₂ A → Op₂ A → Set _
80
83
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x
81
84
 
82
 
Absorptive : Op₂ A → Op₂ A → Set
 
85
Absorptive : Op₂ A → Op₂ A → Set _
83
86
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
84
87
 
85
 
Involutive : Op₁ A → Set
 
88
Involutive : Op₁ A → Set _
86
89
Involutive f = ∀ x → f (f x) ≈ x