这是一个类似的问题，但我还没能把它映射到我的用例中。基本上，我想用 Dafny 证明一个带有嵌套量词的基本命题（对于所有 X，都存在 Y），该命题在整数上的一阶逻辑中。我选择的具体命题是：该abs函数在非负整数上是全射。以下是一段精简的代码片段：
function abs(x: int): int {
if x > 0 then x else -x
}
// Passes the verifier
lemma AbsSurjectiveFor(y: int)
requires y >= 0
ensures exists x :: abs(x) == y
{
assert abs(y) == y;
}
// Error in this lemma (universal generalization of the above)
lemma AbsSurjective()
ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
{
// Forall introduction syntax
forall y: int | y >= 0
ensures exists x :: abs(x) == y
{
AbsSurjectiveFor(y);
}
}
问题
上述使第二个引理通过的正确语法是什么？
更概括地说，如果我想手动进行证明（比如，以自然演绎的方式），我正在寻找 forall-introduction 和 forall-elimination 规则的语法。我怀疑自己做了一些非常“明显”的错误，但在参考手册中找不到正确的语法。
笔记
Dafny 证明了第一个引理（很简单，不需要引入量词），但是第二个引理却失败了，尽管我完全匹配了Rustan 的答案中给出的语法，该答案建议在引理中使用 forall 语句块。
关于可能出错的地方，我收到了关于使用不带触发器的量词的警告。但是，我并不特别在意触发器，因为我的目的是手动证明 forall/exists 语句。我不确定是否有办法直接关闭触发器，或者告诉 Dafny 根本不要实例化量词，除非我指示它这样做。
输出dafny verify：
$ dafny verify fol-minimal.dfy
fol-minimal.dfy(15,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
|
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
fol-minimal.dfy(18,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
|
18 | forall y: int | y >= 0
| ^^^^^^^^^^^^^^^^^^^^^^
fol-minimal.dfy(16,0): Error: a postcondition could not be proved on this return path
|
16 | {
| ^
fol-minimal.dfy(15,8): Related location: this is the postcondition that could not be proved
|
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^