Dafny中函数外延性证明问题：公理式写法为何不生效？

问题描述 #

用户希望证明：若对于所有输入，函数f和g的返回值均相同，则f与g等价。为此编写了如下lemma：

lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g

用户原本认为这是一条公理，但该写法无法生效，因此询问：Dafny中是否不成立函数外延性？

解答 #

Dafny支持函数外延性，但你不能通过手动声明这类lemma来使用它——函数外延性是Dafny内置的核心公理之一，不需要额外定义或证明。

当你需要基于“所有输入下函数返回值相同”推导“函数等价”时，直接给出forall x :: f(x) == g(x)作为前提，Dafny的自动推理器会自动应用内置的函数外延性公理，得出f == g的结论。

比如下面这个示例可以直接通过验证：

lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g
{
  // 无需额外证明代码，Dafny自动完成推导
}

如果你的代码无法通过验证，大概率不是函数外延性不生效的问题，可能是以下原因：

• 涉及的不是纯函数（比如带有副作用的方法），这类对象不适用函数外延性；
• 上下文存在其他约束条件，干扰了自动推理器的判断；
• 函数类型的参数或返回值涉及更复杂的类型，需要手动添加辅助推理步骤。

内容的提问来源于stack exchange，提问作者Gordon Sau