如何在Dafny中完成分数加法等式j/2 + k/2 = (j+k)/2的证明

• 你写的引理后置条件j / 2 + k / 2 == (j + k) / 2在Dafny默认的整数地板除规则下并非普遍成立，比如j=1、k=5时，左边运算结果是0+2=2，右边是6/2=3，两边不等，命题本身存在反例，Dafny自然无法证明，断言报错属于正常结果。
• 你推导过程中把整数除法当成了实数除法使用，Dafny中自然数的1/2会直接计算为0，所以j*(1/2)等价于j*0，推导逻辑本身就不成立。

场景1：保留整数运算，证明分数加法性质 #

方案1：添加前置限制条件 #

如果仅需要证明j、k均为偶数时等式成立，给引理加对应的requires约束即可，示例代码如下：

lemma adding_fraction_int(j: nat, k: nat)
    requires j % 2 == 0 && k % 2 == 0
    ensures j / 2 + k / 2 == (j + k) / 2
{
    var a := j / 2;
    var b := k / 2;
    assert j == 2 * a && k == 2 * b;
    calc {
        j / 2 + k / 2;
        a + b;
        (2*a + 2*b) / 2;
        (j + k) / 2;
    }
}

方案2：修正为整数场景下普遍成立的命题 #

不加前置条件的整数除法对应的正确等式为j/2 + k/2 + (j%2 + k%2)/2 == (j + k)/2，该命题对所有自然数成立，Dafny可直接验证通过。

场景2：使用普通实数除法，避免地板除 #

如果需要和常规数学的分数运算逻辑对齐，直接将变量类型声明为real即可，Dafny对real类型的除法会执行普通实数运算，不会做地板截断，示例代码如下：

lemma adding_fraction_real(j: real, k: real)
    ensures j / 2.0 + k / 2.0 == (j + k) / 2.0
{
    calc {
        j / 2.0 + k / 2.0;
        j * (1.0/2.0) + k * (1.0/2.0);
        (1.0/2.0) * (j + k);
        (j + k) / 2.0;
    }
}

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