Coqで大学院試験

今日はCoqを使って大学院試験を解いてみよう。
題材は京都大学 理学研究科 数学専攻の数学の問題だ。
せっかくなので一番 新しい平成１９年度の問題に挑戦してみよう。
（＊＊
　注意！！今回Coqを使ってこの問題を解いたが、Coqが大学院試験を自動的に解いたわけではない！Coqは証明を書く紙と鉛筆の代わりをしてくれただけだ！この記事は私が紙に書いた３行ほどの答案を再びCoq上で記述し直したにすぎない！Coqは単なるProof Assistantなのだ！
＊）

問題：行列の正則性の判定問題。

Coqで形式化したのが次のコードだ。

Definition A : Mat3 :=    (* まずAという行列を仮定する。 *)
  (fun i j:s3 =>
    match i,j with
    | I, I => 1
    | I, II => (2#p1)
    | I, III => (3#p1)
    | II, I => (2#p1)
    | II, II => 0
    | II, III => (2#p1)
    | III, I => (3#p1)
    | III, II => (2#p1)
    | III, III => 1
    end).

Theorem prob1_l : IsSeisoku A.    (* これが示すべき問題　*)

ただし、行列は　3*3 -> Q　の関数として表現し、有理数体を用いて証明した。
そして、正則行列は次のように、自然に定義した（Mat3は３次正方行列型、E3は３次元単位行列を表す）。

Definition IsSeisoku (m:Mat3) :Prop := 
  exists m':Mat3, Eq (mult m m') E3.

証明はなるべく基本的なタクティックのみを用いて証明するようにしてみた。
それでは証明を見てみよう。

Proof.     (* さあ！証明を始めよう！ *)
Definition B:Mat3 :=    (* まず、行列Bを定義する。 *)
(fun i j:s3 =>
    match i,j with
    | I, I => q1_4_opp
    | I, II => q1_4
    | I, III => q1_4
    | II, I => q1_4
    | II, II => q2_4_opp
    | II, III => q1_4
    | III, I => q1_4
    | III, II => q1_4
    | III, III => q1_4_opp
    end).
exists B.      (* このBを候補として選択する。 *)
unfold Eq in |- *; intros.  (* 行列のイクォリティを展開する。 *)
case i; case j.　　　　　　(* i,jに関してそれぞれ場合分け、９つのサブゴールができる　*)
(*　ここでサブゴールを証明するための補助lemmaを9こ作る。　*)
Lemma lemma1 : mult A B I I == E3 I I.
Proof.
unfold E3 in |- *.
case (s3_eq_dec I I).
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold Qmult in |- *; unfold Qplus in |- *; unfold Qeq in |- *.
   reflexivity.
 intro H; elim H; reflexivity.
Qed.
(* 以下同様 *)
Lemma lemma2 : mult A B I II == E3 I II.
Proof.
unfold E3 in |- *.
case (s3_eq_dec I II).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold Qmult in |- *; unfold Qplus in |- *; unfold Qeq in |- *.
   reflexivity.
Qed.

Lemma lemma3 : mult A B I III == E3 I III.
Proof.
unfold E3 in |- *.
case (s3_eq_dec I III).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold Qmult in |- *; unfold Qplus in |- *; unfold Qeq in |- *.
   simpl in |- *.
   reflexivity.
Qed.

Lemma lemma4 : mult A B II I == E3 II I.
Proof.
unfold E3 in |- *.
case (s3_eq_dec II I).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold Qmult in |- *; unfold Qplus in |- *; unfold Qeq in |- *;
    simpl in |- *.
   reflexivity.
Qed.


Lemma lemma5 : QArith.Qeq (mult A B II II) (E3 II II).
Proof.
unfold E3 in |- *.
case (s3_eq_dec II II).
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold QArith.Qmult in |- *; unfold QArith.Qplus in |- *;
    unfold QArith.Qeq in |- *.
   simpl in |- *.
   reflexivity.
 intro H; elim H; reflexivity.
Qed.

Lemma lemma6 : QArith.Qeq (mult A B II III) (E3 II III).
Proof.
unfold E3 in |- *.
case (s3_eq_dec II III).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold QArith.Qmult in |- *; unfold QArith.Qplus in |- *;
    unfold QArith.Qeq in |- *.
   simpl in |- *.
   reflexivity.
Qed.

Lemma lemma7 : QArith.Qeq (mult A B III I) (E3 III I).
Proof.
unfold E3 in |- *.
case (s3_eq_dec III I).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold QArith.Qmult in |- *; unfold QArith.Qplus in |- *;
    unfold QArith.Qeq in |- *.
   simpl in |- *.
   reflexivity.
Qed.

Lemma lemma8 : QArith.Qeq (mult A B III II) (E3 III II).
Proof.
unfold E3 in |- *.
case (s3_eq_dec III II).
 intro H; elim H.
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold QArith.Qmult in |- *; unfold QArith.Qplus in |- *;
    unfold QArith.Qeq in |- *.
   simpl in |- *.
   reflexivity.
Qed.

Lemma lemma9 : QArith.Qeq (mult A B III III) (E3 III III).
Proof.
unfold E3 in |- *.
case (s3_eq_dec III III).
 intro; unfold mult in |- *.
   unfold A in |- *; unfold B in |- *.
   unfold QArith.Qmult in |- *; unfold QArith.Qplus in |- *;
    unfold QArith.Qeq in |- *.
   simpl in |- *.
   reflexivity.
 intro H; elim H; reflexivity.
Qed.

(* これで９個のlemmaができた！あとはこれを適用するだけ。 *)
 apply lemma1.
 apply lemma2.
 apply lemma3.
 apply lemma4.
 apply lemma5.
 apply lemma6.
 apply lemma7.
 apply lemma8.
 apply lemma9.
Qed.

できた！！