2012年03月22日

補足:inversionやinduction

ちょっと説明してないのもどうかと思ったので。


述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う(inductionはかなり稀か)。

「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら怒られた」という経験がある人もいるだろう。

実はこれもまったく同じ原因である。

というのも、tacticは一般に関数や項を作るからだ。


introやapplyのように簡単なtacticは対応する項も割と簡単(関数抽象・関数適用)である。

一方、inversionは結構小難しいことをする。

しかし、小難しいことをしようが何をしようが*1必ず結果は項を作る。

そしてinversionはパターンマッチを作る。

だから怒られる。


inductionは実際には特定の関数をゴールに適用する。

しかし、その関数がパターンマッチを使うため、SetやTypeを返す関数が作成できない。

だから無理、と。


つまりは、根源はすべてパターンマッチができないことである、ということ。

*1:admitでもしない限り。

posted by chiguri at 22:17| Comment(0) | TrackBack(0) | Coq

述語のdestruct

これ見る人いるのかな・・・


昨日の話と全然連続しないが、昨日のシリーズの続き。

Propに属する帰納型(以下、述語と記述)の展開の話。

Coqのマニュアルだとここの4.5.4のAllowed elimination sortsのあたり。

実際のところ、使用者からして気になる部分はそう多くなくて、大体がこの部分。

しかし、非常に読みにくい。

というわけで簡単な説明をする。


destructといいながら、Curry-Howard対応から実際にはパターンマッチなのでこちらを使う。

内容は、パターンマッチで述語を場合分けすると、ある特定の場合にできない場合がある、というもの。

ちなみにSetやTypeに属する帰納型ではどんなものでも返せる。


さて、特定の場合、と言っているがどんな場合かと言うと、返す値が述語じゃないときである。

逆に言うと述語ならOK。SetとかTypeとか(述語でない)型自体とか全部ダメ。

この理由は、proof irrelevanceという考え方から来ている。

まあ、問題を見るにはextractionを考えればいい。


Proof irrelevanceは、簡単に言うと「証明なんてプログラムと関係ないんだから、プログラムとしては無視して問題ないよね?」ということ。

顕著な例がextraction。Coqから別の言語のコードに変換すること。

証明はきれいさっぱり消えるし、依存型も述語部分が消える。

いやはや、なかなか良くできている。


だが、消えるのだから困ることもある。

こんなプログラムが書けたらどうなるだろう?

fun x : or P Q =>
 match x with
 | or_intror _ => true
 | or_introl _ => false
 end

trueやfalseはbool型、boolはSet。orはProp。

さて、extractionするとどうなる?

  1. 関数の引数xは消える。or P Qが述語だから。
  2. trueやfalseは消えない。boolはSetだから。

で、何が出る?関数じゃないことはわかるが、true?false?

つまりはこれがまずい、ということである。*1 *2 *3


だが、この問題、実は例外があって・・・

と言っても長くなるのでまた今度。

実は例外がないとそれはそれで困るのだ。*4

*1:もう少し体系に踏み込めば、これは「気にしない」はずの証明を「プログラムから気にしている」わけで、その意味でおかしい。

*2:実際、先週のPROでこの問題に引っかかった人がいたようだ。

*3:最初はPropがimpredicative sortだからか、とも思っていたが、昨日のオプションを試してもSetからTypeへのパターンマッチが可能なのでそういうわけでもなさそうだ。

*4:逆にこの例外のおかげで自分の研究では少し困ったんだが。

posted by chiguri at 19:00| Comment(0) | TrackBack(0) | Coq

2012年03月21日

pCICとは

ちょっと基本的なところから行こう。

pCICと書いているが、まあ多くの人はそんなもの知るまい。

ちなみに、Coqについてそれなりの知識を持っていることを前提に話をするので、せめて利用者としての経験を要求する。


pCICはpredicative Calculus of Inductive Constructionの略称。

pがつかないCICをある。これはCoqがバージョン7まで使っていた計算。

差はSetというソートがpredicativeになったこと。*1

predicativeかimpredicativeかの差はここ(Coqのドキュメントへ)にある。

簡単に説明すると、全称限量の型が(量化されている変数の型によらず)結果の型だけで決まる場合(Setに属する型が結果なら全称限量全体がSetになる)impredicative、そうでなくて量化されている変数に依存する場合はpredicative。

