coq - 简化匿名函数中的表达式的简单方法？

Question

假设我需要证明以下内容：

x: nat

(fun _ : nat => 0) = (fun y : nat => if beq_nat x y then 0 else 0)

由于y不在环境中，看起来我无法破坏beq_nat x y以简化右侧。有没有一种简单的方法来简化匿名函数中的表达式？

除了能够使两个函数看起来相等之外，有没有办法通过显示它们在所有输入上产生相同的值来推断两个函数是相同的？

编辑：我意识到我可能会要求不可能的事情，因为这些函数不一样，只是当应用于参数时它们会产生相同的值。我不确定 Coq 是如何解释这一点的。

score 1 · Accepted Answer

我相信这是一种所谓的情况functional extensionality，您想证明两个函数在扩展上是相等的（从调用者的角度来看，它们的行为相同）。

你不能直接在 Coq 中证明它（因为=它是一个定义相等，所以它不是真的），但是如果你愿意，你可以 require 这个模块：

这将为您提供功能可扩展性的公理。您可以调用该策略，该策略extensionality y.将使您可以访问y.

1 回答 1