Coq のモジュールシステムについて，使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに，モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思う…

依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが，その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りま…

前回のうまくいかない elim の続きで，Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが，こういうことを細かく解説したものを読ん…

tactic が proof term を生成していく様子を何度か観察しましたが，何のためにそんなことをしていたかというと，ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。例と…