[Coq] TPPmark2014 : Theorem Prover Advent Calendar

　TPP (Theorem proving and provers for reliable theory and implementations) 2014 という定理証明系に関するワークショップがあり、毎年秋〜冬に日本で開催されています。
 　TPPでは毎年TPPmarkという問題が出題され、参加者（あるいは解きたい人）が、各自自分の好きな定理証明系で問題を解いてその解答を紹介したりします。で、今年の問題は2014年の九州大学の入試問題（数IIB問題の[2]。リンクは河合塾サイト）の問題だ、と種明かしがありました。
 　参加者の解答はgithubで公開されています。

 　で、自分の解答の解説を。基本的に誘導に従い、高校数学の範囲で解いたつもりです。 

まず色々便利な様に、３づつ大きくなる場合の自然数の帰納法を定義します。

Theorem nat_ind_3 : forall P: nat -> Prop, P 0 -> P 1 -> P 2 -> 
  (forall n, P n -> P (S(S(S n)))) -> forall n, P n. 

次に３での商とか余りを定義します。

Fixpoint div3(n:nat):nat := match n with 
| S(S(S n')) => S (div3 n') 
| _ => 0 
end. 

Fixpoint mod3(n:nat):nat := match n with 
| S(S(S n')) => mod3 n' 
| _ => n 
end. 

これらに関する簡単な補題を幾つか証明しますが、特に３で割った余りに関する場合分け

Lemma mod3_012 : forall n, (mod3 n = 0) \/ (mod3 n = 1) \/ (mod3 n = 2). 

を証明しておくと、場合分け出来る様になるので便利です。
mod 3に関しては下記のような性質を証明し、以後の書き換えで使用します。

Lemma mod3_idem : forall n, mod3 (mod3 n) = mod3 n. 
Lemma mod3_add_hom: forall p q, mod3 (mod3 p + mod3 q) = mod3 (p + q). 
Lemma mod3_mul_hom: forall p q, mod3 (mod3 p * mod3 q) = mod3 (p * q). 

ここは３で割った剰余系をsetoidで作ることも考えましたが、そこまで必要無いと考え止めました。

問題１は、mod3_012で場合分けと、mod3_add_homでの書き換えを行えばOKです。

Theorem mod3_square_01 : forall a, (mod3 (a*a) = 0) \/ (mod3 (a*a) = 1). 

問題２もほぼ同様に a, b, cについて３で割った余りについて計算すればなんとかなります。

Theorem all_mod3_0 : forall a b c, a*a + b*b = 3*c*c -> 
  (mod3 a = 0) /\ (mod3 b = 0) /\ (mod3 c = 0). 

問題２と

Lemma mod3_0_q : forall n, mod3 n = 0 -> exists q, n = 3*q. 

とを使うと、a, b, cはそれぞれ３の倍数であることが言え、次の様な補題が言えます。

Lemma shrink_by_3 : forall a b c, a*a + b*b = 3*c*c -> 
  (exists a' b' c', a = 3*a' /\ b = 3*b' /\ c = 3*c' /\ 
  a'*a' + b'*b' = 3*c'*c'). 

上記の補題から無限降下列が得られます。 で、無限降下法はCoqのライブラリに無いので、整楚帰納法から証明します。

Theorem infinite_descent : forall P : nat -> Prop, 
  (forall n : nat, P n -> exists2 m : nat, m < n & P m) -> 
  forall n : nat, ~ P n. 

この整楚帰納法を使いやすい証明課題を３つ作ります。

Lemma cond_of_a: forall a, ~( ~(a=0) /\ (exists b c:nat, a*a+b*b = 3*c*c)). 
Lemma cond_of_b: forall b, ~( ~(b=0) /\ (exists a c:nat, a*a+b*b = 3*c*c)). 
Lemma cond_of_c: forall c, ~( ~(c=0) /\ (exists a b:nat, a*a+b*b = 3*c*c)). 

これは無限降下法とshrink_by_3を用いて証明出来ます。 この３つから問題３の証明を出来ます。

Theorem abc_are_0 : forall a b c:nat, a*a+b*b = 3*c*c -> 
  (a = 0 /\ b = 0 /\ c = 0). 

　最後に宣伝。東京ではCoqの勉強会であるSF読み進捗ダメです会議 #13 #readcoqart #Coqというのを月一回、開催しています。Coqに興味のある方は、一度遊びにきませんか？