How to prove fraction addition in dafny

user_13630719 0
Viewed 88

I want to prove the following about fraction addition. Namely j/2+k/2 = (j+k)/2. To do so, I have the following below:

lemma adding_fraction(j: nat, k: nat)
    ensures j / 2 + k / 2 == (j + k) / 2
{
    assert j / 2 + k / 2
        == j * (1 / 2) + k * (1 / 2)
        == (1/2) * (j + k)
        == (j + k) / 2
    assert j/2 + k/2 == (j + k) / 2;
}

I get an invalid AssertStmt error on the last like of this lemma. I'm not entirely sure why. Moreover I'm not sure why dafny is unable to prove this about addition already. Could someone provide some assistance on how I can prove this lemma?

I see one error actually now. Namely in dafny 1/2 == 0 is true. So all division seems to be done with a floor operation. That said in the code above is j%2=0 and k%2=0 then dafny's able to prove it no problem. How can I force dafny not to use floor? This is an issue since in real life: 1/2 + 5/2 = 6/2 = 3 but in dafny with floor: 1/2 + 5/2 = 0 + 2 = 2.

dafny fractions
1 Answers

First, the lemma is not true. If j and k are both odd, then j / 2 + k / 2 will be one less than (j + k) / 2 because division is truncating integer division. For example, we can prove the following counterexample in Dafny

lemma counterexample()
  ensures var j := 1; var k := 3;
    !(j / 2 + k / 2 == (j + k) / 2)
{}

As to your other question, you are missing a semicolon on the second to last line. Dafny's error message could be improved here, but it's good to keep in mind in the future that any time Dafny reports an "invalid ", it's a syntax error and you should be on the lookout for typos. The full Dafny message for this error is (roughly)

tmp.dfy(8,4): Error: invalid AssertStmt
1 parse errors detected in tmp.dfy

You can see that it at least contains a line number (for the assertion after the missing semicolon) and the phrase "parse errors" on the second line of the error message.

After fixing this syntax error, there are several semantic errors having to do with not being able to prove the assertions. The underlying cause for these is that the lemma is false.

user_4382670
Related