在idris中证明地图id = id？

Question

我只是开始玩idris和定理证明一般.我可以在互联网上关注大多数基本事实证据的例子,所以我想尝试一些我自己的任意事物.所以,我想为map的以下基本属性编写一个证明术语:

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

直觉上,我可以想象证明应该如何工作:获取任意列表l并分析map id l的可能性.如果l是空的,那很明显; 当l非空时,它基于函数应用程序保持相等的概念.所以,我可以这样做:

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

这就像一个所有声明.如何将其转化为所涉及功能相等的证明？

Answer 1

你不能.伊德里斯的类型理论(如Coq和Agda)不支持一般的扩展性.鉴于两种功能f,并g认为"行为相同的",你将永远无法证明Not (f = g),但你只能够证明f = g,如果f和g的定义相同,可达α和ETA等价左右.不幸的是,当你考虑更高阶函数时,情况会变得更糟; 在Coq标准库中有关于此类的定理,但我现在似乎无法找到或记住它.