Coq の rewrite について少し考えた。
まず、rewrite の対象として自然数を扱う実験用に、 命題の中に自然数を好き勝手に書けるよう、X という命題を用意する。 (なお証明したいわけではないので、証明できないものにしてある)
Definition X (n : nat) := False.
また、簡単な定理として、2 + 4 = 1 + 5 というもの L という名前で用意しておく。
Lemma L : 2 + 4 = 1 + 5.
reflexivity.
Qed.
Print L.
(*
L = @eq_refl nat (1 + 5)
: 2 + 4 = 1 + 5
*)
X (1 + 5) という命題の証明の中で、rewrite<- L とすると、 予想通り、L の右から左への書き換えなので、命題が X (2 + 4) に書き換えられる。 証明項をみると、これは eq_rec という関数の呼び出しを構築するようだ。
Goal X (1 + 5). rewrite<- L. (* f (2 + 4) *) Show Proof. (* (@eq_rec nat (2 + 4) (fun n : nat => X n) ?Goal (1 + 5) L) *) Abort.
では、直接 eq_rec の呼び出しを構築してみよう。 ここでは refine を使う。 これでも同様に命題は X (2 + 4) に書き換えられる。
Goal X (1 + 5). refine (@eq_rec nat (2 + 4) (fun n => X n) _ (3+3) (@eq_refl nat (4+2))). (* X (2 + 4) *) Abort.
eq_rec の中身を調べてみよう。 eq_rec は eq_rect を呼び出している。
Print eq_rec.
(*
eq_rec =
fun (A : Type) (x : A) (P : A -> Set) => @eq_rect A x P
: forall (A : Type) (x : A) (P : A -> Set),
P x -> forall y : A, x = y -> P y
*)
eq_rect は dependent match になっている。
Print eq_rect.
(*
eq_rect =
fun (A : Type) (x : A) (P : A -> Type) (f : P x) (y : A) (e : x = y) =>
match e in (_ = y0) return (P y0) with
| eq_refl => f
end
: forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, x = y -> P y
*)
あと、eq の定義は以下のようになっている。
Print eq. (* Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x *)
dependent match を直接構築してみよう。 こうすると命題は (X (2 + 4) ではなく) X (4 + 2) に書き換えられる。 まぁ、構築した証明項の中に 2 + 4 は入っていないので 2 + 4 が出てきたらそれは変だけど。 こうなるのは、match の body の型は return X y の y を、 コンストラクタの定義から取り出した情報で埋めたものになるからである。 コンストラクタ (eq_refl) の定義では、x = x という型の値を構築するとなっていて、 この右側が y に対応する。 で、x には引数として 4+2 を与えているので y は 4+2 になるのだろう。
Goal X (1 + 5). refine ( match @eq_refl nat (4+2) in _ = y return X y with | eq_refl => _ end). (* X (4 + 2) *) Abort.
cast すれば、X (2 + 4) にすることはできる。
Goal X (1 + 5). refine ( match @eq_refl nat (4+2) in _ = y return X y with | eq_refl => (_ : X (2 + 4)) end). (* X (2 + 4) *) Abort.
Canonical Structure をちゃんと調べたことがなかったので、少し調べた。
マニュアルは (あと、昨日読んだ本も) 意味のある、でも少し複雑な例で説明されているので、 意味はないけれど単純な例を自分で作ってみた。
Structure struct_type := struct_cstr { type_field : Type; nat_field : nat }.
Definition struct_val1 := struct_cstr bool 1.
Definition struct_val2 := struct_cstr bool 2.
Definition f (x : struct_type) (y : type_field x) := nat_field x.
Compute f struct_val1 true.
Fail Compute f _ true.
(* ここの _ は引数 x を推論させる指定だが、これは推論できない。
手がかりは type_field x が bool であるということだけだが、
それを満たす x は struct_val1 でも struct_val2 でも、
あるいは struct_cstr bool N で作った何でもいいので推論できないのは当然 *)
Compute f _ (true : type_field struct_val1). (* = 1 *)
Compute f _ (true : type_field struct_val2). (* = 2 *)
(* 第2引数yのところを cast の形で
type_field struct_val1 とか type_field struct_val2 と書いておくと、
推論してくれる *)
Goal type_field struct_val1 = type_field struct_val2.
Proof. exact (@eq_refl Type bool). Qed.
(* type_field struct_val1 と type_field struct_val2 は結局のところ
bool なので、convertible である。
convertible なものは Gallina では同じものとして扱われる、
というのは推論が終わってからの話で、
推論中は convertible なものであっても違う扱いになることがあるのだな。 *)
Canonical Structure struct_val1' := struct_val1.
(* type_field x が bool であるときに x を struct_val1 であると
推論するように設定する *)
Compute f _ true. (* = 1 *)
(* Canonical Structure の設定により、_ は struct_val1 と推論され、
struct_val1 の nat_field の 1 が返ってくる *)
Definition f1 := f _ true.
Print f1. (* f1 = f struct_val1' true *)
(* 推論の結果、実際に埋められるものは Canonical Structure で := の左に
書いた識別子が使われるようだ。
わざわざ識別子を指定させるのはここで使うためなのだな。 *)
Fail Compute f _ 0.
(*
The term "0" has type "nat" while it is expected to have type
"type_field ?x".
*)
(* type_field x が nat であるときに x がなんであるかは設定していないので、
ここでは失敗する *)
Canonical Structure struct_val2' := struct_val2.
(*
struct_val2' is defined
Ignoring canonical projection to S by nat_field in struct_val2': redundant
with struct_val1' [redundant-canonical-projection,typechecker]
Ignoring canonical projection to bool by type_field in struct_val2':
redundant with struct_val1' [redundant-canonical-projection,typechecker]
*)
(* type_field x が bool であるときの x を以前とは異なる struct_val2 と設定してみようとすると、
無視されると警告される
*)
Compute f _ true. (* = 1 *)
(* 警告にあったように無視され、f _ true の _ は struct_val1 に推論され、1 が返ってくる。
もし、struct_val2 に推論されるなら、2 が返ってくるはずである。 *)
なお、Canonical Structure struct_val1' := struct_val1. を Canonical struct_val1' := struct_val1. とか、 Canonical struct_val1. と書けるようにするのは SSReflect の機能の模様。
なら、Canonical struct_val1 って書くと、何で埋めるのか、 と疑問に思ってやってみると、以下のように struct_val1 そのものが埋められる模様。
From mathcomp Require Import ssreflect.
Structure struct_type := struct_cstr { type_field : Type; nat_field : nat }.
Definition struct_val1 := struct_cstr bool 1.
Definition f (x : struct_type) (y : type_field x) := nat_field x.
Canonical struct_val1.
Definition f1 := f _ true.
Print f1. (* f1 = f struct_val1 true *)
では、Canonical struct_cstr bool 1. とかするとどうなるか、というと、 これは syntax error だった。
elim. と apply: XXX_ind と同じ結果になるかどうか、について少し調べてみた。
違う結果になる、と思った原因は以下の経験があったからであり、(SSReflectではなく) Coq の elim と apply nat_ind の話だった。
Goal forall n, n + 0 = n. intro n. elim n. (* subgoal: 0 + 0 = 0 subgoal: forall n0 : nat, n0 + 0 = n0 -> S n0 + 0 = S n0 *) Abort. Goal forall n, n + 0 = n. intro n. apply nat_ind. (* subgoal: n + 0 = 0 subgoal: forall n0 : nat, n + 0 = n0 -> n + 0 = S n0 *) Abort.
ただし、これは SSReflect でも似た挙動になる。
From mathcomp Require Import all_ssreflect. Goal forall n, n + 0 = n. move=> n. elim: n. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal forall n, n + 0 = n. move=> n. apply: nat_ind. (* subgoal: n + 0 = 0 subgoal: forall n0 : nat, n + 0 = n0 -> n + 0 = n0.+1 *) Abort.
しかし、これは elim: n と apply: nat_ind. の比較になっていて、 記述されていた elim. と apply: nat_ind. の比較になっていない。 elim. をするには move=> n する前の状態でなければならないので、 その状態だと以下のように同じになる。
From mathcomp Require Import all_ssreflect. Goal forall n, n + 0 = n. elim. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal forall n, n + 0 = n. apply: nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *)
Coq の elim や induction は引数が必要なので、SSReflect の elim. 相当のことはできないが、 apply については同じ結果になる。
Goal forall n, n + 0 = n. apply nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> S n + 0 = S n *)
ただし、以下のように定義した関数 f を使った状態では、 Coq の apply と SSReflect の apply: は異なる結果になる。
Coq では以下のようになり、これは証明できない。
Definition f z := forall n, n + z = n. Goal f 0. apply nat_ind. (* subgoal: f 0 subgoal: forall n : nat, f n -> f (S n) *)
SSReflect では以下のようになり、うまくいく。
From mathcomp Require Import all_ssreflect. Definition f z := forall n, n + z = n. Goal f 0. apply: nat_ind. (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *)
この違いは apply と apply: で nat_ind の P の探しかたが違うことに起因する。
nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n
Coq の apply には、補題の結論が P x であり、ゴールの結論が g y という形の場合は P を g、x を y にマッチさせるという仕掛けが入っている。
それに対して SSReflect の apply: t は、以下のような refine を順に試して最初にうまくいったものを使う、となっている。
refine t refine (t _) refine (t _ _) ...
この f 0 については、_ が 3つの場合と 4 つの場合に成功する。
From mathcomp Require Import all_ssreflect. Definition f z := forall n, n + z = n. Goal f 0. refine (nat_ind _ _ _). (* subgoal: 0 + 0 = 0 subgoal: forall n : nat, n + 0 = n -> n.+1 + 0 = n.+1 *) Abort. Goal f 0. refine (nat_ind _ _ _ _). (* subgoal: f 0 subgoal: forall n : nat, f n -> f n.+1 *) Abort.
この場合には _ が少ない 3つのほうが証明がうまくいくケースであったが、 複数の可能性がある場合に、常に少ない方が証明がうまくいくものであるかはわからない。
<URL:http://www.morikita.co.jp/books/book/3287>
計算で可能なことは計算でやったほうが証明が簡単になるというのはポアンカレ原理というらしい。 でも検索しても出てこないなぁ。 1902年ということなので、「科学と仮説」という本に載っているのかな。
それはそれとして、読んでいて気がついたこと:
CertiCoq の proof elimination はどうなっているのだろうか。
From CertiCoq Require Import CertiCoq.
Definition nat3 := 3.
CertiCoq Compile nat3.
Definition sig3eq : { n | n = 3 }.
Proof.
exists 3.
reflexivity.
Qed.
Print sig3eq.
(*
sig3eq =
@exist nat
(fun n : nat => @eq nat n (S (S (S O))))
(S (S (S O)))
(@eq_refl nat (S (S (S O))))
: @sig nat (fun n : nat => @eq nat n (S (S (S O))))
*)
CertiCoq Compile sig3eq.
Definition sig3lt : { n | 0 < n }.
Proof.
exists 3.
auto.
Qed.
Print sig3lt.
(*
sig3lt =
@exist nat
(fun n : nat => lt O n)
(S (S (S O)))
(le_S (S O) (S (S O)) (le_S (S O) (S O) (le_n (S O))))
: @sig nat (fun n : nat => lt O n)
*)
CertiCoq Compile sig3eq.
で、実行すると以下のような結果が出てきた。
nat3 の 0(0(0(0))) は前にみたとおりで、S (S (S O)) だろう。
extraction だと nat3, sig3eq, sig3lt は同じ結果が出てくるので、 CertiCoq の proof elimination は証明が完全には消えないのだろうな。
sig3eq, sig3lt は sig 型のコンストラクタであるところの exist で作られた値だが、exist の型は以下のとおりで 4引数である。
exist : forall (A : Type) (P : forall _ : A, Prop) (x : A) (_ : P x), @sig A P
だが、実行結果の 0(0(0(0(0))),0(565fdb20,0)) はたぶん 2引数になっている。 A と P は型と命題なのでこれらは消しているのだろう。 そして、残っている最初の引数は 3 なのでで、x だろう。 で、後の引数はおそらく、P x の証明だろう。
生成されたコードをみると、証明の部分に入る値は sig3eq と sig3lt でだいたい同じで、 また、(@eq_refl nat (S (S (S O)))) や (le_S (S O) (S (S O)) (le_S (S O) (S O) (le_n (S O)))) のような複雑な値を作っているようには見えない。 また、なにか自己参照をしている感じで、これはあれだな。 Letouzey2004 で出てきた、let rec f x = f の f だろう。 (実際には let __ = let rec f _ = Obj.repr f in Obj.repr f の __)
つまり、証明の中身は自分自身を返す謎の関数に置き換えるが、 完全に除去することはしないのではないかな。
証明に対応する値が残っていれば、strict evaluation でも変なことはおきないし、 まぁ、そんなものか。
Gallina 全体を扱うということは、依存型を扱う必要がある。 proof elimination で消えてしまうものはいいとして、消えないもの、 とくに以下のような、値によって型が変わるものをどう扱うか気になる。 (以下の例では、bool な b の値によって f1 と f2 の返値は bool か nat か変化する)
Definition ft (b : bool) := if b then bool else nat. Definition f1 (b : bool) : ft b := match b return ft b with | true => true | false => 0 end. Definition f2 (b : bool) : ft b := match b return ft b with | true => false | false => 1 end. CertiCoq Compile f1. CertiCoq Compile f2.
というわけで CertiCoq でコンパイルして、f1 と f2 のコンパイル結果の違いを眺めるなどしてみたところ、 たぶん、uniform representation という気がする。 つまり、任意の値は (ポインタかもしれないけど) 1 word で表現できるというやつである。 そういう表現であれば、OCaml の Obj.magic 相当 (あるいは、C の pointer や整数の cast) が 可能であり、依存型であっても動作するコードを生成するのはなんとかなる。
GC (というか、メモリ管理) のところを調べれば確認できるだろ、ということで以下のあたりをながめると やはりそれっぽい。
というか、なんか見覚えがある感じの構造や用語が... おぉ、gc.h の先頭に The current Certicoq code generator uses Ocaml object formats と書いてある。 やはり。
いつのまにか CertiCoq が公開されていたので、動かしてみた。 (CertiCoq というのは、証明された Gallina のコンパイラ。 Gallina は Coq の中に入っている依存型で ML っぽい言語)
<URL:https://github.com/PrincetonUniversity/certicoq>
コンパイルはだいたい README.md に書いてあるとおりでいけた。
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev opam switch -A 4.05.0 coq87 eval `opam config env` opam install coq.8.7.1 opam pin add coq 8.7.1 opam install coq-template-coq coq-ext-lib coq-squiggle-eq.dev coq-paramcoq make make install sh make_plugin.sh make install
make_plugin.sh は ちょっと変で、stat -f "%m" file というのコマンドは手元では動かない。 (mtime を調べているっぽいが... そういう stat コマンドがあるかどうかよくわからない -> NetBSD 1.6 発祥の stat にあるようだ。) 適当にいじってどうにかした。
次のステップは plugin/README.md に書いてあり、CertiCoq Compile ref. というコマンドが使えるようになるようだ。
試しに以下のようにしてみる。
From CertiCoq Require Import CertiCoq. Definition nat3 := 3. CertiCoq Compile nat3.
すると、Top.nat3.c というファイルが生成された。 内容は以下のとおり。
struct thread_info;
struct thread_info {
unsigned int *alloc;
unsigned int *limit;
struct heap *heap;
unsigned int args[1024];
};
extern void body(struct thread_info *tinfo);
extern void garbage_collect(unsigned int *, struct thread_info *);
extern _Bool is_ptr(unsigned int);
unsigned int const body_info_0100111[2] = { 6, 0, };
void body(struct thread_info *tinfo)
{
unsigned int x110;
unsigned int x111;
unsigned int kapf_0000111;
unsigned int k_1000111;
unsigned int *alloc;
unsigned int *limit;
unsigned int *args;
alloc = (*tinfo).alloc;
limit = (*tinfo).limit;
args = (*tinfo).args;
if (!(*body_info_0100111 <= limit - alloc)) {
(garbage_collect)(body_info_0100111, tinfo);
alloc = (*tinfo).alloc;
}
x110 = 1U;
x111 = (unsigned int) (alloc + 1U);
alloc = alloc + 2U;
*((unsigned int *) x111 + -1) = 1024U;
*((unsigned int *) x111 + 0) = x110;
kapf_0000111 = (unsigned int) (alloc + 1U);
alloc = alloc + 2U;
*((unsigned int *) kapf_0000111 + -1) = 1024U;
*((unsigned int *) kapf_0000111 + 0) = x111;
k_1000111 = (unsigned int) (alloc + 1U);
alloc = alloc + 2U;
*((unsigned int *) k_1000111 + -1) = 1024U;
*((unsigned int *) k_1000111 + 0) = kapf_0000111;
*(args + 1U) = k_1000111;
return;
}
まぁ、まじめなコンパイラなので、もとのコードは想像しにくい。
これを動かすためのコードを探すと、theories/Runtime にそれっぽいのがあった。 theories/Runtime/Makefile には three というサンプルプログラムを作るルールが書いてあるのだが、 ソースが見当たらない。 なので、必要な runtime だけビルドしてみる。
cd ~/coq/certicoq/theories/Runtime make main.o nogc.o
で、さっき生成した Top.nat3.c のところに戻って、コンパイルしてみる。 (コンパイルオプションは theories/Runtime/Makefile に書いてあったもの)
gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/nogc.o Top.nat3.c
で、実行してみる。
% ./a.out Time taken 0 seconds 0 milliseconds 0(0(0(0)))
まぁ、動いたんですかね。
次は、自然数の 3 じゃなくて、10 を試してみる。
Definition nat10 := 10. CertiCoq Compile nat10.
これで Top.nat10.c が生成され、実行すると以下のようになる。
% ./a.out Time taken 0 seconds 0 milliseconds 0(0(0(0(0(0(0(0(0(0(0))))))))))
まぁ、0 の数がコンストラクタの数なのだろう、たぶん。
3 が 0(0(0(0))) ということは S が 3個と O が 1個。 10 が 0(0(0(0(0(0(0(0(0(0(0)))))))))) ということは S が 10個と O が 1個。
nat も素朴にコンストラクタで構成するわけだな。
では、この前報告した strict evaluation だと無限再帰になるやつを試してみよう。
Definition fstarg (x y : bool) := x. Fixpoint f (z : bool) := fstarg true (f z). Definition g := f true. CertiCoq Compile g.
これで Top.g.c が生成され、コンパイルして実行してみる。
% gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/nogc.o Top.g.c (警告省略) % ./a.out Ran out of heap, and no garbage collector present!
お、GC が必要ですか。
さっきの theories/Runtime で make gc.o として GC を作ってもう一回。
% gcc -m32 -g -O2 ~/coq/certicoq/theories/Runtime/main.o ~/coq/certicoq/theories/Runtime/gc.o Top.g.c % ./a.out Ran out of generations
こんどはしばらく時間がたった後にエラーになった。 まぁこれは CertiCoq の責任じゃない (Coq でどうにかすべき) だろうけど。