フェルマ数は互いに素

フェルマ数は互いに素
Any two Fermat numbers are coprime.
===============================

@suharahiromichi

2023/7/31


```coq:

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) $$


```coq:

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 $$
から証明します。



```coq:

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 に対して同じ最大公約数を持つ条件


```coq:

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 として、次のかたちで使用します。


```coq:

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 の場合 "^" は右結合であることに注意してください。ただし、ここではできるだけ括弧をつけるようにします。



```coq:

Definition fermat n := (2 ^ (2 ^ n)).+1.

Lemma fermatE n : fermat n = (2 ^ (2 ^ n)).+1.
Proof. by []. Qed.


```

## 補題：フェルマ数は1より大きい


```coq:

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.



```

## 補題：フェルマ数は奇数である


```coq:

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 $$


```coq:

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) $$


```coq:

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）の右辺に対して、繰り返し適用すると総乗（Π）の式になります。


```coq:

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 $ で割り切ることができることが証明できます。


```coq:

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 _ _)``。


```coq:

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

https://mathcomp-schools.gitlabpages.inria.fr/2022-12-school/school


[2] フェルマー数とその性質 - 高校数学の美しい物語

https://manabitimes.jp/math/730





```