自分が中二レベルであることを証明する
旧聞になりますが「大学生の４人に１人「平均」分からず 数学基本調査、論理力欠如明確に」より引用。
「偶数に奇数を足すと必ず奇数になる」ことを数式と文章で説明する中２レベルの問題
ということらしいので coq を使って自分が中二レベルあることを証明してみましょう！
まずは奇数とは、偶数とは何なのかを帰納的に定義してやりましょう。
Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n).
見たままですね。証明したい定理はこんな感じじゃないでしょうか。
Theorem odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
では証明してみましょう。とりあえず何も考えずに n について induction してみます。
Proof. induction n.
すると次のようなゴールができます。
2 subgoals ______________________________________(1/2) forall m : nat, odd 0 -> even m -> odd (0 + m) ______________________________________(2/2) forall m : nat, odd (S n) -> even m -> odd (S n + m)
一つ目は仮定に明らかに仮定に矛盾があるのでそれを示すだけです。
intros m odd_O. inversion odd_O.
問題は二つ目ですね。
intros m odd_Sn even_m. simpl. constructor. inversion odd_Sn as [n' even_n n'_eq_n].
すると環境が、
1 subgoal n : nat IHn : forall m : nat, odd n -> even m -> odd (n + m) m : nat odd_Sn : odd (S n) even_m : even m n' : nat even_n : even n n'_eq_n : n' = n ______________________________________(1/1) even (n + m)
はい明らかに仮定足りませんね。困りました。
何も考えずに induction n したわけですが、この結果、帰納法で得られる仮定は n が奇数である場合のものです。ゴールがそうなんだから当然ですね。しかし、帰納法の二つ目のステップでは n が偶数の場合について証明を求められます。帰納法で得られる仮定は n が偶数の場合に適用できるものが欲しい。
結論からいうと、以下のような補題をまず示せばいいことになります。
Lemma aux : forall n m, (odd n -> even m -> odd (n + m)) /\ (even n -> even m -> even (n + m)).
ようは n が奇数の場合についてだけでなく、偶数の場合についても一緒に証明してやろう、というわけです。そうすることで、証明することは増えたけれど、帰納法で得られる仮定も増えてハッピー。
ということで次こそは証明してみせましょう。例によってとりあえず induction してみます。
Proof. induction n.
するとこんなゴールが現れる。
2 subgoals ______________________________________(1/2) forall m : nat, (odd 0 -> even m -> odd (0 + m)) /\ (even 0 -> even m -> even (0 + m)) ______________________________________(2/2) forall m : nat, (odd (S n) -> even m -> odd (S n + m)) /\ (even (S n) -> even m -> even (S n + m))
一つ目はサクッと終わらせましょう。
intro m. split. intro odd_O. inversion odd_O. auto.
するとこうなる。
1 subgoal n : nat IHn : forall m : nat, (odd n -> even m -> odd (n + m)) /\ (even n -> even m -> even (n + m)) ______________________________________(1/1) forall m : nat, (odd (S n) -> even m -> odd (S n + m)) /\ (even (S n) -> even m -> even (S n + m))
適当に intro してばらします。
intro m. split.
すると、最初にどんづまったときのような環境が現れてくる。
2 subgoals n : nat IHn : forall m : nat, (odd n -> even m -> odd (n + m)) /\ (even n -> even m -> even (n + m)) m : nat ______________________________________(1/2) odd (S n) -> even m -> odd (S n + m) ______________________________________(2/2) even (S n) -> even m -> even (S n + m)
前回と違って、十分に強い仮定があるので何とかなりそうですね。はい何とかなります。めんどくさいので色々すっ飛ばします。
intros odd_Sn even_m. simpl. constructor. inversion odd_Sn as [n' even_n n'_eq_n]. destruct (IHn m) as [oeo eee]. exact (eee even_n even_m). intros even_Sn even_m. simpl. constructor. inversion even_Sn as [|n' odd_n n'_eq_n]. destruct (IHn m) as [oeo eee]. exact (oeo odd_n even_m). Qed.
Proof. intros n m. destruct (aux n m). assumption. Qed.
やったー中二レベルになれたよー。
さて無事証明できたわけですが、なんというか、しっくりこないんですよね。何故偶数と奇数を帰納的に定義してやったにも関わらず、数学的帰納法（nat の構造に関する帰納法）で証明しているのか。折角定義してやったんだから、偶数と奇数の構造に関する帰納法で証明したい、という気持ちが生まれるのは自然なことだと思います。というか、普通に人間証明機が証明するときはそうやってると思うのです。
問題は、偶数と奇数が mutually inductive に定義されていることで…偶数の構造に関する帰納法も、奇数の構造に関する帰納法も coq は自動的に定義してくれるんですが、「偶数と奇数の構造」に関する帰納法は定義してくれないんですね…困りました。
困ってたら id:erutuf さんが素敵なコマンドを教えてくれました。
めでたし、めでたし。
追記：途中で補題変えたりした関係でなんかおかしくなってたのを直しました。ところで偶数に奇数を足すと必ず奇数になることを証明しろといわれたのに、奇数に偶数を足すと必ず奇数になることを証明しちゃってますね…まあ plus_comm で許して ＞＜
