興味のある物件の簡単な検索機能と、その機能が正しいことの証明があります。関数を評価し、正しさの証明を使用して元のプロパティの定理を取得したいと考えています。残念ながら、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 の時間が 2 倍になることも興味深いです。
すべてがcoqでシンボリックに行われるため遅いことは理解していますが、単純な関数を直接評価できれば非常に便利です。それを行う方法はありますか？リンクされたリストの代わりにネイティブの整数を使用するだけで、おそらく大いに役立つでしょう。