Coq始めた。

いやちょっと前から斜め読みしてたけど、限界が来たので、少し真面目に第一章からやる。

http://proofcafe.org/sf/
https://github.com/moritanon/Coq_study

gitも久しぶり触るのでなんもかんも忘れてる。仕事では使ってないし。

---

Theorem bin_nat_comm : forall (b:bin),
  bin_to_nat (succ_bin b) = S (bin_to_nat b).

で、

Theorem bin_nat_comm : forall (b:bin) (n:nat),
  bin_to_nat (succ_bin b) = S (bin_to_nat b).

とか、使用してもいない変数 n を書いてたので、
あとからbin_nat_commを使ったときに、

sub goal nat:

という謎の文言が出て死んだ。(自分がデバッグで)

それはともかく、coqで行う証明は麻薬的なところがある。感覚としてテトリスに近い。いやマジで。