パターンマッチができるってことは、extractionできるということである。 singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。 一方、empty definitionはそうも行かない。そもそもCoqのterm上…

これが誰かの何かの役に立てば幸いなのだけれども。 さて、述語に対するパターンマッチは述語以外を返してはいけない、といった。 しかし例外がある。 それは、展開する述語がsingletonまたはempty definitionとして定義されている場合。 この場合はSetやTyp…

ちょっと説明してないのもどうかと思ったので。 述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う（inductionはかなり稀か）。 「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら…

これ見る人いるのかな・・・ 昨日の話と全然連続しないが、昨日のシリーズの続き。 Propに属する帰納型（以下、述語と記述）の展開の話。 Coqのマニュアルだとここの4.5.4のAllowed elimination sortsのあたり。 実際のところ、使用者からして気になる部分は…

ちょっと基本的なところから行こう。 pCICと書いているが、まあ多くの人はそんなもの知るまい。 ちなみに、Coqについてそれなりの知識を持っていることを前提に話をするので、せめて利用者としての経験を要求する。 pCICはpredicative Calculus of Inductive…

先週の発表で、「Coqをいじりたい人向けに情報をまとめておいたら役に立ちそう」という言葉をもらった。 そんなのどんだけいるんだろう・・・と思わなくもないが、実際端から端まで読んだわけでもないし（読まなくてもブラックボックスのまま使える部分も多…