読者です 読者をやめる 読者になる 読者になる

任意の自然数a,b,cについてa*a+b*b=c*cのときにa,b,cすべてが奇数ではないことを証明してみた

Coq

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ライブラリ。これをまともに探さずに証明しようとしていたので結構無理そーな気がしていましたが、このライブラリのおかげで証明できました。

広告を非表示にする