git.iko.soy/Idris-dev
on master help sign in
Further simplify Nat proofs
1f56ca8Nick Drozd
libs/prelude/Prelude/Nat.idr+14−23
compare with master
unifiedsplit
@@ -557,26 +557,21 @@ multCommutative (S left) right =
557 rewrite multRightSuccPlus right left in
557 rewrite multRightSuccPlus right left in
558 Refl
558 Refl
559
559
560−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
561− left * (centre + right) = (left * centre) + (left * right)
562−multDistributesOverPlusRight Z centre right = Refl
563−multDistributesOverPlusRight (S left) centre right =
564− let inductiveHypothesis = multDistributesOverPlusRight left centre right in
565− rewrite inductiveHypothesis in
566− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in
567− rewrite sym (plusAssociative centre (mult left centre) right) in
568− rewrite plusCommutative (mult left centre) right in
569− rewrite plusAssociative centre right (mult left centre) in
570− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in
571− Refl
572−
573total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
560total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
574 (left + centre) * right = (left * right) + (centre * right)
561 (left + centre) * right = (left * right) + (centre * right)
575−multDistributesOverPlusLeft left centre right =
562+multDistributesOverPlusLeft Z centre right = Refl
576− rewrite multCommutative (left + centre) right in
563+multDistributesOverPlusLeft (S k) centre right =
564+ rewrite multDistributesOverPlusLeft k centre right in
565+ rewrite plusAssociative right (k * right) (centre * right) in
566+ Refl
567+
568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
569+ left * (centre + right) = (left * centre) + (left * right)
570+multDistributesOverPlusRight left centre right =
571+ rewrite multCommutative left (centre + right) in
577− rewrite multCommutative left right in
572+ rewrite multCommutative left centre in
578− rewrite multCommutative centre right in
573+ rewrite multCommutative left right in
579− multDistributesOverPlusRight right left centre
574+ multDistributesOverPlusLeft centre right left
580
575
581total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
576total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
582 left * (centre * right) = (left * centre) * right
577 left * (centre * right) = (left * centre) * right
@@ -588,11 +583,7 @@ multAssociative (S left) centre right =
588 Refl
583 Refl
589
584
590total multOneLeftNeutral : (right : Nat) -> 1 * right = right
585total multOneLeftNeutral : (right : Nat) -> 1 * right = right
591−multOneLeftNeutral Z = Refl
586+multOneLeftNeutral right = plusZeroRightNeutral right
592−multOneLeftNeutral (S right) =
593− let inductiveHypothesis = multOneLeftNeutral right in
594− rewrite inductiveHypothesis in
595− Refl
596
587
597total multOneRightNeutral : (left : Nat) -> left * 1 = left
588total multOneRightNeutral : (left : Nat) -> left * 1 = left
598multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
589multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left