Dafny验证乘法交换律引理时的递减子句错误排查

你遇到的问题核心是对Dafny递减子句的严格递减要求理解有误：

Dafny的decreases子句要求每次递归调用时，指定的表达式必须严格小于当前值（基于自然数的标准小于关系）。你调用MultCommutative(y, x)时，x + y和y + x是完全相等的，根本不满足严格递减的条件，所以Dafny会报错。你误以为x + y ≻ y + x成立，但实际上两者是相等的，不存在严格的大小关系。

另外你的代码还有一个遗漏：没有处理x < y的分支，这会导致引理无法覆盖所有情况，后续验证也会失败。

解决方法 #

最直接的调整是把递减子句改成字典序，利用decreases x, y：

• 当y < x时，递归调用的参数是(y, x)，字典序中(y, x)严格小于(x, y)（因为第一个元素y < x），满足Dafny的递减要求。
• 同时补全x < y的分支逻辑，完成完整的证明链。

修改后的代码示例：

function Mult(x: nat, y: nat): nat
{
    if y == 0 then 0 else x + Mult(x, y - 1)
}

lemma {:induction false} MultCommutative(x: nat, y: nat)
    decreases x, y  // 使用字典序作为递减度量
    ensures Mult(x, y) == Mult(y, x)
{
    if x == y {
        // 相等时显然成立
    } else if x == 0 {
        // 0乘任何数都是0，直接断言完成证明
        assert Mult(0, y) == 0;
        assert Mult(y, 0) == 0;
    } else if y < x {
        // 字典序(y, x) < (x, y)，满足递减要求
        MultCommutative(y, x);
    } else {
        // 处理x < y的情况，递归调用后完成推导
        MultCommutative(x, y - 1);
        // 基于Mult的定义展开等式
        assert Mult(x, y) == x + Mult(x, y - 1);
        assert Mult(y, x) == Mult(y - 1, x) + x;
        // 结合递归假设Mult(x, y-1) == Mult(y-1, x)，等式成立
    }
}

额外说明 #

如果坚持用x + y作为递减度量，你需要调整递归逻辑，确保每次调用的x + y严格小于当前值。比如在y < x的分支中，不要直接交换参数，而是先通过其他引理（比如加法交换律）将Mult(x,y)转化为Mult(y,x)，但这种方式不如字典序直接高效。

内容的提问来源于stack exchange，提问作者Paul.0416