証明について

Software Foundationsを読んでると、時々、「なんか自明でない定理考えて証明しろ」とか無茶振りしてくるけど、数学に慣れてない人間にんなこと言われても途方に暮れるわけだ。

そもそも、何か命題があって、それを証明する必要があるかどうか、ということがまず分からない。

n + m = m + n を証明しろ。とか言われても、当たり前じゃねーか。とか思ってしまうだけなのだ。つまるところ、自明でない定理って言われても、+ とか、listのcons/snocについての定理なんて正直全部自明に見える。

実際に他の証明で使うときに、ああなるほど必要なんだな。ということが分かる訳だが。

今回のpal l -> l = rev l の証明もそう。
snoc l x = l ++ [x].
の証明が途中必要になるわけだが、それの証明が必要になる。ということ自体が、実際に他の証明で必要になるときまで、思い付くことが出来ない。
自明なのになんでsimplで簡約出来ないんだ。という事実に直面して初めて、ああ必要なんだな。戻って証明するか。ということになる。

そいうのが予め分かったりすのが数学センスというやつなんだろう。40過ぎると遣り直しはキツい。