主页 / coding / 问题 / 77699115
Accepted
pratyai
Asked: 2023-12-21 23:58:29 +0800 CST

证明“序列中的每个元素都是 0 ==> 序列中每个索引处的元素都是 0”是违反直觉的。该如何推理呢？

  • 772
lemma blah(p:nat->bool, xs:seq<nat>)
  requires forall t | t in xs :: p(t)
  ensures forall i | 0 <= i < |xs| :: p(xs[i]) {}

lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) {
  // blah(x => x == 0, xs);
}

所以，我正在尝试 dafny 版本4.4.0，并且正在努力理解上面的代码片段。它大致匹配这里两个相关引理之一；但我稍微简化了它们。

我的理解是，zero_is_zero引理基本上是引理的概括（本例中的blah属性是）。因此，如果有的话，自动验证应该更容易。我期望通过索引访问时，序列中的元素将被视为与同一元素无法区分。px => x == 0zero_is_zero

在实践中，事实证明这blah是自动验证的（即我在引理主体中没有做任何事情）。但因为zero_is_zero我必须显式调用blah以表明它确实适用于 property x => x == 0，然后突然间它不再是问题了。

对此有何解释？

谢谢！

dafny

1 个回答

  1. Best Answer

    在 Dafny 中，触发器的概念对于任何存在或 forall 运算符都很重要。此处您已将其指定x in xs为值为零的触发器。因此，您需要调用该触发器来获取要验证的序列。

    lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) 
{
    forall k | 0 <= k < |xs|
        ensures xs[k] == 0
    {
      assert xs[k] in xs;
    }
}
    • 1

相关问题