git.iko.soy/Idris-dev
on master help sign in
More additions to the Nat file.
8079a69Dominic Mulligan
lib/prelude/nat.idr+115−34
compare with master
unifiedsplit
@@ -92,9 +92,9 @@ pred (S n) = n
92--------------------------------------------------------------------------------
92--------------------------------------------------------------------------------
93
93
94fib : Nat -> Nat
94fib : Nat -> Nat
95−fib O = O
95+fib O = 0
96−fib (S O) = S O
96+fib (S O) = 1
97−fib (S (S n)) = plus (fib (S n)) (fib n)
97+fib (S (S n)) = fib (S n) + fib n
98
98
99--------------------------------------------------------------------------------
99--------------------------------------------------------------------------------
100-- GCD and LCM
100-- GCD and LCM
@@ -159,103 +159,124 @@ succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
159succInjective left right refl = refl
159succInjective left right refl = refl
160
160
161-- Plus
161-- Plus
162−plusZeroLeftNeutral : (right : Nat) -> plus O right = right
162+plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
163plusZeroLeftNeutral right = refl
163plusZeroLeftNeutral right = refl
164
164
165−plusZeroRightNeutral : (left : Nat) -> plus left O = left
165+plusZeroRightNeutral : (left : Nat) -> left + 0 = left
166plusZeroRightNeutral O = refl
166plusZeroRightNeutral O = refl
167plusZeroRightNeutral (S n) =
167plusZeroRightNeutral (S n) =
168 let inductiveHypothesis = plusZeroRightNeutral n in
168 let inductiveHypothesis = plusZeroRightNeutral n in
169 ?plusZeroRightNeutralStepCase
169 ?plusZeroRightNeutralStepCase
170
170
171plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
171plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
172− S (plus left right) = plus left (S right)
172+ S (left + right) = left + (S right)
173plusSuccRightSucc O right = refl
173plusSuccRightSucc O right = refl
174plusSuccRightSucc (S left) right =
174plusSuccRightSucc (S left) right =
175 let inductiveHypothesis = plusSuccRightSucc left right in
175 let inductiveHypothesis = plusSuccRightSucc left right in
176 ?plusSuccRightSuccStepCase
176 ?plusSuccRightSuccStepCase
177
177
178plusCommutative : (left : Nat) -> (right : Nat) ->
178plusCommutative : (left : Nat) -> (right : Nat) ->
179− plus left right = plus right left
179+ left + right = right + left
180plusCommutative O right = ?plusCommutativeBaseCase
180plusCommutative O right = ?plusCommutativeBaseCase
181plusCommutative (S left) right =
181plusCommutative (S left) right =
182 let inductiveHypothesis = plusCommutative left right in
182 let inductiveHypothesis = plusCommutative left right in
183 ?plusCommutativeStepCase
183 ?plusCommutativeStepCase
184
184
185plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
185plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
186− plus left (plus centre right) = plus (plus left centre) right
186+ left + (centre + right) = (left + centre) + right
187plusAssociative O centre right = refl
187plusAssociative O centre right = refl
188plusAssociative (S left) centre right =
188plusAssociative (S left) centre right =
189 let inductiveHypothesis = plusAssociative left centre right in
189 let inductiveHypothesis = plusAssociative left centre right in
190 ?plusAssociativeStepCase
190 ?plusAssociativeStepCase
191
191
192plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
193− (p : left = right) -> plus left c = plus right c
193+ (p : left = right) -> left + c = right + c
194plusMonotonicRight left right c refl = refl
194plusMonotonicRight left right c refl = refl
195
195
196plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
197− (p : left = right) -> plus c left = plus c right
197+ (p : left = right) -> c + left = c + right
198plusMonotonicLeft left right c refl = refl
198plusMonotonicLeft left right c refl = refl
199
199
200−plusOneSucc : (right : Nat) -> plus (S O) right = S right
200+plusOneSucc : (right : Nat) -> 1 + right = S right
201plusOneSucc n = refl
201plusOneSucc n = refl
202
202
203+plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
204+ (p : left + right = left + right') -> right = right'
205+plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
206+plusLeftCancel (S left) right right' p =
207+ let inductiveHypothesis = plusLeftCancel left right right' in
208+ ?plusLeftCancelStepCase
209+
210+plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
211+ (p : left + right = left' + right) -> left = left'
212+plusRightCancel left left' O p = ?plusRightCancelBaseCase
213+plusRightCancel left left' (S right) p =
214+ let inductiveHypothesis = plusRightCancel left left' right in
215+ ?plusRightCancelStepCase
216+
217+plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
218+ (p : left + right = left) -> right = O
219+plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
220+plusLeftLeftRightZero (S left) right p =
221+ let inductiveHypothesis = plusLeftLeftRightZero left right in
222+ ?plusLeftLeftRightZeroStepCase
223+
203-- Mult
224-- Mult
204−multZeroLeftZero : (right : Nat) -> mult O right = O
225+multZeroLeftZero : (right : Nat) -> O * right = O
205multZeroLeftZero right = refl
226multZeroLeftZero right = refl
206
227
207−multZeroRightZero : (left : Nat) -> mult left O = O
228+multZeroRightZero : (left : Nat) -> left * O = O
208multZeroRightZero O = refl
229multZeroRightZero O = refl
209multZeroRightZero (S left) =
230multZeroRightZero (S left) =
210 let inductiveHypothesis = multZeroRightZero left in
231 let inductiveHypothesis = multZeroRightZero left in
211 ?multZeroRightZeroStepCase
232 ?multZeroRightZeroStepCase
212
233
213multRightSuccPlus : (left : Nat) -> (right : Nat) ->
234multRightSuccPlus : (left : Nat) -> (right : Nat) ->
214− mult left (S right) = plus left (mult left right)
235+ left * (S right) = left + (left * right)
215multRightSuccPlus O right = refl
236multRightSuccPlus O right = refl
216multRightSuccPlus (S left) right =
237multRightSuccPlus (S left) right =
217 let inductiveHypothesis = multRightSuccPlus left right in
238 let inductiveHypothesis = multRightSuccPlus left right in
218 ?multRightSuccPlusStepCase
239 ?multRightSuccPlusStepCase
219
240
220multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
241multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
221− mult (S left) right = plus right (mult left right)
242+ (S left) * right = right + (left * right)
222multLeftSuccPlus left right = refl
243multLeftSuccPlus left right = refl
223
244
224multCommutative : (left : Nat) -> (right : Nat) ->
245multCommutative : (left : Nat) -> (right : Nat) ->
225− mult left right = mult right left
246+ left * right = right * left
226multCommutative O right = ?multCommutativeBaseCase
247multCommutative O right = ?multCommutativeBaseCase
227multCommutative (S left) right =
248multCommutative (S left) right =
228 let inductiveHypothesis = multCommutative left right in
249 let inductiveHypothesis = multCommutative left right in
229 ?multCommutativeStepCase
250 ?multCommutativeStepCase
230
251
231multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
252multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
232− mult left (plus centre right) = plus (mult left centre) (mult left right)
253+ left * (centre + right) = (left * centre) + (left * right)
233multDistributesOverPlusRight O centre right = refl
254multDistributesOverPlusRight O centre right = refl
234multDistributesOverPlusRight (S left) centre right =
255multDistributesOverPlusRight (S left) centre right =
235 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
256 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
236 ?multDistributesOverPlusRightStepCase
257 ?multDistributesOverPlusRightStepCase
237
258
238multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
259multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
239− mult (plus left centre) right = plus (mult left right) (mult centre right)
260+ (left + centre) * right = (left * right) + (centre * right)
240multDistributesOverPlusLeft O centre right = refl
261multDistributesOverPlusLeft O centre right = refl
241multDistributesOverPlusLeft (S left) centre right =
262multDistributesOverPlusLeft (S left) centre right =
242 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
263 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
243 ?multDistributesOverPlusLeftStepCase
264 ?multDistributesOverPlusLeftStepCase
244
265
245multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
266multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
246− mult left (mult centre right) = mult (mult left centre) right
267+ left * (centre * right) = (left * centre) * right
247multAssociative O centre right = refl
268multAssociative O centre right = refl
248multAssociative (S left) centre right =
269multAssociative (S left) centre right =
249 let inductiveHypothesis = multAssociative left centre right in
270 let inductiveHypothesis = multAssociative left centre right in
250 ?multAssociativeStepCase
271 ?multAssociativeStepCase
251
272
252−multOneLeftNeutral : (right : Nat) -> mult (S O) right = right
273+multOneLeftNeutral : (right : Nat) -> 1 * right = right
253multOneLeftNeutral O = refl
274multOneLeftNeutral O = refl
254multOneLeftNeutral (S right) =
275multOneLeftNeutral (S right) =
255 let inductiveHypothesis = multOneLeftNeutral right in
276 let inductiveHypothesis = multOneLeftNeutral right in
256 ?multOneLeftNeutralStepCase
277 ?multOneLeftNeutralStepCase
257
278
258−multOneRightNeutral : (left : Nat) -> mult left (S O) = left
279+multOneRightNeutral : (left : Nat) -> left * 1 = left
259multOneRightNeutral O = refl
280multOneRightNeutral O = refl
260multOneRightNeutral (S left) =
281multOneRightNeutral (S left) =
261 let inductiveHypothesis = multOneRightNeutral left in
282 let inductiveHypothesis = multOneRightNeutral left in
@@ -263,59 +284,68 @@ multOneRightNeutral (S left) =
263
284
264-- Minus
285-- Minus
265minusSuccSucc : (left : Nat) -> (right : Nat) ->
286minusSuccSucc : (left : Nat) -> (right : Nat) ->
266− minus (S left) (S right) = minus left right
287+ (S left) - (S right) = left - right
267minusSuccSucc left right = refl
288minusSuccSucc left right = refl
268
289
269−minusZeroLeft : (right : Nat) -> minus O right = O
290+minusZeroLeft : (right : Nat) -> 0 - right = O
270minusZeroLeft right = refl
291minusZeroLeft right = refl
271
292
272−minusZeroRight : (left : Nat) -> minus left O = left
293+minusZeroRight : (left : Nat) -> left - 0 = left
273minusZeroRight O = refl
294minusZeroRight O = refl
274minusZeroRight (S left) = refl
295minusZeroRight (S left) = refl
275
296
276−minusZeroN : (n : Nat) -> O = minus n n
297+minusZeroN : (n : Nat) -> O = n - n
277minusZeroN O = refl
298minusZeroN O = refl
278minusZeroN (S n) = minusZeroN n
299minusZeroN (S n) = minusZeroN n
279
300
280−minusOneSuccN : (n : Nat) -> S O = minus (S n) n
301+minusOneSuccN : (n : Nat) -> S O = (S n) - n
281minusOneSuccN O = refl
302minusOneSuccN O = refl
282minusOneSuccN (S n) = minusOneSuccN n
303minusOneSuccN (S n) = minusOneSuccN n
283
304
305+minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
306+ left - centre - right = left - (centre + right)
307+minusMinusMinusPlus O O right = refl
308+minusMinusMinusPlus (S left) O right = refl
309+minusMinusMinusPlus O (S centre) right = refl
310+minusMinusMinusPlus (S left) (S centre) right =
311+ let inductiveHypothesis = minusMinusMinusPlus left centre right in
312+ ?minusMinusMinusPlusStepCase
313+
284-- Power
314-- Power
285powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
315powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
286− mult base (power base exp)
316+ base * (power base exp)
287powerSuccPowerLeft base exp = refl
317powerSuccPowerLeft base exp = refl
288
318
289multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
319multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
290− mult (power base exp) (power base exp') = power base (plus exp exp')
320+ (power base exp) * (power base exp') = power base (exp + exp')
291multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
321multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
292multPowerPowerPlus base (S exp) exp' =
322multPowerPowerPlus base (S exp) exp' =
293 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
323 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
294 ?multPowerPowerPlusStepCase
324 ?multPowerPowerPlusStepCase
295
325
296−powerZeroOne : (base : Nat) -> power base O = S O
326+powerZeroOne : (base : Nat) -> power base 0 = S O
297powerZeroOne base = refl
327powerZeroOne base = refl
298
328
299−powerOneNeutral : (base : Nat) -> power base (S O) = base
329+powerOneNeutral : (base : Nat) -> power base 1 = base
300powerOneNeutral O = refl
330powerOneNeutral O = refl
301powerOneNeutral (S base) =
331powerOneNeutral (S base) =
302 let inductiveHypothesis = powerOneNeutral base in
332 let inductiveHypothesis = powerOneNeutral base in
303 ?powerOneNeutralStepCase
333 ?powerOneNeutralStepCase
304
334
305−powerOneSuccOne : (exp : Nat) -> power (S O) exp = S O
335+powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
306powerOneSuccOne O = refl
336powerOneSuccOne O = refl
307powerOneSuccOne (S exp) =
337powerOneSuccOne (S exp) =
308 let inductiveHypothesis = powerOneSuccOne exp in
338 let inductiveHypothesis = powerOneSuccOne exp in
309 ?powerOneSuccOneStepCase
339 ?powerOneSuccOneStepCase
310
340
311−powerSuccSuccMult : (base : Nat) -> power base (S (S O)) = mult base base
341+powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
312powerSuccSuccMult O = refl
342powerSuccSuccMult O = refl
313powerSuccSuccMult (S base) =
343powerSuccSuccMult (S base) =
314 let inductiveHypothesis = powerSuccSuccMult base in
344 let inductiveHypothesis = powerSuccSuccMult base in
315 ?powerSuccSuccMultStepCase
345 ?powerSuccSuccMultStepCase
316
346
317powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
347powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
318− power (power base exp) exp' = power base (mult exp exp')
348+ power (power base exp) exp' = power base (exp * exp')
319powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
349powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
320powerPowerMultPower base exp (S exp') =
350powerPowerMultPower base exp (S exp') =
321 let inductiveHypothesis = powerPowerMultPower base exp exp' in
351 let inductiveHypothesis = powerPowerMultPower base exp exp' in
@@ -326,7 +356,7 @@ predSucc : (n : Nat) -> pred (S n) = n
326predSucc n = refl
356predSucc n = refl
327
357
328minusSuccPred : (left : Nat) -> (right : Nat) ->
358minusSuccPred : (left : Nat) -> (right : Nat) ->
329− minus left (S right) = pred (minus left right)
359+ left - (S right) = pred (left - right)
330minusSuccPred O right = refl
360minusSuccPred O right = refl
331minusSuccPred (S left) O =
361minusSuccPred (S left) O =
332 let inductiveHypothesis = minusSuccPred left O in
362 let inductiveHypothesis = minusSuccPred left O in
@@ -495,3 +525,54 @@ plusZeroRightNeutralStepCase = proof {
495 trivial;
525 trivial;
496}
526}
497
527
528+minusMinusMinusPlusStepCase = proof {
529+ intros;
530+ rewrite inductiveHypothesis;
531+ trivial;
532+}
533+
534+plusLeftLeftRightZeroBaseCase = proof {
535+ intros;
536+ rewrite p;
537+ trivial;
538+}
539+
540+plusLeftLeftRightZeroStepCase = proof {
541+ intros;
542+ refine inductiveHypothesis;
543+ let p' = succInjective (plus left right) left p;
544+ rewrite p';
545+ trivial;
546+}
547+
548+plusRightCancelStepCase = proof {
549+ intros;
550+ refine inductiveHypothesis;
551+ refine succInjective;
552+ rewrite sym (plusSuccRightSucc left right);
553+ rewrite sym (plusSuccRightSucc left' right);
554+ rewrite p;
555+ trivial;
556+}
557+
558+plusRightCancelBaseCase = proof {
559+ intros;
560+ rewrite (plusZeroRightNeutral left);
561+ rewrite (plusZeroRightNeutral left');
562+ rewrite p;
563+ trivial;
564+}
565+
566+plusLeftCancelStepCase = proof {
567+ intros;
568+ let injectiveProof = succInjective (plus left right) (plus left right') p;
569+ rewrite (inductiveHypothesis injectiveProof);
570+ trivial;
571+}
572+
573+plusLeftCancelBaseCase = proof {
574+ intros;
575+ rewrite p;
576+ trivial;
577+}
578+