Dafny: property '2*x*y <= x^2+y^2' holds with primitive operations (like 'x*x'), but not when I define operations in my own (like 'power(x,2)')

Question

I am trying to prove a property in Dafny, which makes use of powers.

Concretely, this one: forall x,y in Reals : 2xy <= x^2+y^2. I implemented this idea in the following lemma:

lemma product2_lessEqual_powProduct (x:real, y:real)
    requires 0.0<x<=1.0 && 0.0<y<=1.0
    ensures 2.0*x*y <= (x*x)+(y*y)
    {}

Which is verified with no problem (I guess some automatic induction is performed below).

However, I would like to use an own power function in order to make power(x,2) instead of x*x. Thus, I took a power function from https://github.com/bor0/dafny-tutorial/blob/master/pow.dfy, which is as follows:

function method power(A:int, N:nat):int
{
    if (N==0) then 1 else A * power(A,N-1)
}

method pow(A:int, N:int) returns (x:int)
    requires N >= 0
    ensures x == power(A, N)
{
    x := 1;
    var i := N;

    while i != 0
        invariant x == power(A, (N-i))
    { 
        x := x * A;
        i := i - 1;
    }
} 

However, since I am using real values for the basis of the exponential, I modified it a bit so that it works for exponentials:

function method power(A:real, N:nat):real
{
    if (N==0) then 1.0 else A * power(A,N-1)
}

method pow(A:real, N:int) returns (x:real)
    requires N >= 0
    ensures x == power(A, N)
{
    x := 1.0;
    var i := N;

    while i != 0
        invariant x == power(A, (N-i))
    { 
        x := x * A;
        i := i - 1;
    }
} 

Thus, I wanted to test it with the previous lemma:

lemma product2_lessEqual_powProduct (x:real, y:real)
    requires 0.0<x<=1.0 && 0.0<y<=1.0
    ensures 2.0*x*y <= power(x,2)+power(y,2)
    {}

Surprisingly, it tells me the typical A postcondition might not hold on this return path.Verifier.

Can anyone explain why this happens? Why is it verifying with primitive operations of Dafny, but not when I define them functions? And how could I prove this lemma now?

Answer 1

Even though second parameter of power is concrete and small, Dafny is not doing enough unrolling to prove desired fact. Adding {:fuel 2} to power makes proof go through. You can read more about fuel here https://dafny.org/dafny/DafnyRef/DafnyRef.html#sec-fuel

function method {:fuel 2} power(A:real, N:nat):real
{
    if (N==0) then 1.0 else A * power(A,N-1)
}

method pow(A:real, N:int) returns (x:real)
    requires N >= 0
    ensures x == power(A, N)
{
    x := 1.0;
    var i := N;

    while i != 0
        invariant x == power(A, (N-i))
    { 
        x := x * A;
        i := i - 1;
    }
} 

lemma product2_lessEqual_powProduct (x:real, y:real)
    requires 0.0<x<=1.0 && 0.0<y<=1.0
    ensures 2.0*x*y <= power(x,2)+power(y,2)
    {}

Answer 2

It's surprising until you realize that there is a mathematical theory for A*A, but power(A, 2) requires two unfolding of power to have a meaning.

If you want your function to work seamlessly with the theory and prove your last lemma, you can give it precise postconditions:

function method power(A:real, N:nat): (result: real)
  ensures N == 1 ==> result == A
  ensures N == 2 ==> result == A*A
{
    if (N==0) then 1.0 else A * power(A,N-1)
}

I tested it, your second lemma verifies.