Coq で証明をしているときに，これまで証明してきた定理やライブラリの中にどのような定理があるのかを全部覚えておくわけにはいかないので， Search コマンド等を使って使いたい定理を見つけます*1．具体的には， Search SearchAbout SearchPattern SearchR…

Coq の便利な機能の一つとしてプログラムの extraction がある．この機能を使えば，性質が証明された関数を OCaml や Haskell, Scheme などで実際に使うことができる．知らない人は下のページをどうぞ．（下のほうのリンクほど詳しく説明してあります．） に…

ようやく Problem 2 ができた．証明が長くなってきたので，ここに貼らずに github に置くことにした．git も github も使ったことがないので変なことをしているかもしれない．何か気付いたことがあったら教えて頂けると嬉しいです．レポジトリはこちら https…