Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
