Idris：有没有办法在等式证明中引用抽象变量？

Question

这个问题最简单的例子（但不是我能展示的唯一例子）是：假设我得到了一个高阶函数f : (a -> b) -> c。我想证明f = (\g => f (\x => g x))。

根据我自己的推理，它应该非常简单：只需应用 eta 等价两次（一次在内部，然后在外部）。

如果我想证明f = (\x => f x)，一个简单的Refl 就足够了：这让我认为“Idris 知道 eta 等价”。但话又说回来，同样的解决方案不适用于f = (\g => f (\x => g x))。

那时，我尝试使用rewrite，但找不到在(\g => f (\x => g x)) 中引用g 的方法：

lemma : {g : a -> b} -> g = (\x => g x)
lemma = Refl

theorem : {f : (a -> b) -> c} ->
          f = (\g => f (\x => g x))
theorem = rewrite (lemma {g = _}) in Refl

但是，当然，Idris 无法弄清楚 _ 应该是什么，我也不知道。

当然，这可以进一步简化为证明(\g => f g) = (\g => f (\x => g x)) 的问题，因为 Idris 知道相等是传递的并且知道 eta 等价（至少当它没有“隐藏”在 lambda 抽象中时）。

我开始相信我正在经历的事情正在以某种方式发生，因为 Idris 不知道可扩展性：有没有其他方法可以证明这一点（不调整我正在使用的平等概念，例如使用setoids)?

我正在使用来自 git 的 Idris 1.3.2。

Answer 1

你可以假设外延性：

postulate
funext : {f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g

theorem : {f : (a -> b) -> c} -> f = (\g => f (\x => g x))
theorem = funext $ \g => Refl