述語のdestructの例外
これが誰かの何かの役に立てば幸いなのだけれども。
さて、述語に対するパターンマッチは述語以外を返してはいけない、といった。
しかし例外がある。
それは、展開する述語がsingletonまたはempty definitionとして定義されている場合。
この場合はSetやTypeやnatやOやSを返すことが許される。
・・・いや、なにそのなんとかdefinitionって、と言いたくなるだろうがまずは説明を聞いてくれ。
そもそもパターンマッチが述語以外を返してはいけないのは、述語関係のものをすべて消したときに結果が一意にならないからだ。
昨日の問題も、要するにtrueかfalseに決まらないから問題なのだ。
よって、述語の状態が結果に影響を与えなければいい。
究極的には、分岐しなければいい。
つまりそういうことだ。
empty definitionとはコンストラクタを持たない述語のことであり、またsingleton definitionとはパラメータとして述語関係の値以外持たないようなコンストラクタを一つしか持たない述語のことである。
後者はずいぶんややこしいが、つまりはコンストラクタがひとつで、コンストラクタの中にnatだとかSetだとかが入っていなければいい、というもの。
これらはパターンマッチでの展開が結果に影響を与えないので、特別に述語以外を返す展開が許される。
さて、これはどういう場合に役に立つのだろうか？
こんな場面を想定してほしい。
「述語や値の混じった関数を作らなければならない状態で、ある述語が明らかにおかしな値をとった。しかしinversionが使えない。さてどうするか。」
昨日の補足で挙げたinversionができないケースをより細かくしただけだが。
この答えは、Falseを経由する、である。
Falseはboolのfalseではなく、Propに属する矛盾を意味する述語であり、定義は以下のとおり。
Inductive False : Prop := .
典型的なempty definitionである。
したがって、Falseのパターンマッチは許されている。
実際の流れは以下のとおり。
- 述語の矛盾が確定した時点でexfalsoやelimtype FalseなどのtacticでFalseの作成に移る。
- Falseの証明に述語のinversionを使う。*1
inversionを使って場合わけをしたいときは、データのdestructの後に上の流れを使ってありえない場合を排除するとうまくいく。*2
このように、例外があることで「述語の存在上ありえない状態」を排除することができる。
そんなにこの状態にはまることはないと思うが、もしあったら参考にしてほしい。
補足：Falseのパターンマッチのextraction
パターンマッチができるってことは、extractionできるということである。
singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。
一方、empty definitionはそうも行かない。そもそもCoqのterm上は分岐がないのだ。
しかもFalse自体は述語なので消える運命にある。
ではどうなるのか？
結果はこれまた簡単、assert（やそれに類するもの）を使って異常状態であることを知らせる。
なぜなら、検証した結果としてはそこに来ることを想定していないわけだから。
というわけで、これでextractionも可能となり、すべてが丸く収まったわけである。
これで終わり？まだもうひとつある。でもそれはいつ書くか不明。
