2012年12月06日

ちなみに

ML/LL Advent Calendarのネタとしてはいくつか思いついたものがあって、

  • Linear Logic
  • Linear Lisp(別のAdvent Calendarで出たようなので避けて賢明か)
  • Module Type(Coqの)
  • Moonlit Lo...げふんげふん

なんだったか忘れたね。

posted by chiguri at 20:32| Comment(0) | TrackBack(0) | 雑多

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 ... := ...とk


ここで記事は途切れて・・・ない。

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とか、ダメ、絶対。

*1:matchはLtacにもある。

*2:Gallinaの範囲に帰納型の宣言はない。この宣言、CICの項ではあるのだが・・・

*3:Calculus of Construction、人によってはCoCと略す。

*4:ちなみに実際に元のスクリプトを使うと、eq_indではなくeq_ind_rを使った証明になる。rewrite <- IHnならeq_indとf_equalを使った証明。eq_indでいいじゃん・・・

*5:letとfunは型付け規則が違う。funは中身を展開しないが、letは展開した結果で行う。

posted by chiguri at 13:52| Comment(0) | TrackBack(0) | Coq