为什么不能推断出该dafny后置条件？

问题描述

我已经证明了一些纯粹的存在性引理（没有结果），与此相似：

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吗？

解决方法

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

为了证明存在量词，验证者尝试寻找证人。在寻找证人时，验证者不会尝试所有可能的数学术语，甚至不会尝试尝试出现在程序其他位置的每个术语。取而代之的是，验证者将注意力集中在出现在证明上下文和中的其他地方，并且在量词上具有“匹配模式”的形状。在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,r)
  {
    q := q + 1;
    r := r - y;
  }
}

将证明您的程序。然后，IDE还将向您显示已选择Mul(y,r)作为触发器。

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

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