[Coq] Monads in Coq

Personal memorandum for studying functional languages, theorem proving, and formal verification. But other topics might be included. Written in Japanese (Shift-JIS Encoding). 社内勉強会でMonad入門の話をして、その時にCoqを用いて説明しました。 あまりHaskellに慣れてないのでCoq使ったんですが、CoqではMonad則を証明する必要があるので、実は寧ろ説明に適していました。 HaskellだとMonad則がなぜ必要なのか示すのが面倒そう（任意の関数、なんてのはQuickCheckでも作れ無さそうな気がする）ですが、CoqではそもそもMonad則を満たすことを示さないと、Monadを使えません。 サンプルコー