为何Dafny中zero_is_zero引理需显式调用blah才能验证？

这是Dafny自动验证器的启发式推理策略导致的差异，核心在于抽象谓词与具体谓词的处理逻辑不同：

• 对于通用引理blah：
  引理中的p是抽象谓词，Dafny验证器在处理这种抽象场景时，会直接利用序列的内置基本性质——合法索引对应的元素必然属于该序列（即xs[i] in xs当0<=i<|xs|）。当需要证明ensures里的p(xs[i])时，验证器会自动匹配requires中的forall t in xs :: p(t)，直接完成推导，所以不需要任何实现代码。

• 对于特例引理zero_is_zero：
  这里的谓词是具体的x == 0，Dafny的自动推理启发式规则不会主动将requires中的“所有属于xs的元素都是0”，和“所有索引对应的元素都是0”这两个命题关联起来。验证器不会自动触发“xs[k] in xs”这个性质来完成量词的实例化，因此需要显式调用blah，相当于给验证器明确提示：要利用“序列索引元素属于序列”这个逻辑来完成推导。

你也可以手动添加一步断言替代调用blah，同样能让验证器自动通过验证，本质是帮验证器点明需要用到的序列性质：

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

内容的提问来源于stack exchange，提问作者pratyai