今はpredicativeなので、forall x : Type, natなどとするとSetではなくTypeになる(逆に言うと、CICではSetになる)。


今日はこの説明だけにしておこうかな。

ちなみに、変な言い方だけれどもpCICと正確に書かない場合もある。

というのも、(p)CICはCoqくらいしか使わないので(少なくとも利用しているシステムで最も有名なものはCoqなので)、CIC=Coqが使っているシステム、くらいに考えている人が多いため。

別に文句はないけど、希に見るので驚かないように。

*1:ちなみに、Coq起動時に-impredicative-sortというオプションでCICを利用したCoqのモードに移る。

posted by chiguri at 19:04| Comment(0) | TrackBack(0) | Coq

2012年03月20日

pCICの細かな部分

先週の発表で、「Coqをいじりたい人向けに情報をまとめておいたら役に立ちそう」という言葉をもらった。

そんなのどんだけいるんだろう・・・と思わなくもないが、実際端から端まで読んだわけでもないし(読まなくてもブラックボックスのまま使える部分も多い)、まとめられる限りまとめるのも重要か。

そんなことを考えたが、そもそも私がみるCoqの実装部分は、pCICの細かな部分がかかわってくる話なのだ。

どないせいと・・・


というわけで、実装について少し説明する前に、pCICの話をしないとなあ、と思った次第。

論文にも書いた内容なので、そんなにここに乗せるのも難しくないはず。

分量を考えなければな。

まあ、今日これから、というわけでもないが・・・

posted by chiguri at 15:06| Comment(0) | TrackBack(0) | Coq

2011年12月15日

Ltacを知りcrushを読む

これはTheorem Proving Advent Calendarの15日目の記事である。

二回目じゃないのかって?人数不足だ。気にしてはいけない。


さて、今日の記事が何に関する記事かは見れば一目瞭然。

Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを読み解くことである。


・・・と書いたが、正直まじめに説明すると長さの関係上やっていられないので、crushの動きを簡単に知る程度にする。

なお、今回もまた内容の関係上背景をあまり長くかけないので、一通りCoqの知識を持っているものとする。

それでも無理なのだからもはやどうしようもない。

crushって何?

有名な、といっておきながらそれか、といわれそうだが、一応説明する。

crushというのは、Coqの初級者以上*1が読むと勉強になること請け合いの、Certified Programming with Dependent Typesという本(略称CPDT)*2で頻繁に使われる、証明を省略するためのtacticsである。

省略する、といったが、実際に中身を見ると確かに証明しているため、(本当の意味で省略である)admitとは異なる。

要するに、証明が自動化されているわけである。

crushの定義

このcrushだが、Ltacで記述されている。

その定義は下の通り。

Ltac crush := crush' false fail.

言うまでもなく、このcrush'もまた別に定義されている。

それらを遡ると、全体で100行前後くらいになる。


さて、crushの書いてあるソースをここで一応リンクしておきたい。

CPDTのリポジトリ中にあるCpdtTactics.vの150行目である。

手元にほしいならば先にあげたページのtarballから展開してほしい。

src/CpdtTactics.vが対象ファイルである。


コードを見るとsimplHyp、inster、crush'の三つが大きいことがわかるが、実はinsterは読まなくてよいので今回は省略し、残りの二つを読む。

ただし、今回は別に詳細を説明したいわけではないので適度に手を抜くし、また動作全体を追うことはしない。

Ltacの基本

Ltacも通常のCoqの項同様に、関数型に似た構成をとる。

パターンマッチがあり、関数があり、letがある。

また、追加としていくつかの特殊なデータがある。

たとえばgoalは特殊なデータで、仮定の集合と証明するゴールの型の組である。

これまたパターンマッチで処理する。

ただし、パターンマッチの挙動が少し異なるので、その点に関しては軽く触れておきたい。

match goal with
| H : _ |- _ => ...
end

こんな例を考える。なお、...は省略しているだけである。こんなコードではない。

パターンにおいて、|-の左が仮定、右がゴールである。

網羅性について

Ltacのパターンマッチは網羅的である必要はない。

たとえば上のパターンマッチは仮定が何もないケースがかかれていないが、その場合Ltacでは失敗するだけである。

証明時にエラーが出ることがあるが、要するにあれが出る、というだけだ。

