I want to prove that the following code returns a given amount (money) in 5 and 3 bills/coins:

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 :(
  }
}

The base cases seem to work just fine (Dafny can assert that sum([3, 5]) == amount, for example), but it’s struggling with the recursive case.

I’ve added additional assertions to make the failure clear, in the end what I want to assert is the ensures clause, that assert sum(result) == amount it’s true for the recursive case.