git.iko.soy/Idris-dev
on master help sign in
Remove tactic proofs in Nat
e2b1427Edwin Brady
libs/prelude/Prelude/Nat.idr+73−296
compare with master
unifiedsplit
@@ -407,28 +407,29 @@ total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
407plusZeroRightNeutral Z = Refl
407plusZeroRightNeutral Z = Refl
408plusZeroRightNeutral (S n) =
408plusZeroRightNeutral (S n) =
409 let inductiveHypothesis = plusZeroRightNeutral n in
409 let inductiveHypothesis = plusZeroRightNeutral n in
410− ?plusZeroRightNeutralStepCase
410+ rewrite inductiveHypothesis in Refl
411
411
412total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
412total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
413 S (left + right) = left + (S right)
413 S (left + right) = left + (S right)
414plusSuccRightSucc Z right = Refl
414plusSuccRightSucc Z right = Refl
415plusSuccRightSucc (S left) right =
415plusSuccRightSucc (S left) right =
416 let inductiveHypothesis = plusSuccRightSucc left right in
416 let inductiveHypothesis = plusSuccRightSucc left right in
417− ?plusSuccRightSuccStepCase
417+ rewrite inductiveHypothesis in Refl
418
418
419total plusCommutative : (left : Nat) -> (right : Nat) ->
419total plusCommutative : (left : Nat) -> (right : Nat) ->
420 left + right = right + left
420 left + right = right + left
421−plusCommutative Z right = ?plusCommutativeBaseCase
421+plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
422plusCommutative (S left) right =
422plusCommutative (S left) right =
423 let inductiveHypothesis = plusCommutative left right in
423 let inductiveHypothesis = plusCommutative left right in
424− ?plusCommutativeStepCase
424+ rewrite inductiveHypothesis in
425+ rewrite plusSuccRightSucc right left in Refl
425
426
426total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
427total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
427 left + (centre + right) = (left + centre) + right
428 left + (centre + right) = (left + centre) + right
428plusAssociative Z centre right = Refl
429plusAssociative Z centre right = Refl
429plusAssociative (S left) centre right =
430plusAssociative (S left) centre right =
430 let inductiveHypothesis = plusAssociative left centre right in
431 let inductiveHypothesis = plusAssociative left centre right in
431− ?plusAssociativeStepCase
432+ rewrite inductiveHypothesis in Refl
432
433
433total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
434total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
434 (p : left = right) -> left + c = right + c
435 (p : left = right) -> left + c = right + c
@@ -443,24 +444,26 @@ plusOneSucc n = Refl
443
444
444total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
445total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
445 (p : left + right = left + right') -> right = right'
446 (p : left + right = left + right') -> right = right'
446−plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase
447+plusLeftCancel Z right right' p = p
447plusLeftCancel (S left) right right' p =
448plusLeftCancel (S left) right right' p =
448 let inductiveHypothesis = plusLeftCancel left right right' in
449 let inductiveHypothesis = plusLeftCancel left right right' in
449− ?plusLeftCancelStepCase
450+ inductiveHypothesis (succInjective _ _ p)
450
451
451total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
452total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
452 (p : left + right = left' + right) -> left = left'
453 (p : left + right = left' + right) -> left = left'
453−plusRightCancel left left' Z p = ?plusRightCancelBaseCase
454+plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
455+ rewrite sym (plusZeroRightNeutral left') in
456+ p
454plusRightCancel left left' (S right) p =
457plusRightCancel left left' (S right) p =
455− let inductiveHypothesis = plusRightCancel left left' right in
458+ plusRightCancel left left' right
456− ?plusRightCancelStepCase
459+ (succInjective _ _ (rewrite plusSuccRightSucc left right in
460+ rewrite plusSuccRightSucc left' right in p))
457
461
458total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
462total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
459 (p : left + right = left) -> right = Z
463 (p : left + right = left) -> right = Z
460−plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase
464+plusLeftLeftRightZero Z right p = p
461plusLeftLeftRightZero (S left) right p =
465plusLeftLeftRightZero (S left) right p =
462− let inductiveHypothesis = plusLeftLeftRightZero left right in
466+ plusLeftLeftRightZero left right (succInjective _ _ p)
463− ?plusLeftLeftRightZeroStepCase
464
467
465-- Mult
468-- Mult
466total multZeroLeftZero : (right : Nat) -> Z * right = Z
469total multZeroLeftZero : (right : Nat) -> Z * right = Z
@@ -468,16 +471,18 @@ multZeroLeftZero right = Refl
468
471
469total multZeroRightZero : (left : Nat) -> left * Z = Z
472total multZeroRightZero : (left : Nat) -> left * Z = Z
470multZeroRightZero Z = Refl
473multZeroRightZero Z = Refl
471−multZeroRightZero (S left) =
474+multZeroRightZero (S left) = multZeroRightZero left
472− let inductiveHypothesis = multZeroRightZero left in
473− ?multZeroRightZeroStepCase
474
475
475total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
476total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
476 left * (S right) = left + (left * right)
477 left * (S right) = left + (left * right)
477multRightSuccPlus Z right = Refl
478multRightSuccPlus Z right = Refl
478multRightSuccPlus (S left) right =
479multRightSuccPlus (S left) right =
479 let inductiveHypothesis = multRightSuccPlus left right in
480 let inductiveHypothesis = multRightSuccPlus left right in
480− ?multRightSuccPlusStepCase
481+ rewrite inductiveHypothesis in
482+ rewrite plusAssociative left right (mult left right) in
483+ rewrite plusAssociative right left (mult left right) in
484+ rewrite plusCommutative right left in
485+ Refl
481
486
482total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
487total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
483 (S left) * right = right + (left * right)
488 (S left) * right = right + (left * right)
@@ -485,43 +490,57 @@ multLeftSuccPlus left right = Refl
485
490
486total multCommutative : (left : Nat) -> (right : Nat) ->
491total multCommutative : (left : Nat) -> (right : Nat) ->
487 left * right = right * left
492 left * right = right * left
488−multCommutative Z right = ?multCommutativeBaseCase
493+multCommutative Z right = rewrite multZeroRightZero right in Refl
489multCommutative (S left) right =
494multCommutative (S left) right =
490 let inductiveHypothesis = multCommutative left right in
495 let inductiveHypothesis = multCommutative left right in
491− ?multCommutativeStepCase
496+ rewrite inductiveHypothesis in
497+ rewrite multRightSuccPlus right left in
498+ Refl
492
499
493total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
500total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
494 left * (centre + right) = (left * centre) + (left * right)
501 left * (centre + right) = (left * centre) + (left * right)
495multDistributesOverPlusRight Z centre right = Refl
502multDistributesOverPlusRight Z centre right = Refl
496multDistributesOverPlusRight (S left) centre right =
503multDistributesOverPlusRight (S left) centre right =
497 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
504 let inductiveHypothesis = multDistributesOverPlusRight left centre right in
498− ?multDistributesOverPlusRightStepCase
505+ rewrite inductiveHypothesis in
506+ rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
507+ rewrite sym (plusAssociative centre (mult left centre) right) in
508+ rewrite plusCommutative (mult left centre) right in
509+ rewrite plusAssociative centre right (mult left centre) in
510+ rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in
511+ Refl
499
512
500total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
513total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
501 (left + centre) * right = (left * right) + (centre * right)
514 (left + centre) * right = (left * right) + (centre * right)
502multDistributesOverPlusLeft Z centre right = Refl
515multDistributesOverPlusLeft Z centre right = Refl
503multDistributesOverPlusLeft (S left) centre right =
516multDistributesOverPlusLeft (S left) centre right =
504 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
517 let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
505− ?multDistributesOverPlusLeftStepCase
518+ rewrite inductiveHypothesis in
519+ rewrite plusAssociative right (mult left right) (mult centre right) in
520+ Refl
506
521
507total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
522total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
508 left * (centre * right) = (left * centre) * right
523 left * (centre * right) = (left * centre) * right
509multAssociative Z centre right = Refl
524multAssociative Z centre right = Refl
510multAssociative (S left) centre right =
525multAssociative (S left) centre right =
511 let inductiveHypothesis = multAssociative left centre right in
526 let inductiveHypothesis = multAssociative left centre right in
512− ?multAssociativeStepCase
527+ rewrite inductiveHypothesis in
528+ rewrite multDistributesOverPlusLeft centre (mult left centre) right in
529+ Refl
513
530
514total multOneLeftNeutral : (right : Nat) -> 1 * right = right
531total multOneLeftNeutral : (right : Nat) -> 1 * right = right
515multOneLeftNeutral Z = Refl
532multOneLeftNeutral Z = Refl
516multOneLeftNeutral (S right) =
533multOneLeftNeutral (S right) =
517 let inductiveHypothesis = multOneLeftNeutral right in
534 let inductiveHypothesis = multOneLeftNeutral right in
518− ?multOneLeftNeutralStepCase
535+ rewrite inductiveHypothesis in
536+ Refl
519
537
520total multOneRightNeutral : (left : Nat) -> left * 1 = left
538total multOneRightNeutral : (left : Nat) -> left * 1 = left
521multOneRightNeutral Z = Refl
539multOneRightNeutral Z = Refl
522multOneRightNeutral (S left) =
540multOneRightNeutral (S left) =
523 let inductiveHypothesis = multOneRightNeutral left in
541 let inductiveHypothesis = multOneRightNeutral left in
524− ?multOneRightNeutralStepCase
542+ rewrite inductiveHypothesis in
543+ Refl
525
544
526-- Minus
545-- Minus
527total minusSuccSucc : (left : Nat) -> (right : Nat) ->
546total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@@ -558,29 +577,37 @@ minusMinusMinusPlus (S left) Z right = Refl
558minusMinusMinusPlus Z (S centre) right = Refl
577minusMinusMinusPlus Z (S centre) right = Refl
559minusMinusMinusPlus (S left) (S centre) right =
578minusMinusMinusPlus (S left) (S centre) right =
560 let inductiveHypothesis = minusMinusMinusPlus left centre right in
579 let inductiveHypothesis = minusMinusMinusPlus left centre right in
561− ?minusMinusMinusPlusStepCase
580+ rewrite inductiveHypothesis in
581+ Refl
562
582
563total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
583total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
564 (left + right) - (left + right') = right - right'
584 (left + right) - (left + right') = right - right'
565plusMinusLeftCancel Z right right' = Refl
585plusMinusLeftCancel Z right right' = Refl
566plusMinusLeftCancel (S left) right right' =
586plusMinusLeftCancel (S left) right right' =
567 let inductiveHypothesis = plusMinusLeftCancel left right right' in
587 let inductiveHypothesis = plusMinusLeftCancel left right right' in
568− ?plusMinusLeftCancelStepCase
588+ rewrite inductiveHypothesis in
589+ Refl
569
590
570total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
591total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
571 (left - centre) * right = (left * right) - (centre * right)
592 (left - centre) * right = (left * right) - (centre * right)
572multDistributesOverMinusLeft Z Z right = Refl
593multDistributesOverMinusLeft Z Z right = Refl
573multDistributesOverMinusLeft (S left) Z right =
594multDistributesOverMinusLeft (S left) Z right =
574− ?multDistributesOverMinusLeftBaseCase
595+ rewrite (minusZeroRight (plus right (mult left right))) in Refl
575multDistributesOverMinusLeft Z (S centre) right = Refl
596multDistributesOverMinusLeft Z (S centre) right = Refl
576multDistributesOverMinusLeft (S left) (S centre) right =
597multDistributesOverMinusLeft (S left) (S centre) right =
577 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
598 let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
578− ?multDistributesOverMinusLeftStepCase
599+ rewrite inductiveHypothesis in
600+ rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
601+ Refl
579
602
580total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
603total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
581 left * (centre - right) = (left * centre) - (left * right)
604 left * (centre - right) = (left * centre) - (left * right)
582multDistributesOverMinusRight left centre right =
605multDistributesOverMinusRight left centre right =
583− ?multDistributesOverMinusRightBody
606+ rewrite multCommutative left (minus centre right) in
607+ rewrite multDistributesOverMinusLeft centre right left in
608+ rewrite multCommutative centre left in
609+ rewrite multCommutative right left in
610+ Refl
584
611
585-- Power
612-- Power
586total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
613total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
@@ -589,10 +616,13 @@ powerSuccPowerLeft base exp = Refl
589
616
590total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
617total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
591 (power base exp) * (power base exp') = power base (exp + exp')
618 (power base exp) * (power base exp') = power base (exp + exp')
592−multPowerPowerPlus base Z exp' = ?multPowerPowerPlusBaseCase
619+multPowerPowerPlus base Z exp' =
620+ rewrite sym (plusZeroRightNeutral (power base exp')) in Refl
593multPowerPowerPlus base (S exp) exp' =
621multPowerPowerPlus base (S exp) exp' =
594 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
622 let inductiveHypothesis = multPowerPowerPlus base exp exp' in
595− ?multPowerPowerPlusStepCase
623+ rewrite sym inductiveHypothesis in
624+ rewrite sym (multAssociative base (power base exp) (power base exp')) in
625+ Refl
596
626
597total powerZeroOne : (base : Nat) -> power base 0 = S Z
627total powerZeroOne : (base : Nat) -> power base 0 = S Z
598powerZeroOne base = Refl
628powerZeroOne base = Refl
@@ -601,26 +631,27 @@ total powerOneNeutral : (base : Nat) -> power base 1 = base
601powerOneNeutral Z = Refl
631powerOneNeutral Z = Refl
602powerOneNeutral (S base) =
632powerOneNeutral (S base) =
603 let inductiveHypothesis = powerOneNeutral base in
633 let inductiveHypothesis = powerOneNeutral base in
604− ?powerOneNeutralStepCase
634+ rewrite inductiveHypothesis in Refl
605
635
606total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
636total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
607powerOneSuccOne Z = Refl
637powerOneSuccOne Z = Refl
608powerOneSuccOne (S exp) =
638powerOneSuccOne (S exp) =
609 let inductiveHypothesis = powerOneSuccOne exp in
639 let inductiveHypothesis = powerOneSuccOne exp in
610− ?powerOneSuccOneStepCase
640+ rewrite inductiveHypothesis in Refl
611
641
612total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
642total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
613powerSuccSuccMult Z = Refl
643powerSuccSuccMult Z = Refl
614−powerSuccSuccMult (S base) =
644+powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
615− let inductiveHypothesis = powerSuccSuccMult base in
616− ?powerSuccSuccMultStepCase
617
645
618total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
646total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
619 power (power base exp) exp' = power base (exp * exp')
647 power (power base exp) exp' = power base (exp * exp')
620−powerPowerMultPower base exp Z = ?powerPowerMultPowerBaseCase
648+powerPowerMultPower base exp Z = rewrite multZeroRightZero exp in Refl
621powerPowerMultPower base exp (S exp') =
649powerPowerMultPower base exp (S exp') =
622 let inductiveHypothesis = powerPowerMultPower base exp exp' in
650 let inductiveHypothesis = powerPowerMultPower base exp exp' in
623− ?powerPowerMultPowerStepCase
651+ rewrite inductiveHypothesis in
652+ rewrite multRightSuccPlus exp exp' in
653+ rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in
654+ Refl
624
655
625-- Pred
656-- Pred
626total predSucc : (n : Nat) -> pred (S n) = n
657total predSucc : (n : Nat) -> pred (S n) = n
@@ -630,11 +661,10 @@ total minusSuccPred : (left : Nat) -> (right : Nat) ->
630 left - (S right) = pred (left - right)
661 left - (S right) = pred (left - right)
631minusSuccPred Z right = Refl
662minusSuccPred Z right = Refl
632minusSuccPred (S left) Z =
663minusSuccPred (S left) Z =
633− let inductiveHypothesis = minusSuccPred left Z in
664+ rewrite minusZeroRight left in Refl
634− ?minusSuccPredStepCase
635minusSuccPred (S left) (S right) =
665minusSuccPred (S left) (S right) =
636 let inductiveHypothesis = minusSuccPred left right in
666 let inductiveHypothesis = minusSuccPred left right in
637− ?minusSuccPredStepCase'
667+ rewrite inductiveHypothesis in Refl
638
668
639-- ifThenElse
669-- ifThenElse
640total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
670total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
@@ -717,9 +747,7 @@ total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
717minimumSuccSucc Z Z = Refl
747minimumSuccSucc Z Z = Refl
718minimumSuccSucc (S left) Z = Refl
748minimumSuccSucc (S left) Z = Refl
719minimumSuccSucc Z (S right) = Refl
749minimumSuccSucc Z (S right) = Refl
720−minimumSuccSucc (S left) (S right) =
750+minimumSuccSucc (S left) (S right) = Refl
721− let inductiveHypothesis = minimumSuccSucc left right in
722− ?minimumSuccSuccStepCase
723
751
724total maximumZeroNRight : (right : Nat) -> maximum Z right = right
752total maximumZeroNRight : (right : Nat) -> maximum Z right = right
725maximumZeroNRight Z = Refl
753maximumZeroNRight Z = Refl
@@ -734,9 +762,7 @@ total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
734maximumSuccSucc Z Z = Refl
762maximumSuccSucc Z Z = Refl
735maximumSuccSucc (S left) Z = Refl
763maximumSuccSucc (S left) Z = Refl
736maximumSuccSucc Z (S right) = Refl
764maximumSuccSucc Z (S right) = Refl
737−maximumSuccSucc (S left) (S right) =
765+maximumSuccSucc (S left) (S right) = Refl
738− let inductiveHypothesis = maximumSuccSucc left right in
739− ?maximumSuccSuccStepCase
740
766
741total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
767total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
742sucMaxL Z = Refl
768sucMaxL Z = Refl
@@ -754,252 +780,3 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
754sucMinR Z = Refl
780sucMinR Z = Refl
755sucMinR (S l) = cong (sucMinR l)
781sucMinR (S l) = cong (sucMinR l)
756
782
757−--------------------------------------------------------------------------------
758−-- Proofs
759−--------------------------------------------------------------------------------
760−
761−powerPowerMultPowerStepCase = proof {
762− intros;
763− rewrite sym inductiveHypothesis;
764− rewrite sym (multRightSuccPlus exp exp');
765− rewrite (multPowerPowerPlus base exp (mult exp exp'));
766− trivial;
767−}
768−
769−powerPowerMultPowerBaseCase = proof {
770− intros;
771− rewrite sym (multZeroRightZero exp);
772− trivial;
773−}
774−
775−powerSuccSuccMultStepCase = proof {
776− intros;
777− rewrite (multOneRightNeutral base);
778− rewrite sym (multOneRightNeutral base);
779− trivial;
780−}
781−
782−powerOneSuccOneStepCase = proof {
783− intros;
784− rewrite inductiveHypothesis;
785− rewrite sym (plusZeroRightNeutral (power (S Z) exp));
786− trivial;
787−}
788−
789−powerOneNeutralStepCase = proof {
790− intros;
791− rewrite inductiveHypothesis;
792− trivial;
793−}
794−
795−multAssociativeStepCase = proof {
796− intros;
797− rewrite sym (multDistributesOverPlusLeft centre (mult left centre) right);
798− rewrite inductiveHypothesis;
799− trivial;
800−}
801−
802−minusSuccPredStepCase' = proof {
803− intros;
804− rewrite sym inductiveHypothesis;
805− trivial;
806−}
807−
808−minusSuccPredStepCase = proof {
809− intros;
810− rewrite (minusZeroRight left);
811− trivial;
812−}
813−
814−multPowerPowerPlusStepCase = proof {
815− intros;
816− rewrite inductiveHypothesis;
817− rewrite (multAssociative base (power base exp) (power base exp'));
818− trivial;
819−}
820−
821−multPowerPowerPlusBaseCase = proof {
822− intros;
823− rewrite (plusZeroRightNeutral (power base exp'));
824− trivial;
825−}
826−
827−multOneRightNeutralStepCase = proof {
828− intros;
829− rewrite inductiveHypothesis;
830− trivial;
831−}
832−
833−multOneLeftNeutralStepCase = proof {
834− intros;
835− rewrite (plusZeroRightNeutral right);
836− trivial;
837−}
838−
839−multDistributesOverPlusLeftStepCase = proof {
840− intros;
841− rewrite sym inductiveHypothesis;
842− rewrite sym (plusAssociative right (mult left right) (mult centre right));
843− trivial;
844−}
845−
846−multDistributesOverPlusRightStepCase = proof {
847− intros;
848− rewrite sym inductiveHypothesis;
849− rewrite sym (plusAssociative (plus centre (mult left centre)) right (mult left right));
850− rewrite (plusAssociative centre (mult left centre) right);
851− rewrite sym (plusCommutative (mult left centre) right);
852− rewrite sym (plusAssociative centre right (mult left centre));
853− rewrite sym (plusAssociative (plus centre right) (mult left centre) (mult left right));
854− trivial;
855−}
856−
857−multCommutativeStepCase = proof {
858− intros;
859− rewrite sym (multRightSuccPlus right left);
860− rewrite inductiveHypothesis;
861− trivial;
862−}
863−
864−multCommutativeBaseCase = proof {
865− intros;
866− rewrite (multZeroRightZero right);
867− trivial;
868−}
869−
870−multRightSuccPlusStepCase = proof {
871− intros;
872− rewrite inductiveHypothesis;
873− rewrite sym inductiveHypothesis;
874− rewrite sym (plusAssociative right left (mult left right));
875− rewrite sym (plusCommutative right left);
876− rewrite (plusAssociative left right (mult left right));
877− trivial;
878−}
879−
880−multZeroRightZeroStepCase = proof {
881− intros;
882− rewrite inductiveHypothesis;
883− trivial;
884−}
885−
886−plusAssociativeStepCase = proof {
887− intros;
888− rewrite inductiveHypothesis;
889− trivial;
890−}
891−
892−plusCommutativeStepCase = proof {
893− intros;
894− rewrite (plusSuccRightSucc right left);
895− rewrite inductiveHypothesis;
896− trivial;
897−}
898−
899−plusSuccRightSuccStepCase = proof {
900− intros;
901− rewrite inductiveHypothesis;
902− trivial;
903−}
904−
905−plusCommutativeBaseCase = proof {
906− intros;
907− rewrite sym (plusZeroRightNeutral right);
908− trivial;
909−}
910−
911−plusZeroRightNeutralStepCase = proof {
912− intros;
913− rewrite inductiveHypothesis;
914− trivial;
915−}
916−
917−maximumSuccSuccStepCase = proof {
918− intros;
919− rewrite sym (ifThenElseSuccSucc (lte left right) (S right) (S left));
920− trivial;
921−}
922−
923−minimumSuccSuccStepCase = proof {
924− intros;
925− rewrite (ifThenElseSuccSucc (lte left right) (S left) (S right));
926− trivial;
927−}
928−
929−multDistributesOverMinusRightBody = proof {
930− intros;
931− rewrite sym (multCommutative left (minus centre right));
932− rewrite sym (multDistributesOverMinusLeft centre right left);
933− rewrite sym (multCommutative centre left);
934− rewrite sym (multCommutative right left);
935− trivial;
936−}
937−
938−multDistributesOverMinusLeftStepCase = proof {
939− intros;
940− rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right));
941− trivial;
942−}
943−
944−multDistributesOverMinusLeftBaseCase = proof {
945− intros;
946− rewrite (minusZeroRight (plus right (mult left right)));
947− trivial;
948−}
949−
950−plusMinusLeftCancelStepCase = proof {
951− intros;
952− rewrite inductiveHypothesis;
953− trivial;
954−}
955−
956−minusMinusMinusPlusStepCase = proof {
957− intros;
958− rewrite inductiveHypothesis;
959− trivial;
960−}
961−
962−plusLeftLeftRightZeroBaseCase = proof {
963− intros;
964− rewrite p;
965− trivial;
966−}
967−
968−plusLeftLeftRightZeroStepCase = proof {
969− intros;
970− refine inductiveHypothesis;
971− let p' = succInjective (plus left right) left p;
972− rewrite p';
973− trivial;
974−}
975−
976−plusRightCancelStepCase = proof {
977− intros;
978− refine inductiveHypothesis;
979− refine succInjective _ _ ?;
980− rewrite sym (plusSuccRightSucc left right);
981− rewrite sym (plusSuccRightSucc left' right);
982− rewrite p;
983− trivial;
984−}
985−
986−plusRightCancelBaseCase = proof {
987− intros;
988− rewrite (plusZeroRightNeutral left);
989− rewrite (plusZeroRightNeutral left');
990− rewrite p;
991− trivial;
992−}
993−
994−plusLeftCancelStepCase = proof {
995− intros;
996− let injectiveProof = succInjective (plus left right) (plus left right') p;
997− rewrite (inductiveHypothesis injectiveProof);
998− trivial;
999−}
1000−
1001−plusLeftCancelBaseCase = proof {
1002− intros;
1003− rewrite p;
1004− trivial;
1005−}