Agda入門にまんまと失敗して、Coqを入門してみることにした。
このチュートリアルをやっている。
色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。
で、このチュートリアルは、とりあえず手を動かしてみるものとしてはありだと思う。
ただ、体系的な解説ではないのでなんとなく理解が深まっている感がしなかったり（個人的に）、徐々に辛くなってくる（気がする）
とりあえず僕は証明駆動開発の前で死んでいる。ちゃんと理解して読み込んで進んでいないからかもしれない。
割と挫折気味なので、簡単な定理でも証明しまくって経験値を積んでやろうかなと思ってきた。
とりあえず交換法則でも証明するか！
ということでやってみたのがこれ
なんかひどい出来・・・
でもこれでなんとなく証明の感覚がつかめた気がする
簡単な定理を証明するために標準ライブラリの関数を使ってしまっているのが残念なので、これをまた証明してImportを消すという遊びをしながら証明に慣れたい。
数学的素養は全くなくて、高校数学でも証明はとても苦手だったのでまぁ苦手なわけでとりあえず慣れよう。うん。
もっとシンプルに証明できるはずだし。
