Dafny是否支持构造性证明？如何利用方法推导存在性断言

Dafny完全支持构造性证明，你的思路是对的：实现一个满足后置条件的方法，本质就是为forall a,b: nat :: exists c: nat :: a+c == b || b+c == a这个命题提供构造性证人。但你遇到的问题是，Dafny的验证器不会自动把你的Difference方法和断言里的存在量词关联起来，得我们显式指定证人的来源。

下面给你几种可行的解决方式：

1. 用witness关键字关联方法和断言 #

你可以在存在量词断言里，用witness关键字告诉验证器：用Difference(a,b)返回的c作为存在性的证人。因为你的Difference方法已经通过验证满足后置条件，所以验证器会直接复用这个证明来确认断言成立。

修改后的代码：

method Difference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  c := if a > b then a - b else b - a;
}

method Main() {
  assert forall a: nat, b: nat :: exists c: nat :: 
    witness Difference(a, b)  // 显式指定证人来源
    a + c == b || b + c == a;
}

2. 用Lemma封装构造性证明 #

如果这个方法只是用于证明而非实际执行，更推荐用lemma来封装——Lemma是Dafny专门用于证明逻辑的构造，默认不会被编译成可执行代码，更适合纯推理场景：

// 用lemma封装构造性证明逻辑
lemma ExistsDifference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  c := if a > b then a - b else b - a;
}

method Main() {
  assert forall a: nat, b: nat :: exists c: nat :: 
    witness ExistsDifference(a, b)
    a + c == b || b + c == a;
}

3. 直接在断言中写出证人表达式 #

如果你不想额外定义方法或lemma，也可以直接在断言里写出c的构造逻辑，让验证器直接检查这个表达式是否满足条件：

method Main() {
  assert forall a: nat, b: nat :: exists c: nat :: 
    c == if a > b then a - b else b - a && 
    (a + c == b || b + c == a);
}

为什么原代码会失败？ #

Dafny的验证器不会自动扫描所有可用方法来寻找存在量词的证人——它需要明确的指引。构造性证明的核心是提供具体的实例（这里就是c的取值），无论是通过witness引用已有方法，还是直接写出表达式，都是在给验证器这个关键的实例线索。

内容的提问来源于stack exchange，提问作者Jason Orendorff