git.iko.soy/Idris-dev
on master help sign in
Fixed broken instances following e-mail conversation with Edwin in nat.idr. Changed fixity of semigroup and group operators from right to left.
bc983bbDominic Mulligan
lib/prelude/algebra.idr+5−5
compare with master
unifiedsplit
@@ -2,12 +2,12 @@ module prelude.algebra
2
2
3import builtins
3import builtins
4
4
5−%access public
6−
7-- XXX: change?
5-- XXX: change?
8−infix 6 <->
6+infixl 6 <->
9−infix 6 <+>
7+infixl 6 <+>
10−infix 6 <*>
8+infixl 6 <*>
9+
10+%access public
11
11
12-- Sets equipped with a single binary operation that is associative. Must
12-- Sets equipped with a single binary operation that is associative. Must
13-- satisfy the following laws:
13-- satisfy the following laws:
lib/prelude/nat.idr+87−77
@@ -44,6 +44,51 @@ total power : Nat -> Nat -> Nat
44power base O = S O
44power base O = S O
45power base (S exp) = mult base $ power base exp
45power base (S exp) = mult base $ power base exp
46
46
47+--------------------------------------------------------------------------------
48+-- Comparisons
49+--------------------------------------------------------------------------------
50+
51+data LTE : Nat -> Nat -> Set where
52+ lteZero : LTE O right
53+ lteSucc : LTE left right -> LTE (S left) (S right)
54+
55+total GTE : Nat -> Nat -> Set
56+GTE left right = LTE right left
57+
58+total LT : Nat -> Nat -> Set
59+LT left right = LTE (S left) right
60+
61+total GT : Nat -> Nat -> Set
62+GT left right = LT right left
63+
64+total lte : Nat -> Nat -> Bool
65+lte O right = True
66+lte left O = False
67+lte (S left) (S right) = lte left right
68+
69+total gte : Nat -> Nat -> Bool
70+gte left right = lte right left
71+
72+total lt : Nat -> Nat -> Bool
73+lt left right = lte (S left) right
74+
75+total gt : Nat -> Nat -> Bool
76+gt left right = lt right left
77+
78+total minimum : Nat -> Nat -> Nat
79+minimum left right =
80+ if lte left right then
81+ left
82+ else
83+ right
84+
85+total maximum : Nat -> Nat -> Nat
86+maximum left right =
87+ if lte left right then
88+ right
89+ else
90+ left
91+
47--------------------------------------------------------------------------------
92--------------------------------------------------------------------------------
48-- Type class instances
93-- Type class instances
49--------------------------------------------------------------------------------
94--------------------------------------------------------------------------------
@@ -85,35 +130,48 @@ record Multiplicative : Set where
85record Additive : Set where
130record Additive : Set where
86 getAdditive : Nat -> Additive
131 getAdditive : Nat -> Additive
87
132
88−-- XXX: infix operators don't seem to be being exported correctly from
89−-- algebra.idr?
90−--instance Monoid Multiplicative where
133+instance Semigroup Multiplicative where
91−-- neutral = getMultiplicative $ S O
92−-- left <+> right = getMultiplicative $ left' * right'
134+ (<+>) left right = getMultiplicative $ left' * right'
93−-- where
135+ where
94−-- left' : Nat
136+ left' : Nat
95−-- left' =
137+ left' =
96−-- case left of
138+ case left of
97−-- getMultiplicative m => m
139+ getMultiplicative m => m
98−
140+
99−-- right' : Nat
141+ right' : Nat
100−-- right' =
142+ right' =
101−-- case right of
143+ case right of
102−-- getMultiplicative m => m
144+ getMultiplicative m => m
103−
145+
104−--instance Monoid Additive where
146+instance Semigroup Additive where
105−-- neutral = getAdditive $ O
106−-- left <+> right = getAdditive $ left' + right'
147+ left <+> right = getAdditive $ left' + right'
107−-- where
148+ where
108−-- left' : Nat
149+ left' : Nat
109−-- left' =
150+ left' =
110−-- case left of
151+ case left of
111−-- getAdditive m => m
152+ getAdditive m => m
112−
153+
113−-- right' : Nat
154+ right' : Nat
114−-- right' =
155+ right' =
115−-- case right of
156+ case right of
116−-- getAdditive m => m
157+ getAdditive m => m
158+
159+instance Monoid Multiplicative where
160+ neutral = getMultiplicative $ S O
161+
162+instance Monoid Additive where
163+ neutral = getAdditive O
164+
165+instance MeetSemilattice Nat where
166+ meet = minimum
167+
168+instance JoinSemilattice Nat where
169+ join = maximum
170+
171+instance Lattice Nat where { }
172+
173+instance BoundedJoinSemilattice Nat where
174+ bottom = O
117
175
118--------------------------------------------------------------------------------
176--------------------------------------------------------------------------------
119-- Auxilliary notions
177-- Auxilliary notions
@@ -136,51 +194,6 @@ fib (S (S n)) = fib (S n) + fib n
136-- GCD and LCM
194-- GCD and LCM
137--------------------------------------------------------------------------------
195--------------------------------------------------------------------------------
138
196
139−--------------------------------------------------------------------------------
140−-- Comparisons
141−--------------------------------------------------------------------------------
142−
143−data LTE : Nat -> Nat -> Set where
144− lteZero : LTE O right
145− lteSucc : LTE left right -> LTE (S left) (S right)
146−
147−total GTE : Nat -> Nat -> Set
148−GTE left right = LTE right left
149−
150−total LT : Nat -> Nat -> Set
151−LT left right = LTE (S left) right
152−
153−total GT : Nat -> Nat -> Set
154−GT left right = LT right left
155−
156−total lte : Nat -> Nat -> Bool
157−lte O right = True
158−lte left O = False
159−lte (S left) (S right) = lte left right
160−
161−total gte : Nat -> Nat -> Bool
162−gte left right = lte right left
163−
164−total lt : Nat -> Nat -> Bool
165−lt left right = lte (S left) right
166−
167−total gt : Nat -> Nat -> Bool
168−gt left right = lt right left
169−
170−total minimum : Nat -> Nat -> Nat
171−minimum left right =
172− if lte left right then
173− left
174− else
175− right
176−
177−total maximum : Nat -> Nat -> Nat
178−maximum left right =
179− if lte left right then
180− right
181− else
182− left
183−
184--------------------------------------------------------------------------------
197--------------------------------------------------------------------------------
185-- Division and modulus
198-- Division and modulus
186--------------------------------------------------------------------------------
199--------------------------------------------------------------------------------
@@ -712,9 +725,6 @@ plusZeroRightNeutralStepCase = proof {
712 trivial;
725 trivial;
713}
726}
714
727
715−
716−---------- Proofs ----------
717−
718maximumCommutativeStepCase = proof {
728maximumCommutativeStepCase = proof {
719 intros;
729 intros;
720 rewrite (boolElimSuccSucc (lte left right) right left);
730 rewrite (boolElimSuccSucc (lte left right) right left);