As per https://homes.cs.washington.edu/~jrw12/InductionExercises.html I am tring to prove sum and sum_cont are equivalent. I get to:
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 (\ans => k (x + ans))
sum_cont : List Nat -> Nat
sum_cont l = sum_cont' l (\x => x)
sum_cont_correct' : (xs : List Nat) -> (x : Nat) -> sum_cont' xs (\ans => plus x ans) = plus x (sum xs)
sum_cont_correct' [] acc = Refl
sum_cont_correct' (x :: xs) acc =
rewrite plusAssociative acc x (sum xs) in
?todo
Where the hole todo has type:
sum_cont' xs (\ans => plus acc (plus x ans)) = plus (plus acc x) (sum xs)
I'd like to apply the rewrite plusAssociative acc x ans, but ans is not in scope at the top. How do I apply the rewrite under the lambda, to a variable I can't bind?
The question How do I prove a "seemingly obvious" fact when relevant types are abstracted by a lambda in Idris? seems to answer some similar points, but ultimately suggests using cong, which is inappropriate here as I can't make the outer pieces similar until after I apply the inner rewrite.
You can't rewrite under lambdas unless you are willing to assume the functional extensionality axiom. In my opinion the answer you linked explains that very well.
By the way, a related system -- Coq has facilities (viz. the setoid_rewrite tactic) that make it easier to rewrite under binders (I tried to explain it in this answer). But I am not aware of its analogue in Idris.
However, you can do the proof without the axiom or some other machinery like setoids as follows.
Let's prove a more general lemma first:
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) = sum_cont_correct' (k . (x+)) xs
Now the proof of the sum_cont_correct lemma is just a one-liner:
sum_cont_correct : (xs : List Nat) -> sum_cont xs = sum xs
sum_cont_correct = sum_cont_correct' id