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中引用(\g => f (\x => g x))的方法：

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