kが奇数の時、a^k + 1 が a + 1 で割り切れることの別証明

kが奇数の時、``a^k + 1`` が ``a + 1`` で割り切れることの別証明
===============================

@suharahiromichi

2023/09/10

2023/12/10 修正


```coq:

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


```

# はじめに
以前の投稿（文献 [1]）で、n乗の和の因数分解の応用として、kが奇数の時、``a^k + 1`` が ``a + 1`` で割り切れることを証明しました。これには、別の証明があります（文献 [2]）。因数分解せず、0からaまでの有限環$$ Z_{a + 1} $$を利用して解くものです。
この有限環の型をMathComp では ``Z_(a + 1)`` または ``'Z_a.+1`` 型と書きます。``a.+1`` は、自然数の後者関数の単行演算子なので同じことですが、``.+1``の表記のほうがよく使われます。
証明自体は技巧的でとても短いのですが、自然数ではなく環を使った証明になること、また、Coqの処理系の問題として、ゴールの表示が正しくない（``'Z_a.+1`` 型の等式である旨が表示されない）ことも理解を難しくしています。ここでは、ゴールの表示を補いならがら、MathConmpでの環の扱いに慣れるために、証明をステップバイステップで見ていきたいと思います。

ソースコードは以下にあります。
https://gitlab.com/proofcafe/acs/-/blob/main/acs_le5_dvd_exp.v?ref_type=heads


# 準備
先頭で、``all_ssreflect``に加えて、``all_algebra``をImportしていますが、これでは不足なので、次のように``GRing.Theory``をImportするとともに、ディフォルトのスコープを ring にします。そのため、nat の式は明示的に``%N``を後ろにつける必要があります。


```coq:

Import GRing.Theory.
Import Num.Theory.           (* unitf_gt0 などを使えるようにする。 *)
Import intZmod.              (* addz など *)
Import intRing.              (* mulz など *)
Import Order.Theory.         (* 不等号関連 *)
Local Open Scope ring_scope. (* リングスコープをディフォルトにする。 *)


```

## 補足説明：
ここでは、``%N``、``%:R``、``: Z``、``:> nat`` という、型注釈が使われます。どれも、後置で、式の一部分の型を指定することに違いはありませんが、少しずつ働きが違います。以下でそれを説明します。


- ``%T`` は、必ず``(x op y)%T`` の形で使用され、Notation で定義された複数ある op のうち、T の型のスコープのもの（簡単にいうと、T型を返すものを使うことを指示します。


```coq:

Locate "_ * _".
Check muln : nat -> nat -> nat.
Check mulq : rat -> rat -> rat.
Check (1 * 2)%N.                            (* muln が選ばれる。*)
Check (1 * 2)%Q.                            (* mulq が選ばれる。 *)


```
単に``1``と書いても、それは Notation で定義された複数から、スコープにあわせて選ばれます。


```coq:

Check (S O) : nat.
Check @Rat (1, 1)%Z _ : rat.
Check 1%N.                                  (* (S O) が選ばれる。 *)
Check 1%Q.                                  (* Rat ... が選ばれる。 *)


```
重大な補足。``%T`` は、スコープによって解釈の変わる Notation に対してだけた効果があります。つまり、コンストラクタ自体に対しては意味がありません。


```coq:

Check true%N.                               (* bool のまま *)
Check O%Q.                                  (* nat のまま *)


```

- ``%:T`` は、後置演算子で、実体は関数です。Locateで確認できます。スコープとの合わせ技である場合もあります。


```coq:

Locate "%:Z".                               (* Posz と同じ。 *)
(* ring scope で ``nat -> int`` である。nat scope ではエラーになることに注意 *)
Check O%:Z.                                 (* int *)
Check Posz O.                               (* Posz : nat -> int *)


```
いつも ``%:Z`` が Posz であるわけでなく、ring_scope (または int_scope) 以外はエラーになる。


```coq:

Local Close Scope ring_scope.
Fail Check O%:Z.
Check Posz O.                               (* int *)
Local Open Scope ring_scope.


```
また、int型に対して、``%:Z`` をつけると、単純にエラーになります。


```coq:

Fail Check (Posz O) %:Z.


```
ring_scope のとき、nat型なら``%:Z``を適用でき、``bool -> nat`` のCoercion は効くので、
``bool -> nat`` のcoercionの後、Posz が適用されます。


```coq:

Check true %:Z.


```

- ``: T`` は、狭い意味での型注釈ですが、coercionを起こします。
 - ``bool -> nat`` のcoercionは nat_of_bool
 - ``nat -> int`` のcoercionは Poszです。
coercionの一覧は、Print Graph でわかります。


```coq:

Print Graph.
Set Printing Coercions.

```

```
[nat_of_bool] : bool >-> nat (reversible)
[Posz] : nat >-> int
```


```coq:

Check true : nat.
Check nat_of_bool true.                     (* nat *)

Check O : int.
Check Posz O.                               (* int *)


```
両方が同時の場合もあります。


```coq:

Check true : int.
Check Posz (nat_of_bool true).              (* int *)

Unset Printing Coercions.


```

