在idris中證明map id = id？

Question

我剛開始玩idris和定理證明一般。我可以在互聯網上查看大部分基本事實證明的例子，所以我想嘗試我自己的任意東西。所以，我想要寫一個證明長期在地圖的以下基本屬性：

map : (a -> b) -> List a -> List b 
prf : map id = id 

直覺，我能想象的證明應如何工作：取一個任意列表L和分析地圖ID L中的可能性。當l空着時，很明顯;當 l非空時，它基於函數應用程序保持相等的概念。 所以，我可以做這樣的事情：

prf' : (l : List a) -> map id l = id l 

這就像一個爲所有聲明。我怎樣才能把它變成所涉及功能平等的證明？

Answer 1

你不能。伊德里斯的類型理論（如Coq's和Agda's）不支持一般的擴展性。給定兩個功能f和g「行爲相同」，您將永遠無法證明Not (f = g)，但只有在f和g定義相同時才能證明f = g，直到alpha和eta等價。不幸的是，當你考慮高階函數時情況會變得更糟;在Coq標準庫中有這樣一個定理，但我現在似乎無法找到或記住它。