在Dafny中，能否证明integer/natural除法与真实除法之间的关系？

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. Here's the almost-working Dafny proof 证明 (a + n * b) % b == a % b 对于自然数。）

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 没有根据其他。那么它们是如何定义的呢？我写下了我最好的猜测：

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

Answer 2

Jason 自己的回答很棒！我将只添加一个关于除法公理的注释。

不幸的是，在 Dafny 的源代码中没有容易找到这些公理的地方，因为它们内置于底层求解器 Z3 中。通过阅读非线性 integer/real 算术 here 的理论，您可能会找到一些有用的东西。但事情有点复杂，因为这些文档通常非常抽象地定义事物，通过引用 "the mathematical definition" 而不是拼写出来。

也就是说，也许更有用的资源是查看其他人在历史上如何处理 Dafny 中的非线性（主要是整数）算法。为此，我建议阅读作为 IronFleet 项目的一部分开发的数学库 here。（首先阅读名称中包含单词 "nonlinear" 的文件；这些是最接近公理的最低级证明。）

在Dafny中，能否证明integer/natural除法与真实除法之间的关系？

In Dafny, can the relationship between integer/natural division and real division be proved?

integer-division

dafny