达夫尼“真实”真的是“真实”吗

Question

我想证明有关导数和极限的陈述，但没能取得进展，所以我想知道Dafny的

real

类型是否真的与实数相符。

Dafny 的文档指出：

Dafny 支持两种数字类型，基于整数，其中包括所有整数的基本类型

int

，以及基于实数的，其中包括所有实数的基本类型

real

所以我假设我可以证明关于（类型值）的所有陈述

real

我可以证明关于实数的陈述。

据我了解，Dafny 本身并没有指定实数的公理。它转换为 boogie，而 boogie 又依赖于 SMT 求解器，通常是 z3。 z3 指向 SMT-Lib 的 Reals 理论，该理论陈述了“实闭域”公理，我希望这是 z3 以及布吉和 Dafny 实数的基础。

基于这些我尝试过

lemma all_positive_elements_have_a_square_root(x: real)
  requires x >= 0.0
  ensures exists root: real :: x == root * root
{}

但是验证失败。我不会付出更多的努力，因为 - 不知道公理 - 我不知道如何帮助验证者。

我试图说服自己 z3 real 表现更好：

$ cat /tmp/reals.z3 
(declare-const x Real)
(assert (= (* x x) 2.0))
(check-sat)
(get-model)
$ z3 /tmp/reals.z3 
sat
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 1))
)

实数理论中 z3 中的“根对象”是什么？解释了此输出的含义，它确实表明 z3 可以证明具有所需属性的实数的存在，这不能仅从有序域公理得出.

Dafny 再次未能验证这一点：

lemma sqrt2_exists()
  ensures exists root: real :: 2.0 == root * root
{}

那么有没有办法利用 Dafny

reals

或不仅仅是

rationals

这一事实，即具有完整性？

Answer 1

我不确定如何验证该声明。然而，达夫尼可以推理实数。

function div(x: real, y: real): (z: real)
    requires y != 0.0
{
    x/y
}

lemma sqrt(x: real, y: real) 
    requires x > 0.0
    requires y > 0.0 && y*y ==x
{
    assert div(x, y) == y;
    var sq :| sq != 0.0 && div(x, sq) == sq;
}

标准方法似乎是要求它作为公理存在，并且 Dafny 接受了它。

一个实现

至于定义衍生品，这将是一项很好的工作。我在here实现了一些序列极限的基本定义和示例。如果您可以将其一直扩展到衍生品，我将有兴趣看到它。