the property of recursive function

[dreamqin68]

Hi All,

I wrote a function that sums a sequence and found that the function does not satisfy that the sum of the whole sequence is equal to the sum of the parts.

function add(number:int, initial:int) :int
{
    var returnValue := number + initial;
    returnValue
}

function sum(input:seq<int>, initial:int): (re:int)
    decreases |input|
    ensures |input|==1 ==> postConT1(input, initial, re)
{
    var length := |input|;
    if length > 0 then
        var tempValue := add(input[0], initial);        
        sum(input[1..], tempValue)
    else
        initial
}

predicate postConT1(input:seq<int>, initial:int, re:int)
    requires |input| == 1
{
    var tempValue := add(input[0], initial);
    tempValue == re
}

lemma test1(input:seq<int>, initial:int)
{
    var length := |input|;

    if length > 0
    {
        var tempValue := sum(input[..length-1], initial);
        var temp2Value := sum([input[length-1]], tempValue);

        var temp3Value := sum(input, initial);        

        assert temp3Value == temp2Value;
    }
}

The output shows assert temp3Value == temp2Value might not hold.
I think this should be obviously hold. Where did I make a mistake?

Thanks in advance!

[MikaelMayer]

How do you think it should obviously hold? Dafny is not convinced. There are several things that makes it hard to reason: Everything non-trivial involving recursivity is not straightforward for Dafny. In your case, you want to prove:

sum([input[length-1], ...input[0...length-1]]) == sum(input)

which means that you want to prove that the sum is invariant when you rotate the list. Think about it for a moment. It probably works down the road because addition is commutative. If you had "-" instead of "+", then obviously it would not work. So there is probably some work to do.

So here is advice:

1. Add a postcondition to the lemma about what you want to prove.

 ensures 
    var length := |input|;
    length > 0 ==> sum([input[length-1]], sum(input[..length-1], initial)) == sum(input, initial)

2. Split the lemma in the base case (length == 0 and length == 1) and the recurring case.
3. Try to invoke the lemma recursively on a sub-list of input
4. Try to prove the induction hypothesis.

[dreamqin68]

Thanks for your reply.

What I want to prove is not adding in reverse order, but adding the first length-1 numbers first and then adding the last number.

sum([input[0..length-1], input[length-1]) == sum(input)

The order of this addition is the same as the original. So if there is "-", it should also work. So I think it should obviously hold.

[cpitclaudel]

You probably need to assert that input == input[..length - 1] + [input[length-1]] (the prelude doesn't include this as an axiom, it needs to be proved by extensionality)

[dreamqin68]

I add assert input == input[..length-1] + [input[length-1]]; before assert temp3Value == temp2Value; But it still dosen't hold.