SumSimplify.idr

module SumSimplify

%default total

-- from https://gist.github.com/iitalics/e060f27a04bba797f8bd3aa0ac04b3a3

-- 1+..+n = n*(n+1)/2

sumUpTo : Nat -> Nat
sumUpTo  Z    = Z
sumUpTo (S n) = S n + sumUpTo n

divTwoFloor : Nat -> Nat
divTwoFloor Z         = Z
divTwoFloor (S Z)     = Z
divTwoFloor (S (S n)) = S $ divTwoFloor n

divTwoDouble : (n : Nat) -> n = divTwoFloor (2*n)
divTwoDouble Z = Refl
divTwoDouble (S n) = rewrite multDistributesOverPlusRight 2 1 n in
                     cong $ divTwoDouble n

twoSumSimplify : (n : Nat) -> 2 * sumUpTo n = n * S n
twoSumSimplify Z = Refl
twoSumSimplify (S n) = 
  rewrite multDistributesOverPlusRight 2 (S n) (sumUpTo n) in
  rewrite twoSumSimplify n in  
  rewrite sym $ multDistributesOverPlusLeft 2 n (S n) in
  multCommutative (2 + n) (S n)

sumSimplify : (n : Nat) -> sumUpTo n = divTwoFloor (n * S n)
sumSimplify n = trans (divTwoDouble (sumUpTo n))
                      (cong {f=divTwoFloor} $ twoSumSimplify n)