dafny - 不变但无法证明的 forall

Question

在这段代码中

https://rise4fun.com/Dafny/DmBh

断言 forall x:: x in multisetOfTree(t.right) ==> t.root <= x;

在第 36 行没有证明，但是它是不变量的一部分。实际上，您可以取消注释第 31 行中的不变量并注释第 36 行并且它可以工作。

Answer 1

问题是您在 的定义中缺少括号isABB。

它应该是：

predicate isABB (t:Tree<int>)
{
match t
    case Empty => true
    case Node(l,d,r) => isABB(l) && isABB(r) 
                        && (forall x :: x in multisetOfTree(l) ==> x <= t.root)
                        && (forall x :: x in multisetOfTree(r) ==> t.root <= x)
}