LL/ML Advent Calendar 6日目: gaLLinaで証明する
この記事はLL/ML Advent Calendarの6日目の記事である。
今年はなかなかに なごやこわい なアドベントカレンダーが出てきたなあ、とかつぶやいたら気づいたら犠牲参加者になっていた。
やっぱり なごやこわい 。
LL名古屋に似たようなのがあるようだが？
あの有名なmzpさんが似たような題で発表をしたらしい。
が、録画されたUstreamの動画を見たところ、ぜんぜんGallinaの話をしてない。
そりゃないぜとっつぁんmzpさん。
というわけで、今回は実際にGallinaを使って（証明して）みよう、という話。
Coqの中の言語
Coqはいくつもの言語を持っている。
いやほんと。Coqはシステム全体の総称。
CoqではVernacularとGallinaとLtacが主に使われて、あとはRussel（Programコマンドのシステム名）とかが入っている。
ほかは知らない。あるかもしれないし、ないかもしれない。
Vernacular
基本的にあなたがトップレベルで書いているのはVernacular。
私が書くのもVernacular。
このVernacularはコマンド記述言語。
DefinitionとかTheoremとかInductiveとかFixpointとかClassとかRecordとかGoalとかSearchとかSearchAboutとかPrintとかCheckとか全部Vernacular。
NotationとかCoInductiveとかLocateとか（以下略
Ltac
証明といえばLtac。
applyとか(e)autoとかintro(s)とかinductionとかrewriteとかinversionとかomegaとかgeneralizeとか全部Ltac。
revertとかelimとかcongruenceとか(ry
Gallina
Coqの項記述言語。
fun x => tとかmatch a with ... endとかforall P : Prop, ...とか全部Gallina。*1
fix f p ... {struct p} : T := ...とかcofix f ... := ...とｋ
ここで記事は途切れて・・・ない。
Gallinaで証明？
が、あくまで項記述言語。
当然Ltacなんて使えない。
で、Vernacularはできる限り避けるわけだけど・・・
帰納型の宣言ができない。
関数の宣言は無理やりできなくもないが、帰納型ばかりは対処のしようがない*2。
しかし、帰納型を入れないと完全にCC*3になってしまうので、そこだけは我慢する。
また、型チェックができないといけないので、Checkコマンドだけは使うことにする。
残念ながらつまらない例
つまらない例しか出さない（出せない）。
Goal forall n : nat, n + 0 = n. Proof. intro n; induction n. reflexivity. simpl; rewrite IHn; reflexivity. Qed.
これをGallinaでやろう。
とりあえず問題の整理。
- 証明にLtac使ってる
- +ってなに？
まあ、実際のところLtac使ってる、なんてPrintコマンドで項を出してしまえばいいんだけど・・・
四苦八苦しながらとりあえずLtacを使わずに書いたものは以下のとおり*4。
Check
(nat_ind (fun n : nat => n + 0 = n)
(eq_refl 0)
(fun (n0 : nat) (IHn : n0 + 0 = n0) =>
eq_ind (n0 + 0)
(fun n1 : nat => S (n0 + 0) = S n1)
(eq_refl (S (n0 + 0)))
n0
IHn) : forall n : nat, n + 0 = n).ちなみに最後の型注釈は表示される型を強制するため。
あとは+が気に食わないので、+を展開してみる。
Check
((fun plus : nat -> nat -> nat =>
nat_ind (fun n : nat => plus n 0 = n)
(eq_refl 0)
(fun (n0 : nat) (IHn : plus n0 0 = n0) =>
eq_ind (plus n0 0)
(fun n1 : nat => S (plus n0 0) = S n1)
(eq_refl (S (plus n0 0)))
n0
IHn) : forall n : nat, plus n 0 = n)
(fix plus (n m : nat) :=
match n with
| O => m
| S n' => S (plus n' m)
end))
> Error: In environment
> plus : nat -> nat -> nat
> The term "eq_refl 0" has type "0 = 0" while it is expected to have type
> "(fun n : nat => plus n 0 = n) 0".はて、どうやらplus 0 0が0だと信じられないらしい。
ああそうか、代入してくれないからか。
じゃあletでOKだな*5。
Check
(let plus : nat -> nat -> nat :=
fix plus (n m : nat) :=
match n with
| O => m
| S n' => S (plus n' m)
end in
nat_ind (fun n : nat => plus n 0 = n)
(eq_refl 0)
(fun (n0 : nat) (IHn : plus n0 0 = n0) =>
eq_ind (plus n0 0)
(fun n1 : nat => S (plus n0 0) = S n1)
(eq_refl (S (plus n0 0)))
n0
IHn) : forall n : nat, plus n 0 = n).通った通った。
欲を言えばnat_indとかeq_indとかも消したい。
そこまでやったら死にそうだから今回はやめておく。
まとめ
できる限りGallinaで証明を書くとこうなる、というのを見せた。
関数はlet束縛、rewriteはeq_indを使えばできる。
なんて非現実的。VernacularとLtac万歳。
ちなみに、まじめに上のコードは手で書いているので、しばらくeq_indの使い方のわからなさとエラーメッセージの意味不明さに泣きそうになった。
最後に
vernacuLar×gaLLina×Ltacとか、ダメ、絶対。
