I am not able to prove a simple property: if 0<=a<=1 & 0<=b<=1 & -1<=c<=1 then a*b*c==1 ==> a=1 & b=1 & c=1.
I first tested the following:
lemma threepowers(a:real,b:real,c:real)
requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
{
if (a<1.0 || b<1.0 || c<1.0){
assert a*b*c < 1.0;
}
}
But the assertion fails.
So I decided to prove it by cases, as follows (note that I only show a couple of cases):
lemma threepowers(a:real,b:real,c:real)
requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
{
if (a==1.0){
if ((b == 1.0 && c!=1.0)||(b != 1.0 && c==1.0)){
assert a*b*c!=1.0;
}
else if (b != 1.0 && c!=1.0){
assert a*b*c!=1.0;
}
}
}
But Dafny is not able to verify that if b and c are both not 1 (i.e., they are smaller than 1, taking into account the requires), then the product a*b*c is not 1.
What basic issue am I missing?
Of course, note that a Z3 call is not able to prove it either:
lemma threepowers(a:real,b:real,c:real)
requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
{
assert forall x:real :: forall y:real :: forall z:real :: (0.0<=x<1.0) || (0.0<=y<1.0) || (-1.0<=z<1.0) ==> (x*y*z<1.0);
}
I found a two-line proof for a variant of your problem
lemma threepowers(a:real,b:real,c:real)
requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
{
if a*b*c == 1.0 && a < 1.0 && b < 1.0 && b != 0.0 && c != 0.0 {
}
}
but because I find the process more interesting that the solution, here is the methodology I followed.
lemma twopowers(a: real, b: real)
requires 0.0<=a<=1.0 && 0.0<=b<=1.0
ensures a*b==1.0 ==> a==1.0 && b==1.0
{
}
That did not work either. So I started to follow verification debugging techniques and inserted
if a*b == 1.0 { // Just added
assert a==1.0 && b==1.0; // Just added
} // Just added
but that did not work yet. My next move was to think. Well, if it cannot prove that a == 1.0, I can assume that a != 1.0 and perhaps obtain a proof by contradiction. So my proof changed to
if a*b == 1.0 {
if a != 1.0 { // Just added
assert false; // Just added
} // Just added
assert a==1.0 && b==1.0;
}
And curiously, it conditionally proved the two assertions a==1.0 and b==1.0
So now, how do I prove there is a contradiction?
Well, the only thing I could try was to derive more facts. Since a is not 1, it has to be strictly less than 1, so I asserted it.
if a*b == 1.0 {
if a != 1.0 {
assert a < 1.0; // Just added
assert false; // Still not verifying
}
assert a==1.0 && b==1.0;
}
Then, since I knew that a*b == 1.0, I thought I would be able to derive that a*b < 1.0 * b. but it turned out, this is not true.
if a*b == 1.0 {
if a != 1.0 {
assert a < 1.0;
assert a*b < 1.0*b; // Does not verify
assert false; // OK now
}
assert a==1.0 && b==1.0;
}
The reason is obvious. If b is zero, there should be an equality. So, I needed the case split b != 0 And suddenly, the entire function verified.
if a*b == 1.0 {
if a != 1.0 {
assert a < 1.0;
if b != 0.0 {
assert a*b < 1.0*b;
} else {
assert a*b == 1.0*b;
}
assert false;
}
assert a==1.0 && b==1.0;
}
Dafny figured out that, in one case a*b < 1.0*b <= b <= 1, so a*b < 1 and we had a contradiction.
In the other case, a*b == 0 so 0 == 1 and that's another contradiction.
So I tried a similar strategy for your lemma, it was a bit longer, but I found the solution above by trial and error.
I first changed the interval of c to 0.0<=c<=1.0, and then supposed that a*b*c == 1. Then I tried a < 1.0, then b < 1.0 and then what if b != 0 and c != 0, and it arrived not only at a contradiction in this case, but it was enough for the verifier to figure out all the other cases.
I then simplified the nested if-else structure until I kept the minimum of the proof, and voilà !
Then, to make it easier to reproduce, I did another experiment. I created the skeleton of a proof:
if a*b*c == 1.0 {
if a < 1.0 || b < 1.0 || c < 1.0 {
if a < 1.0 {
assert false;
} else if b < 1.0 {
assert false;
} else {
assert c < 1.0;
assert false;
}
}
assert a==1.0 && b==1.0 && c==1.0;
}
Only the two first assert were failing. I focused on the first. I added the split if a != 0.0 with an assert false in its body, and only the first branch was failing.
Similarly, I added the split if b != 0.0 with assert false in its body, and only the first branch was failing.
Then I added the triple split if c < 0.0 { assert false; } else if c == 0.0 { assert false; } else { assert c > 0.0; assert false; }
And only the third assert was failing.
Then, in this branch, I added assertions to prove manually the contradiction:
assert c*b > 0.0;
assert a*(b*c) < 1.0*(b*c);
assert c*b <= 1.0; // Failing
I added two new assertions in front of the failing assert:
assert b <= 1.0;
assert b*c <= 1.0 * b;
And the second one did the trick.
Then, all my job was to simplify the proof. I removed all the else { assert false; } for example. I removed the wrapper if a < 1.0 || b < 1.0 || c < 1.0 { since proving it on one case make it possible to prove it for all cases. I collapsed the tower of ifs, and my proof became the simple
if a*b*c == 1.0 && a < 1.0 && a != 0.0 && b != 0.0 && c > 0.0 {
assert b*c <= 1.0 * b;
}
From here one would be very happy to have a proof, but I did one more step: I put the assertion in the condition:
if a*b*c == 1.0 && a < 1.0 && a != 0.0 && b != 0.0 && c > 0.0 && b*c <= 1.0 * b {
}
and that worked! I was even able to remove c > 0.0 and a*b*c == 1.0 and here is the shortest proof I could find:
if a < 1.0 && a != 0.0 && b != 0.0 && b*c <= 1.0 * b {}