いろいろだめだ

リストなどの構造に対する帰納というのがいまいち分かってない。

チュートリアルみたいな簡単なのは出来るんだけど、ちょいと難しくなるとお手上げ。
というより、真ん中の難しさというのが、初学者にたいして何時も存在しない気がする。

はるか昔、Cを学んだとき。

はいprintf。ファイル。構造体。ポインタ。これで入門は終りです。

で次。

ウィンドウハンドルがあーたら、メッセージキューがどーした、クラスライブラリがどうした。リソースがどうしたああした。

挫折。

Coqもすげー似てる。気がする。

consによるlistのlengthの帰納法の証明とかの次に、いきなり、鳩の巣原理とか、rev l = l -> pal lとかの証明に飛ぶのはなんとかならんのか。人の証明見てもさっぱり理解出来ん。