为什么没有推断出这个愚蠢的后置条件？

Question

我以与此类似的建设性方式证明了一些纯粹存在的引理（没有结果）：

https://rise4fun.com/Dafny/Wvly

lemma DivModExistsUnique_Lemma (x:nat, y:nat)  
requires y != 0
ensures exists q:nat, r:nat :: x == y*q + r &&  r < y 
{
var q:nat, r:nat := 0, x;
while r >= y 
  invariant x == y*q + r
  {
  q := q + 1;
  r := r - y;
  }
assert x == y*q + r &&  r < y;
}

我想不出为什么这个后置条件不是从证明中的最后一个断言中推断出来的。

可以给 Dafny 一些额外的提示吗？

Answer 1

很好的证明！问题是后置条件中的量词没有涉及r的“匹配模式”（也称为“触发器”）。 Dafny 对此提出警告。那是什么意思呢？

为了证明存在量词，验证者会尝试寻找见证人。在寻找见证人时，验证者不会尝试数学中所有可能的术语，甚至不会尝试出现在程序其他地方的每个术语。相反，验证者将其注意力限制在都出现在证明上下文中的其他地方并且具有量词的“匹配模式”形状的术语。在 Dafny IDE（VS Code 或 Emacs）中，您可以将光标放在量词上，IDE 将显示 Dafny 选择的触发器。 （同样，在您的情况下，它会改为“无触发器”。）

关于触发器可以和不能是什么有一定的规则（请参阅Dafny FAQ 或 StackOverflow 上的许多已回答问题）。对于q，验证者将选择术语y*q 作为触发器。这是允许的，因为 Dafny 允许 * 出现在触发器中。但是，r 唯一可能有用的触发器是 ... + r 和 r < ...，这两者都不允许，因为触发器不允许提及 + 或 <。因此，Dafny 没有找到量词的触发器，这实质上意味着它永远不会找到证明存在量词的证人。

要解决此问题，您可以引入一个涉及量化变量的函数。例如，

function MulAdd(a: nat, b: nat, c: nat): nat {
  a*b + c
}

lemma DivModExistsUnique_Lemma(x:nat, y:nat)  
  requires y != 0
  ensures exists q:nat, r:nat :: x == MulAdd(y, q, r) && r < y
{
  var q:nat, r:nat := 0, x;
  while r >= y 
    invariant x == MulAdd(y, q, r)
  {
    q := q + 1;
    r := r - y;
  }
}

将证明您的程序。然后 IDE 还会显示 Mul(y, q, r) 被选为触发器。

没有触发器的量词往往是只使用“内置符号”的量词，如+、< 和&&。当你的问题有其他功能时，验证者通常可以找到触发器。

对于您的证明，我认为最优雅的解决方案是使用引理外参数。这意味着引理可以“返回”它计算的q 和r。它还使引理更易于使用，因为否则引理的调用者通常需要对量词进行 Skolemize（您在 Dafny 中使用 assign-such-that 运算符 :| 执行此操作 - 顺便说一下，这也涉及触发器)。但是您说您（出于某种原因）试图避免超出参数。如果是这样，那么MulAdd 函数就可以解决问题。