git.iko.soy/Idris-dev
on master help sign in
Simplify some Nat proofs
7ecd2ffNick Drozd
libs/prelude/Prelude/Nat.idr+23−43
compare with master
unifiedsplit
@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =
512
512
513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
514 (p : left + right = left' + right) -> left = left'
514 (p : left + right = left' + right) -> left = left'
515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in
515+plusRightCancel left left' right p =
516− rewrite sym (plusZeroRightNeutral left') in
516+ plusLeftCancel right left left' $
517− p
517+ rewrite plusCommutative right left in
518−plusRightCancel left left' (S right) p =
518+ rewrite plusCommutative right left' in
519− plusRightCancel left left' right
519+ p
520− (succInjective _ _ (rewrite plusSuccRightSucc left right in
521− rewrite plusSuccRightSucc left' right in p))
522
520
523total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
521total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
524 (p : left + right = left) -> right = Z
522 (p : left + right = left) -> right = Z
525−plusLeftLeftRightZero Z right p = p
523+plusLeftLeftRightZero left right p =
526−plusLeftLeftRightZero (S left) right p =
524+ plusLeftCancel left right Z $
527− plusLeftLeftRightZero left right (succInjective _ _ p)
525+ rewrite plusZeroRightNeutral left in
526+ p
528
527
529-- Mult
528-- Mult
530total multZeroLeftZero : (right : Nat) -> Z * right = Z
529total multZeroLeftZero : (right : Nat) -> Z * right = Z
@@ -573,12 +572,11 @@ multDistributesOverPlusRight (S left) centre right =
573
572
574total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
573total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
575 (left + centre) * right = (left * right) + (centre * right)
574 (left + centre) * right = (left * right) + (centre * right)
576−multDistributesOverPlusLeft Z centre right = Refl
575+multDistributesOverPlusLeft left centre right =
577−multDistributesOverPlusLeft (S left) centre right =
576+ rewrite multCommutative (left + centre) right in
578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
577+ rewrite multCommutative left right in
579− rewrite inductiveHypothesis in
578+ rewrite multCommutative centre right in
580− rewrite plusAssociative right (mult left right) (mult centre right) in
579+ multDistributesOverPlusRight right left centre
581− Refl
582
580
583total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
581total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
584 left * (centre * right) = (left * centre) * right
582 left * (centre * right) = (left * centre) * right
@@ -597,11 +595,7 @@ multOneLeftNeutral (S right) =
597 Refl
595 Refl
598
596
599total multOneRightNeutral : (left : Nat) -> left * 1 = left
597total multOneRightNeutral : (left : Nat) -> left * 1 = left
600−multOneRightNeutral Z = Refl
598+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
601−multOneRightNeutral (S left) =
602− let inductiveHypothesis = multOneRightNeutral left in
603− rewrite inductiveHypothesis in
604− Refl
605
599
606-- Minus
600-- Minus
607total minusSuccSucc : (left : Nat) -> (right : Nat) ->
601total minusSuccSucc : (left : Nat) -> (right : Nat) ->
@@ -689,10 +683,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z
689powerZeroOne base = Refl
683powerZeroOne base = Refl
690
684
691total powerOneNeutral : (base : Nat) -> power base 1 = base
685total powerOneNeutral : (base : Nat) -> power base 1 = base
692−powerOneNeutral Z = Refl
686+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
693−powerOneNeutral (S base) =
694− let inductiveHypothesis = powerOneNeutral base in
695− rewrite inductiveHypothesis in Refl
696
687
697total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
688total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
698powerOneSuccOne Z = Refl
689powerOneSuccOne Z = Refl
@@ -701,8 +692,7 @@ powerOneSuccOne (S exp) =
701 rewrite inductiveHypothesis in Refl
692 rewrite inductiveHypothesis in Refl
702
693
703total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
694total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
704−powerSuccSuccMult Z = Refl
705−powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl
695+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl
706
696
707total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
697total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
708 power (power base exp) exp' = power base (exp * exp')
698 power (power base exp) exp' = power base (exp * exp')
@@ -796,34 +786,24 @@ minimumIdempotent Z = Refl
796minimumIdempotent (S k) = cong (minimumIdempotent k)
786minimumIdempotent (S k) = cong (minimumIdempotent k)
797
787
798total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
788total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
799−minimumZeroZeroRight Z = Refl
789+minimumZeroZeroRight right = Refl
800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right
801
790
802total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
791total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
803−minimumZeroZeroLeft Z = Refl
792+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
804−minimumZeroZeroLeft (S left) = Refl
805
793
806total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
794total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
807 minimum (S left) (S right) = S (minimum left right)
795 minimum (S left) (S right) = S (minimum left right)
808−minimumSuccSucc Z Z = Refl
796+minimumSuccSucc left right = Refl
809−minimumSuccSucc (S left) Z = Refl
810−minimumSuccSucc Z (S right) = Refl
811−minimumSuccSucc (S left) (S right) = Refl
812
797
813total maximumZeroNRight : (right : Nat) -> maximum Z right = right
798total maximumZeroNRight : (right : Nat) -> maximum Z right = right
814−maximumZeroNRight Z = Refl
799+maximumZeroNRight right = Refl
815−maximumZeroNRight (S right) = Refl
816
800
817total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
801total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
818−maximumZeroNLeft Z = Refl
802+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl
819−maximumZeroNLeft (S left) = Refl
820
803
821total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
804total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
822 S (maximum left right) = maximum (S left) (S right)
805 S (maximum left right) = maximum (S left) (S right)
823−maximumSuccSucc Z Z = Refl
806+maximumSuccSucc left right = Refl
824−maximumSuccSucc (S left) Z = Refl
825−maximumSuccSucc Z (S right) = Refl
826−maximumSuccSucc (S left) (S right) = Refl
827
807
828total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
808total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
829sucMaxL Z = Refl
809sucMaxL Z = Refl