述語の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:逆にこの例外のおかげで自分の研究では少し困ったんだが。

補足：inversionやinduction

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


述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う（inductionはかなり稀か）。
「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら怒られた」という経験がある人もいるだろう。
実はこれもまったく同じ原因である。
というのも、tacticは一般に関数や項を作るからだ。


introやapplyのように簡単なtacticは対応する項も割と簡単（関数抽象・関数適用）である。
一方、inversionは結構小難しいことをする。
しかし、小難しいことをしようが何をしようが*1必ず結果は項を作る。
そしてinversionはパターンマッチを作る。
だから怒られる。


inductionは実際には特定の関数をゴールに適用する。
しかし、その関数がパターンマッチを使うため、SetやTypeを返す関数が作成できない。
だから無理、と。


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

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