- ``:> T`` は、``x = y :> T`` のように、等式の一部として使われます。
``(x : T) = (y : T)`` の構文糖衣です。なので、以下の説明では、後者の書き方をしたいと思います。

``=``のほかに、``<>``、``==``、``!=`` も使えます。いずれも3項演算子ですから、``(x = y) :> T`` とは書けません。


```coq:

Check true = O :> int.
Check (true : int) = (O : int).


```
最後に、``:``は右結合で、``=``より結合度が低いので、
``((X : T1) : T2) = ((Y : T1) : T2)``という書き方になる場合があります。


# 補題 - サイズkの有限環において、``k - 1`` は ``-1`` に等しい。
文献 [2] に沿って、補題を証明します。

``k.-1`` はスコープによらず nat なので、最初に ``%R``で環にします。両辺を有限型 ``'Z_k`` に変換して、比較します（コアーションではないので、説明を補足すること）。

```(k.-1%:R : 'Z_k) = (-1 : 'Z_k)```

前提となる``1 < k`` は、自然数の不等式なので、全体に``%N``をつけます。



```coq:

Lemma pred_Zp (k : nat) : (1 < k)%N -> k.-1%:R = -1 :> 'Z_k.
Proof.

```

この証明は、1行で済ますことができます。


```coq:

  by case: k => // k Hkgt0; rewrite -subn1 natrB ?char_Zp ?sub0r.
  Restart.


```

1行づつ見ていきましょう。


``k = 0`` の場合は前提矛盾で成立するので、それを片付けます。以降は``k.+1``だけを考えます。
以下ではゴールを ``(* Goal *)`` の後に書くことにします。


```coq:

  case: k => // k Hkgt0.
  (* Goal *) Check k.+1.-1%:R = -1 :> 'Z_k.+1.


```

補題``subn1``を使って、自然数の前者演算子（``■.-1``）を通常の引き算（``■ - 1``）に置き換えます。


```coq:

  Check subn1 : forall n : nat, (n - 1)%N = n.-1.
  have <- : (k.+1 - 1)%N = k.+1.-1 by rewrite subn1.
  (* Goal *) Check (k.+1 - 1)%:R = -1 :> 'Z_k.+1.


```

補題``natrB``を使って、``■ - 1``を自然数の引き算から環の引き算に変換します。
``%:R``を分配するようにも見えます。


```coq:

  Check natrB : forall (R : ringType) (m n : nat), (n <= m)%N -> (m - n)%:R = m%:R - n%:R :> R.
  Check natrB : forall (R : ringType) (m n : nat), (n <= m)%N -> ((m - n)%:R : R) = (m%:R - n%:R : R).
  (* ``:> R`` や ``: R`` の R は引数で展開されますが、``%:R`` は展開されないことに注意してください。 *)
  have -> : (k.+1 - 1)%:R = k.+1%:R - 1 :> 'Z_k.+1 by rewrite natrB.
  (* apply: (@natrB 'Z_k.+1 k.+1 1 (_ : 0 < k.+1)%N) *)
  (* Goal *) Check k.+1%:R - 1 = -1 :> 'Z_k.+1.


```

有限環``'Z_k.+1``の上で``k.+1`` は ``0``に等しいので、補題``char_Zp``を使って、その書き換えをします。


```coq:

  Check char_Zp : forall p : nat, (1 < p)%N -> p%:R = 0 :> 'Z_p.
  have -> : k.+1%:R = 0 :> 'Z_k.+1 by rewrite char_Zp.
  (* apply: @char_Zp k.+1 (_ : 1 < k.+1)%N *)
  (* Goal *) Check 0 - 1 = -1 :> 'Z_k.+1.


```

補題``sub0r``で、``0 - 1`` を ``-1``に書き換えることで、両辺を等しくします。


```coq:

  Check sub0r : forall (V : zmodType) (x : V), 0 - x = - x.
  have -> : 0 - 1 = - 1 by move=> t; rewrite sub0r.
  (* Goal *) Check -1 = -1 :> 'Z_k.+1.

  done.
Qed.


```

# kが奇数の時、``a^k + 1`` が ``a + 1`` で割り切れることの証明


```coq:

Lemma dvd_exp_odd (a k : nat) : (0 < a)%N -> odd k -> (a.+1 %| (a ^ k).+1)%N.
Proof.

```

この証明は、2行で済ますことができます。


```coq:

  move=> aP kO; apply/eqP; rewrite -val_Zp_nat//.
  by rewrite -natr1 natrX pred_Zp// -signr_odd kO addNr.  
  Restart.


```

これも、1行ずつ見ていきましょう。


```coq:

  move=> HaP HkO.

```

ゴールの ``a.+1 %| (a ^ k).+1`` は、 ``(a ^ k).+1 %% a.+1 == 0``
の構文糖衣ですから、``==``を``=``には変換しておきます。


```coq:

  apply/eqP.
  (* Goal *) Check ((a ^ k).+1 %% a.+1)%N = 0%N :> nat.


```

