-
Notifications
You must be signed in to change notification settings - Fork 2
/
Property.agda
111 lines (82 loc) · 2.63 KB
/
Property.agda
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
open import Level
open import CancellativeAbelianMonoid
module Property
(a l : Level)
(m : CancellativeAbelianMonoid a l)
where
open import Algebra
open import Algebra.FunctionProperties
open import Algebra.Structures
open import Data.Product
open import Data.Sum
open import Level
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary
open import Relation.Unary
open import Cancel
{-
The original proof is written by Thierry Coquand.
http://www.cs.ru.nl/~freek/comparison/comparison.pdf
-}
Carrier : Set a
Carrier = CancellativeAbelianMonoid.Carrier m
infixl 7 _∙_
infix 4 _≈_
_≈_ : Carrier -> Carrier -> Set l
_≈_ = CancellativeAbelianMonoid._≈_ m
_∙_ : Carrier -> Carrier -> Carrier
_∙_ = CancellativeAbelianMonoid._∙_ m
ε : Carrier
ε = CancellativeAbelianMonoid.ε m
----
semigroup : Semigroup a l
semigroup = CancellativeAbelianMonoid.semigroup m
isSemigroup : IsSemigroup _≈_ _∙_
isSemigroup = Semigroup.isSemigroup semigroup
----
assoc : Associative _≈_ _∙_
assoc = IsSemigroup.assoc isSemigroup
∙-cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
∙-cong = IsSemigroup.∙-cong isSemigroup
----
≈-setoid : Setoid a l
≈-setoid = Semigroup.setoid semigroup
isPreorder : IsPreorder _≡_ _≈_
isPreorder = Setoid.isPreorder ≈-setoid
----
≈-refl : Reflexive _≈_
≈-refl = IsPreorder.refl isPreorder
≈-trans : Transitive _≈_
≈-trans = IsPreorder.trans isPreorder
----
isEquivalence : IsEquivalence _≈_
isEquivalence = Setoid.isEquivalence ≈-setoid
----
≈-sym : Symmetric _≈_
≈-sym = IsEquivalence.sym isEquivalence
----
commutativeMonoid : CommutativeMonoid a l
commutativeMonoid = CancellativeAbelianMonoid.commutativeMonoid m
isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
isCommutativeMonoid
= CommutativeMonoid.isCommutativeMonoid commutativeMonoid
----
comm : Commutative _≈_ _∙_
comm = IsCommutativeMonoid.comm isCommutativeMonoid
cancel : Cancel _≈_ _∙_
cancel = IsCancellativeAbelianMonoid.cancel
(CancellativeAbelianMonoid.isCancellativeAbelianMonoid m)
square : (x : Carrier) -> Carrier
square x = x ∙ x
multiple : (p : Carrier) -> Rel Carrier l
multiple p = λ (x y : Carrier) -> (p ∙ x) ≈ y
_divides_ : Rel Carrier (l ⊔ a)
x divides y = ∃ (λ z → (x ∙ z) ≈ y)
_isPrime : Pred Carrier (l ⊔ a)
p isPrime = (x y : Carrier) -> p divides (x ∙ y) ->
(p divides x) ⊎ (p divides y)
Square : Rel Carrier (l ⊔ a)
Square = λ (p x : Carrier) → ∃ (λ y → p ∙ square x ≈ square y)
_isNotSquare : Pred Carrier (l ⊔ a)
p isNotSquare = (x y : Carrier) → ¬ ((p ∙ square x) ≈ square y)