証明とは非常に個人的なもの

もちろん、今までにない証明なら話は別ですが。

今朝もうっかりAgdaで Free Monoid の普遍問題と朝5時まで。そういうのやる年じゃないんだけどな。中毒性あるって
話だったけど、確かにそのとおりです。

わからない時はググって見るわけですが、ばっちり同じ問題をやっていても、かなり違う。Agda は式の変形が付いているだけ
かなりましで、Coq の証明は読むための証明じゃないからなぁ。Agda でも、

<pre>
unique : (xs : List A) → γ ′ xs φ xs
unique [] = ε-homo
unique (x xs) = M-trans (-homo [ x ] xs)
(M-trans (-cong (eq x) (unique xs))
(-cong (proj identity (f x)) (M-refl {φ xs})))
</pre>

とか書いてあってもわからないよ。

でも、

Kleene Closure is Free Monoid
http://www.proofwiki.org/wiki/Kleene_Closure_is_Free_Monoid

こちらはわかりやすい。

日本語Wikipeida の Monoid / 普遍問題を書いたのは誰なんだろう? 昔は、もっとまともだったと思うのだが、
可換図さえないって、どういうことなのかと小一時間問い詰めたい感じです。

でも、証明って全部書いてあるわけじゃないんだよね。自分で証明を追うとの読むのとではかなり違う。それと同じくらい
Agda で書くのは違う感じ。

また、人のAgdaの証明があっても、かなり違っていることが多い。Agda は特にトンデモ記号を使う人が多い。おかげで
7x14 なフォントをだいぶ作った。

Reasoning という式変形の部分に手を入れたりすると、Emacs よりも Customize されてしまう感じ。Agda は、あくまでも
自分のためのものなのかも。

もちろん、library はちゃんとしているんだけどね。

300行ぐらいの証明が多いので、行き詰っても「あらゆる組み合わせを試している」うちに、なんとかなってしまうことが
多いようです。新しい関数を作るとかは難易度高い。