LL/ML Advent Calendar 6日目: gaLLinaで証明する

Coq

この記事は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とか、ダメ、絶対。

*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は展開した結果で行う。

SML#をビルドし・・・ようとした。

PC

以前使ってみようとしたときにlibgmpがないことがわかっていたので、先にmingw32-libgmpを入れてみた。
だが、思わぬところ（configure）で時間かかってしまった。
bash上で./configureをすると、-lgmpがどうのこうのといってくる。


またお前か！


で、いろいろ調べたらmingw32-gmpというパッケージがあり、それを入れたら通った。
その割に、configureの最後にエラーが出たのが気になるのだけれども・・・
まあ、とりあえずml.grm.smlのコンパイルで詰まったようだ。

新しいPCいじりは楽しいなあ

PC

いや、楽しいばかりじゃなくて面倒なことも多いけど。
Lavie Zを買った。
軽いなあ。


しかし、やはり今までのPCではいろいろ設定していたから何から始めていいのかわからないというのがある。
ログオン画面でユーザー選択を自動化したいとか。
ただし、パスワードは入れたい。
さてどうするか。


調べると、Yahoo!知恵袋に同じ質問があった。
が、回答はネガティブ。
ちなみにこのベストアンサー、はっきりいうと間違いである。
まず二点指摘があるので、それを書く。
ちなみにどうやるのか、は少し後ろへ。

問題1：他の回答者へのコメント

もう一人の回答者にいろいろ言っているが、この操作自体は正しい。
ただ、これをやってしまうと質問者の意図にあっていない*1。
出鱈目という前に何が間違っているかくらい指摘すればいいのに。

問題2：無理なこととしたいこと

質問者がしたいことはクラシックログオンではなく、単にユーザー選択なしにパスワード入力をしたいだけだ。
「ようこそ」の文字の直後に自分のユーザーが選択されていてほしいのだ。
別にクラシックログオンをする必要性は全くない。


以上がこの回答の問題だが、一番の問題は「できません」と断言していることである。
が、できたのだからどうしようもない。

ユーザーを自動的に選択させる

残念ながら、複数のユーザーがある時に自動的に選択させるのはわからない。
が、一つなら多少おばかさんなWindowsでも選択してくれるはずである。
いや、ユーザー一つでもされないだろ？という反論はごもっともだが、それはこちらから見える範囲では、という前提を忘れている。
隠れたユーザーまだ残っている。


コンピューターを右クリックし、管理を出すと左に「ローカルユーザーとグループ」という項目が見つかる。
このユーザーを見ると、下矢印のついたGuestやAdministratorとかが見えるはずである。
そして、自分のユーザーと・・・ほか二つほど、私の環境ではHDSHAREUSERとHomeGroupUser$があった。
GuestやAdministratorが無効になっているので、下矢印が付いてる＝無効、と思ってよさそうだ。
さて、ほかにあった二つは・・・無効ではなさそうだ。
つまり、有効なユーザー≠自分だけ、ということになる。


ここまで書けばわかるだろう。
この二つを無効にしたら自動で選択されるようになったのだ。*2


ただ、一応注意しておくと、これらは何らかの理由で存在しているので何が起こるか分かったものじゃないということがある。
何かあったら追記でもすると思うが、くれぐれも自己責任で。

*1:この操作だと、自動ログオンになり、パスワード入力を求められない。

*2:それぞれのユーザーを右クリックし、プロパティを開くと「アカウントを無効にする」というチェックボックスがあるのでそれを入れる。

ふと

雑多

ときどきTwitterで出てくる「言葉狩り」という現象についてちょっと気になったので書いている。
言葉狩りといっても、ある特定の語を禁止し、別の言葉に言い換えてしまうことがほとんどなのだが*1。
いわゆる差別用語とか、特定の侮蔑とか、言いにくいが児ポ関係とか。


特にこの差別用語とかの類では、昔からいくつもの「言葉狩り」が行われてきた。
まあ、直感的には一時的な効果が見込める気がするのはわからなくもない。
だけど、そもそも「言葉狩り」の効果は一時的なんだろうか？
それともそれなりに長期間の効果が見込めるのだろうか？


ここまで何度も行ったんだから、その結果としてどうなったか、が見えてもおかしくないはずなのだが・・・
寡聞にして、それが長期的な効果をもたらしたとは聞いたことがないし、狩られた言葉以外に別の用語が出てくるのは必然だろう。
それは一体なんのためなんだろうか・・・？
それとも、おおっぴらにはなっていないが効果があったのだろうか？
そんなことを気にしてしまった。

*1:それが本質かはよくわからない。