さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら
Σ(●△●)＜Isabelleの人が一人で大半埋めてるじゃねえか！？
というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。
え、CoqとAgdaのことはnotogawaさんが書いてただろって？
細けえこたぁいいんだよ！
・CoqとAgda、どちらを使うべき？
好きな方を選べば良いと思うのですが、個人的な考えを挙げます。
1:性質＋証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関してはAgdaもたくさん使われていますので、それこそ好みでいいでしょう（個人的にはCoqがいいと思いますが）。
2:プログラム記述＋検証についてはCoqの方がいいです。こちらは型や関数の記述自体は割と単純であることを想定しています。tacticもいいですし、SSReflectも便利（らしい）です。
3:型を複雑にして、いろいろな性質を型に持たせたプログラミングをしたいならAgdaの方がいいです。Coqだとプログラムを証明と一緒に（tacticで）書く勇気が必要になります（そうじゃないとやっていられません）。慣れればそれなりにできますが、いちいちイライラします。
4:型の階層を意識したいなら断然Agdaです。なにせCoqはSet/Prop/Typeの区別しかしませんし（内部でTypeのヒエラルキーは計算していますが、表に見えづらいです）。
1は比較的どちらでも良いですし、4は迷いようがありません。
したがって、おそらく悩むことが多いのは2/3の問題でしょう。
選択の一助になれば幸いです。
ちなみに、OCamlとHaskellの一方を使っているから、はほとんど理由になりません。
どうせ大した差ではありません。
スタートアップで一日差がつくかつかないかくらいです。
・inversion大好き
inversion tacticは便利です。（すでに何回主張したか忘れた）
簡単に説明すると、inversion tacticは「この帰納的述語が成り立つためにはどういうことが成り立っている必要がある？」というのを定義から見つけてくる優れものです。
このとき、成り立たないパターン（帰納的述語のコンストラクタのパラメータに一致しない）があるときは勝手にそれらに関して矛盾を作って証明してくれます。
（よって「起こりうるパターンが一つもない」、つまり矛盾していれば証明完了するわけですが、それはあくまで結果論）
inversionなかったらCoqの証明を勧めるとかありえませんね。
（ただしinversionの生成する項ははっきり言って読めない）
Agdaで同じこと？・・・reflection使えば、できたりするのかな・・・？
・で、証明しないの？
最近AgdaでD-Case書きまくってるので勘弁してください。
次があったら例題使って、最初の4分類が何を言いたいのか書いてもいいのですが・・・
