In Idris, use rewrite under a lambda

Question

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 (the answer you linked explains that in great detail). However, you can do the proof without the axiom or some other machinery like setoids. Spoiler alert: here is a gist that shows a possible approach. — Anton Trunov
Thanks! Could you transform that into an answer? I think it's the right thing. What the linked question doesn't really answer is why Idris doesn't ship with functional extensionality, but reddit.com/r/haskell/comments/3jw3xm/dependent_haskell_vs_idris/… seems to cover it — Neil Mitchell

Anton Trunov Anton Trunov · Accepted Answer · 2017-05-12T13:48:20

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

In Idris, use rewrite under a lambda

1 Answers