algorithmproofdafny

Dafny simple proof about giving change not working


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.


Solution

  • You need a lemma to explain to Dafny mathematical facts about functions which seem obvious to us but are not obvious to 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);
      }
    }