Hoare論理をCoqでやってみたかったのでソフトウェアの基礎を読んでいた。何かしら書いておかないと自分のなかで記憶がまたゼロに戻ってしまうので何かしら書いておく。当たり前のことをたくさん書く。あと、答えをそのまま書くのはよくないらしいので、Coqの…