Dafny中传递性逻辑疑问：前两断言成立第三断言为何失败？

给定三个断言（前两个验证通过，第三个失败）：

assert forall k: int :: start <= k <= m && k != p_i && k != i && 2*k+1 <= m ==> (heap_condition(p_a, k, m) <==> ((2*k <= m) ==> (p_a[(k)-1] >= p_a[(2*k)-1])) && ((2*k+1 <= m) ==> (p_a[(k)-1] >= p_a[(2*k+1)-1])));
assert forall k: int :: start <= k <= m && k != p_i && k != i && 2*k+1 <= m ==> heap_condition(p_a, k, m);
assert forall k: int :: start <= k <= m && k != p_i && k != i && 2*k+1 <= m ==> ((2*k <= m) ==> (p_a[(k)-1] >= p_a[(2*k)-1])) && ((2*k+1 <= m) ==> (p_a[(k)-1] >= p_a[(2*k+1)-1]));

heap_condition的谓词定义如下：

predicate heap_condition(a: seq<int>, k: int, m: int)    
requires 1 <= |a|;
requires 1 <= k;
requires m <= |a|;
requires k <= m; 
{
        ((2*k <= m) ==> (a[(k)-1] >= a[(2*k)-1])) && ((2*k+1 <= m) ==> (a[(k)-1] >= a[(2*k+1)-1]))
}

原本预期的逻辑推导链为：

A ==> (B <==> C)  
A ==> B  
A ==> C

但实际第三个断言（即A ==> C）验证失败，核心原因如下：

符号对应与谓词的前置条件限制 #

先明确各符号对应的逻辑表达式：

• A：start <= k <= m && k != p_i && k != i && 2*k+1 <= m
• B：heap_condition(p_a, k, m)
• C：((2*k <= m) ==> (p_a[(k)-1] >= p_a[(2*k)-1])) && ((2*k+1 <= m) ==> (p_a[(k)-1] >= p_a[(2*k+1)-1]))

从heap_condition的定义看，只有在满足其requires前置条件的情况下，B和C才是完全等价的。但第一个断言A ==> (B <==> C)成立，并不代表B和C在所有A成立的场景下无条件等价——因为A成立时，heap_condition的前置条件可能未被满足。

空真（Vacuous Truth）的影响 #

验证工具对于带前置条件的谓词（如heap_condition），当前置条件不满足时，会将涉及该谓词的蕴含式视为空真（即整个表达式为真，无需检查后续逻辑）：

• 第二个断言A ==> B成立，可能是因为当A成立但heap_condition的前置条件不满足时，工具直接判定该蕴含式为真，而非B本身为真；
• 第一个断言A ==> (B <==> C)同理，当前置条件不满足时，B <==> C会被工具视为空真，无需验证B和C的实际等价性。

但第三个断言A ==> C是直接检查C的布尔值：无论heap_condition的前置条件是否满足，C都是一个可直接求值的表达式。当A成立但C的实际值为假时，断言就会失败。

总结 #

前两个断言的成立依赖于工具对“前置条件不满足的谓词”的空真处理，而第三个断言无此豁免，直接验证C的实际逻辑结果。这就导致了看似符合逻辑传递性的推导，实际却不成立的情况。

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