フェルマ数は互いに素
Any two Fermat numbers are coprime.
2023/7/31
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
はじめに
非負整数 $n$ に対して
$$ F_n = 2 ^ {2 ^ n} + 1 $$
で定義される、$F_n$をフェルマ数といいます。これが素数であるというフェルマの予想は $F_5$で否定されましたが、「任意のふたつのフェルマ数は、互いに素である」という性質があります。これを証明してみましょう。
補題
一般的な補題を証明しておきます。
2乗引く1
お馴染みの公式ですが、証明しておきます。
$$ m^2 - 1 = (m + 1)\ (m - 1) $$
Lemma sqrn_sub1_exp m : (m ^ 2).-1 = m.+1 * m.-1.
Proof.
rewrite -[in RHS]addn1 -[in RHS]subn1 mulnC.
by rewrite -subn_sqr exp1n subn1.
Qed.
総乗はその要素で割り切れる
$ 0 \le k \lt n $ のとき、
$$ a_k \mid \prod_{i=0}^{n-1} a_i $$
自明ですが、Coqの場合は証明が必要です。
$$ \prod_{i=0}^{n-1} a_i = (\prod_{i=0}^{k-1} a_i)\ a_k\ (\prod_{i=k}^{n-1} a_i) $$
と分解したのち、掛け算の順番を入れ替えて、
$$ a_k \mid X\ a_k $$
から証明します。
Lemma prod_dvdn a n k : 0 <= k < n -> (a k) %| \prod_(0 <= i < n)(a i).
Proof.
move=> /andP [H0 Hn].
(*
\prod_(0 <= i < n)(a i) を
(\prod(0 <= i < k)(a i)) * (a k) * (\prod(k.+1 <= i < n)(a i)) に分解する。
*)
rewrite (@big_cat_nat _ _ _ k 0 n) //=; last rewrite ltnW //=.
rewrite (@big_ltn _ _ _ k n) //=.
(* これは (a k) で割り切れる。 *)
by rewrite [(a k) * _]mulnC mulnA dvdn_mull.
Qed.
n と j が m に対して同じ最大公約数を持つ条件
Lemma dvdn_gcdn m n j : j <= n -> m %| (n - j) -> gcdn m n = gcdn m j.
Proof.
move=> Hmn /dvdnP.
case=> i H1.
have -> : n = i * m + j by rewrite -H1 subnK.
by rewrite gcdnMDl.
Qed.
実際には、j = 2 として、次のかたちで使用します。
Check (fun m n => @dvdn_gcdn m n 2)
: forall m n : nat, 2 <= n -> m %| n - 2 -> gcdn m n = gcdn m 2.
フェルマ数
フェルマ数の定義
フェルマ数 $ F_n = 2 ^ {2 ^ n} + 1 $ を定義します。
fermat n = (2 ^ 2 ^ n) + 1
MathComp の場合 "^" は右結合であることに注意してください。ただし、ここではできるだけ括弧をつけるようにします。
Definition fermat n := (2 ^ (2 ^ n)).+1.
Lemma fermatE n : fermat n = (2 ^ (2 ^ n)).+1.
Proof. by []. Qed.
補題：フェルマ数は1より大きい
Check ltnS : forall m n : nat, (m < n.+1) = (m <= n).
Check ltnS : forall m n : nat, (m.+1 <= n.+1) = (m <= n).
Lemma fermat_gt1 n : 1 < fermat n.
Proof.
by rewrite /fermat ltnS expn_gt0.
Qed.
補題：フェルマ数は奇数である
Lemma odd_fermat n : odd (fermat n).
Proof.
by rewrite /fermat oddS oddX negb_or andbT neq_ltn expn_gt0.
Qed.
フェルマ数の漸化式
漸化式（その1）
$$ F_0 = 3 $$
Lemma fermat_0 : fermat 0 = 3.
Proof.
by rewrite fermatE.
Qed.
また、$ 0 \lt n $ のとき、$ F_n $ と $ F_{n - 1} $
の間には、次の関係があります。
$$ F_n - 2 = F_{n - 1}\ (F_{n - 1} - 2) $$
Lemma l_pof2_gt0 n : 0 < 2 ^ n.
Proof.
rewrite expn_gt0.
by apply/orP/or_introl.
Qed.
Lemma fermat_n n : 0 < n -> (fermat n).-2 = (fermat n.-1) * (fermat n.-1).-2.
Proof.
move=> Hn.
rewrite /fermat.
have H m : 0 < m -> m.+1.-2 = m.-1 by rewrite -[m.+1]addn1 -subn2 -subn1 -subnBA.
rewrite H; last by rewrite l_pof2_gt0.
rewrite H; last by rewrite l_pof2_gt0.
rewrite -sqrn_sub1_exp.
by rewrite -expnM -expnSr prednK.
Qed.
漸化式（その2）
$$ F_n - 2 = \prod_{i=0}^{n-1} F_i $$
漸化式（その1）の右辺に対して、繰り返し適用すると総乗（Π）の式になります。
Lemma fermat_rec n : (fermat n).-2 = \prod_(0 <= i < n)(fermat i).
Proof.
elim : n => [| n IHn].
(* (fermat 0).-2 = \prod_(0 <= i < 0) fermat i *)
- rewrite big_nil.
by rewrite fermat_0.
(* (fermat n.+1).-2 = \prod_(0 <= i < n.+1) fermat i *)
- rewrite big_nat_recr //= -IHn mulnC.
by apply: fermat_n.
Qed.
フェルマ数は互いに素
フェルマ数の漸化式（その2）から、$ F_n - 2 $ は $n$より小さい $m$ の $ F_m $ で割り切ることができることが証明できます。
Lemma dvdn_fermat m n : 0 <= m < n -> fermat m %| (fermat n).-2.
Proof.
move=> H0n.
rewrite fermat_rec.
by apply: prod_dvdn.
Qed.
証明したかったもの
coprime を unfold したのち、先の補題 dvdn_gcdn で書き換えたて得られたサブゴールは、すでに証明した三つの補題を使って証明できます。
- フェルマ数は奇数である。
- フェルマ数は1より大きい。
- $ F_n - 2 $ は $ F_m $ で割り切れる。
なお、最初のサブゴールは、coprime を fold しています-/(coprime _ _)。
Lemma coprime_fermat m n : m < n -> coprime (fermat m) (fermat n).
Proof.
move=> Hmn.
rewrite /coprime.
rewrite (@dvdn_gcdn _ _ 2).
- by rewrite -/(coprime _ _) coprimen2 odd_fermat.
- by rewrite fermat_gt1.
- by rewrite subn2 dvdn_fermat.
Qed.
参考文献
この問題は [1] の exercise2 からとりました。回答も同じページから参照できますが、演習問題なので、次に習うbigop (ΣやΠ) を使わずに証明しています。[2] にあるように、フェルマ数のΠを使った漸化式を導いて証明するほうが易しかったので、それで証明してみました。
[1] Math Comp School & Workshop - 2022
[2] フェルマー数とその性質 - 高校数学の美しい物語