Dafny中实数相等性问题：x>0时x²正性证明失败

问题分析 #

这不是Dafny的Bug，而是其自动定理 prover 的推理局限性导致的。虽然逻辑上val1 * val1 > 0.0完全满足BothPos引理的x > 0.0前置条件，但Dafny无法自动将已知的复合表达式（val1 * val1）的 positivity 与引理调用时的参数关联起来。

解决方法 #

方法1：添加显式断言引导推理 #

在调用BothPos前，显式断言val1 * val1 > 0.0，帮助prover将该事实与引理的前置条件匹配：

lemma SquarePos(val1: real, val2: real)
    requires val1 * val1 == val2
    requires val1 * val1 > 0.0
    ensures val2 > 0.0
{
    assert val1 * val1 > 0.0; // 显式断言，消除prover的推理障碍
    BothPos(val1 * val1, val2);
}

方法2：直接利用相等性传递（无需调用BothPos） #

由于val1 * val1 == val2且val1 * val1 > 0.0，根据实数相等的传递性，val2 > 0.0直接成立，无需额外引理调用，Dafny可自动验证：

lemma SquarePos(val1: real, val2: real)
    requires val1 * val1 == val2
    requires val1 * val1 > 0.0
    ensures val2 > 0.0
{
    // 无需任何代码，Dafny自动从前置条件推导出后置条件
}

方法3：将复合表达式赋值给变量（可选） #

把val1 * val1赋值给一个临时变量，prover更容易识别变量的属性，从而匹配BothPos的前置条件：

lemma BothPos(x: real, y: real)
    requires x > 0.0
    requires x == y
    ensures y > 0.0
{
}

lemma SquarePos(val1: real, val2: real)
    requires val1 * val1 == val2
    requires val1 * val1 > 0.0
    ensures val2 > 0.0
{
    let square = val1 * val1;
    BothPos(square, val2); 
}

总结 #

Dafny的自动推理并非全能，对于复合表达式作为参数的场景，偶尔需要显式的断言或变量赋值来引导prover关联已知事实。上述方法都能解决你遇到的验证问题。

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