2014年12月06日

Theorem Prover Advent Calendar 6日目:Coqでの前向き証明を始めるまで

タイトルの通り、これはTheorem Prover Advent Calendarの6日目のための記事である。


MizarやIsarをご存じだろうか?
Mizarは数学的な体系について性質を証明し、その証明が正しいことを機械で確認する、というのが目的である。
そのため、比較的証明を自然言語(英語)で書いたものに似せている。
実際の証明は、「こういう仮定がある。これを変形するとこうである。この補題からこういうことが言える。これはゴールと等価であるため、成立することが言える。」のように、仮定から前向きに証明を行うことがよく行われる。
この前向き証明だが、比較的読みやすいのが特徴である。
Isarは、このMizarの書き方をIsabelle上で使えるようにしたシステムである。
どうやら、証明が終わった後に前向き証明に書き換えるということを行われることも多いらしい。


さて、Isabelleに実装されていることをCoqで実装されていないと言うことがあろうか。
いやたくさんあるけど。
しかもかなりほしいものばっかりだけど。
スレッジハンマーとか。
ただし、今回紹介するこの機能に関しては、普通に論文も出て、さらに現在のCoqに実装されている。
マニュアルの11章を見よう。
ここからはそれを見ながらの話になる。


以上、前置き終わり。
ところで、前向きと書いたが、この機能自体は宣言的(declarative)という方が一般的だ。
すまないがタイトル変えるの面倒なので流して欲しい。
そして、マニュアルを書いている人はどうやら数学的証明と呼びたいようだ。
もう何でもいいや。

とりあえずここで書いている「数学的証明言語」とは、本来の証明の記述よりも弱いものらしい(11.1.3)。
記述時に使う自動証明がうまくいかなかった場合に、不完全な(普段で言うadmitで飛ばしたような)証明が書けてしまう。
この方向での証明で、なぜ不完全なものを書けるようにしたのか首を傾げるのだが、著者としては初学者が容易に学べるようにしたい、等の意図があったらしい。
エラーと切り替えられるようにした方が良いと思うのだが(admitにそういう機能が欲しい)。
ちなみに、不完全な証明を書くと、コマンドを打つ度に何度も何度も「これが証明できないよ」と言ってくる。

この機能の、標準的(legacy)Coqとの違いは大体以下の通り(上も含めている)。
  • focusという機能で「今から証明するものを一つに絞る」機能がある。表示範囲が圧迫されない意味では悪くなさそうな機能だ。

  • 証明できないようなものを書いても「後で埋められるようにwarning出すだけにしている」。(上に書いた)

  • 通常のtacticはコマンドの特定の位置に書くか、escapeコマンドで一旦通常モードに戻して使わせる。特定の場所とは、例えばそのときに成り立つ命題を作る際のusingの直後。ちなみに、by 変数かusing tacticで進めるのが主だが、何も書かないとfirst-orderで解くらしい(11.3.14)。これで解けないと「不完全な証明」となる。

  • 変数名などの自動生成は可能だが、必ず_から始まり、次のコマンドの終了後消える(11.2.1)。これは変数名の衝突を避けることと、名前つけるのが面倒なことのバランス取れてるかもしれない。必要なら名前をつけろ、というのも理解できる。


想定環境も書いてあるが、普通にCoqを使う範囲ならば問題なさそうだ。
coqtopやcoqide、Proof-Generalもある。
他にもあるが、今回はちょっと放っておこう。
例えばPCoqが使えないと書いてあるけれど、そもそも今まともに使えるのかわからない(バージョン1.4が2003年2月に出ている。2013年ではない。私が大学に入る直前だ。)。


内容に入ろう。
文法が11.2に載っている。
全体としては証明構造を記述するのが主で、ほとんど対応するのは基本的なtacticだ。
命題などをより具体的に書かせている点が違う。
基本的に命題を具体的に書くが、ゴールだけは何度も書かなくて良いように特殊な名前としてthesisが使えるらしい。
"thesis"はみんなだいすき学位論文・・・という意味もあるが、ここでは主張する命題のこと(辞書を見よう)。

文法は読み慣れていないと分かりづらいので、とりあえず動かすのが定石。
11.3で機能を説明しているので、見ていこう。

