代码之家 › 专栏 › 技术社区 › Jason Orendorff

在dafny中,整数/自然除法和实数除法之间的关系可以证明吗?

dafny integer-division

1

Jason Orendorff · 技术社区 · 6 年前

我想证明这一点:

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

我不知道从哪里开始——这似乎是不言而喻的。

如果我知道公理是 ,我可以在那里工作,但我在dafny源代码中乱翻,找不到 nat 部门。( 我是布吉2 布吉要求你定义自己的代码,所以我想它们可能在某个地方,也许是C代码中。)

(更广泛的背景:我试图证明 (a + n * b) % b == a % b 对于自然数,使用 this approach . 这是 almost-working Dafny proof )

2 回复 | 直到 6 年前

1

3

Jason Orendorff 6 年前

它可以分为三行:

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 .

2

1

James Wilcox 6 年前

杰森自己的回答很好!我只想加一条关于除法公理的注释。

不幸的是,在dafny的源代码中找这些公理并不容易,因为它们内置于底层的解算器z3中。通过阅读非线性整数/实数运算的理论,你也许能找到一些有用的东西 here . 但事实上,这些文档通常都是非常抽象地定义事物,并引用“数学定义”而不是拼写出来,这让事情有点复杂。

也就是说,也许一个更有用的资源是看看其他人如何处理dafny中的非线性(主要是整数)算法。为此,我建议阅读作为IronFleet项目一部分开发的数学库 here . (首先阅读其名称包含“非线性”一词的文件;这些文件是最接近公理的最低级别证明。)