In Idris, use rewrite under a lambda
idris
Solution
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
Problem
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.