まず「証明の始め方と終わり方」が書いてある。
そしていきなりAnormalyを出す。しかも"Please report"が出るヤツだ。(実装のバグの可能性が高いから報告してくれ、と言うメッセージ。実装をいじったりすると出る)

え??

続いて「proofコマンドは残りが一つじゃないと使えないんだ」といって3つのサブゴールがある例を使う。
ここでもAnormalyを出す。

おい。


エラーメッセージ作れよ。

なんでこんなのがマニュアルに載るんだろう。

そんな愚痴を言っても始まらないので、実行してみる。

Welcome to Coq 8.4pl4 (June 2014)

Coq < Goal True.
1 subgoal

  ============================
   True

Unnamed_thm < proof.
1 focused subgoal (unfocused: 0)

  ============================
   True

Unnamed_thm < thus thesis. (* first-orderで解いている *)
No more subgoals.

Unnamed_thm < end proof.
No more subgoals.

Unnamed_thm < Qed.
Anomaly: Cannot print a raw proof_instr. Please report.

Unnamed_thm <

うん。マニュアル通りの動き・・・え??

Unnamed_thm <


証明が終わってない。

たしかQedの直後は「証明に使ったスクリプトを出す」はず。
ちなみに証明項はできていて、Show Proofで見られる。

Unnamed_thm < Show Proof.
((fun _fact : True => _fact) I)

うん、まあ若干不思議なことをやってるけど、別に問題なさそうだ(おそらく特徴の一つの、自動生成された変数の使い切りのために関数抽象になっているのだと思う)。
だがエラーだ。
エラー対策しろよ。マジメに。

考えてみると、この機能で書いた証明、今までの記述と同じ分けがない。
それで証明の出力関数が死んでるわけだ。

そう考えると、Qedの直後の出力を抑制できれば大丈夫なはずだが、マニュアルを見てもそんなコマンドは見つからない。
そして、この機能の説明がある章、よく見ると「どの例もQedまで行ってない」のだ。

ふざけんな。

調べてみたが、唯一見つかったのが、出力をほぼ完全に抑制するSet Silentコマンド。
あとでUnsetすれば大丈夫だろう、と高をくくって実行。こんな感じになった。

Unnamed_thm < Qed.
Anomaly: Cannot print a raw proof_instr. Please report.

Unnamed_thm < Set Silent.

Unnamed_thm < Qed.

Coq < Unset Silent. (* 左側が変わってるのでうまくいったっぽい *)

Coq < Print All.
 >>>>>>> Library Top
Unnamed_thm : True


Coq < (* Goalだから勝手につけられた名前だができている *)



ようやく始められる状態まで来たが、さすがに今回これ以上書こうという気力が湧かない(日をまたぎかねないというのもある)。
なので、この話はここまでと言うことにしておく。
次回をやる気力が湧けば書くかもしれないが、とりあえずこの問題を回避できれば後は書かれている例題を元に少し試してみるだけなので、それぞれで試すこともできるだろう。
まだ紹介するような機能じゃなかった。

腐ってやがる!早すぎたんだ!

なんてね。
posted by chiguri at 22:06| Comment(1) | 雑多

2014年11月22日

SWI-Prolog-Editor

今いる研究室では、Prologが使われている。
当たり前だけれども、それが問題なわけではない。
ただ、それでもTeraPadで書くというのは、さすがにどうなのよ?と思うわけである。
しかもそれ、Perlモードだから。(拡張子が.plのため)

というわけで、軽くエディタを調べてみることにした。
真っ先に出てきたのはEmacsだったが、TeraPadを使っているのでちょっと、と思ってしまった。
次に出てきたのがこれ、SWI-Prolog-Editor
名前の通り、SWI-Prologを前提とした開発環境。
エディタの説明は上のリンクから公式サイトに行ってもらうとして、入れる際の注意と入れたあとの注意を。
・32bitのSWI-Prologしか対応してない。別に64bit OSでも32bitのPrologが動くのでそっちを入れれば良いけれど、なんかもやっとすると言うか・・・
・言語設定ファイルが読めるので、日本語翻訳したものを突っ込むとインストールからエディタの起動まで全部日本語でできる。ただし一部の記述のフォントが違うせいで、その部分で文字化けする。
・設定(Configuration)は一度エディタを再起動しないと反映されない。フリーカーソルモードは使わない人も多いだろう。あと括弧の対応表示はほしいところ。設定して、再起動。XPCEのマニュアルがないと保存時に(ドイツ語で)文句を言ってくるけれど、別に普通に動くので問題ない。
・フォントの設定はメニューの設定の真上か、エディタ画面で右クリック。なんで設定の中じゃないんだろう。
・構文要素を斜体(italic)にすると、こいつが斜体にしたときの幅を再計算しないために文字がめり込む。Pとか。できれば全部斜体は解除することをオススメ。

