@@ -407,28 +407,29 @@ total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
407407plusZeroRightNeutral Z = Refl
408408plusZeroRightNeutral (S n) =
409409 let inductiveHypothesis = plusZeroRightNeutral n in
410− ?plusZeroRightNeutralStepCase
410+ rewrite inductiveHypothesis in Refl
411411
412412total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
413413 S (left + right) = left + (S right)
414414plusSuccRightSucc Z right = Refl
415415plusSuccRightSucc (S left) right =
416416 let inductiveHypothesis = plusSuccRightSucc left right in
417− ?plusSuccRightSuccStepCase
417+ rewrite inductiveHypothesis in Refl
418418
419419total plusCommutative : (left : Nat) -> (right : Nat) ->
420420 left + right = right + left
421−plusCommutative Z right = ?plusCommutativeBaseCase
421+plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
422422plusCommutative (S left) right =
423423 let inductiveHypothesis = plusCommutative left right in
424− ?plusCommutativeStepCase
424+ rewrite inductiveHypothesis in
425+ rewrite plusSuccRightSucc right left in Refl
425426
426427total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
427428 left + (centre + right) = (left + centre) + right
428429plusAssociative Z centre right = Refl
429430plusAssociative (S left) centre right =
430431 let inductiveHypothesis = plusAssociative left centre right in
431− ?plusAssociativeStepCase
432+ rewrite inductiveHypothesis in Refl
432433
433434total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
434435 (p : left = right) -> left + c = right + c
@@ -443,24 +444,26 @@ plusOneSucc n = Refl
443444
444445total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
445446 (p : left + right = left + right') -> right = right'
446−plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase
447+plusLeftCancel Z right right' p = p
447448plusLeftCancel (S left) right right' p =
448449 let inductiveHypothesis = plusLeftCancel left right right' in
449− ?plusLeftCancelStepCase
450+ inductiveHypothesis (succInjective _ _ p)
450451
451452total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
452453 (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
454457plusRightCancel left left' (S right) p =
455− let inductiveHypothesis = plusRightCancel left left' right in
456− ?plusRightCancelStepCase
458+ plusRightCancel left left' right
459+ (succInjective _ _ (rewrite plusSuccRightSucc left right in
460+ rewrite plusSuccRightSucc left' right in p))
457461
458462total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
459463 (p : left + right = left) -> right = Z
460−plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase
464+plusLeftLeftRightZero Z right p = p
461465plusLeftLeftRightZero (S left) right p =
462− let inductiveHypothesis = plusLeftLeftRightZero left right in
463− ?plusLeftLeftRightZeroStepCase
466+ plusLeftLeftRightZero left right (succInjective _ _ p)
464467
465468-- Mult
466469total multZeroLeftZero : (right : Nat) -> Z * right = Z
@@ -468,16 +471,18 @@ multZeroLeftZero right = Refl
468471
469472total multZeroRightZero : (left : Nat) -> left * Z = Z
470473multZeroRightZero Z = Refl
471−multZeroRightZero (S left) =
472− let inductiveHypothesis = multZeroRightZero left in
473− ?multZeroRightZeroStepCase
474+multZeroRightZero (S left) = multZeroRightZero left
474475
475476total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
476477 left * (S right) = left + (left * right)
477478multRightSuccPlus Z right = Refl
478479multRightSuccPlus (S left) right =
479480 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
481486
482487total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
483488 (S left) * right = right + (left * right)
@@ -485,43 +490,57 @@ multLeftSuccPlus left right = Refl
485490
486491total multCommutative : (left : Nat) -> (right : Nat) ->
487492 left * right = right * left
488−multCommutative Z right = ?multCommutativeBaseCase
493+multCommutative Z right = rewrite multZeroRightZero right in Refl
489494multCommutative (S left) right =
490495 let inductiveHypothesis = multCommutative left right in
491− ?multCommutativeStepCase
496+ rewrite inductiveHypothesis in
497+ rewrite multRightSuccPlus right left in
498+ Refl
492499
493500total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
494501 left * (centre + right) = (left * centre) + (left * right)
495502multDistributesOverPlusRight Z centre right = Refl
496503multDistributesOverPlusRight (S left) centre right =
497504 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
499512
500513total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
501514 (left + centre) * right = (left * right) + (centre * right)
502515multDistributesOverPlusLeft Z centre right = Refl
503516multDistributesOverPlusLeft (S left) centre right =
504517 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
506521
507522total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
508523 left * (centre * right) = (left * centre) * right
509524multAssociative Z centre right = Refl
510525multAssociative (S left) centre right =
511526 let inductiveHypothesis = multAssociative left centre right in
512− ?multAssociativeStepCase
527+ rewrite inductiveHypothesis in
528+ rewrite multDistributesOverPlusLeft centre (mult left centre) right in
529+ Refl
513530
514531total multOneLeftNeutral : (right : Nat) -> 1 * right = right
515532multOneLeftNeutral Z = Refl
516533multOneLeftNeutral (S right) =
517534 let inductiveHypothesis = multOneLeftNeutral right in
518− ?multOneLeftNeutralStepCase
535+ rewrite inductiveHypothesis in
536+ Refl
519537
520538total multOneRightNeutral : (left : Nat) -> left * 1 = left
521539multOneRightNeutral Z = Refl
522540multOneRightNeutral (S left) =
523541 let inductiveHypothesis = multOneRightNeutral left in
524− ?multOneRightNeutralStepCase
542+ rewrite inductiveHypothesis in
543+ Refl
525544
526545-- Minus
527546total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@@ -558,29 +577,37 @@ minusMinusMinusPlus (S left) Z right = Refl
558577minusMinusMinusPlus Z (S centre) right = Refl
559578minusMinusMinusPlus (S left) (S centre) right =
560579 let inductiveHypothesis = minusMinusMinusPlus left centre right in
561− ?minusMinusMinusPlusStepCase
580+ rewrite inductiveHypothesis in
581+ Refl
562582
563583total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
564584 (left + right) - (left + right') = right - right'
565585plusMinusLeftCancel Z right right' = Refl
566586plusMinusLeftCancel (S left) right right' =
567587 let inductiveHypothesis = plusMinusLeftCancel left right right' in
568− ?plusMinusLeftCancelStepCase
588+ rewrite inductiveHypothesis in
589+ Refl
569590
570591total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
571592 (left - centre) * right = (left * right) - (centre * right)
572593multDistributesOverMinusLeft Z Z right = Refl
573594multDistributesOverMinusLeft (S left) Z right =
574− ?multDistributesOverMinusLeftBaseCase
595+ rewrite (minusZeroRight (plus right (mult left right))) in Refl
575596multDistributesOverMinusLeft Z (S centre) right = Refl
576597multDistributesOverMinusLeft (S left) (S centre) right =
577598 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
579602
580603total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
581604 left * (centre - right) = (left * centre) - (left * right)
582605multDistributesOverMinusRight 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
584611
585612-- Power
586613total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =
@@ -589,10 +616,13 @@ powerSuccPowerLeft base exp = Refl
589616
590617total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
591618 (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
593621multPowerPowerPlus base (S exp) exp' =
594622 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
596626
597627total powerZeroOne : (base : Nat) -> power base 0 = S Z
598628powerZeroOne base = Refl
@@ -601,26 +631,27 @@ total powerOneNeutral : (base : Nat) -> power base 1 = base
601631powerOneNeutral Z = Refl
602632powerOneNeutral (S base) =
603633 let inductiveHypothesis = powerOneNeutral base in
604− ?powerOneNeutralStepCase
634+ rewrite inductiveHypothesis in Refl
605635
606636total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
607637powerOneSuccOne Z = Refl
608638powerOneSuccOne (S exp) =
609639 let inductiveHypothesis = powerOneSuccOne exp in
610− ?powerOneSuccOneStepCase
640+ rewrite inductiveHypothesis in Refl
611641
612642total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
613643powerSuccSuccMult Z = Refl
614−powerSuccSuccMult (S base) =
615− let inductiveHypothesis = powerSuccSuccMult base in
616− ?powerSuccSuccMultStepCase
644+powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
617645
618646total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
619647 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
621649powerPowerMultPower base exp (S exp') =
622650 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
624655
625656-- Pred
626657total predSucc : (n : Nat) -> pred (S n) = n
@@ -630,11 +661,10 @@ total minusSuccPred : (left : Nat) -> (right : Nat) ->
630661 left - (S right) = pred (left - right)
631662minusSuccPred Z right = Refl
632663minusSuccPred (S left) Z =
633− let inductiveHypothesis = minusSuccPred left Z in
634− ?minusSuccPredStepCase
664+ rewrite minusZeroRight left in Refl
635665minusSuccPred (S left) (S right) =
636666 let inductiveHypothesis = minusSuccPred left right in
637− ?minusSuccPredStepCase'
667+ rewrite inductiveHypothesis in Refl
638668
639669-- ifThenElse
640670total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->
@@ -717,9 +747,7 @@ total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
717747minimumSuccSucc Z Z = Refl
718748minimumSuccSucc (S left) Z = Refl
719749minimumSuccSucc Z (S right) = Refl
720−minimumSuccSucc (S left) (S right) =
721− let inductiveHypothesis = minimumSuccSucc left right in
722− ?minimumSuccSuccStepCase
750+minimumSuccSucc (S left) (S right) = Refl
723751
724752total maximumZeroNRight : (right : Nat) -> maximum Z right = right
725753maximumZeroNRight Z = Refl
@@ -734,9 +762,7 @@ total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
734762maximumSuccSucc Z Z = Refl
735763maximumSuccSucc (S left) Z = Refl
736764maximumSuccSucc Z (S right) = Refl
737−maximumSuccSucc (S left) (S right) =
738− let inductiveHypothesis = maximumSuccSucc left right in
739− ?maximumSuccSuccStepCase
765+maximumSuccSucc (S left) (S right) = Refl
740766
741767total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
742768sucMaxL Z = Refl
@@ -754,252 +780,3 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
754780sucMinR Z = Refl
755781sucMinR (S l) = cong (sucMinR l)
756782
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−}