@@ -44,6 +44,51 @@ total power : Nat -> Nat -> Nat
4444power base O = S O
4545power base (S exp) = mult base $ power base exp
4646
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+
4792--------------------------------------------------------------------------------
4893-- Type class instances
4994--------------------------------------------------------------------------------
@@ -85,35 +130,48 @@ record Multiplicative : Set where
85130record Additive : Set where
86131 getAdditive : Nat -> Additive
87132
88−-- XXX: infix operators don't seem to be being exported correctly from
89−-- algebra.idr?
90−--instance Monoid Multiplicative where
91−-- neutral = getMultiplicative $ S O
92−-- left <+> right = getMultiplicative $ left' * right'
93−-- where
94−-- left' : Nat
95−-- left' =
96−-- case left of
97−-- getMultiplicative m => m
98−
99−-- right' : Nat
100−-- right' =
101−-- case right of
102−-- getMultiplicative m => m
103−
104−--instance Monoid Additive where
105−-- neutral = getAdditive $ O
106−-- left <+> right = getAdditive $ left' + right'
107−-- where
108−-- left' : Nat
109−-- left' =
110−-- case left of
111−-- getAdditive m => m
112−
113−-- right' : Nat
114−-- right' =
115−-- case right of
116−-- getAdditive m => m
133+instance Semigroup Multiplicative where
134+ (<+>) left right = getMultiplicative $ left' * right'
135+ where
136+ left' : Nat
137+ left' =
138+ case left of
139+ getMultiplicative m => m
140+
141+ right' : Nat
142+ right' =
143+ case right of
144+ getMultiplicative m => m
145+
146+instance Semigroup Additive where
147+ left <+> right = getAdditive $ left' + right'
148+ where
149+ left' : Nat
150+ left' =
151+ case left of
152+ getAdditive m => m
153+
154+ right' : Nat
155+ right' =
156+ case right of
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
117175
118176--------------------------------------------------------------------------------
119177-- Auxilliary notions
@@ -136,51 +194,6 @@ fib (S (S n)) = fib (S n) + fib n
136194-- GCD and LCM
137195--------------------------------------------------------------------------------
138196
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−
184197--------------------------------------------------------------------------------
185198-- Division and modulus
186199--------------------------------------------------------------------------------
@@ -712,9 +725,6 @@ plusZeroRightNeutralStepCase = proof {
712725 trivial;
713726}
714727
715−
716−---------- Proofs ----------
717−
718728maximumCommutativeStepCase = proof {
719729 intros;
720730 rewrite (boolElimSuccSucc (lte left right) right left);