integer-division - 在Dafny中，整数/自然除法和实数除法之间的关系可以证明吗？

Question

我想证明这一点:

lemma NatDivision(a: nat, b: nat)
  requires b != 0
  ensures a / b == (a as real / b as real).Floor

我不知道从哪里开始——这似乎是公理化的。

如果我知道公理是什么，我可以从那里开始工作，但我在 Dafny 源代码中四处寻找，找不到nat 划分的公理。 (This Is Boogie 2 声称 Boogie 要求您定义自己的，所以我想它们就在某个地方，也许在 C# 代码中。)

(更广泛的上下文:我正在尝试使用 this approach 证明 (a + n * b) % b == a % b 对于自然数。这是 almost-working Dafny proof .)

Answer 1

可以分三行来完成:

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.
}

我还没有找到除法的公理。

我是如何找到这个证据的:首先，我假设 Dafny 没有根据另一个来定义自然 split 或真实 split 。那么它们是如何定义的呢？我写下了我最好的猜测:

// 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

从那里开始，在偶然发现上述技巧之前，尝试从这两个事实得出的每一个可能的死胡同都是一件简单的事情。

我有一种预感，证明将取决于每个定义中不适用于另一个定义的某些东西。果然，第一个定义成为证明的第一个断言，余项很重要。第二个定义没有直接使用，但如果你仔细观察，你会发现一个地方，我们假设实数乘法 * b as real 抵消了实数除法 /b as real .