■

Coq in a Hurryの練習問題の一番最後。

とすると であるから、となる正の整数の組のなかで、最小のをとってくる。
すると、であるから。これは矛盾であり２の平方根が有理数でないことの証明になっている。
この証明をCoqを使って書け。

これはとてつもなく難しい問題だ。普通の数学屋は最小のが存在することを何気なく使っているが、この事実は排中律を仮定しないと簡単には証明できない。よって、自然数の無限降下列は存在しないという化石みたいなツールを使って証明しなければならないのである。

とりあえず完成した証明。

Require Import ZArith.

(*
 *
 * ２の平方根が有理数ではないことの証明。
 *
 *)


(*
 * 自然数の列に無限降下列がないことを証明。
 * 今回の証明では正の整数に無限降下列がないことを使うので、このセクションはいらない。
 *)
Section No_Infinite_Dec.
  Variable A: Set.     (* 述語の定義域 *)
  Variable f: A->A.    (* 無限降下列の次の値を返す関数。P x -> P (f x) となるように作る。*)
  Variable h: A->nat.  (* 自然数への対応。P x -> h x > h (f x) となるように作る。 *)

  (* 未満の場合を全て仮定する場合の帰納法 *)
  Lemma induction_h:
    forall P: A -> Prop,
      (forall x:A, (forall y:A, h y < h x -> P y) -> P x) -> forall a, P a.
  intros P F.
  cut (forall n (a:A), h a < n -> P a).
  intros H a.
  apply (H (S (h a))).
  auto with arith.
  induction n.
  intros.
  absurd (h a < 0); auto with arith.
  intros a ltSna.
  apply F.
  intros b lthahb.
  apply IHn.
  apply lt_le_trans with (h a); auto with arith.
  Qed.

  (* 無限降下列が存在したら矛盾 *)
  Lemma no_infinite_dec: forall (P: A->Prop),
     (forall n, P n -> h (f n) < h n) ->
     (forall n, P n -> P (f n)) ->
     forall n, ~P n.
  intros.
  pattern n.
  apply induction_h.
  intros.
  intro.
  apply H1 with (f x); auto.
  Qed.
End No_Infinite_Dec.

(*
 * 正の整数列に無限降下列が存在しないことの証明。
 *)
Section No_Infinite_Dec_Z.
  Open Scope Z_scope.
  Variable A: Set.
  Variable f: A->A.
  Variable h: A->Z.
  Hypothesis pos: forall a, h a > 0. (* 正の整数に限定する。この仮定は P a -> h a > 0 の形に弱められる。*)

  Lemma induction_hZ:
    forall P: A -> Prop,
      (forall x:A, (forall y:A, h y < h x -> P y) -> P x) -> forall a, P a.
  intros P F.
  cut (forall n, n > 0 -> forall (a:A), h a < n -> P a).
  intros H a.
  apply (H (1 + (h a))); cut (h a > 0); auto with zarith.
  intros n nge0.
  pattern n.
  apply Zlt_0_ind; auto with zarith.
  intros.
  apply F.
  intros b lthahb.
  apply H with (x-1).
  split; auto with zarith.
  cut (h a > 0 /\ h a -1 < x-1); auto with zarith.
  auto with zarith.
  Qed.

  Lemma no_infinite_decZ: forall (P: A->Prop),
     (forall n, P n -> h (f n) < h n) ->
     (forall n, P n -> P (f n)) ->
     forall n, ~P n.
  intros.
  pattern n.
  apply induction_hZ.
  intros.
  intro.
  apply H1 with (f x); auto.
  Qed.

End No_Infinite_Dec_Z.

Open Scope Z_scope.

(* 構成する無限降下列に関する簡単な補題をいくつか証明 *)

Lemma next_n_d: forall (n d: Z), n*n = 2*d*d ->
                  (2*d-n)*(2*d-n) = 2*(n-d)*(n-d).
intros.
ring [H].
Qed.

Lemma positive: forall (x y z: Z), x*x-y*y=z -> x>0 -> y>0 -> z>0 -> x > y.
intros.
apply Zgt_square_simpl; auto with zarith.
Qed.

Lemma positive_1: forall (n d: Z), n>0 -> d>0 -> n*n = 2*d*d -> 2*d-n > 0.
intros.
cut (2*d > n); auto with zarith.
apply positive with (2*d*d); auto with zarith.
ring [H1].
Qed.

Lemma positive_2: forall (n d: Z), n>0 -> d>0 -> n*n = 2*d*d -> n-d > 0.
intros.
cut (n > d); auto with zarith.
apply positive with (d*d); auto with zarith.
ring [H1].
Qed.

Lemma positive_3: forall (n d: Z), n>0 -> d>0 -> n*n = 2*d*d -> 2*d - n < n.
intros.
cut (n-d > 0); auto using positive_2.
auto with zarith.
Qed.

(* 簡単な有理数。二つの整数の組 *)

Inductive Q : Set := Q_intro (n d: Z) : Q.

(* 有理数が２の平方根であるかな述語 *)
Definition is_sqrt2 (q: Q) :=
  match q with Q_intro n d => n*n = 2*d*d /\ n > 0 /\ d > 0 end. 

(* 無限降下列の次の有理数を返す関数 *)
Definition next (q: Q) :=
  match q with Q_intro n d => Q_intro (2*d-n) (n-d) end.

(* ２の平方根の次の有理数も２の平方根 *)
Lemma next_is_sqrt2:
  forall q: Q, is_sqrt2 q -> is_sqrt2 (next q).
induction q.
unfold next, is_sqrt2.
intros.
split.
apply next_n_d.
tauto.
split.
apply positive_1; tauto.
apply positive_2; tauto.
Qed.

(* 有理数を正の整数にマップする。今回は分子を使う。*)
Definition get_n_Q (q: Q) :=
  match q with Q_intro n d => Zmax n 1
  end.

(* 次の補題の証明に使う。*)
Lemma always_n: forall (n d: Z), is_sqrt2 (Q_intro n d) -> get_n_Q (Q_intro n d) = n.
intros.
elim H.
intros.
elim H1.
intros.
simpl.
apply Zmax_case_strong; auto with zarith.
Qed.

(* ２の平方根の次の有理数は分子が必ず減少する。*)
Lemma dec: forall q: Q, is_sqrt2 q -> get_n_Q(next(q)) < get_n_Q(q).
induction q.
intros H.
rewrite (always_n n d H).
assert (is_sqrt2 (next (Q_intro n d))) by auto using next_is_sqrt2.
unfold next in * |- *.
rewrite (always_n (2*d - n) (n-d) H0).
apply positive_3; elim H; tauto.
Qed.

(*
 * ２の平方根は有理数ではありえない！
 *)
Theorem sqrt2_is_not_rational:
   forall q:Q, ~is_sqrt2 q.
intros.
eapply no_infinite_decZ with (f := next) (h := get_n_Q).
induction a.
simpl.
apply Zmax_case_strong; auto with zarith.
intros.
auto using dec.
auto using next_is_sqrt2.
Qed.

Coqのコードは色を付けられないのが残念なところである。