Dafny中Lambda函数Requires传播证明问题及处理机制咨询

你的引理核心是验证：对带前置条件的函数f，通过(x: int) requires f.requires(x) => f(x)构造的lambda表达式，其前置条件与原函数f的前置条件完全等价。

Dafny的处理逻辑 #

Dafny对高阶函数（包括lambda）的requires属性采用保守推理策略，不会自动推导嵌套的前置条件关联。这是因为函数类型具有抽象性，验证器无法默认知晓你希望将lambda的requires与原函数的requires直接绑定，需要显式引导证明过程。

手动证明实现 #

可以通过calc块显式展开lambda的requires定义，让验证器明确关联关系：

lemma propagate_requires(f: int -> int, y: int)
ensures ((x: int) requires f.requires(x) => f(x)).requires(y) == f.requires(y)
{
  calc {
    ((x: int) requires f.requires(x) => f(x)).requires(y);
    // 直接替换为lambda声明中定义的前置条件
    f.requires(y);
  }
}

证明思路拆解 #

Dafny中，lambda表达式(x) requires P(x) => E(x)的requires属性就是其声明中指定的P(x)。因此：

• 当你调用该lambda的.requires(y)时，本质就是取P(y)，也就是f.requires(y)
• 等式两边完全等价，通过calc块显式替换后，验证器即可完成证明

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