Coqネタ。
挑戦してみていろいろ勉強になった。試行錯誤はやっぱり勉強になる。勉強中はバックトラックでもタダでは起きない（ｷﾘｯ
時間かかり過ぎですが。
今回はタイトル通り、「任意の自然数a, b, cについて a*a+b*b=c*c のとき、a, b, cすべてが奇数ではないこと」を証明してみました。
本当であればさらに押し進めて、a, b, cのうちどれかは偶数であることも証明すべきかな。。。多分そんなに大変じゃないはず。
Require Import Even. Goal forall (a b c : nat), a*a + b*b = c*c -> ~(odd a /\ odd b /\ odd c). Proof. intros. intro. destruct H0; destruct H1. apply (odd_mult a a) in H0. apply (odd_mult b b) in H1. apply (odd_mult c c) in H2. apply (odd_even_plus (a * a) (b * b)) in H0. rewrite H in H0. apply (not_even_and_odd (c * c) H0). apply H2. apply H1. apply H2. apply H1. apply H0. Qed.
「apply 〜 in 〜」とか知らなかったので証明に結構時間がかかりました。なんとなくわかるとそこからは早かったです。
あとはEvenライブラリ。これをまともに探さずに証明しようとしていたので結構無理そーな気がしていましたが、このライブラリのおかげで証明できました。
