在 Idris 中，在 lambda 下使用 rewrite

Question

根据https://homes.cs.washington.edu/~jrw12/InductionExercises.html我试图证明sum和sum_cont是等价的。我得到：

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

孔 todo 的类型为：

sum_cont' xs (\ans => plus acc (plus x ans)) = plus (plus acc x) (sum xs)

我想应用重写 plusAssociative acc x ans，但 ans 不在顶部的范围内。如何将 lambda 下的重写应用于我无法绑定的变量？

问题 How do I prove a "seemingly obvious" fact when relevant types are abstracted by a lambda in Idris? 似乎回答了一些类似的观点，但最终建议使用 cong，这在这里是不合适的，因为在我应用内部重写之前我无法使外部部分相似.

Answer 1

除非您愿意假设函数外延公理，否则您无法在 lambda 表达式下重写。在我看来，您链接的答案很好地解释了这一点。

顺便说一下，一个相关的系统——Coq 有一些工具（即 setoid_rewrite 策略）可以更容易地在绑定器下重写（我试图在中解释它）。但我不知道它在 Idris 中的类似物。

但是，您可以在没有公理或其他一些机制（例如 setoids）的情况下进行证明，如下所示。

先证明一个更一般的引理：

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

现在 sum_cont_correct 引理的证明只是一行：

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

在 Idris 中，在 lambda 下使用 rewrite

In Idris, use rewrite under a lambda

idris