git.iko.soy/Idris-dev
on master help sign in
More additions to natural numbers theory.
63afafaDominic Mulligan
lib/prelude/nat.idr+179−6
compare with master
unifiedsplit
@@ -150,9 +150,9 @@ maximum left right =
150--------------------------------------------------------------------------------
150--------------------------------------------------------------------------------
151
151
152-- Succ
152-- Succ
153−succMonotonic : (left : Nat) -> (right : Nat) -> (p : left = right) ->
153+eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
154 S left = S right
154 S left = S right
155−succMonotonic left right refl = refl
155+eqSucc left right refl = refl
156
156
157succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
157succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
158 left = right
158 left = right
@@ -189,13 +189,13 @@ plusAssociative (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
192−plusMonotonicRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
192+plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
193 (p : left = right) -> left + c = right + c
193 (p : left = right) -> left + c = right + c
194−plusMonotonicRight left right c refl = refl
194+plusConstantRight left right c refl = refl
195
195
196−plusMonotonicLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
196+plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
197 (p : left = right) -> c + left = c + right
197 (p : left = right) -> c + left = c + right
198−plusMonotonicLeft left right c refl = refl
198+plusConstantLeft left right c refl = refl
199
199
200plusOneSucc : (right : Nat) -> 1 + right = S right
200plusOneSucc : (right : Nat) -> 1 + right = S right
201plusOneSucc n = refl
201plusOneSucc n = refl
@@ -302,6 +302,14 @@ minusOneSuccN : (n : Nat) -> S O = (S n) - n
302minusOneSuccN O = refl
302minusOneSuccN O = refl
303minusOneSuccN (S n) = minusOneSuccN n
303minusOneSuccN (S n) = minusOneSuccN n
304
304
305+minusSuccOne : (n : Nat) -> S n - 1 = n
306+minusSuccOne O = refl
307+minusSuccOne (S n) = refl
308+
309+minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
310+minusPlusZero O m = refl
311+minusPlusZero (S n) m = minusPlusZero n m
312+
305minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
313minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
306 left - centre - right = left - (centre + right)
314 left - centre - right = left - (centre + right)
307minusMinusMinusPlus O O right = refl
315minusMinusMinusPlus O O right = refl
@@ -311,6 +319,28 @@ minusMinusMinusPlus (S left) (S centre) right =
311 let inductiveHypothesis = minusMinusMinusPlus left centre right in
319 let inductiveHypothesis = minusMinusMinusPlus left centre right in
312 ?minusMinusMinusPlusStepCase
320 ?minusMinusMinusPlusStepCase
313
321
322+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
323+ (left + right) - (left + right') = right - right'
324+plusMinusLeftCancel O right right' = refl
325+plusMinusLeftCancel (S left) right right' =
326+ let inductiveHypothesis = plusMinusLeftCancel left right right' in
327+ ?plusMinusLeftCancelStepCase
328+
329+multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
330+ (left - centre) * right = (left * right) - (centre * right)
331+multDistributesOverMinusLeft O O right = refl
332+multDistributesOverMinusLeft (S left) O right =
333+ ?multDistributesOverMinusLeftBaseCase
334+multDistributesOverMinusLeft O (S centre) right = refl
335+multDistributesOverMinusLeft (S left) (S centre) right =
336+ let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
337+ ?multDistributesOverMinusLeftStepCase
338+
339+multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
340+ left * (centre - right) = (left * centre) - (left * right)
341+multDistributesOverMinusRight left centre right =
342+ ?multDistributesOverMinusRightBody
343+
314-- Power
344-- Power
315powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
345powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
316 base * (power base exp)
346 base * (power base exp)
@@ -365,6 +395,94 @@ minusSuccPred (S left) (S right) =
365 let inductiveHypothesis = minusSuccPred left right in
395 let inductiveHypothesis = minusSuccPred left right in
366 ?minusSuccPredStepCase'
396 ?minusSuccPredStepCase'
367
397
398+-- boolElim
399+boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
400+ S (boolElim cond t f) = boolElim cond (S t) (S f)
401+boolElimSuccSucc True t f = refl
402+boolElimSuccSucc False t f = refl
403+
404+boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
405+ left + (boolElim cond t f) = boolElim cond (left + t) (left + f)
406+boolElimPlusPlusLeft True left t f = refl
407+boolElimPlusPlusLeft False left t f = refl
408+
409+boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
410+ (boolElim cond t f) + right = boolElim cond (t + right) (f + right)
411+boolElimPlusPlusRight True right t f = refl
412+boolElimPlusPlusRight False right t f = refl
413+
414+boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->
415+ left * (boolElim cond t f) = boolElim cond (left * t) (left * f)
416+boolElimMultMultLeft True left t f = refl
417+boolElimMultMultLeft False left t f = refl
418+
419+boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->
420+ (boolElim cond t f) * right = boolElim cond (t * right) (f * right)
421+boolElimMultMultRight True right t f = refl
422+boolElimMultMultRight False right t f = refl
423+
424+-- Orders
425+lteNTrue : (n : Nat) -> lte n n = True
426+lteNTrue O = refl
427+lteNTrue (S n) = lteNTrue n
428+
429+lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
430+lteSuccZeroFalse O = refl
431+lteSuccZeroFalse (S n) = refl
432+
433+-- Minimum and maximum
434+minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
435+minimumZeroZeroRight O = refl
436+minimumZeroZeroRight (S right) = minimumZeroZeroRight right
437+
438+minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
439+minimumZeroZeroLeft O = refl
440+minimumZeroZeroLeft (S left) = refl
441+
442+minimumSuccSucc : (left : Nat) -> (right : Nat) ->
443+ minimum (S left) (S right) = S (minimum left right)
444+minimumSuccSucc O O = refl
445+minimumSuccSucc (S left) O = refl
446+minimumSuccSucc O (S right) = refl
447+minimumSuccSucc (S left) (S right) =
448+ let inductiveHypothesis = minimumSuccSucc left right in
449+ ?minimumSuccSuccStepCase
450+
451+minimumCommutative : (left : Nat) -> (right : Nat) ->
452+ minimum left right = minimum right left
453+minimumCommutative O O = refl
454+minimumCommutative O (S right) = refl
455+minimumCommutative (S left) O = refl
456+minimumCommutative (S left) (S right) =
457+ let inductiveHypothesis = minimumCommutative left right in
458+ ?minimumCommutativeStepCase
459+
460+maximumZeroNRight : (right : Nat) -> maximum O right = right
461+maximumZeroNRight O = refl
462+maximumZeroNRight (S right) = refl
463+
464+maximumZeroNLeft : (left : Nat) -> maximum left O = left
465+maximumZeroNLeft O = refl
466+maximumZeroNLeft (S left) = refl
467+
468+maximumSuccSucc : (left : Nat) -> (right : Nat) ->
469+ S (maximum left right) = maximum (S left) (S right)
470+maximumSuccSucc O O = refl
471+maximumSuccSucc (S left) O = refl
472+maximumSuccSucc O (S right) = refl
473+maximumSuccSucc (S left) (S right) =
474+ let inductiveHypothesis = maximumSuccSucc left right in
475+ ?maximumSuccSuccStepCase
476+
477+maximumCommutative : (left : Nat) -> (right : Nat) ->
478+ maximum left right = maximum right left
479+maximumCommutative O O = refl
480+maximumCommutative (S left) O = refl
481+maximumCommutative O (S right) = refl
482+maximumCommutative (S left) (S right) =
483+ let inductiveHypothesis = maximumCommutative left right in
484+ ?maximumCommutativeStepCase
485+
368--------------------------------------------------------------------------------
486--------------------------------------------------------------------------------
369-- Proofs
487-- Proofs
370--------------------------------------------------------------------------------
488--------------------------------------------------------------------------------
@@ -525,6 +643,61 @@ plusZeroRightNeutralStepCase = proof {
525 trivial;
643 trivial;
526}
644}
527
645
646+maximumCommutativeStepCase = proof {
647+ intros;
648+ rewrite (boolElimSuccSucc (lte left right) right left);
649+ rewrite (boolElimSuccSucc (lte right left) left right);
650+ rewrite inductiveHypothesis;
651+ trivial;
652+}
653+
654+maximumSuccSuccStepCase = proof {
655+ intros;
656+ rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
657+ trivial;
658+}
659+
660+minimumCommutativeStepCase = proof {
661+ intros;
662+ rewrite (boolElimSuccSucc (lte left right) left right);
663+ rewrite (boolElimSuccSucc (lte right left) right left);
664+ rewrite inductiveHypothesis;
665+ trivial;
666+}
667+
668+minimumSuccSuccStepCase = proof {
669+ intros;
670+ rewrite (boolElimSuccSucc (lte left right) (S left) (S right));
671+ trivial;
672+}
673+
674+multDistributesOverMinusRightBody = proof {
675+ intros;
676+ rewrite sym (multCommutative left (minus centre right));
677+ rewrite sym (multDistributesOverMinusLeft centre right left);
678+ rewrite sym (multCommutative centre left);
679+ rewrite sym (multCommutative right left);
680+ trivial;
681+}
682+
683+multDistributesOverMinusLeftStepCase = proof {
684+ intros;
685+ rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right));
686+ trivial;
687+}
688+
689+multDistributesOverMinusLeftBaseCase = proof {
690+ intros;
691+ rewrite (minusZeroRight (plus right (mult left right)));
692+ trivial;
693+}
694+
695+plusMinusLeftCancelStepCase = proof {
696+ intros;
697+ rewrite inductiveHypothesis;
698+ trivial;
699+}
700+
528minusMinusMinusPlusStepCase = proof {
701minusMinusMinusPlusStepCase = proof {
529 intros;
702 intros;
530 rewrite inductiveHypothesis;
703 rewrite inductiveHypothesis;