在伊德里斯，在lambda上使用重寫

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策略），使它更容易重寫下綁定（我試圖解釋它在this answer）。但我不知道它在伊德里斯的類比。

但是，您可以按照以下方式進行沒有公理或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