主页 / user-1543749

pratyai's questions

Martin Hope
pratyai
Asked: 2023-12-21 23:58:29 +0800 CST
  • 5
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