2012年03月23日

述語の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のパターンマッチは許されている。


実際の流れは以下のとおり。

  1. 述語の矛盾が確定した時点でexfalsoやelimtype FalseなどのtacticでFalseの作成に移る。
  2. Falseの証明に述語のinversionを使う。*1

inversionを使って場合わけをしたいときは、データのdestructの後に上の流れを使ってありえない場合を排除するとうまくいく。*2


このように、例外があることで「述語の存在上ありえない状態」を排除することができる。

そんなにこの状態にはまることはないと思うが、もしあったら参考にしてほしい。

*1:Falseは述語なので、ここでのinversionの使用は許される。

*2:実は、inversionの内部でやっているのはまさしくこれ。Trueを使う部分もあるが、手動では明らかに無駄。

posted by chiguri at 00:04| Comment(0) | TrackBack(0) | Coq
この記事へのコメント
コメントを書く
お名前:

メールアドレス:

ホームページアドレス:

コメント:

この記事へのトラックバックURL
http://blog.sakura.ne.jp/tb/73554491

この記事へのトラックバック