Isabelle 中的浮点数和区间运算

Question

我在 Isabelle 中使用 Descision_Procs 文件中的 Approximation.thy 进行区间运算。该文件为您提供了一种证明实数不等式的策略，例如：

theorem "3 ≤ x ∧ x ≤ 6 ⟹ sin ( pi / x) > 0.4" by (approximation 10)

现在，我有兴趣尝试实现的核心函数，它似乎是 approx 函数。 Isabelle/HOL 中通过计算证明实值不等式的第 4.5.2 节对此进行了描述。以下是我所做的一些声明：

value "Float 3 (-1)"
value "approx 1 (Num (Float 3 (-2))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Num (Float 3 (-2))) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Var 1) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"

首先，我想问一下你是否知道一种更方便的写浮点数的方法（而不是 Float a b，也许有一种函数 real_to_float r）。然后，您会看到该函数在给定一定精度（我理解为正确小数位数）的情况下计算作为第二个参数给出的操作的上限和下限。

现在，主要问题如下：

最后一个参数的作用是什么？我猜它们是第二个参数中变量的置信区间？
文中说这个函数也实现了区间运算。你能举个例子让我看看这个函数是如何执行区间加法的吗？ ([a,b]+[c,d]=[a+c,b+d])

Answer 1

None 这些东西是为了直接使用；这就是近似方法在它们之上提供便利层的原因。

有real_to_float这样的功能。它的名字是float_of，但它没有任何代码方程，所以你不能真正使用它。可以为它证明一个代码方程，但这会有点乏味。

至于你的其他问题：是的，最后一个参数是一个列表，其中第 i 个元素是一个已知第 i 个变量的值所在的区间。

是的，approx 执行区间运算；事实上，这是它所做工作的核心。它完全按时间间隔运行。可以观察到您提到的示例，例如在执行 x + y 时，其中 x 在 [1;2] 中，y 在 [-1;2] 中：

value "approx 10 (Add (Var 0) (Var 1))
         [Some (Float 1 0, Float 1 1), Some (Float (-1) 0, Float 1 1)]"

哪个returns区间[0;4]:

"Some (Float 0 0, Float 2 1)"
  :: "(float × float) option"

或者，更直接地说：

lemma "(x :: real) ∈ {1..2} ⟹ y ∈ {-1..2} ⟹ x + y ∈ {0..4}"
  by (approximation 10)

Isabelle 中的浮点数和区间运算

Floating and interval arithmetic in Isabelle

floating-point

isabelle

interval-arithmetic