git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1330 from mrb/simplify_nat_max_min
7062857David Christiansen
libs/prelude/Prelude/Nat.idr+39−45
compare with master
unifiedsplit
@@ -146,19 +146,15 @@ gt left right = lt right left
146
146
147||| Find the least of two natural numbers
147||| Find the least of two natural numbers
148total minimum : Nat -> Nat -> Nat
148total minimum : Nat -> Nat -> Nat
149−minimum left right =
149+minimum Z m = Z
150− if lte left right then
150+minimum (S n) Z = Z
151− left
151+minimum (S n) (S m) = S (minimum n m)
152− else
153− right
154
152
155||| Find the greatest of two natural numbers
153||| Find the greatest of two natural numbers
156total maximum : Nat -> Nat -> Nat
154total maximum : Nat -> Nat -> Nat
157−maximum left right =
155+maximum Z m = m
158− if lte left right then
156+maximum (S n) Z = S n
159− right
157+maximum (S n) (S m) = S (maximum n m)
160− else
161− left
162
158
163--------------------------------------------------------------------------------
159--------------------------------------------------------------------------------
164-- Type class instances
160-- Type class instances
@@ -635,8 +631,40 @@ lteSuccZeroFalse Z = refl
635lteSuccZeroFalse (S n) = refl
631lteSuccZeroFalse (S n) = refl
636
632
637-- Minimum and maximum
633-- Minimum and maximum
634+total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
635+maximumAssociative Z c r = refl
636+maximumAssociative (S k) Z r = refl
637+maximumAssociative (S k) (S j) Z = refl
638+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl
639+
640+total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
641+maximumCommutative Z Z = refl
642+maximumCommutative Z (S k) = refl
643+maximumCommutative (S k) Z = refl
644+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl
645+
646+total maximumIdempotent : (n : Nat) -> maximum n n = n
647+maximumIdempotent Z = refl
648+maximumIdempotent (S k) = cong (maximumIdempotent k)
649+
650+total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
651+minimumAssociative Z c r = refl
652+minimumAssociative (S k) Z r = refl
653+minimumAssociative (S k) (S j) Z = refl
654+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl
655+
656+total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
657+minimumCommutative Z Z = refl
658+minimumCommutative Z (S k) = refl
659+minimumCommutative (S k) Z = refl
660+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl
661+
662+total minimumIdempotent : (n : Nat) -> minimum n n = n
663+minimumIdempotent Z = refl
664+minimumIdempotent (S k) = cong (minimumIdempotent k)
665+
638total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
639−minimumZeroZeroRight Z = refl
667+minimumZeroZeroRight Z = refl
640minimumZeroZeroRight (S right) = minimumZeroZeroRight right
668minimumZeroZeroRight (S right) = minimumZeroZeroRight right
641
669
642total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
@@ -652,15 +680,6 @@ minimumSuccSucc (S left) (S right) =
652 let inductiveHypothesis = minimumSuccSucc left right in
680 let inductiveHypothesis = minimumSuccSucc left right in
653 ?minimumSuccSuccStepCase
681 ?minimumSuccSuccStepCase
654
682
655−total minimumCommutative : (left : Nat) -> (right : Nat) ->
656− minimum left right = minimum right left
657−minimumCommutative Z Z = refl
658−minimumCommutative Z (S right) = refl
659−minimumCommutative (S left) Z = refl
660−minimumCommutative (S left) (S right) =
661− let inductiveHypothesis = minimumCommutative left right in
662− ?minimumCommutativeStepCase
663−
664total maximumZeroNRight : (right : Nat) -> maximum Z right = right
683total maximumZeroNRight : (right : Nat) -> maximum Z right = right
665maximumZeroNRight Z = refl
684maximumZeroNRight Z = refl
666maximumZeroNRight (S right) = refl
685maximumZeroNRight (S right) = refl
@@ -678,15 +697,6 @@ maximumSuccSucc (S left) (S right) =
678 let inductiveHypothesis = maximumSuccSucc left right in
697 let inductiveHypothesis = maximumSuccSucc left right in
679 ?maximumSuccSuccStepCase
698 ?maximumSuccSuccStepCase
680
699
681−total maximumCommutative : (left : Nat) -> (right : Nat) ->
682− maximum left right = maximum right left
683−maximumCommutative Z Z = refl
684−maximumCommutative (S left) Z = refl
685−maximumCommutative Z (S right) = refl
686−maximumCommutative (S left) (S right) =
687− let inductiveHypothesis = maximumCommutative left right in
688− ?maximumCommutativeStepCase
689−
690-- div and mod
700-- div and mod
691total modZeroZero : (n : Nat) -> mod 0 n = Z
701total modZeroZero : (n : Nat) -> mod 0 n = Z
692modZeroZero Z = refl
702modZeroZero Z = refl
@@ -852,28 +862,12 @@ plusZeroRightNeutralStepCase = proof {
852 trivial;
862 trivial;
853}
863}
854
864
855−maximumCommutativeStepCase = proof {
856− intros;
857− rewrite (boolElimSuccSucc (lte left right) right left);
858− rewrite (boolElimSuccSucc (lte right left) left right);
859− rewrite inductiveHypothesis;
860− trivial;
861−}
862−
863maximumSuccSuccStepCase = proof {
865maximumSuccSuccStepCase = proof {
864 intros;
866 intros;
865 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
867 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
866 trivial;
868 trivial;
867}
869}
868
870
869−minimumCommutativeStepCase = proof {
870− intros;
871− rewrite (boolElimSuccSucc (lte left right) left right);
872− rewrite (boolElimSuccSucc (lte right left) right left);
873− rewrite inductiveHypothesis;
874− trivial;
875−}
876−
877minimumSuccSuccStepCase = proof {
871minimumSuccSuccStepCase = proof {
878 intros;
872 intros;
879 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));
873 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));