在 idris 中证明 map id = id？

Question

我刚开始玩 idris 和一般的定理证明。我可以遵循互联网上大多数基本事实证明的示例，所以我想自己尝试一些任意的东西。所以，我想为map的以下基本属性写一个证明项：

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

这就像一个 for all 声明。我怎样才能把它变成所涉及的函数相等的证明？

Answer 1

你不能。 Idris 的类型理论（如 Coq 和 Agda 的）不支持一般外延性。给定两个“行为相同”的函数 f 和 g，您将永远无法证明 Not (f = g)，但如果定义了 f 和 g，您将只能证明 f = g相同，直到 alpha 和 eta 等价。不幸的是，当您考虑高阶函数时，情况只会变得更糟。 Coq 标准库中有一个关于此类的定理，但我现在似乎无法找到或记住它。