あと思いついたらいくつかここに書く。
言語設定ファイル(一部翻訳不完全・適宜更新)はここに置いておくので必要な人は持っていってほしい。
文字化け対策で、その部分だけ英語にしようかなと考え中。
posted by chiguri at 23:50| Comment(0) | PC

2014年10月27日

透過SOCKS-SSHプロキシ

前回の多段プロキシの試行はHTTPSの前にあえなく撃沈。
問題点は、プロトコルに対するプロキシでは暗号化に対して微妙なんじゃないか?ということ。
透過でなければ(ようはプロトコルをうまく中継してくれれば)問題ないのだけれども。

そこでRedsocksというHTTPSをうまくやってくれるらしいと書いてあるプロキシを試

ちょっとまて、それじゃ本当にHTTPSしかできない。
できれば、いろんなプロトコルを通したい。俺は使っていないけれどLINEとかLINEとかSteamとか。
学生が互いの連絡に使うのだよ、LINE。俺は使ってないけれど。
結局それでは微妙に終わるのだ。

SOCKSプロキシを前回確かめたのは、SOCKSさえあれば一通りのことができるからだ。
そういえばSSHは通るんだったか・・・
ポートフォワード・・・
ふと、SOCKSのまねごとできないの?という疑問が湧いた。

調べたら、-DでほぼSOCKSプロキシとして動作するという。
これに透過プロキシを組み合わせれば解決?といろいろ試行。
結果、できた。構成はこんな感じ。
クライアント--(ゲートウェイ扱い)-->サーバー--(iptablesによるredirect)-->redsocks--(redsocksによる透過プロキシ)-->ssh--(ポートフォワード)-->外部サーバー-->(外部)
結論としては、危険きわまりないので、事情分からない人は絶対に真似をしないこと。

以下、実現の際に詰まった部分のメモ書き。

詰まった点その1:大体の情報源において、ssh -Dはlocalhostでやっている(安全性考えれば当たり前か)。
localhostならいいのだが、他のマシンから送るには、ポートフォワードのために-gを付けなければならない。(そうでないとconnection refused)
結果として、ssh -Nf -g -D 1080というコマンドに。オプションだらけだ。
まあよしとしよう。

詰まった点その2:大体の情報源において、redsocksはlocalhostでやっている(以下略)。
今回は外部に置いているわけだが、そうなると当然透過プロキシにするためのiptablesの設定が微妙に変わる。
もっともきつかったのは、なぜかINPUTチェインのポリシーをACCEPTにしないと通らなかったことだ。
怖いよこの設定!!

改めて見ると、外部でやるような内容じゃない。
セキュリティのずさんさが目に余る・・・
真面目にいろいろ向上させたいところだが、原因がわからないからなあ。
なんにせよ、とりあえず目標の達成をかくにん。
よかった♡(時代に乗り遅れた)

なお、この記事の真似をしてハッキング被害に遭ったとしても私は「ばーか」としか言いませんのであしからず。
危険だともセキュリティずさんだと言っているし。
posted by chiguri at 20:55| Comment(0) | 雑多

2014年10月24日

Squid、透過多段プロキシの試行

今いる研究室は、大学のネットワークポリシーの関係上、直接ではなく大学のプロキシを通してしかインターネットにアクセスできない。
ああ面倒くさい、家のネットワークと大学のネットワークで切り替えなければならんのか、と思いながら過ごして半年、嫌になってプロキシの自動検出(WPAD、DNSの方)を導入した。
これで良いか、楽になったな、などと思っていたら、なぜかFirefoxが「ネットワークが切り替わったとき」に自動判別をしないという非常にアホな仕様だったので、やはり不便が微妙に解消されない。
本気でChromeとかIEにしてやろうか、などと思ったりもした(これらはネットワークが切り替わると自動で判別しにいく)。
え、FirefoxからIEの情報を見に行け?使ってみれば分かるが、自動検出はプロキシの設定をしないのと同じ扱いになる。無用の長物もここに極まれり。