自然数の剰余（``■ %% a.+1``）は、有限環``'Z_a.+1``上の計算（``■ : 'Z_a.+1``）と同じなので、
補題``val_Zp_nat``を使って書き換えます。

``<-`` の書き換えを見るとわかる通り、自然数■を環にして有限環にしてまた自然数にしたものと、
自然数``■ %% a.+1`` は等しい、というわけです。



```coq:

  Check val_Zp_nat : forall p : nat, (1 < p)%N -> forall n : nat, ((n%:R : 'Z_p) : nat) = (n %% p)%N.
  have <- : ((a ^ k).+1%:R : 'Z_a.+1) = ((a ^ k).+1 %% a.+1)%N :> nat by rewrite val_Zp_nat.
  (* Goal *) Check ((a ^ k).+1%:R : 'Z_a.+1) = 0%N :> nat.


```

以降、左辺の``(a ^ k).+1%:R : 'Z_a.+1`` を ``(a ^ k)%:R + 1 : 'Z_a.+1``に変形します。

左辺の ``.+1`` を 環の ``+ 1`` に変換します。
左辺全体を書き換えるので nat の等式をrewriteします。


```coq:

  Check @natr1 nat (a ^ k) : (a ^ k)%:R + 1 = (a ^ k).+1%:R :> nat.
  have <- : ((a ^ k)%:R + 1 : 'Z_a.+1) = ((a ^ k).+1%:R : 'Z_a.+1) :> nat.
  by rewrite natr1.
  (* Goal *) Check ((a ^ k)%:R + 1 : 'Z_a.+1) = 0%N :> nat.


```

左辺の 自然数どうしのexp ``a ^ k`` をセミリングと自然数のexp ``a ^+ k`` に変換します。
``'Z_a.+1`` 型の等式で書き換えます。


```coq:

  Check @natrX  : forall (R : semiRingType) (n k : nat), (n ^ k)%:R = n%:R ^+ k.
  have -> : (a ^ k)%:R = a%:R ^+ k :> 'Z_a.+1.
  by rewrite natrX. (* @natrX 'Z_a.+1 a k *)
  (* Goal *) Check a%:R ^+ k + 1 = 0%N :> nat.


```

``a`` は、``a+1 - 1`` であり、
``a+1`` の有限環の上で、``a+1 - 1`` は ``-1`` に等しいので、書き換えます、
``'Z_a.+1`` 型の等式で書き換えます。


```coq:

  Check pred_Zp : forall k : nat, (1 < k)%N -> k.-1%:R = -1 :> 'Z_k.
  have -> : a.+1.-1%:R = -1 :> 'Z_a.+1.
  by rewrite pred_Zp.             (* @pred_Zp a.+1 (_ : 1 < a.+1)%N *)
  (* Goal *) Check ((-1) ^+ k + 1 : 'Z_a.+1) = 0%N :> nat.


```

(-1)^k は、k の偶奇で値が決まるので、そのように書き換えます。
``'Z_a.+1`` 型の等式で書き換えます。


```coq:

  Check signr_odd : forall (R : ringType) (k : nat), ((-1) ^+ odd k : R) = ((-1) ^+ k : R).
  Check @signr_odd 'Z_a.+1 : forall (k : nat), (-1) ^+ odd k = (-1) ^+ k :> 'Z_a.+1.
  have <- : (-1) ^+ odd k = (-1) ^+ k :> 'Z_a.+1.
  by rewrite signr_odd.                   (* @signr_odd 'Z_a.+1 k *)
  (* Goal *) Check (((-1) ^+ odd k + 1 : 'Z_a.+1) : nat) = 0%N.


```

k は奇数とわかっているので、``odd k`` は true になります。


```coq:

  rewrite HkO.
  (* Goal *) Check ((-1) ^+ true + 1 : 'Z_a.+1) = 0%N :> nat.


```

true は 1 なので、``(-1)^1`` は -1 ですが、まだ ``'Z_a.+1`` 型の等式の中で書き換えます。


```coq:

  Check (-1) ^+ true = -1 :> 'Z_a.+1.
  have -> : (-1) ^+ true = -1 :> 'Z_a.+1 by done.
  (* Goal *) Check (-1 + 1 : 'Z_a.+1) = 0%N :> nat.


```

左辺の ``-1 + 1`` を 0 に書き換えます。
ただし、``'Z_a.+1`` 型の項を書き換えることに注意してください。


```coq:

  Check addNr : forall x : zmodType, left_inverse 0 -%R +%R.
  Check addNr 1 : -1 + 1 = 0 :>  'Z_a.+1.
  have -> : -1 + 1 = 0 :> 'Z_a.+1.
  by rewrite addNr.


```

有限環 ``'Z_.a+1`` の 0 と、自然数の 0 は等しいので、証明が終わりです。


```coq:

  (* Goal *) Check (0 : 'Z_a.+1) = 0%N :> nat.
  done.
Qed.


```

# 文献


[1] https://qiita.com/suharahiromichi/items/d6a070fe6444b4104598


[2] https://www-sop.inria.fr/teams/marelle/MC-2022/lesson5.v


```