如何用Dafny证明sumDown与sumUp序列求和函数等价？

首先给出两个求和函数的定义：

function sumDown(nums: seq<int>): int {
    if |nums| == 0 then 0 else sumDown(nums[0..(|nums|-1)])+nums[|nums|-1]
}

function sumUp(nums: seq<int>): int {
    if |nums| == 0 then 0 else nums[0]+sumUp(nums[1..])
}

需要证明的引理：

lemma sumsEqual(nums: seq<int>)
    ensures sumDown(nums) == sumUp(nums)
{}

关键证明思路 #

不需要额外定义序列反转方法，直接通过数学归纳法结合分情况讨论即可完成证明，具体步骤如下：

1. 基础情况：空序列
   当nums为空时，sumDown(nums)和sumUp(nums)都直接返回0，等式显然成立。

2. 基础情况：单元素序列
   若nums = [x]，则：

   • sumDown([x]) = sumDown([]) + x = 0 + x = x
   • sumUp([x]) = x + sumUp([]) = x + 0 = x
     两者结果相等，等式成立。

3. 归纳步骤：长度大于1的序列
   假设对于所有长度为k的序列，sumDown(s) == sumUp(s)成立。现在考虑长度为k+1的序列nums：

   • 根据sumDown的递归定义，sumDown(nums) = sumDown(nums[0..k]) + nums[k]
   • 由归纳假设，sumDown(nums[0..k]) == sumUp(nums[0..k])，因此sumDown(nums) = sumUp(nums[0..k]) + nums[k]
   • 根据sumUp的递归定义，sumUp(nums) = nums[0] + sumUp(nums[1..])
   • 利用加法结合律，sumUp(nums[0..k]) + nums[k]等价于nums[0] + sumUp(nums[1..])，也就是sumUp(nums)
   • 由此可得sumDown(nums) == sumUp(nums)，归纳步骤得证。

Dafny代码实现示例 #

把上述逻辑转化为Dafny可验证的代码，显式引导归纳过程：

lemma sumsEqual(nums: seq<int>)
    ensures sumDown(nums) == sumUp(nums)
{
    if nums == [] {
        // 空序列直接满足条件
    } else if |nums| == 1 {
        // 单元素序列直接验证相等
    } else {
        // 对更短的序列应用归纳假设
        sumsEqual(nums[0..(|nums|-1)]);
        sumsEqual(nums[1..]);
        // 用calc块显式推导等式
        calc {
            sumDown(nums);
            == sumDown(nums[0..(|nums|-1)]) + nums[|nums|-1];
            == sumUp(nums[0..(|nums|-1)]) + nums[|nums|-1];
            == sumUp(nums);
        }
    }
}

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