Dafny 关于找零的简单证明不起作用

Question

我想证明以下代码以 5 和 3 个钞票/硬币返回给定金额（金钱）：

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; # this works
    var x := [3];
    assert sum(x) == 3; # this works
    result :=  tmp + x;
    assert sum(x) + sum(tmp) == sum(result); # this fails :(
  }
}

基本情况似乎工作得很好（例如，Dafny 可以断言

sum([3, 5]) == amount

），但它在递归情况下遇到了困难。

我添加了额外的断言来明确失败，最后我要断言的是

ensures

子句，

assert sum(result) == amount

对于递归情况是正确的。

Answer 1

你需要一个引理来向 Dafny 解释有关函数的数学事实，这些函数对我们来说似乎是显而易见的，但对 Dafny 来说却并不明显。

lemma sumConcat(xs: seq<nat>, ys: seq<nat>) 
    ensures sum(xs) + sum(ys) == sum(xs + ys)
{
    if xs == [] {
        assert xs + ys == ys;
        assert sum(xs) == 0;
        assert sum(xs) + sum(ys) == sum(xs + ys);
    }else {
        assert xs == [xs[0]] + xs[1..];
        assert xs + ys == [xs[0]] + xs[1..]+ys;
        sumConcat(xs[1..] , ys);
        assert sum([xs[0]]) == xs[0];
        assert (xs+ys)[1..] == xs[1..]+ys;
        assert sum(xs) + sum(ys) == sum(xs + ys);
    }
}
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;
    sumConcat(tmp, x);
    assert sum(x) + sum(tmp) == sum(result);
  }
}