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

@suharahiromichi

2023/09/10

2023/12/10 修正


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を後ろにつける必要があります。


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型を返すものを使うことを指示します。


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

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


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

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


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

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


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) 以外はエラーになる。


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

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


Fail Check (Posz O) %:Z.

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


Check true %:Z.

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


Print Graph.
Set Printing Coercions.

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


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

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

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


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 とは書けません。


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をつけます。


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

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


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

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

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


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

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


  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を分配するようにも見えます。


  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を使って、その書き換えをします。


  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に書き換えることで、両辺を等しくします。


  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` で割り切れることの証明


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

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


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

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


  move=> HaP HkO.

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


  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 は等しい、というわけです。


  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します。


  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 型の等式で書き換えます。


  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 型の等式で書き換えます。


  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 型の等式で書き換えます。


  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 になります。


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

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


  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 型の項を書き換えることに注意してください。


  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 は等しいので、証明が終わりです。


  (* 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