[Coq] Even + Odd = Odd

日本数学会の「大学生数学基本調査」に基づく数学教育への提言によると、『「偶数と奇数の和が奇数になる」証明を明快に記述できる学生は稀』という調査結果が得られたそうです。

さて Coq で実際証明してみると判りますが、ちょっとした工夫をしないと、

Theorem plus_even_odd_odd : forall n m,
 even n -> odd m -> odd (n+m).

これを証明するのは難しいです。

まず、述語 even, odd を定義します。
標準的には下記の様に相互帰納的に定義するのが良いでしょう。

Inductive even:nat->Prop :=
| even_0 : 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 plus_odd : forall n m,
 (even n -> odd m -> odd (n+m)) /\
 (odd n -> odd m -> even (n+m)).
Proof.
induction n. 
 intros. split.
  intros. simpl. auto.
 intros. inversion H.
intros. split.
 intros. destruct (IHn m). simpl. apply odd_S.
 apply H2.
  inversion H. auto.
 auto.
intros. destruct (IHn m). simpl. apply even_S.
apply H1.
 inversion H. auto.
auto.
Qed.

こうすることで n に関する帰納法が使いやすくなって証明出来ます。
最後に先ほど証明した定理の半分だけ取り出せばOKです。

Theorem plus_even_odd_odd : forall n m,
 even n -> odd m -> odd (n+m).
Proof.
intros. destruct (plus_odd n m). apply H1; auto.
Qed. 

以上、ライブラリや omega などを使わずに証明出来ました。