为何Dafny无法证明谓词体内已定义的断言？

核心逻辑：Dafny自动推理的触发机制与函数抽象性 #

你遇到的问题本质是Dafny自动 prover 对函数抽象性、递归谓词触发条件的处理逻辑导致的：

• 直接用size函数的情况：
  size是有具体实现的递归函数，Dafny prover在处理alpha_weight_balanced的递归约束时，会自动展开size的定义（比如把size(tree)拆成size(left) + size(right) + 1）。这种展开会引入大量树结构的细节，让prover没法直接聚焦在alpha_weight_balanced谓词的核心约束——“子树大小≤α×整树大小”上，反而被琐碎的大小计算分散了推理注意力，因此自动证明失败。

• 用无实现的f包裹size的情况：
  无实现的函数（只有签名，没有body）对Dafny来说是完全抽象的黑盒，prover不会尝试展开或分析它的内部逻辑，只会把f(size(...))当作一个整体的触发项。这时候，prover会直接利用alpha_weight_balanced的递归结构：既然整树满足谓词，那么子树对应的f(size(child)) ≤ α×f(size(tree))约束会被直接实例化。因为f是抽象的，prover不需要纠结它的具体行为，就能顺着谓词的递归定义推出子树大小的约束，所以证明成功。

• 给f加f(a)==a后置条件的情况：
  一旦给f加上这个后置条件，prover就会把f(x) == x这个等式代入所有用到f的地方，相当于把f(size(tree))直接还原成了size(tree)——这就又回到了原始情况：prover再次展开size的定义，推理路径变得复杂，自然没法自动完成证明。

总结 #

这个现象的关键在于：抽象函数能引导Dafny prover聚焦在谓词的递归逻辑上，而具体函数或带等价约束的“伪抽象”函数会让prover陷入细节展开的泥沼，破坏自动推理的触发路径。

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