https://gist.github.com/4243787最近、プログラマの採用面接で解かす問題集みたいな本が出て その中に「ある配列がユニークであるかどうかを示すコードを書け」という問いがあり、Coqで書いてみました。 下記のようなコードになるんだけどついでに配列を逆…

Coqをインストールしたので http://d.hatena.ne.jp/qnighy/20101220/1292829222 この辺を参考に勉強中です。 ついでに自分で命題を考えて証明してみた。 命題は forall (x : nat), x > 1 -> x こんなもの直感的だろ！ といいたい所ですが、論理学の世界では…