この記事はLL/ML Advent Calendarの6日目の記事である。 今年はなかなかに なごやこわい なアドベントカレンダーが出てきたなあ、とかつぶやいたら気づいたら犠牲参加者になっていた。 やっぱり なごやこわい 。 LL名古屋に似たようなのがあるようだが？ あ…

パターンマッチができるってことは、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をいじりたい人向けに情報をまとめておいたら役に立ちそう」という言葉をもらった。 そんなのどんだけいるんだろう・・・と思わなくもないが、実際端から端まで読んだわけでもないし（読まなくてもブラックボックスのまま使える部分も多…

これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって？人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを…

これは、Theorem Proving Advent Calendarの四日目の記事である。 ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。 お題 今回使う道具は、Curry-Howard同型対応、直観主義で失われ…

実は、前回書いたtype class in coqの記事、ちょっと怖いことがある。 このコードを実行すると、メモリを消費したあげくに落ちる。 Check (Compile (CEConst 1)).もちろんEval computeやEval simplでも同様。 なぜかはよくわからないが、まともにCompileの計…

なぜ一度で出来なかったか？ 計画性がないからさ。 さて、ではType classで先ほどの流れをもう一度作ろう。 しかし、先ほどの定義とは、様々な点で異なるので注意。 Class Exp := { Eval : nat }. Instance EConst (n : nat) : Exp := { Eval := n }. Instan…

Coq8.2からType classが導入された。 もともとType classはHaskellにあったものである。 よって、Expression problemもHaskellからやり始めるのが楽である。 だが、私は残念ながらHaskellの世界の住人ではないので、Haskellによる解決に関しては私がこれをや…

一昨日（表示は昨日になるかもしれない）、Coqのサブセットを作ろうかな、と書いた。 でもサブセットってどのくらいよ？という問題が出てくる。 少し考えてみよう。 まず、Coqのサポートしている範囲を挙げる。 言語について：Vernacular（コマンド用言語、…