@@ -1,127 +1,497 @@
1−module prelude.nat
1+module MoreNat
22
33import builtins
4+
5+import prelude.algebra
46import prelude.cast
57
68%access public
79
8−data Nat = O | S Nat
10+data Nat
11+ = O
12+ | S Nat
913
10−instance Cast Nat Int where
11− cast O = 0
12− cast (S k) = 1 + cast k
14+--------------------------------------------------------------------------------
15+-- Syntactic tests
16+--------------------------------------------------------------------------------
1317
14−plus : Nat -> Nat -> Nat
15−plus O y = y
16−plus (S k) y = S (plus k y)
18+isZero : Nat -> Bool
19+isZero O = True
20+isZero (S n) = False
1721
18−eqRespS : m = n -> S m = S n
19−eqRespS refl = refl
22+isSucc : Nat -> Bool
23+isSucc O = False
24+isSucc (S n) = True
2025
21−eqRespS' : S m = S n -> m = n
22−eqRespS' refl = refl
26+--------------------------------------------------------------------------------
27+-- Basic arithmetic functions
28+--------------------------------------------------------------------------------
2329
24−sub : Nat -> Nat -> Nat
25−sub O y = O
26−sub (S k) (S y) = sub k y
27−sub x O = x
30+plus : Nat -> Nat -> Nat
31+plus O right = right
32+plus (S left) right = S (plus left right)
2833
2934mult : Nat -> Nat -> Nat
30−mult O y = O
31−mult (S k) y = plus y (mult k y)
35+mult O right = O
36+mult (S left) right = plus right $ mult left right
37+
38+minus : Nat -> Nat -> Nat
39+minus O right = O
40+minus left O = left
41+minus (S left) (S right) = minus left right
3242
33−instance Eq Nat where
34− O == O = True
35− (S x) == (S y) = x == y
36− O == (S y) = False
37− (S x) == O = False
43+power : Nat -> Nat -> Nat
44+power base O = S O
45+power base (S exp) = mult base $ power base exp
46+
47+--------------------------------------------------------------------------------
48+-- Type class instances
49+--------------------------------------------------------------------------------
50+
51+instance Eq Nat where
52+ Z == Z = True
53+ (S l) == (S r) = l == r
54+ _ == _ = False
55+
56+instance Cast Nat Int where
57+ cast O = 0
58+ cast (S k) = 1 + cast k
3859
3960instance Ord Nat where
40− compare O O = EQ
41− compare O (S k) = LT
42− compare (S k) O = GT
43− compare (S x) (S y) = compare x y
61+ compare O O = EQ
62+ compare O (S k) = LT
63+ compare (S k) O = GT
64+ compare (S x) (S y) = compare x y
4465
4566instance Num Nat where
46− (+) = plus
47− (-) = sub
48− (*) = mult
67+ (+) = plus
68+ (-) = minus
69+ (*) = mult
70+
71+ fromInteger 0 = O
72+ fromInteger n =
73+ if (n > 0) then
74+ (S (fromInteger (n-1)))
75+ else
76+ O
77+
78+--------------------------------------------------------------------------------
79+-- Division and modulus
80+--------------------------------------------------------------------------------
81+
82+--------------------------------------------------------------------------------
83+-- Auxilliary notions
84+--------------------------------------------------------------------------------
85+
86+pred : Nat -> Nat
87+pred O = O
88+pred (S n) = n
89+
90+--------------------------------------------------------------------------------
91+-- Fibonacci and factorial
92+--------------------------------------------------------------------------------
93+
94+fib : Nat -> Nat
95+fib O = O
96+fib (S O) = S O
97+fib (S (S n)) = plus (fib (S n)) (fib n)
98+
99+--------------------------------------------------------------------------------
100+-- GCD and LCM
101+--------------------------------------------------------------------------------
102+
103+--------------------------------------------------------------------------------
104+-- Comparisons
105+--------------------------------------------------------------------------------
106+
107+data LTE : Nat -> Nat -> Set where
108+ lteZero : LTE O right
109+ lteSucc : LTE left right -> LTE (S left) (S right)
110+
111+GTE : Nat -> Nat -> Set
112+GTE left right = LTE right left
113+
114+LT : Nat -> Nat -> Set
115+LT left right = LTE (S left) right
116+
117+GT : Nat -> Nat -> Set
118+GT left right = LT right left
119+
120+lte : Nat -> Nat -> Bool
121+lte O right = True
122+lte left O = False
123+lte (S left) (S right) = lte left right
124+
125+gte : Nat -> Nat -> Bool
126+gte left right = lte right left
127+
128+lt : Nat -> Nat -> Bool
129+lt left right = lte (S left) right
130+
131+gt : Nat -> Nat -> Bool
132+gt left right = lt right left
133+
134+minimum : Nat -> Nat -> Nat
135+minimum left right =
136+ if lte left right then
137+ left
138+ else
139+ right
140+
141+maximum : Nat -> Nat -> Nat
142+maximum left right =
143+ if lte left right then
144+ right
145+ else
146+ left
147+
148+--------------------------------------------------------------------------------
149+-- Properties
150+--------------------------------------------------------------------------------
151+
152+-- Succ
153+succMonotonic : (left : Nat) -> (right : Nat) -> (p : left = right) ->
154+ S left = S right
155+succMonotonic left right refl = refl
156+
157+succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
158+ left = right
159+succInjective left right refl = refl
160+
161+-- Plus
162+plusZeroLeftNeutral : (right : Nat) -> plus O right = right
163+plusZeroLeftNeutral right = refl
164+
165+plusZeroRightNeutral : (left : Nat) -> plus left O = left
166+plusZeroRightNeutral O = refl
167+plusZeroRightNeutral (S n) =
168+ let inductiveHypothesis = plusZeroRightNeutral n in
169+ ?plusZeroRightNeutralStepCase
170+
171+plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
172+ S (plus left right) = plus left (S right)
173+plusSuccRightSucc O right = refl
174+plusSuccRightSucc (S left) right =
175+ let inductiveHypothesis = plusSuccRightSucc left right in
176+ ?plusSuccRightSuccStepCase
177+
178+plusCommutative : (left : Nat) -> (right : Nat) ->
179+ plus left right = plus right left
180+plusCommutative O right = ?plusCommutativeBaseCase
181+plusCommutative (S left) right =
182+ let inductiveHypothesis = plusCommutative left right in
183+ ?plusCommutativeStepCase
184+
185+plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
186+ plus left (plus centre right) = plus (plus left centre) right
187+plusAssociative O centre right = refl
188+plusAssociative (S left) centre right =
189+ let inductiveHypothesis = plusAssociative left centre right in
190+ ?plusAssociativeStepCase
191+
192+plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
193+ (p : left = right) -> plus left c = plus right c
194+plusMonotonicRight left right c refl = refl
195+
196+plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
197+ (p : left = right) -> plus c left = plus c right
198+plusMonotonicLeft left right c refl = refl
199+
200+plusOneSucc : (right : Nat) -> plus (S O) right = S right
201+plusOneSucc n = refl
202+
203+-- Mult
204+multZeroLeftZero : (right : Nat) -> mult O right = O
205+multZeroLeftZero right = refl
206+
207+multZeroRightZero : (left : Nat) -> mult left O = O
208+multZeroRightZero O = refl
209+multZeroRightZero (S left) =
210+ let inductiveHypothesis = multZeroRightZero left in
211+ ?multZeroRightZeroStepCase
212+
213+multRightSuccPlus : (left : Nat) -> (right : Nat) ->
214+ mult left (S right) = plus left (mult left right)
215+multRightSuccPlus O right = refl
216+multRightSuccPlus (S left) right =
217+ let inductiveHypothesis = multRightSuccPlus left right in
218+ ?multRightSuccPlusStepCase
219+
220+multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
221+ mult (S left) right = plus right (mult left right)
222+multLeftSuccPlus left right = refl
223+
224+multCommutative : (left : Nat) -> (right : Nat) ->
225+ mult left right = mult right left
226+multCommutative O right = ?multCommutativeBaseCase
227+multCommutative (S left) right =
228+ let inductiveHypothesis = multCommutative left right in
229+ ?multCommutativeStepCase
230+
231+multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
232+ mult left (plus centre right) = plus (mult left centre) (mult left right)
233+multDistributesOverPlusRight O centre right = refl
234+multDistributesOverPlusRight (S left) centre right =
235+ let inductiveHypothesis = multDistributesOverPlusRight left centre right in
236+ ?multDistributesOverPlusRightStepCase
237+
238+multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
239+ mult (plus left centre) right = plus (mult left right) (mult centre right)
240+multDistributesOverPlusLeft O centre right = refl
241+multDistributesOverPlusLeft (S left) centre right =
242+ let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
243+ ?multDistributesOverPlusLeftStepCase
244+
245+multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
246+ mult left (mult centre right) = mult (mult left centre) right
247+multAssociative O centre right = refl
248+multAssociative (S left) centre right =
249+ let inductiveHypothesis = multAssociative left centre right in
250+ ?multAssociativeStepCase
251+
252+multOneLeftNeutral : (right : Nat) -> mult (S O) right = right
253+multOneLeftNeutral O = refl
254+multOneLeftNeutral (S right) =
255+ let inductiveHypothesis = multOneLeftNeutral right in
256+ ?multOneLeftNeutralStepCase
257+
258+multOneRightNeutral : (left : Nat) -> mult left (S O) = left
259+multOneRightNeutral O = refl
260+multOneRightNeutral (S left) =
261+ let inductiveHypothesis = multOneRightNeutral left in
262+ ?multOneRightNeutralStepCase
263+
264+-- Minus
265+minusSuccSucc : (left : Nat) -> (right : Nat) ->
266+ minus (S left) (S right) = minus left right
267+minusSuccSucc left right = refl
268+
269+minusZeroLeft : (right : Nat) -> minus O right = O
270+minusZeroLeft right = refl
271+
272+minusZeroRight : (left : Nat) -> minus left O = left
273+minusZeroRight O = refl
274+minusZeroRight (S left) = refl
275+
276+minusZeroN : (n : Nat) -> O = minus n n
277+minusZeroN O = refl
278+minusZeroN (S n) = minusZeroN n
279+
280+minusOneSuccN : (n : Nat) -> S O = minus (S n) n
281+minusOneSuccN O = refl
282+minusOneSuccN (S n) = minusOneSuccN n
283+
284+-- Power
285+powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
286+ mult base (power base exp)
287+powerSuccPowerLeft base exp = refl
288+
289+multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
290+ mult (power base exp) (power base exp') = power base (plus exp exp')
291+multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
292+multPowerPowerPlus base (S exp) exp' =
293+ let inductiveHypothesis = multPowerPowerPlus base exp exp' in
294+ ?multPowerPowerPlusStepCase
295+
296+powerZeroOne : (base : Nat) -> power base O = S O
297+powerZeroOne base = refl
298+
299+powerOneNeutral : (base : Nat) -> power base (S O) = base
300+powerOneNeutral O = refl
301+powerOneNeutral (S base) =
302+ let inductiveHypothesis = powerOneNeutral base in
303+ ?powerOneNeutralStepCase
304+
305+powerOneSuccOne : (exp : Nat) -> power (S O) exp = S O
306+powerOneSuccOne O = refl
307+powerOneSuccOne (S exp) =
308+ let inductiveHypothesis = powerOneSuccOne exp in
309+ ?powerOneSuccOneStepCase
310+
311+powerSuccSuccMult : (base : Nat) -> power base (S (S O)) = mult base base
312+powerSuccSuccMult O = refl
313+powerSuccSuccMult (S base) =
314+ let inductiveHypothesis = powerSuccSuccMult base in
315+ ?powerSuccSuccMultStepCase
316+
317+powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
318+ power (power base exp) exp' = power base (mult exp exp')
319+powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
320+powerPowerMultPower base exp (S exp') =
321+ let inductiveHypothesis = powerPowerMultPower base exp exp' in
322+ ?powerPowerMultPowerStepCase
323+
324+-- Pred
325+predSucc : (n : Nat) -> pred (S n) = n
326+predSucc n = refl
327+
328+minusSuccPred : (left : Nat) -> (right : Nat) ->
329+ minus left (S right) = pred (minus left right)
330+minusSuccPred O right = refl
331+minusSuccPred (S left) O =
332+ let inductiveHypothesis = minusSuccPred left O in
333+ ?minusSuccPredStepCase
334+minusSuccPred (S left) (S right) =
335+ let inductiveHypothesis = minusSuccPred left right in
336+ ?minusSuccPredStepCase'
337+
338+--------------------------------------------------------------------------------
339+-- Proofs
340+--------------------------------------------------------------------------------
341+
342+powerPowerMultPowerStepCase = proof {
343+ intros;
344+ rewrite sym inductiveHypothesis;
345+ rewrite sym (multRightSuccPlus exp exp');
346+ rewrite (multPowerPowerPlus base exp (mult exp exp'));
347+ trivial;
348+}
349+
350+powerPowerMultPowerBaseCase = proof {
351+ intros;
352+ rewrite sym (multZeroRightZero exp);
353+ trivial;
354+}
355+
356+powerSuccSuccMultStepCase = proof {
357+ intros;
358+ rewrite (multOneRightNeutral base);
359+ rewrite sym (multOneRightNeutral base);
360+ trivial;
361+}
362+
363+powerOneSuccOneStepCase = proof {
364+ intros;
365+ rewrite inductiveHypothesis;
366+ rewrite sym (plusZeroRightNeutral (power (S O) exp));
367+ trivial;
368+}
369+
370+powerOneNeutralStepCase = proof {
371+ intros;
372+ rewrite inductiveHypothesis;
373+ trivial;
374+}
375+
376+multAssociativeStepCase = proof {
377+ intros;
378+ rewrite sym (multDistributesOverPlusLeft centre (mult left centre) right);
379+ rewrite inductiveHypothesis;
380+ trivial;
381+}
382+
383+minusSuccPredStepCase' = proof {
384+ intros;
385+ rewrite sym inductiveHypothesis;
386+ trivial;
387+}
388+
389+minusSuccPredStepCase = proof {
390+ intros;
391+ rewrite (minusZeroRight left);
392+ trivial;
393+}
394+
395+multPowerPowerPlusStepCase = proof {
396+ intros;
397+ rewrite inductiveHypothesis;
398+ rewrite (multAssociative base (power base exp) (power base exp'));
399+ trivial;
400+}
49401
50− fromInteger 0 = O
51− fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O
402+multPowerPowerPlusBaseCase = proof {
403+ intros;
404+ rewrite (plusZeroRightNeutral (power base exp'));
405+ trivial;
406+}
52407
53−plusnO : (m : Nat) -> m + O = m
54−plusnO O = refl
55−plusnO (S k) = eqRespS (plusnO k)
408+multOneRightNeutralStepCase = proof {
409+ intros;
410+ rewrite inductiveHypothesis;
411+ trivial;
412+}
56413
57−plusn_Sm : (n, m : Nat) -> (plus n (S m)) = S (plus n m)
58−plusn_Sm O m = refl
59−plusn_Sm (S j) m = eqRespS (plusn_Sm _ _)
414+multOneLeftNeutralStepCase = proof {
415+ intros;
416+ rewrite (plusZeroRightNeutral right);
417+ trivial;
418+}
60419
61−plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
62−plus_commutes O m = sym (plusnO m)
63−plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk
420+multDistributesOverPlusLeftStepCase = proof {
421+ intros;
422+ rewrite sym inductiveHypothesis;
423+ rewrite sym (plusAssociative right (mult left right) (mult centre right));
424+ trivial;
425+}
64426
65−plus_commutes_Sk = proof {
427+multDistributesOverPlusRightStepCase = proof {
66428 intros;
67− refine sym;
68− rewrite sym ih;
69− rewrite plusn_Sm m k;
429+ rewrite sym inductiveHypothesis;
430+ rewrite sym (plusAssociative (plus centre (mult left centre)) right (mult left right));
431+ rewrite (plusAssociative centre (mult left centre) right);
432+ rewrite sym (plusCommutative (mult left centre) right);
433+ rewrite sym (plusAssociative centre right (mult left centre));
434+ rewrite sym (plusAssociative (plus centre right) (mult left centre) (mult left right));
70435 trivial;
71436}
72437
73−plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p
74−plus_assoc O m p = refl
75−plus_assoc (S k) m p = let ih = plus_assoc k m p in eqRespS ih
438+multCommutativeStepCase = proof {
439+ intros;
440+ rewrite sym (multRightSuccPlus right left);
441+ rewrite inductiveHypothesis;
442+ trivial;
443+}
76444
77−multnO : (n : Nat) -> (n * O) = O
78−multnO O = refl
79−multnO (S k) = multnO k
445+multCommutativeBaseCase = proof {
446+ intros;
447+ rewrite (multZeroRightZero right);
448+ trivial;
449+}
450+
451+multRightSuccPlusStepCase = proof {
452+ intros;
453+ rewrite inductiveHypothesis;
454+ rewrite sym inductiveHypothesis;
455+ rewrite sym (plusAssociative right left (mult left right));
456+ rewrite sym (plusCommutative right left);
457+ rewrite (plusAssociative left right (mult left right));
458+ trivial;
459+}
460+
461+multZeroRightZeroStepCase = proof {
462+ intros;
463+ rewrite inductiveHypothesis;
464+ trivial;
465+}
80466
81−multn_Sm : (n, m : Nat) -> n * S m = n + n * m
82−multn_Sm O m = refl
83−multn_Sm (S k) m = let ih = multn_Sm k m in ?multnSmSk
467+plusAssociativeStepCase = proof {
468+ intros;
469+ rewrite inductiveHypothesis;
470+ trivial;
471+}
84472
85−mult_commutes : (n, m : Nat) -> n * m = m * n
86−mult_commutes O m = ?mult_commO
87−mult_commutes (S k) m = let ih = mult_commutes k m in ?mult_commSk
473+plusCommutativeStepCase = proof {
474+ intros;
475+ rewrite (plusSuccRightSucc right left);
476+ rewrite inductiveHypothesis;
477+ trivial;
478+}
88479
89−mult_commSk = proof {
480+plusSuccRightSuccStepCase = proof {
90481 intros;
91− rewrite sym ih;
92− rewrite multn_Sm m k;
482+ rewrite inductiveHypothesis;
93483 trivial;
94484}
95485
96−mult_commO = proof {
97− intro;
98− rewrite multnO m;
486+plusCommutativeBaseCase = proof {
487+ intros;
488+ rewrite sym (plusZeroRightNeutral right);
99489 trivial;
100490}
101491
102−multnSmSk = proof {
492+plusZeroRightNeutralStepCase = proof {
103493 intros;
104− rewrite plus_commutes (mult k m) m;
105− rewrite sym (plus_assoc k (mult k m) m);
106− rewrite ih;
107− rewrite plus_commutes m (mult k (S m));
494+ rewrite inductiveHypothesis;
108495 trivial;
109496}
110497
111−data Cmp : Nat -> Nat -> Set where
112− cmpLT : (y : Nat) -> Cmp x (x + S y)
113− cmpEQ : Cmp x x
114− cmpGT : (x : Nat) -> Cmp (y + S x) y
115−
116−cmp : (n, m : Nat) -> Cmp n m
117−cmp O O = cmpEQ
118−cmp (S n) O = cmpGT _
119−cmp O (S n) = cmpLT _
120−cmp (S x) (S y) with (cmp x y)
121− cmp (S x) (S x) | cmpEQ = cmpEQ
122− cmp (S (y + S x)) (S y) | cmpGT _ = cmpGT _
123− cmp (S x) (S (x + S y)) | cmpLT _ = cmpLT _
124−
125− data LE : Nat -> Nat -> Set where
126− leO : LE O n
127− leS : LE x y -> LE (S x) (S y)