もう向いてないんじゃないかと思いました………。 現実逃避したい。 うんCoqでClassicalをつかった証明の練習。 ここにあるやつ。 参照： http://coq.inria.fr/library/Coq.Logic.Classical_Prop.html Section Classical_Prop. Require Import Relations_1. Req…

相変わらずCoq書いてるけど進歩ないすなぁ。Coqの特徴ってのはまあ、Inductive型が使えて帰納法ができてハッピーというアレなんだけど、あまりそこに到達していないとこがなんとも。 証明中にやりたくてもできないという知識的欠陥で、Arithmeticの周辺でラ…