証明が証明を呼ぶ

なんだかんだで昼前に起床.

証明が証明を呼び,がっはっは,という感じに.非形式的な証明ってどれだけ行間があるのか痛感させられる.しかもちょこちょこ行間として難問が現れる.Coq 力が足りないだけなのか数学力が足りないのかはたまたその両方か,よくわからん...が,そうもいってられないので,一旦 notation にはこだわらないで証明を完成させるのが得策かもしれない.

閑話休題.(以下はもはや日記とは関係ないメタ記述だけど)これ書いてたらアイデアが降って来た.詰まったら別のことやるの大事.とにかく手を動かし続けろ!