git.iko.soy/Idris-dev
on master help sign in
Add assoc, commut, and idemp proofs for min and max
522c3d8mrb
libs/prelude/Prelude/Nat.idr+33−35
compare with master
unifiedsplit
@@ -631,8 +631,40 @@ lteSuccZeroFalse Z = refl
631lteSuccZeroFalse (S n) = refl
631lteSuccZeroFalse (S n) = refl
632
632
633-- 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+
634total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
635−minimumZeroZeroRight Z = refl
667+minimumZeroZeroRight Z = refl
636minimumZeroZeroRight (S right) = minimumZeroZeroRight right
668minimumZeroZeroRight (S right) = minimumZeroZeroRight right
637
669
638total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
@@ -648,15 +680,6 @@ minimumSuccSucc (S left) (S right) =
648 let inductiveHypothesis = minimumSuccSucc left right in
680 let inductiveHypothesis = minimumSuccSucc left right in
649 ?minimumSuccSuccStepCase
681 ?minimumSuccSuccStepCase
650
682
651−total minimumCommutative : (left : Nat) -> (right : Nat) ->
652− minimum left right = minimum right left
653−minimumCommutative Z Z = refl
654−minimumCommutative Z (S right) = refl
655−minimumCommutative (S left) Z = refl
656−minimumCommutative (S left) (S right) =
657− let inductiveHypothesis = minimumCommutative left right in
658− ?minimumCommutativeStepCase
659−
660total maximumZeroNRight : (right : Nat) -> maximum Z right = right
683total maximumZeroNRight : (right : Nat) -> maximum Z right = right
661maximumZeroNRight Z = refl
684maximumZeroNRight Z = refl
662maximumZeroNRight (S right) = refl
685maximumZeroNRight (S right) = refl
@@ -674,15 +697,6 @@ maximumSuccSucc (S left) (S right) =
674 let inductiveHypothesis = maximumSuccSucc left right in
697 let inductiveHypothesis = maximumSuccSucc left right in
675 ?maximumSuccSuccStepCase
698 ?maximumSuccSuccStepCase
676
699
677−total maximumCommutative : (left : Nat) -> (right : Nat) ->
678− maximum left right = maximum right left
679−maximumCommutative Z Z = refl
680−maximumCommutative (S left) Z = refl
681−maximumCommutative Z (S right) = refl
682−maximumCommutative (S left) (S right) =
683− let inductiveHypothesis = maximumCommutative left right in
684− ?maximumCommutativeStepCase
685−
686-- div and mod
700-- div and mod
687total modZeroZero : (n : Nat) -> mod 0 n = Z
701total modZeroZero : (n : Nat) -> mod 0 n = Z
688modZeroZero Z = refl
702modZeroZero Z = refl
@@ -848,28 +862,12 @@ plusZeroRightNeutralStepCase = proof {
848 trivial;
862 trivial;
849}
863}
850
864
851−maximumCommutativeStepCase = proof {
852− intros;
853− rewrite (boolElimSuccSucc (lte left right) right left);
854− rewrite (boolElimSuccSucc (lte right left) left right);
855− rewrite inductiveHypothesis;
856− trivial;
857−}
858−
859maximumSuccSuccStepCase = proof {
865maximumSuccSuccStepCase = proof {
860 intros;
866 intros;
861 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
867 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));
862 trivial;
868 trivial;
863}
869}
864
870
865−minimumCommutativeStepCase = proof {
866− intros;
867− rewrite (boolElimSuccSucc (lte left right) left right);
868− rewrite (boolElimSuccSucc (lte right left) right left);
869− rewrite inductiveHypothesis;
870− trivial;
871−}
872−
873minimumSuccSuccStepCase = proof {
871minimumSuccSuccStepCase = proof {
874 intros;
872 intros;
875 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));
873 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));