在 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# 代码中。）

（更广泛的背景：我试图证明 (a + n * b) % b == a % b 用于自然数，使用 this approach。这是 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 确实没有定义自然除法或真实除法。那么它们是如何定义的呢？我写下了我的最佳猜测：

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

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

不幸的是，在 Dafny 的源代码中查找这些公理并不容易，因为它们内置于底层求解器 Z3 中。通过阅读非线性整数/实数算术理论here，您可能会发现一些有用的东西。但事情有点复杂，因为这些文档通常非常抽象地定义事物，通过引用“数学定义”而不是拼写出来。

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