必要に応じてtryなどを使うことで例外処理も可能である。

マッチングの順序

Coqのマニュアルを見ると「リニアじゃない」とかかれている。

この意味を説明するために上の例を用いる。

今書いている証明は仮定が二つあるとする。これらをH0とH1としよう。

すると、上のコードでは、まずH0がHとして束縛される。なお、ここからわかるとおり、Hは仮定の名前ではなく、パターンマッチに使われている変数である。

H0を試して失敗した場合、Coqは次にH1をHとして束縛する

論理型プログラミングを知っている人は、バックトラックを行っていると思ってほしい。

なお、H1も失敗した場合は、このパターンマッチ全体は失敗する。


とりあえずこの二点は覚えておいてほしい。

全体の簡略化

それぞれのコードを見たいのだが、まずcrushとcrush'のコードを見る。*3

Ltac crush' lemmas invOne :=
  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
  let rewriter := autorewrite with cpdt in *;
    repeat (match goal with
              | [ H : ?P |- _ ] =>
                match P with
                  | context[JMeq] => fail 1
                  | _ => (rewrite H; [])
                    || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
                      || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
                end
            end; autorewrite with cpdt in *)
  in (sintuition; rewriter;
      match lemmas with
        | false => idtac
        | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
          repeat (simplHyp invOne; intuition)); un_done
      end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

Ltac crush := crush' false fail.

さて、crush'の定義を追うと、全ての再帰呼び出し時の引数が呼び出し時と同じであることに気づくだろう。

今回はcrushを読み解くだけなので、この前提としてcrushの引数でcrush'を部分評価してみよう。

lemmasをfalseに、invOneをfailにし、評価を行う。idtacが常に成功することを考慮すると、crushは次のcrush''と等価になる。*4

