@@ -15,11 +15,11 @@ data Nat
1515-- Syntactic tests
1616--------------------------------------------------------------------------------
1717
18−isZero : Nat -> Bool
18+total isZero : Nat -> Bool
1919isZero O = True
2020isZero (S n) = False
2121
22−isSucc : Nat -> Bool
22+total isSucc : Nat -> Bool
2323isSucc O = False
2424isSucc (S n) = True
2525
@@ -27,20 +27,20 @@ isSucc (S n) = True
2727-- Basic arithmetic functions
2828--------------------------------------------------------------------------------
2929
30−plus : Nat -> Nat -> Nat
30+total plus : Nat -> Nat -> Nat
3131plus O right = right
3232plus (S left) right = S (plus left right)
3333
34−mult : Nat -> Nat -> Nat
34+total mult : Nat -> Nat -> Nat
3535mult O right = O
3636mult (S left) right = plus right $ mult left right
3737
38−minus : Nat -> Nat -> Nat
38+total minus : Nat -> Nat -> Nat
3939minus O right = O
4040minus left O = left
4141minus (S left) (S right) = minus left right
4242
43−power : Nat -> Nat -> Nat
43+total power : Nat -> Nat -> Nat
4444power base O = S O
4545power base (S exp) = mult base $ power base exp
4646
@@ -49,7 +49,7 @@ power base (S exp) = mult base $ power base exp
4949--------------------------------------------------------------------------------
5050
5151instance Eq Nat where
52− O == O = True
52+ Z == Z = True
5353 (S l) == (S r) = l == r
5454 _ == _ = False
5555
@@ -68,21 +68,60 @@ instance Num Nat where
6868 (-) = minus
6969 (*) = mult
7070
71− fromInteger = intToNat where
71+ fromInteger = fromInteger'
72+ where
7273 %assert_total
73− intToNat : Int -> Nat
74− intToNat 0 = O
75− intToNat n = if (n > 0) then S (fromInteger (n-1)) else O
76−
77−--------------------------------------------------------------------------------
78−-- Division and modulus
79−--------------------------------------------------------------------------------
74+ fromInteger' : Int -> Nat
75+ fromInteger' 0 = O
76+ fromInteger' n =
77+ if (n > 0) then
78+ S (fromInteger' (n - 1))
79+ else
80+ O
81+
82+record Multiplicative : Set where
83+ getMultiplicative : Nat -> Multiplicative
84+
85+record Additive : Set where
86+ getAdditive : Nat -> Additive
87+
88+instance Semigroup Multiplicative where
89+ left <.> right = getMultiplicative $ left' * right'
90+ where
91+ left' : Nat
92+ left' =
93+ case left of
94+ getMultiplicative m => m
95+
96+ right' : Nat
97+ right' =
98+ case right of
99+ getMultiplicative m => m
100+
101+instance Semigroup Additive where
102+ left <.> right = getAdditive $ left' + right'
103+ where
104+ left' : Nat
105+ left' =
106+ case left of
107+ getAdditive m => m
108+
109+ right' : Nat
110+ right' =
111+ case right of
112+ getAdditive m => m
113+
114+instance Monoid Multiplicative where
115+ neutral = getMultiplicative $ S O
116+
117+instance Monoid Additive where
118+ neutral = getAdditive $ O
80119
81120--------------------------------------------------------------------------------
82121-- Auxilliary notions
83122--------------------------------------------------------------------------------
84123
85−pred : Nat -> Nat
124+total pred : Nat -> Nat
86125pred O = O
87126pred (S n) = n
88127
@@ -90,9 +129,9 @@ pred (S n) = n
90129-- Fibonacci and factorial
91130--------------------------------------------------------------------------------
92131
93−fib : Nat -> Nat
94−fib O = 0
95−fib (S O) = 1
132+total fib : Nat -> Nat
133+fib O = O
134+fib (S O) = S O
96135fib (S (S n)) = fib (S n) + fib n
97136
98137--------------------------------------------------------------------------------
@@ -107,113 +146,141 @@ data LTE : Nat -> Nat -> Set where
107146 lteZero : LTE O right
108147 lteSucc : LTE left right -> LTE (S left) (S right)
109148
110−GTE : Nat -> Nat -> Set
149+total GTE : Nat -> Nat -> Set
111150GTE left right = LTE right left
112151
113−LT : Nat -> Nat -> Set
152+total LT : Nat -> Nat -> Set
114153LT left right = LTE (S left) right
115154
116−GT : Nat -> Nat -> Set
155+total GT : Nat -> Nat -> Set
117156GT left right = LT right left
118157
119−lte : Nat -> Nat -> Bool
158+total lte : Nat -> Nat -> Bool
120159lte O right = True
121160lte left O = False
122161lte (S left) (S right) = lte left right
123162
124−gte : Nat -> Nat -> Bool
163+total gte : Nat -> Nat -> Bool
125164gte left right = lte right left
126165
127−lt : Nat -> Nat -> Bool
166+total lt : Nat -> Nat -> Bool
128167lt left right = lte (S left) right
129168
130−gt : Nat -> Nat -> Bool
169+total gt : Nat -> Nat -> Bool
131170gt left right = lt right left
132171
133−minimum : Nat -> Nat -> Nat
172+total minimum : Nat -> Nat -> Nat
134173minimum left right =
135174 if lte left right then
136175 left
137176 else
138177 right
139178
140−maximum : Nat -> Nat -> Nat
179+total maximum : Nat -> Nat -> Nat
141180maximum left right =
142181 if lte left right then
143182 right
144183 else
145184 left
146185
186+--------------------------------------------------------------------------------
187+-- Division and modulus
188+--------------------------------------------------------------------------------
189+
190+total mod : Nat -> Nat -> Nat
191+mod left O = left
192+mod left (S right) = mod' left left right
193+ where
194+ total mod' : Nat -> Nat -> Nat -> Nat
195+ mod' O centre right = centre
196+ mod' (S left) centre right =
197+ if lte centre right then
198+ centre
199+ else
200+ mod' left (centre - (S right)) right
201+
202+total div : Nat -> Nat -> Nat
203+div left O = S left -- div by zero
204+div left (S right) = div' left left right
205+ where
206+ total div' : Nat -> Nat -> Nat -> Nat
207+ div' O centre right = O
208+ div' (S left) centre right =
209+ if lte centre right then
210+ O
211+ else
212+ S (div' left (centre - (S right)) right)
213+
147214--------------------------------------------------------------------------------
148215-- Properties
149216--------------------------------------------------------------------------------
150217
151218-- Succ
152−eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
219+total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
153220 S left = S right
154221eqSucc left right refl = refl
155222
156−succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
223+total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
157224 left = right
158225succInjective left right refl = refl
159226
160227-- Plus
161−plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
228+total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
162229plusZeroLeftNeutral right = refl
163230
164−plusZeroRightNeutral : (left : Nat) -> left + 0 = left
231+total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
165232plusZeroRightNeutral O = refl
166233plusZeroRightNeutral (S n) =
167234 let inductiveHypothesis = plusZeroRightNeutral n in
168235 ?plusZeroRightNeutralStepCase
169236
170−plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
237+total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
171238 S (left + right) = left + (S right)
172239plusSuccRightSucc O right = refl
173240plusSuccRightSucc (S left) right =
174241 let inductiveHypothesis = plusSuccRightSucc left right in
175242 ?plusSuccRightSuccStepCase
176243
177−plusCommutative : (left : Nat) -> (right : Nat) ->
244+total plusCommutative : (left : Nat) -> (right : Nat) ->
178245 left + right = right + left
179246plusCommutative O right = ?plusCommutativeBaseCase
180247plusCommutative (S left) right =
181248 let inductiveHypothesis = plusCommutative left right in
182249 ?plusCommutativeStepCase
183250
184−plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
251+total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
185252 left + (centre + right) = (left + centre) + right
186253plusAssociative O centre right = refl
187254plusAssociative (S left) centre right =
188255 let inductiveHypothesis = plusAssociative left centre right in
189256 ?plusAssociativeStepCase
190257
191−plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
258+total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192259 (p : left = right) -> left + c = right + c
193260plusConstantRight left right c refl = refl
194261
195−plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
262+total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196263 (p : left = right) -> c + left = c + right
197264plusConstantLeft left right c refl = refl
198265
199−plusOneSucc : (right : Nat) -> 1 + right = S right
266+total plusOneSucc : (right : Nat) -> 1 + right = S right
200267plusOneSucc n = refl
201268
202−plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
269+total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
203270 (p : left + right = left + right') -> right = right'
204271plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
205272plusLeftCancel (S left) right right' p =
206273 let inductiveHypothesis = plusLeftCancel left right right' in
207274 ?plusLeftCancelStepCase
208275
209−plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
276+total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
210277 (p : left + right = left' + right) -> left = left'
211278plusRightCancel left left' O p = ?plusRightCancelBaseCase
212279plusRightCancel left left' (S right) p =
213280 let inductiveHypothesis = plusRightCancel left left' right in
214281 ?plusRightCancelStepCase
215282
216−plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
283+total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
217284 (p : left + right = left) -> right = O
218285plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
219286plusLeftLeftRightZero (S left) right p =
@@ -221,95 +288,95 @@ plusLeftLeftRightZero (S left) right p =
221288 ?plusLeftLeftRightZeroStepCase
222289
223290-- Mult
224−multZeroLeftZero : (right : Nat) -> O * right = O
291+total multZeroLeftZero : (right : Nat) -> O * right = O
225292multZeroLeftZero right = refl
226293
227−multZeroRightZero : (left : Nat) -> left * O = O
294+total multZeroRightZero : (left : Nat) -> left * O = O
228295multZeroRightZero O = refl
229296multZeroRightZero (S left) =
230297 let inductiveHypothesis = multZeroRightZero left in
231298 ?multZeroRightZeroStepCase
232299
233−multRightSuccPlus : (left : Nat) -> (right : Nat) ->
300+total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
234301 left * (S right) = left + (left * right)
235302multRightSuccPlus O right = refl
236303multRightSuccPlus (S left) right =
237304 let inductiveHypothesis = multRightSuccPlus left right in
238305 ?multRightSuccPlusStepCase
239306
240−multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
307+total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
241308 (S left) * right = right + (left * right)
242309multLeftSuccPlus left right = refl
243310
244−multCommutative : (left : Nat) -> (right : Nat) ->
311+total multCommutative : (left : Nat) -> (right : Nat) ->
245312 left * right = right * left
246313multCommutative O right = ?multCommutativeBaseCase
247314multCommutative (S left) right =
248315 let inductiveHypothesis = multCommutative left right in
249316 ?multCommutativeStepCase
250317
251−multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
318+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
252319 left * (centre + right) = (left * centre) + (left * right)
253320multDistributesOverPlusRight O centre right = refl
254321multDistributesOverPlusRight (S left) centre right =
255322 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
256323 ?multDistributesOverPlusRightStepCase
257324
258−multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
325+total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
259326 (left + centre) * right = (left * right) + (centre * right)
260327multDistributesOverPlusLeft O centre right = refl
261328multDistributesOverPlusLeft (S left) centre right =
262329 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
263330 ?multDistributesOverPlusLeftStepCase
264331
265−multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
332+total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
266333 left * (centre * right) = (left * centre) * right
267334multAssociative O centre right = refl
268335multAssociative (S left) centre right =
269336 let inductiveHypothesis = multAssociative left centre right in
270337 ?multAssociativeStepCase
271338
272−multOneLeftNeutral : (right : Nat) -> 1 * right = right
339+total multOneLeftNeutral : (right : Nat) -> 1 * right = right
273340multOneLeftNeutral O = refl
274341multOneLeftNeutral (S right) =
275342 let inductiveHypothesis = multOneLeftNeutral right in
276343 ?multOneLeftNeutralStepCase
277344
278−multOneRightNeutral : (left : Nat) -> left * 1 = left
345+total multOneRightNeutral : (left : Nat) -> left * 1 = left
279346multOneRightNeutral O = refl
280347multOneRightNeutral (S left) =
281348 let inductiveHypothesis = multOneRightNeutral left in
282349 ?multOneRightNeutralStepCase
283350
284351-- Minus
285−minusSuccSucc : (left : Nat) -> (right : Nat) ->
352+total minusSuccSucc : (left : Nat) -> (right : Nat) ->
286353 (S left) - (S right) = left - right
287354minusSuccSucc left right = refl
288355
289−minusZeroLeft : (right : Nat) -> 0 - right = O
356+total minusZeroLeft : (right : Nat) -> 0 - right = O
290357minusZeroLeft right = refl
291358
292−minusZeroRight : (left : Nat) -> left - 0 = left
359+total minusZeroRight : (left : Nat) -> left - 0 = left
293360minusZeroRight O = refl
294361minusZeroRight (S left) = refl
295362
296−minusZeroN : (n : Nat) -> O = n - n
363+total minusZeroN : (n : Nat) -> O = n - n
297364minusZeroN O = refl
298365minusZeroN (S n) = minusZeroN n
299366
300−minusOneSuccN : (n : Nat) -> S O = (S n) - n
367+total minusOneSuccN : (n : Nat) -> S O = (S n) - n
301368minusOneSuccN O = refl
302369minusOneSuccN (S n) = minusOneSuccN n
303370
304−minusSuccOne : (n : Nat) -> S n - 1 = n
371+total minusSuccOne : (n : Nat) -> S n - 1 = n
305372minusSuccOne O = refl
306373minusSuccOne (S n) = refl
307374
308−minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
375+total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
309376minusPlusZero O m = refl
310377minusPlusZero (S n) m = minusPlusZero n m
311378
312−minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
379+total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
313380 left - centre - right = left - (centre + right)
314381minusMinusMinusPlus O O right = refl
315382minusMinusMinusPlus (S left) O right = refl
@@ -318,14 +385,14 @@ minusMinusMinusPlus (S left) (S centre) right =
318385 let inductiveHypothesis = minusMinusMinusPlus left centre right in
319386 ?minusMinusMinusPlusStepCase
320387
321−plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
388+total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
322389 (left + right) - (left + right') = right - right'
323390plusMinusLeftCancel O right right' = refl
324391plusMinusLeftCancel (S left) right right' =
325392 let inductiveHypothesis = plusMinusLeftCancel left right right' in
326393 ?plusMinusLeftCancelStepCase
327394
328−multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
395+total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
329396 (left - centre) * right = (left * right) - (centre * right)
330397multDistributesOverMinusLeft O O right = refl
331398multDistributesOverMinusLeft (S left) O right =
@@ -335,45 +402,45 @@ multDistributesOverMinusLeft (S left) (S centre) right =
335402 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
336403 ?multDistributesOverMinusLeftStepCase
337404
338−multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
405+total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
339406 left * (centre - right) = (left * centre) - (left * right)
340407multDistributesOverMinusRight left centre right =
341408 ?multDistributesOverMinusRightBody
342409
343410-- Power
344−powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
411+total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
345412 base * (power base exp)
346413powerSuccPowerLeft base exp = refl
347414
348−multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
415+total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
349416 (power base exp) * (power base exp') = power base (exp + exp')
350417multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
351418multPowerPowerPlus base (S exp) exp' =
352419 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
353420 ?multPowerPowerPlusStepCase
354421
355−powerZeroOne : (base : Nat) -> power base 0 = S O
422+total powerZeroOne : (base : Nat) -> power base 0 = S O
356423powerZeroOne base = refl
357424
358−powerOneNeutral : (base : Nat) -> power base 1 = base
425+total powerOneNeutral : (base : Nat) -> power base 1 = base
359426powerOneNeutral O = refl
360427powerOneNeutral (S base) =
361428 let inductiveHypothesis = powerOneNeutral base in
362429 ?powerOneNeutralStepCase
363430
364−powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
431+total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
365432powerOneSuccOne O = refl
366433powerOneSuccOne (S exp) =
367434 let inductiveHypothesis = powerOneSuccOne exp in
368435 ?powerOneSuccOneStepCase
369436
370−powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
437+total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
371438powerSuccSuccMult O = refl
372439powerSuccSuccMult (S base) =
373440 let inductiveHypothesis = powerSuccSuccMult base in
374441 ?powerSuccSuccMultStepCase
375442
376−powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
443+total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
377444 power (power base exp) exp' = power base (exp * exp')
378445powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
379446powerPowerMultPower base exp (S exp') =
@@ -381,10 +448,10 @@ powerPowerMultPower base exp (S exp') =
381448 ?powerPowerMultPowerStepCase
382449
383450-- Pred
384−predSucc : (n : Nat) -> pred (S n) = n
451+total predSucc : (n : Nat) -> pred (S n) = n
385452predSucc n = refl
386453
387−minusSuccPred : (left : Nat) -> (right : Nat) ->
454+total minusSuccPred : (left : Nat) -> (right : Nat) ->
388455 left - (S right) = pred (left - right)
389456minusSuccPred O right = refl
390457minusSuccPred (S left) O =
@@ -395,50 +462,50 @@ minusSuccPred (S left) (S right) =
395462 ?minusSuccPredStepCase'
396463
397464-- boolElim
398−boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
465+total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
399466 S (boolElim cond t f) = boolElim cond (S t) (S f)
400467boolElimSuccSucc True t f = refl
401468boolElimSuccSucc False t f = refl
402469
403−boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
470+total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
404471 left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
405472boolElimPlusPlusLeft True left t f = refl
406473boolElimPlusPlusLeft False left t f = refl
407474
408−boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
475+total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
409476 (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
410477boolElimPlusPlusRight True right t f = refl
411478boolElimPlusPlusRight False right t f = refl
412479
413−boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
480+total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
414481 left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
415482boolElimMultMultLeft True left t f = refl
416483boolElimMultMultLeft False left t f = refl
417484
418−boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
485+total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
419486 (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
420487boolElimMultMultRight True right t f = refl
421488boolElimMultMultRight False right t f = refl
422489
423490-- Orders
424−lteNTrue : (n : Nat) -> lte n n = True
491+total lteNTrue : (n : Nat) -> lte n n = True
425492lteNTrue O = refl
426493lteNTrue (S n) = lteNTrue n
427494
428−lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
495+total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
429496lteSuccZeroFalse O = refl
430497lteSuccZeroFalse (S n) = refl
431498
432499-- Minimum and maximum
433−minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
500+total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
434501minimumZeroZeroRight O = refl
435502minimumZeroZeroRight (S right) = minimumZeroZeroRight right
436503
437−minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
504+total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
438505minimumZeroZeroLeft O = refl
439506minimumZeroZeroLeft (S left) = refl
440507
441−minimumSuccSucc : (left : Nat) -> (right : Nat) ->
508+total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
442509 minimum (S left) (S right) = S (minimum left right)
443510minimumSuccSucc O O = refl
444511minimumSuccSucc (S left) O = refl
@@ -447,7 +514,7 @@ minimumSuccSucc (S left) (S right) =
447514 let inductiveHypothesis = minimumSuccSucc left right in
448515 ?minimumSuccSuccStepCase
449516
450−minimumCommutative : (left : Nat) -> (right : Nat) ->
517+total minimumCommutative : (left : Nat) -> (right : Nat) ->
451518 minimum left right = minimum right left
452519minimumCommutative O O = refl
453520minimumCommutative O (S right) = refl
@@ -456,15 +523,15 @@ minimumCommutative (S left) (S right) =
456523 let inductiveHypothesis = minimumCommutative left right in
457524 ?minimumCommutativeStepCase
458525
459−maximumZeroNRight : (right : Nat) -> maximum O right = right
526+total maximumZeroNRight : (right : Nat) -> maximum O right = right
460527maximumZeroNRight O = refl
461528maximumZeroNRight (S right) = refl
462529
463−maximumZeroNLeft : (left : Nat) -> maximum left O = left
530+total maximumZeroNLeft : (left : Nat) -> maximum left O = left
464531maximumZeroNLeft O = refl
465532maximumZeroNLeft (S left) = refl
466533
467−maximumSuccSucc : (left : Nat) -> (right : Nat) ->
534+total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
468535 S (maximum left right) = maximum (S left) (S right)
469536maximumSuccSucc O O = refl
470537maximumSuccSucc (S left) O = refl
@@ -473,7 +540,7 @@ maximumSuccSucc (S left) (S right) =
473540 let inductiveHypothesis = maximumSuccSucc left right in
474541 ?maximumSuccSuccStepCase
475542
476−maximumCommutative : (left : Nat) -> (right : Nat) ->
543+total maximumCommutative : (left : Nat) -> (right : Nat) ->
477544 maximum left right = maximum right left
478545maximumCommutative O O = refl
479546maximumCommutative (S left) O = refl
@@ -482,6 +549,11 @@ maximumCommutative (S left) (S right) =
482549 let inductiveHypothesis = maximumCommutative left right in
483550 ?maximumCommutativeStepCase
484551
552+-- div and mod
553+total modZeroZero : (n : Nat) -> mod 0 n = O
554+modZeroZero O = refl
555+modZeroZero (S n) = refl
556+
485557--------------------------------------------------------------------------------
486558-- Proofs
487559--------------------------------------------------------------------------------
@@ -642,6 +714,9 @@ plusZeroRightNeutralStepCase = proof {
642714 trivial;
643715}
644716
717+
718+---------- Proofs ----------
719+
645720maximumCommutativeStepCase = proof {
646721 intros;
647722 rewrite (boolElimSuccSucc (lte left right) right left);