ここのところ、SOFTWARE FOUNDATIONSに取り組んでいます。
これは、coqを使用して「高信頼ソフトウェアに関する広範囲の数学的基礎を学べる。」とのことです。
本日完了したのは、第一巻のinduction:帰納法による証明まで、練習問題が用意されており下記に示す難易度だそうです。。汗）
⇒私は★＝１日で解きました。。大汗） おつむのヨロシイ人は数分で解けるそうです。 最後の練習問題は★５つでウルトラ難くネットで回答を探して解析。。五日かかりました。
最後の練習問題に「normalizeを定義するのに nat_to_bin や bin_to_nat を使ってはいけません！」
とあったが、それを下記に置いた。
SOFTWARE FOUNDATIONSに
⇒「絶対にこの教材の練習問題の解答を皆に見える場所には置かないでください！」
とありますが、上記はSOFTWARE FOUNDATIONS中の練習問題では無いのでOKかなと思います。