Ltac crush'' :=
  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp fail; intuition; try subst); try congruence in
  let rewriter := autorewrite with cpdt in *;
    repeat (match goal with
              | [ H : ?P |- _ ] =>
                match P with
                  | context[JMeq] => fail 1
                  | _ => (rewrite H; [])
                    || (rewrite H; [ | solve [ crush'' ] ])
                      || (rewrite H; [ | solve [ crush'' ] | solve [ crush'' ] ])
                end
            end; autorewrite with cpdt in *)
  in (sintuition; rewriter; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

今度はもう一つのsimplHypの番だ。

Ltac simplHyp invOne :=
  let invert H F :=
    inList F invOne; (inversion H; fail)
    || (inversion H; [idtac]; clear H; try subst) in
  match goal with
    | [ H : ex _ |- _ ] => destruct H

    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
      (assert (X = Y); [ assumption | fail 1 ])
      || (injection H;
        match goal with
          | [ |- X = Y -> G ] =>
            try clear H; intros; try subst
        end)
    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
      (assert (X = Y); [ assumption
        | assert (U = V); [ assumption | fail 1 ] ])
      || (injection H;
        match goal with
          | [ |- U = V -> X = Y -> G ] =>
            try clear H; intros; try subst
        end)

    | [ H : ?F _ |- _ ] => invert H F
    | [ H : ?F _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F

    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H

    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
  end.

invOneをfailにしても小さくならない?それは甘いといわざるを得ない。

invertは24-28行目のブロックで呼ばれているが、invertの第一引数は常に関数が渡される。

したがって、invert H Fは常にinList F failを呼ぶ。

inListの定義は、第二引数に第一引数が入っているかを調べるものだが、真っ当に考えてfailに関数部Fが入っているはずが無い。*5

よって、このinListの呼び出しは常に失敗し、そしてinvertの呼び出しも常に失敗する。

つまり、invertを呼ぶ=パターンマッチ失敗、と見ていい。

ではさらに書き換えていこう。*6

Ltac simplHyp' :=
  match goal with
    | [ H : ex _ |- _ ] => destruct H

    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
      (assert (X = Y); [ assumption | fail 1 ])
      || (injection H;
        match goal with
          | [ |- X = Y -> G ] =>
            try clear H; intros; try subst
        end)
    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
      (assert (X = Y); [ assumption
        | assert (U = V); [ assumption | fail 1 ] ])
      || (injection H;
        match goal with
          | [ |- U = V -> X = Y -> G ] =>
            try clear H; intros; try subst
        end)

    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H

    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
  end.

それなりに小さくなった。

ではそれぞれを見ていこう。

simplHyp'

さて、simplHyp'は始まって早々にgoalのパターンマッチを行っている。

最初のケース(3行目)は「existsで囲まれている要素が仮定にあったら」「それを分解しなさい」といっている。

別に難しくはない。


次のケース(5行目)は「同じ関数を適用した結果が等しいという仮定があったら」「引数の等号にしなさい」である。

仮定に引数の等価性がすでにわかっている場合は無視する(6行目)*7ことにし、関数側がコンストラクタであるような場合(7-11行目)に対応している。

8行目から11行目は「実際に引数の等号が出来たか」を確認するためであり、出来てなかったら失敗するようになっている。

いちいち事前のチェックや事後のチェックにいろんな技術が必要なあたり、面倒である。

12行目のケースは先ほどの二引数版である。特に不思議なことはしていないので省略。


次のブロック(21-22行目)はexistTというコンストラクタの場合であり*8、同じ型から取れて、それが等号ならその中身も同じ、というものと、単によくわからないからinversionする、という二つに分かれる。

最後のブロックはどうでもいいだろうから無視する。*9


総じて何してるかというと、等式や述語を展開して仮定やゴールを単純にしようとしているわけである。

crush''

Ltac crush'' :=
  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp'; intuition; try subst); try congruence in
  let rewriter := autorewrite with cpdt in *;
    repeat (match goal with
              | [ H : ?P |- _ ] =>
                match P with
                  | context[JMeq] => fail 1
                  | _ => (rewrite H; [])
                    || (rewrite H; [ | solve [ crush'' ] ])
                      || (rewrite H; [ | solve [ crush'' ] | solve [ crush'' ] ])
                end
            end; autorewrite with cpdt in *)
  in (sintuition; rewriter; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).

ほぼ再掲である。

冷静に見てみると割とやっていることはむちゃくちゃだ。

まず、sintuitionは全体をsimpl、intuitionで分解、変数を出来る限り消す、simplHyp'を試して分解して変数を消すのを失敗するまで繰り返す、等価性を使って証明してみる、といった流れ。

残りはrewriterなのだが、これがなかなか面倒くさいことをやっていて、一文なのですぐわかる。単にヒントデータベースcpdtを使ってautorewriteし、その後、全ての仮定について書き換えを試みる。

ただし、この仮定の中にJMeq(John Meyer equality)がある場合はまずいらしく、その仮定を飛ばす。また、当然その仮定が等式でなければ飛ばす。

等式の場合で前提がある場合は、その前提を再びcrushで解こうとする。

この試行が終わった場合、再びautorewriteを行い、上の試行を繰り返す。

sintuitionが構造の単純化を行い、rewriterが書き換えられそうな場所を全て書き換えていく、という中身らしい。


この内容を元に考えると、crushの中身は、単純化する、書き換える、単純化する、書き換える、単純化する、omegaで解いてみる、それで駄目なら仮定が矛盾していると思ってomegaで解いてみる、と。

思った以上にomega頼りだ。


というか、変形してomegaしてる以外なにもしない。

つまりcrushとは

がんばったomegaである。


なんだろうこの敗北感・・・

すごく読むのに時間がかかったのに・・・*10


なお、全然Ltacの勉強じゃない、という突っ込みは受け付けないのであしからず。

*1:曲がり間違っても初心者は読んではならない。

*2:正確にはまだ本になっていないが、著者いわく「本当にもうすぐMIT Pressから出るよ!」とのこと。

*3:crush'のインデントが違和感あったので修正している。

*4:ここでinsterは消えるため、今回は読まない。

*5:そもそもfailはtacticsであり、FはGallina上の関数である。

*6:この流れは部分評価ではない。Fとfailの関係を与えないと不可能。

*7:assumptionが原因の失敗では||以降が実行され、fail 1の失敗では||を突破してパターンマッチの結果が失敗となる。

*8:existのPropが全てTypeになったものだと思ってほしい。

*9:injectionがコンストラクタを展開するものだとわかれば自明。

*10:部分評価を思いついたのがある程度読み解いた後だったのが災いした。

posted by chiguri at 12:23| Comment(0) | TrackBack(0) | Coq