Coqですべての自然数は偶数または奇数だと証明してみたよ

離散数学の授業で定理証明器のことをちょっと触れたいと思って、証明の例題に使っている上記命題をCoqで証明してみました。多分いろいろ上手くないと思うのだけれどもさらしてみます。

Require Import Classical.
Require Import Arith.
Require Import Omega.

Definition even (n:nat) := (exists m:nat, n = 2 * m).
Definition odd (n:nat) := (exists m:nat, n = 2 * m +1).

Theorem even_or_odd : forall n:nat, even n\/odd n.
intros.
elim n.
left.
unfold even.
exists 0.
ring.
intros.
elim H.
intros.
right.
elim H0.
intros.
unfold odd.
rewrite H1.
exists (x).
ring.
intros.
left.
elim H0.
intros.
unfold even.
rewrite H1.
exists (x+1).
ring.
Qed.

Theorem lem1 : forall n m:nat, n<=m ->2*n<>2*m+1.
intros.
omega.
Qed.

Theorem lem2 : forall n m:nat, 2*n<>2*m+1. 
intros.
assert (UH1 : n<=m \/ n>=m+1).
omega.
elim UH1.
apply lem1.
intros.
assert (UH2 : 2*n>=2*m+2).
omega.
omega.
Qed.

Theorem not_even_and_odd : forall n:nat, ~(even n/\odd n).
intros.
red.
intros.
elim H.
unfold even.
unfold odd.
intro.
intro.
elim H0.
intro.
elim H1.
intro.
intros.
assert (UH1 : 2*x=2*x0+1).
rewrite <- H3.
rewrite H2.
ring.
generalize UH1.
apply lem2.
Qed.

Theorem not_even_implies_odd : forall n:nat, 	~even n->odd n.
intro.
intro.
assert (UH2 : even n\/odd n).
apply even_or_odd.
elim UH2.
intro.
tauto.
tauto.
Qed.

Theorem not_odd_implies_even : forall n:nat, ~odd n->even n.
intros.
assert (UH1 : even n\/odd n).
apply even_or_odd.
elim UH1.
tauto.
intro.
tauto.
Qed.

Theorem even_implies_not_odd : forall n:nat, even n->~odd n.
intros.
assert (UH1 : ~(even n/\odd n)).
apply (not_even_and_odd).
red.
intro.
auto.
Qed.

Theorem odd_implies_not_even : forall n:nat, odd n->~even n.
intros.
assert(UH1 : ~(even n/\odd n)).
apply not_even_and_odd.
red.
intro.
auto.
Qed.

うわー、バックスラッシュが￥になっているからすげー見づらい。でも面倒なので放置します。