とりあえずブラウザの切り替えは悩むとして、他にないのかと考えることにした。
幸い、研究室のインフラ自体はそれなりに自由に動かして問題ないので(だからWPADを導入した)、ルーター付近で何かできないか、と思ったりした。
いろいろ調べると、透過プロキシというのがあるという。
なるほど、来たリクエストをプロキシとして通す。これなら自分でプロキシの設定がなどといわなくて良い。ゲートウェイがうまくやってくれるわけだ。

ふと気づくと、透過プロキシは直接そのサーバーがアクセスを行うものだった。調べども調べどもその用例ばかり。
これはどうだろうと考えたが、昔そういえば多段串とか聞いた。透過プロキシが多段プロキシとして動作するならどうだろうか?

というわけで、仮想サーバーとしてUbuntu、その上にSquidをインストールし、試してみることにした。
Squidの設定は普通に調べれば出る。
透過プロキシの設定は、待ち受けポートにtransparentを付けるだけ。あとはiptablesで80番ポート行きのパケットをむりやりその待ち受けポートへ投げる。
多段プロキシの設定は、親のプロキシの設定及びアクセス方法を親のプロキシ経由のみに限定。
やってみたところ・・・ビンゴ!
透過多段プロキシによって、プロキシを設定しなくてもHTTPアクセスができるようになった。

・・・80番ポート?あれ、HTTPSは?

調べたら、Squidでの透過プロキシはHTTPSに対応できない、とのこと。
夢、絶たれる・・・

redsocksという(透過)SOCKSプロキシに、なにかHTTPSプロキシがどうの、と書かれているのを見つけたので、機会を見つけてそちらもチャレンジしてみよう。
あ、ちなみに大学のプロキシはSOCKSプロキシではないので、いろんなSOCKSプロキシ通すもの(widecapとかいろいろあるらしいが)は全て使えない。
redsocksも当然SOCKSプロキシとしては使えないわけだが・・・HTTPS使えればだいぶ違うし・・・


おまけ:SOCKSプロキシかどうかはcurl -x socks5://hogehoge という感じでcurlを使ったproxy設定をすることで確かめた。便利だ。覚えておこう。
posted by chiguri at 00:03| Comment(0) | PC

2013年12月25日

進捗アドベントカレンダーを開いた感想

進捗アドベントカレンダー、昨日で全ての記事がそろいました。
参加してくださった皆様、ありがとうございます。
でもやっぱりこんなのに参加するなんて奇特な方々だなあ、と思います。

さて、振り返ってみると、一番手(私)がいきなり出したは良いけどconnpassのページを更新してなかったり、なんだか記事の最初で「なんでこんな企画考えたんでしょうあの人」なんていってきた方がお二方ほどいたり・・・
なんかばたばたしてますね。
しかも皆さんなんだかんだで進捗ありありでしたね。
お一人くらい、「進捗ダメです」画像を五つくらい並べてくるかと思ってたんですが。
・・・ああそうか、始めた人間がくそまじめっぽそうなのを書いてしまったからですね。
空気読んでないのは私でした。申し訳ないです。

まあしかし、日付が変わる前から担当者のTwitterのページを開いて、そこからブログがあればそこも開いておいて、日付が変わってすぐとか、ちょこちょこチェックして、ということをやるのはなかなか楽しかったです。
本人が申告する前にconnpassの更新始めたりとか。

そういえば、申告方法を事前に決めていなかったのにあとで気づいたのが一番の失敗でしたね。
最終的には皆さんが私にtweetすることで私が載せる、という形にしてしまいましたが。

アドベントカレンダーを次にやるとしたら、次の二点を気をつけたいですね。
・担当日をどうするか。参加時点で希望を出した方が楽。Qiitaさんのアドベントカレンダーは参加する日付も指定出来るみたいなのでそっちの方が良かったかな。
・申告、更新方法をどうするか。これまたQiitaさんだと自分で更新できましたね。やっぱそっちの(ry

以上、ちょっとした反省とか所感でした。
これから一週間という短い間の年末、なんとか少しでも進捗を出したいものですね。
posted by chiguri at 00:56| Comment(0) | 雑多