Dafny: comparing lexicographic tuples

Question

I am working through the book "Program Proofs". Specifically, I am doing exercise 5.9.

My attempt is as follows:

function Mult(x: nat, y: nat): nat
{
    if y == 0 then 0 else x + Mult(x, y - 1)
}

lemma {:induction false} MultCommutative(x: nat, y: nat)
    decreases x + y
    ensures Mult(x, y) == Mult(y, x)
{
    if x == y {
        // Trivial
    } else if x == 0 {
        MultCommutative(x, y - 1);
    } else if y < x {
        MultCommutative(y, x);
    }
}

Dafny does not verify at MultCommutative(y, x), with the error that the decreases clause might not decrease. However, I do not understand this.

To my knowledge, Dafny should check whether the following lexicographical tuple comparison holds: x + y ≻ y, x. Which holds, as x + y exceeds y. Therefore, I do not understand why Dafny still says that the decreases clause might not decrease.

Answer 1

Since you have explicitly mentioned decrease clause, Dafny will use that decrease clause. Your assumption that it will compare x + y with tuple x, y is wrong. It would have chosen tuple x, y if you haven't provided decrease clause. In both case it will compare decrease clause of invoking function/lemma with decrease clause of called function/lemma.

Edit: Dafny doesn't compare decrease clause of caller with parameter tuple of callee. It compares decrease clause of caller with decrease clause of callee. Since here caller and callee are same, it is same expression. If either of these don't have decrease clause, decrease clause will be defaulted to parameter tuple - but it still compares decrease clause of caller and callee.

See this example

lemma Test(x: nat, y: nat)
  decreases y
{
    if y > 0 {
        Test(y+1, 0);
    }
}

It is counter to your argument as y is less than tuple y+1, 0 but it still verifies.

Take case when it is called with x = 3 and y = 2. Here x + y is 5 and when you call recursively in last else if branch it will be x = 2 and y = 3 but x + y is 5 still. It is not decreasing hence Dafny is complaining.