主页 / coding / 问题 / 79586887
Accepted
Caleb Stanford
Asked: 2025-04-22 23:47:19 +0800 CST

Dafny 中的量词介绍：证明 abs 是全射

  • 772

这是一个类似的问题，但我还没能把它映射到我的用例中。基本上，我想用 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
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
dafny

1 个回答

  1. Best Answer

    您可以通过将条件移到谓词函数中来验证这一点。触发器本质上是验证器用来识别某些条件何时成立的符号。它们在技术上与谓词函数并不相同，但在大多数情况下，它们可以等同。触发器的一个重要要求是它们不能包含算术运算。

    因此，像这样的语句x + 1 > 0不是有效的触发器。但是，一旦你将它移到谓词函数中，predicate nextGTZ(x: int) { x + 1 > 0}就可以进行类似的蕴涵操作nextGTZ(x) ==> Q(x)，并且它会识别该触发器。

    我建议你先做一下这个练习。此外，还可以阅读这个常见问题解答。

    较旧的问题：这里

    module CalebStanford {
    function abs(x: int): int {
        if x > 0 then x else -x
    }

    predicate IsNat(x: int)
    {
        x >= 0
    }

    // Passes the verifier
    lemma AbsSurjectiveFor(y: int)
        requires IsNat(y)
        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 :: IsNat(y) ==> (exists x :: abs(x) == y)
    {
        // Forall introduction syntax
        forall y: int | IsNat(y)
        ensures exists x :: abs(x) == y
        {
            AbsSurjectiveFor(y);
        }
    }
}
    • 2

相关问题