SumCont.idr

--http://stackoverflow.com/questions/43879173/in-idris-use-rewrite-under-a-lambda

%default total

sum : List Nat -> Nat
sum [] = 0
sum (x :: xs) = x + sum xs

sum_cont' : {a : Type} -> List Nat -> (Nat -> a) -> a
sum_cont' [] k = k 0
sum_cont' (x :: xs) k = sum_cont' xs (k . (+ x))

sum_cont : List Nat -> Nat
sum_cont l = sum_cont' l id

sum_cont_correct' : (k : Nat -> ty) -> (xs : List Nat) -> sum_cont' xs k = k (sum xs)
sum_cont_correct' k [] = Refl
sum_cont_correct' k (x :: xs) =
  rewrite plusCommutative x (sum xs) in
  sum_cont_correct' (k . (+ x)) xs

sum_cont_correct : (xs : List Nat) -> sum_cont xs = sum xs
sum_cont_correct = sum_cont_correct' id