Coq

存在型を全称限量子と代数的データ型でエンコードする

HaskellのGHC言語拡張に含まれる存在型は、existential quantifierを使わずにuniversal quantifierと代数的データ型を組み合わせて表現されます。以前からどうしてこんなことができるのかと思っていたのでそのカラクリを調べてみました。GHC言語拡張では存在…

プログラミングCoqの2章をHaskellに翻訳してみた

皆さん、小悪魔CoqチュートリアルことプログラミングCoq読んでいますか?僕は大変楽しく読ませていただいています。今日第2章にあたるProof-editing mode であそぼうが公開されました。今回はCoqの証明支援の側面がよくわかる章になっていて興味深いのですが…