I would like to prove this:
lemma NatDivision(a: nat, b: nat)
requires b != 0
ensures a / b == (a as real / b as real).Floor
I don't know where to start—this seems almost axiomatic.
If I knew what the axioms were, I could work from there, but I poked around in the Dafny source code and couldn't find axioms for nat division. (This Is Boogie 2 claims Boogie requires you to define your own, so I imagine they're there somewhere, maybe in C# code.)
(The broader context: I'm trying to prove that (a + n * b) % b == a % b for natural numbers, using this approach. Here's the almost-working Dafny proof.)
It can be done in three lines:
lemma NatDivision(a: nat, b: nat)
requires b != 0
ensures a / b == (a as real / b as real).Floor
{
// A basic fact about the natural division and modulo operations:
assert a == (a / b) * b + (a % b);
// Cast some values to `real`, because this is a programming language.
// (In math, 7 and 7.0 are the same object and this wouldn't be needed...)
assert a as real == (a / b) as real * b as real + (a % b) as real;
// Divide through by b.
assert a as real / b as real == (a / b) as real + (a % b) as real / b as real;
// Aha! That reveals that the real quotient `a as real / b as real` is equal
// to the natural quotient `a / b` (a natural number) plus a fraction.
// This looks enough like `Floor` that Dafny can take it from here.
}
I still haven't found the axioms for division.
How I found this proof: First, I assumed that Dafny does not define either natural division or real division in terms of the other. So then how are they defined? I wrote down my best guesses:
// natural division
a / b == the unique number q | a == q * b + r, 0 <= r < b.
// real division
a / b == the unique number q | q * b == a
From there it was a simple matter of trying every possible dead end that can be derived from these two facts before stumbling upon the trick above.
I had a hunch the proof would hinge on something in each definition that did not hold for the other. Sure enough, the first definition became the first assertion of the proof, and the remainder term was important. The second definition is not used directly, but if you look closely you can see a spot where we assume that real multiplication * b as real cancels out real division / b as real.