4

我对我感兴趣的属性有一个简单的搜索功能，并证明该功能是正确的。我想评估函数，并使用正确性证明来获得原始属性的定理。不幸的是，coq 中的评估非常缓慢。作为一个简单的例子，考虑寻找平方根：

(*
Coq 8.4
A simple example to demonstrate searching.
Timings are rough and approximate.
*)

Require Import Peano_dec.

Definition SearchSqrtLoop :=
  fix f i n := if eq_nat_dec (i * i) n
  then i
  else match i with
  | 0 => 0  (* ~ Square n \/ n = 0 *)
  | S j => f j n
  end
.

Definition SearchSqrt n := SearchSqrtLoop n n.

(*
Compute SearchSqrt 484.
takes about 30 seconds.
*)

Theorem sqrt_484a : SearchSqrt 484 = 22.
  apply eq_refl. (* 100 seconds *)
Qed.  (* 50 seconds *)

Theorem sqrt_484b : SearchSqrt 484 = 22.
  vm_compute.  (* 30 seconds *)
  apply eq_refl.
Qed.  (* 30 seconds *)

Theorem sqrt_484c (a : nat) : SearchSqrt 484 = 22.
  apply eq_refl.  (* 100 seconds *)
Qed.  (* 50 seconds *)

Theorem sqrt_484d (a : nat) : SearchSqrt 484 = 22.
  vm_compute.  (* 60 seconds *)
  apply eq_refl.
Qed.  (* 60 seconds *)

现在尝试Python中的相应函数：

def SearchSqrt(n):
  for i in range(n, -1, -1):
    if i * i == n:
      return i
  return 0

或者更字面意义上的

def SearchSqrtLoop(i, n):
  if i * i == n:
    return i
  if i == 0:
    return 0
  return SearchSqrtLoop(i - 1, n)

def SearchSqrt(n):
  return SearchSqrtLoop(n, n)

该函数在 Python 中几乎是即时的，但在 coq 中需要几分钟，具体取决于您尝试调用它的方式。同样令人好奇的是，添加一个额外的变量会使 vm_compute 花费两倍的时间。

我知道一切都是在 coq 中象征性地完成的，因此速度很慢，但如果我可以直接评估简单的函数，那将非常有用。有没有办法做到这一点？仅使用本机整数而不是链表可能会有很大帮助。

4

2 回答 2

3

如果您使用二进制算术而不是一元算术，您将获得加速。看看 NArith 和 ZArith。

http://coq.inria.fr/library/

如果您在 OCaml、Haskell 或 Scheme 上运行代码，您还将获得加速。

http://coq.inria.fr/refman/Reference-Manual025.html

于 2013-11-03T12:44:16.113 回答
3

在标准库 ( ) 中有一个更有效的求平方根的函数sqrt：

以下平方根函数是线性的（并且是尾递归的）。有了皮亚诺的代表，我们不能做得更好。有关更快的算法，请参阅Psqrt// ...ZsqrtNsqrt

Require Import Coq.Init.Nat.

Theorem sqrt_484a_v2 : sqrt 484 = 22.
  Time apply eq_refl.
Time Qed.

正如Time告诉我们的那样，它的工作速度要快得多（比 快 200 倍左右sqrt_484a）。

这种性能差异的原因在于SearchSqrt它的第一个参数在每次迭代时平方，这是一个昂贵的操作。

sqrt另一方面， 的实现基于奇数定理（1 + 3 + 5 + ... 是平方数）。只需计算可以适合输入参数的递增间隔的数量，n这将是 的整数平方根。n例如 22 = (1 + 3 + 5 + 7) + 6，这意味着 22 中有 4 个区间（长度1为 、3、5和7），因此sqrt 22 = 4（我们对残值 6 不感兴趣）。

于 2016-12-31T11:45:20.437 回答