dafny

Real number equality in Dafny: proving x^2 is positive for x > 0

I came across the following strange example of real number equality in Dafny, after a student pointed me to a related issue. First, when we have two real numbers that are equal, and one of them is positive, Dafny (as expected) is able to prove that the other is also positive:

lemma BothPos(x: real, y: real)
    requires x > 0.0
    requires x == y
    ensures y > 0.0
{
    // proved
}

However, if we replace one of the reals with its square, then Dafny is unable to apply the above lemma. Dafny complains that a precondition could not be proven, and is thus seemingly unaware that val1 * val1 > 0.0, even though this is present as an immediate preceding precondition to the lemma.

lemma SquarePos(val1: real, val2: real)
    requires val1 * val1 == val2
    requires val1 * val1 > 0.0
    ensures val2 > 0.0
{
    // Precondition for this call could not be proved: x > 0.0
    BothPos(val1 * val1, val2);
}

Output:

$ dafny verify temp.dfy 
temp.dfy(16,11): Error: a precondition for this call could not be proved
   |
16 |     BothPos(val1 * val1, val2);
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^

temp.dfy(3,15): Related location: this is the precondition that could not be proved
  |
3 |     requires x > 0.0
  |              ^^^^^^^

$ dafny --version
4.10.0

Is this a bug in Dafny? I can't think of another reason this could fail. Possibly something to do with constructive reals, but Dafny is not based on constructive logic.

Is there another way to prove the above lemma?

Related:

Solution

  • Triggers can't include arithmetic so basically it gets confused about what quantities are what.

    function prod(x: real, y: real): real {
    x * y
}

lemma SquarePos(val1: real, val2: real)
    requires prod(val1 , val1) == val2
    ensures val2 >= 0.0
{
}

lemma prodBothPos(x: real, y: real)
    requires x > 0.0
    requires y > 0.0
    ensures prod(x, y) > 0.0
{
}

lemma prodBothNeg(x: real, y: real)
    requires x < 0.0
    requires y < 0.0
    ensures prod(x, y) > 0.0
{
}

lemma UsesSquarePos(x: real)     
requires x != 0.0     
ensures prod(x, x) > 0.0 
{     
    assert prod(x, x) != 0.0 by {
        if x > 0.0 {
            prodBothPos(x, x);
        } else {
            prodBothNeg(x, x);
        }
    }
}

    For example, to get the definition of a supremum in Dafny moving addition and subtraction into functions helped form triggers that could be used in proofs.

    Edit: To fix the issue required a few more lemmas.