在Dafny中，能否证明整数/自然除法和实数除法之间的关系？

Question

我想证明这一点：

\n\n

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

\n\n

我不知道从哪里开始\xe2\x80\x94这似乎几乎是不言而喻的。

\n\n

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

\n\n

（更广泛的背景：我正在尝试使用这种方法(a + n * b) % b == a % b证明自然数的这一点。这是几乎可行的达夫尼证明。）

\n

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

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

我如何找到这个证明：首先，我假设达夫尼没有根据另一个来定义自然除法或实除法。那么它们是如何定义的呢？我写下了我最好的猜测：

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