述語の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するとどうなる?
- 関数の引数xは消える。or P Qが述語だから。
- trueやfalseは消えない。boolはSetだから。
で、何が出る?関数じゃないことはわかるが、true?false?
つまりはこれがまずい、ということである。*1 *2 *3
だが、この問題、実は例外があって・・・
と言っても長くなるのでまた今度。
実は例外がないとそれはそれで困るのだ。*4