Dafny找零算法递归证明失败求助：用3和5凑指定金额

我需要证明以下Dafny代码可返回由3和5面额纸币/硬币组成的指定金额：

function sum(ns: seq<nat>): nat
{
  if |ns| == 0 then
    0
  else
    ns[0] + sum(ns[1..])
}

method Change(amount: nat)
  returns (result: seq<nat>)
  requires amount >= 8
  ensures forall i :: 0 <= i <= |result| - 1 ==> result[i] == 3 || result[i] == 5
  ensures sum(result) == amount
{
  if amount == 8 {
    result := [3, 5];
    assert sum(result) == amount;
  } else if amount == 9 {
    result := [3, 3, 3 ];
    assert sum(result) == amount;
  } else if amount == 10 {
    result := [5, 5];
    assert sum(result) == amount;
  } else {
    var tmp := Change(amount - 3);
    assert sum(tmp) == amount - 3; # 此断言验证通过
    var x := [3];
    assert sum(x) == 3; # 此断言验证通过
    result :=  tmp + x;
    assert sum(x) + sum(tmp) == sum(result); # 此断言验证失败 :(
  }
}

基础情况验证正常（例如Dafny可断言sum([3, 5]) == amount），但递归场景下验证受阻。我添加了额外断言明确失败点，最终需证明递归case中ensures条款sum(result) == amount成立。

解决方案 #

问题出在Dafny无法自动推导序列拼接后的和等于两个序列和的总和这个性质。我们需要给sum函数添加一个引理（Lemma）来显式证明该性质，让验证器认可sum(tmp + x) = sum(tmp) + sum(x)。

修改后的完整代码如下：

function sum(ns: seq<nat>): nat
{
  if |ns| == 0 then
    0
  else
    ns[0] + sum(ns[1..])
}

// 引理：证明两个序列拼接后的和等于各自和的总和
lemma SumConcatenation(s1: seq<nat>, s2: seq<nat>)
  ensures sum(s1 + s2) == sum(s1) + sum(s2)
{
  if |s1| == 0 {
    // 空序列拼接另一个序列等于原序列，空序列的和为0
    assert s1 + s2 == s2;
    assert sum(s1) == 0;
  } else {
    // 递归证明子序列的拼接性质
    SumConcatenation(s1[1..], s2);
    // 展开sum的定义，结合递归结论推导
    assert sum(s1 + s2) == s1[0] + sum(s1[1..] + s2);
    assert sum(s1[1..] + s2) == sum(s1[1..]) + sum(s2);
  }
}

method Change(amount: nat)
  returns (result: seq<nat>)
  requires amount >= 8
  ensures forall i :: 0 <= i <= |result| - 1 ==> result[i] == 3 || result[i] == 5
  ensures sum(result) == amount
{
  if amount == 8 {
    result := [3, 5];
    assert sum(result) == amount;
  } else if amount == 9 {
    result := [3, 3, 3 ];
    assert sum(result) == amount;
  } else if amount == 10 {
    result := [5, 5];
    assert sum(result) == amount;
  } else {
    var tmp := Change(amount - 3);
    assert sum(tmp) == amount - 3;
    var x := [3];
    assert sum(x) == 3;
    result := tmp + x;
    // 调用引理，让验证器认可拼接序列的和的性质
    SumConcatenation(tmp, x);
    // 基于引理推导总和等于目标金额
    assert sum(result) == sum(tmp) + sum(x);
    assert sum(result) == (amount - 3) + 3 == amount;
  }
}

验证说明 #

1. 引理SumConcatenation通过递归方式证明了序列拼接的和的性质：对于任意两个序列s1和s2，sum(s1 + s2)等于sum(s1)加sum(s2)。
2. 在递归分支中调用该引理后，Dafny就能顺利验证sum(result) == amount的断言，进而满足方法的后置条件。

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