ssreflectのインストール時とcoqインストール時に違うverのocamlが使われていると嵌る

通常は、tarballとってきてmake installでいけるのだが、使っているcoqをコンパイルしたときのocamlと
ssreflectのプラグインをコンパイルするときのocamlのバージョンが違っているとinterface mismatchが出る。
このとき、parsing.cmxなどのロード中のモジュール「on Pervasives」などと原因となったモジュールの名前が表示されるので、ocamlobjinfo /usr/local/lib/coq/parsiong.cmx | grep Pervasives等でハッシュを見ることで確認できる。
coqを現在の版のocamlで再度コンパイルしインストールしなおすことで対処する。

存在限量子を解釈する際に勘違い

松坂の集合位相入門P.19あたりにある集合系のすべての要素を対象にした和集合をCoqの帰納型で表現しようとしたが、それを使って本文の命題を証明するときに問題が発生した。

本文中では

∪V = {x|∃ A∈V (x∈A)}

というような∃量化を使った定義だったが、 これをCoqで使われるような表記に直す際に

forall x:U, exists A:Ensemble U, A∈V -> x∈A

という解釈をしてしまい、AがVに含まれない場合を考慮しなければならなくなった。集合系Vに含まれる筈の集合Aを議論する際にそれはないだろうと。

本文中の式を日本語で「定義されるXの全ての要素に対して、xを含むようなVの元Aが存在する」というように解釈すると、なんとなく後半が含意でなく論理積を表現しているようなにおいがするんだけど・・・∃より∀の方が使い慣れているので、こちらを使った定義でよく使われる含意を使った形式につられてしまったのだろうか

{x : P | Q}

というような表記を使う形式だとPを|の右側に持ってくる際に、∀の場合は含意、∃の場合は論理積というようなパターンだったので多分最初の定義が間違ってる筈。