/
Nat.idr
646 lines (528 loc) · 17.9 KB
/
Nat.idr
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
module Data.Nat
%default total
export
Uninhabited (Z = S n) where
uninhabited Refl impossible
export
Uninhabited (S n = Z) where
uninhabited Refl impossible
public export
isZero : Nat -> Bool
isZero Z = True
isZero (S n) = False
public export
isSucc : Nat -> Bool
isSucc Z = False
isSucc (S n) = True
public export
data IsSucc : (n : Nat) -> Type where
ItIsSucc : IsSucc (S n)
export
Uninhabited (IsSucc Z) where
uninhabited ItIsSucc impossible
public export
isItSucc : (n : Nat) -> Dec (IsSucc n)
isItSucc Z = No absurd
isItSucc (S n) = Yes ItIsSucc
public export
power : Nat -> Nat -> Nat
power base Z = S Z
power base (S exp) = base * (power base exp)
public export
hyper : Nat -> Nat -> Nat -> Nat
hyper Z a b = S b
hyper (S Z) a Z = a
hyper (S(S Z)) a Z = Z
hyper n a Z = S Z
hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
public export
pred : Nat -> Nat
pred Z = Z
pred (S n) = n
-- Comparisons
public export
data NotBothZero : (n, m : Nat) -> Type where
LeftIsNotZero : NotBothZero (S n) m
RightIsNotZero : NotBothZero n (S m)
public export
data LTE : (n, m : Nat) -> Type where
LTEZero : LTE Z right
LTESucc : LTE left right -> LTE (S left) (S right)
export
Uninhabited (LTE (S n) Z) where
uninhabited LTEZero impossible
public export
GTE : Nat -> Nat -> Type
GTE left right = LTE right left
public export
LT : Nat -> Nat -> Type
LT left right = LTE (S left) right
public export
GT : Nat -> Nat -> Type
GT left right = LT right left
export
succNotLTEzero : Not (LTE (S m) Z)
succNotLTEzero LTEZero impossible
export
fromLteSucc : LTE (S m) (S n) -> LTE m n
fromLteSucc (LTESucc x) = x
export
isLTE : (m, n : Nat) -> Dec (LTE m n)
isLTE Z n = Yes LTEZero
isLTE (S k) Z = No succNotLTEzero
isLTE (S k) (S j)
= case isLTE k j of
No contra => No (contra . fromLteSucc)
Yes prf => Yes (LTESucc prf)
export
lteRefl : {n : Nat} -> LTE n n
lteRefl {n = Z} = LTEZero
lteRefl {n = S k} = LTESucc lteRefl
export
lteSuccRight : LTE n m -> LTE n (S m)
lteSuccRight LTEZero = LTEZero
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
export
lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft (LTESucc x) = lteSuccRight x
export
lteTransitive : LTE n m -> LTE m p -> LTE n p
lteTransitive LTEZero y = LTEZero
lteTransitive (LTESucc x) (LTESucc y) = LTESucc (lteTransitive x y)
export
lteAddRight : (n : Nat) -> LTE n (n + m)
lteAddRight Z = LTEZero
lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)
export
notLTEImpliesGT : {a, b : Nat} -> Not (a `LTE` b) -> a `GT` b
notLTEImpliesGT {a = 0 } not_z_lte_b = absurd $ not_z_lte_b LTEZero
notLTEImpliesGT {a = S a} {b = 0 } notLTE = LTESucc LTEZero
notLTEImpliesGT {a = S a} {b = S k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc))
export
notLTImpliesGTE : {a, b : _} -> Not (LT a b) -> GTE a b
notLTImpliesGTE notLT = fromLteSucc $ notLTEImpliesGT notLT
public export
lte : Nat -> Nat -> Bool
lte Z right = True
lte left Z = False
lte (S left) (S right) = lte left right
public export
gte : Nat -> Nat -> Bool
gte left right = lte right left
public export
lt : Nat -> Nat -> Bool
lt left right = lte (S left) right
public export
gt : Nat -> Nat -> Bool
gt left right = lt right left
public export
minimum : Nat -> Nat -> Nat
minimum Z m = Z
minimum (S n) Z = Z
minimum (S n) (S m) = S (minimum n m)
public export
maximum : Nat -> Nat -> Nat
maximum Z m = m
maximum (S n) Z = S n
maximum (S n) (S m) = S (maximum n m)
-- Proofs on S
export
eqSucc : (0 left, right : Nat) -> left = right -> S left = S right
eqSucc _ _ Refl = Refl
export
succInjective : (0 left, right : Nat) -> S left = S right -> left = right
succInjective _ _ Refl = Refl
export total
SIsNotZ : (S x = Z) -> Void
SIsNotZ Refl impossible
||| Auxiliary function:
||| mod' fuel a b = a `mod` (S b)
||| assuming we have enough fuel
public export
mod' : Nat -> Nat -> Nat -> Nat
mod' Z centre right = centre
mod' (S fuel) centre right =
if lte centre right then
centre
else
mod' fuel (minus centre (S right)) right
public export
modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
modNatNZ left Z p = void (p Refl)
modNatNZ left (S right) _ = mod' left left right
export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNotZ
||| Auxiliary function:
||| div' fuel a b = a `div` (S b)
||| assuming we have enough fuel
public export
div' : Nat -> Nat -> Nat -> Nat
div' Z centre right = Z
div' (S fuel) centre right =
if lte centre right then
Z
else
S (div' fuel (minus centre (S right)) right)
-- 'public' to allow type-level division
public export
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
export partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNotZ
export partial
divCeilNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
Z => divNatNZ x y p
S _ => S (divNatNZ x y p)
export partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
public export
divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
divmod' Z centre right = (Z, centre)
divmod' (S fuel) centre right =
if lte centre right then
(Z, centre)
else
let qr = divmod' fuel (minus centre (S right)) right
in (S (fst qr), snd qr)
public export
divmodNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> (Nat, Nat)
divmodNatNZ left Z p = void (p Refl)
divmodNatNZ left (S right) _ = divmod' left left right
public export
Integral Nat where
div = divNat
mod = modNat
export partial
gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
gcd a Z = a
gcd Z b = b
gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNotZ)
export partial
lcm : Nat -> Nat -> Nat
lcm _ Z = Z
lcm Z _ = Z
lcm a (S b) = divNat (a * (S b)) (gcd a (S b))
--------------------------------------------------------------------------------
-- An informative comparison view
--------------------------------------------------------------------------------
public export
data CmpNat : Nat -> Nat -> Type where
CmpLT : (y : _) -> CmpNat x (x + S y)
CmpEQ : CmpNat x x
CmpGT : (x : _) -> CmpNat (y + S x) y
export
cmp : (x, y : Nat) -> CmpNat x y
cmp Z Z = CmpEQ
cmp Z (S k) = CmpLT _
cmp (S k) Z = CmpGT _
cmp (S x) (S y) with (cmp x y)
cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
cmp (S x) (S x) | CmpEQ = CmpEQ
cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
-- Proofs on +
export
plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
plusZeroLeftNeutral _ = Refl
export
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z = Refl
plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl
export
plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
plusSuccRightSucc Z _ = Refl
plusSuccRightSucc (S left) right = rewrite plusSuccRightSucc left right in Refl
export
plusCommutative : (left, right : Nat) -> left + right = right + left
plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
plusCommutative (S left) right =
rewrite plusCommutative left right in
rewrite plusSuccRightSucc right left in
Refl
export
plusAssociative : (left, centre, right : Nat) ->
left + (centre + right) = (left + centre) + right
plusAssociative Z _ _ = Refl
plusAssociative (S left) centre right =
rewrite plusAssociative left centre right in Refl
export
plusConstantRight : (left, right, c : Nat) -> left = right ->
left + c = right + c
plusConstantRight _ _ _ Refl = Refl
export
plusConstantLeft : (left, right, c : Nat) -> left = right ->
c + left = c + right
plusConstantLeft _ _ _ Refl = Refl
export
plusOneSucc : (right : Nat) -> 1 + right = S right
plusOneSucc _ = Refl
export
plusLeftCancel : (left, right, right' : Nat) ->
left + right = left + right' -> right = right'
plusLeftCancel Z _ _ p = p
plusLeftCancel (S left) right right' p =
plusLeftCancel left right right' (succInjective _ _ p)
export
plusRightCancel : (left, left', right : Nat) ->
left + right = left' + right -> left = left'
plusRightCancel left left' right p =
plusLeftCancel right left left' $
rewrite plusCommutative right left in
rewrite plusCommutative right left' in
p
export
plusLeftLeftRightZero : (left, right : Nat) ->
left + right = left -> right = Z
plusLeftLeftRightZero left right p =
plusLeftCancel left right Z $
rewrite plusZeroRightNeutral left in
p
export
plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
plusLteMonotoneRight p Z r LTEZero = rewrite plusCommutative r p in
lteAddRight p
plusLteMonotoneRight p (S q) (S r) (LTESucc l) = LTESucc $ plusLteMonotoneRight p q r l
export
plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
plusLteMonotoneLeft p q r p_lt_q
= rewrite plusCommutative p q in
rewrite plusCommutative p r in
plusLteMonotoneRight p q r p_lt_q
zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0
zeroPlusLeftZero 0 0 Refl = Refl
zeroPlusLeftZero (S k) b _ impossible
zeroPlusRightZero : (a,b : Nat) -> (0 = a + b) -> b = 0
zeroPlusRightZero 0 0 Refl = Refl
zeroPlusRightZero (S k) b _ impossible
-- Proofs on *
export
multZeroLeftZero : (right : Nat) -> Z * right = Z
multZeroLeftZero _ = Refl
export
multZeroRightZero : (left : Nat) -> left * Z = Z
multZeroRightZero Z = Refl
multZeroRightZero (S left) = multZeroRightZero left
export
multRightSuccPlus : (left, right : Nat) ->
left * (S right) = left + (left * right)
multRightSuccPlus Z _ = Refl
multRightSuccPlus (S left) right =
rewrite multRightSuccPlus left right in
rewrite plusAssociative left right (left * right) in
rewrite plusAssociative right left (left * right) in
rewrite plusCommutative right left in
Refl
export
multLeftSuccPlus : (left, right : Nat) ->
(S left) * right = right + (left * right)
multLeftSuccPlus _ _ = Refl
export
multCommutative : (left, right : Nat) -> left * right = right * left
multCommutative Z right = rewrite multZeroRightZero right in Refl
multCommutative (S left) right =
rewrite multCommutative left right in
rewrite multRightSuccPlus right left in
Refl
export
multDistributesOverPlusLeft : (left, centre, right : Nat) ->
(left + centre) * right = (left * right) + (centre * right)
multDistributesOverPlusLeft Z _ _ = Refl
multDistributesOverPlusLeft (S k) centre right =
rewrite multDistributesOverPlusLeft k centre right in
rewrite plusAssociative right (k * right) (centre * right) in
Refl
export
multDistributesOverPlusRight : (left, centre, right : Nat) ->
left * (centre + right) = (left * centre) + (left * right)
multDistributesOverPlusRight left centre right =
rewrite multCommutative left (centre + right) in
rewrite multCommutative left centre in
rewrite multCommutative left right in
multDistributesOverPlusLeft centre right left
export
multAssociative : (left, centre, right : Nat) ->
left * (centre * right) = (left * centre) * right
multAssociative Z _ _ = Refl
multAssociative (S left) centre right =
rewrite multAssociative left centre right in
rewrite multDistributesOverPlusLeft centre (mult left centre) right in
Refl
export
multOneLeftNeutral : (right : Nat) -> 1 * right = right
multOneLeftNeutral right = plusZeroRightNeutral right
export
multOneRightNeutral : (left : Nat) -> left * 1 = left
multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
-- Proofs on minus
export
minusSuccSucc : (left, right : Nat) ->
minus (S left) (S right) = minus left right
minusSuccSucc _ _ = Refl
export
minusZeroLeft : (right : Nat) -> minus 0 right = Z
minusZeroLeft _ = Refl
export
minusZeroRight : (left : Nat) -> minus left 0 = left
minusZeroRight Z = Refl
minusZeroRight (S _) = Refl
export
minusZeroN : (n : Nat) -> Z = minus n n
minusZeroN Z = Refl
minusZeroN (S n) = minusZeroN n
export
minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
minusOneSuccN Z = Refl
minusOneSuccN (S n) = minusOneSuccN n
export
minusSuccOne : (n : Nat) -> minus (S n) 1 = n
minusSuccOne Z = Refl
minusSuccOne (S _) = Refl
export
minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
minusPlusZero Z _ = Refl
minusPlusZero (S n) m = minusPlusZero n m
export
plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m
plusMinusLte Z m _ = rewrite minusZeroRight m in
plusZeroRightNeutral m
plusMinusLte (S _) Z lte = absurd lte
plusMinusLte (S n) (S m) lte = rewrite sym $ plusSuccRightSucc (minus m n) n in
cong S $ plusMinusLte n m (fromLteSucc lte)
export
minusMinusMinusPlus : (left, centre, right : Nat) ->
minus (minus left centre) right = minus left (centre + right)
minusMinusMinusPlus Z Z _ = Refl
minusMinusMinusPlus (S _) Z _ = Refl
minusMinusMinusPlus Z (S _) _ = Refl
minusMinusMinusPlus (S left) (S centre) right =
rewrite minusMinusMinusPlus left centre right in Refl
export
plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
minus (left + right) (left + right') = minus right right'
plusMinusLeftCancel Z _ _ = Refl
plusMinusLeftCancel (S left) right right' =
rewrite plusMinusLeftCancel left right right' in Refl
export
multDistributesOverMinusLeft : (left, centre, right : Nat) ->
(minus left centre) * right = minus (left * right) (centre * right)
multDistributesOverMinusLeft Z Z _ = Refl
multDistributesOverMinusLeft (S left) Z right =
rewrite minusZeroRight (right + (left * right)) in Refl
multDistributesOverMinusLeft Z (S _) _ = Refl
multDistributesOverMinusLeft (S left) (S centre) right =
rewrite multDistributesOverMinusLeft left centre right in
rewrite plusMinusLeftCancel right (left * right) (centre * right) in
Refl
export
multDistributesOverMinusRight : (left, centre, right : Nat) ->
left * (minus centre right) = minus (left * centre) (left * right)
multDistributesOverMinusRight left centre right =
rewrite multCommutative left (minus centre right) in
rewrite multDistributesOverMinusLeft centre right left in
rewrite multCommutative centre left in
rewrite multCommutative right left in
Refl
export
zeroMultEitherZero : (a,b : Nat) -> a*b = 0 -> Either (a = 0) (b = 0)
zeroMultEitherZero 0 b prf = Left Refl
zeroMultEitherZero (S a) b prf = Right $ zeroPlusLeftZero b (a * b) (sym prf)
-- power proofs
-- multPowerPowerPlus : (base, exp, exp' : Nat) ->
-- power base (exp + exp') = (power base exp) * (power base exp')
-- multPowerPowerPlus base Z exp' =
-- rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
-- multPowerPowerPlus base (S exp) exp' =
-- rewrite multPowerPowerPlus base exp exp' in
-- rewrite sym $ multAssociative base (power base exp) (power base exp') in
-- Refl
--powerOneNeutral : (base : Nat) -> power base 1 = base
--powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
--
--powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
--powerOneSuccOne Z = Refl
--powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
--
--powerPowerMultPower : (base, exp, exp' : Nat) ->
-- power (power base exp) exp' = power base (exp * exp')
--powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
--powerPowerMultPower base exp (S exp') =
-- rewrite powerPowerMultPower base exp exp' in
-- rewrite multRightSuccPlus exp exp' in
-- rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
-- Refl
-- minimum / maximum proofs
export
maximumAssociative : (l, c, r : Nat) ->
maximum l (maximum c r) = maximum (maximum l c) r
maximumAssociative Z _ _ = Refl
maximumAssociative (S _) Z _ = Refl
maximumAssociative (S _) (S _) Z = Refl
maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl
export
maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
maximumCommutative Z Z = Refl
maximumCommutative Z (S _) = Refl
maximumCommutative (S _) Z = Refl
maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
export
maximumIdempotent : (n : Nat) -> maximum n n = n
maximumIdempotent Z = Refl
maximumIdempotent (S k) = cong S $ maximumIdempotent k
export
minimumAssociative : (l, c, r : Nat) ->
minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z _ _ = Refl
minimumAssociative (S _) Z _ = Refl
minimumAssociative (S _) (S _) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
export
minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
minimumCommutative Z Z = Refl
minimumCommutative Z (S _) = Refl
minimumCommutative (S _) Z = Refl
minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
export
minimumIdempotent : (n : Nat) -> minimum n n = n
minimumIdempotent Z = Refl
minimumIdempotent (S k) = cong S $ minimumIdempotent k
export
minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
export
minimumSuccSucc : (left, right : Nat) ->
minimum (S left) (S right) = S (minimum left right)
minimumSuccSucc _ _ = Refl
export
maximumZeroNLeft : (left : Nat) -> maximum left Z = left
maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl
export
maximumSuccSucc : (left, right : Nat) ->
S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc _ _ = Refl
export
sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
sucMaxL Z = Refl
sucMaxL (S l) = cong S $ sucMaxL l
export
sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
sucMaxR Z = Refl
sucMaxR (S l) = cong S $ sucMaxR l
export
sucMinL : (l : Nat) -> minimum (S l) l = l
sucMinL Z = Refl
sucMinL (S l) = cong S $ sucMinL l
export
sucMinR : (l : Nat) -> minimum l (S l) = l
sucMinR Z = Refl
sucMinR (S l) = cong S $ sucMinR l
-- Algebra -----------------------------
public export
Semigroup Nat where
(<+>) = plus
public export
Monoid Nat where
neutral = Z