フィボナッチ数の最大公約数 (GCD of Fibonacci Numbers)
2022/01/21
2022/01/29 GCDの帰納法について修正した。
このソースは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/math/ssr_fib_3.v
はじめに
m番めとn番めフィボナッチ数の最大公約数は、mとnの最大公約数番めのフィボナッチ数に等しい、という定理があります。
gcd(F_m, F_n) = F_{gcd(m, n)}
これは エドゥアール・リュカ (ルーカス）が最初に報告したのをクヌース先生が紹介して広まったのだそうです。TAOCP[2]に掲載されているようですが、私が読んだのは [1]と[1'] のほうで、証明は演習問題(6.27)になっています。
そこで、早速答えをみると、フィボナッチ数の加法定理に相当する式から、「$ m > n $ ならば、$ gcd(F_m, F_n) = gcd(F_{m - n}, F_n) $であることに注意して、帰納法使って証明せよ」、とだけ書いてあります。
証明を集めたサイト[3]を見ても書いてあることは同じで、[4]はもう少し詳しいですが、帰納法のところは証明というより説明になっています。
では、この定理の証明をCoqでやってみましょう、とりあえず、以下の方針でおこないます。
-
gcdに関する帰納法が肝なので、そこは Coq の Functional Induction [5] に任せる。
-
1.のためには、Function コマンドで自分でフィボナッチ数を定義する必要がある。それも [5] を参考にした。
-
MathComp の GCDに関する豊富な補題を使うために、2.の定義とMathCompのGCDの定義が同じであることを証明しておく。
MathCompで証明をするならば、MathCompで定義されている自然数の最大公約数の関数 gcdn について、なんらかのかたちで帰納法の原理を用意するのが正しいアプローチですが、それは [7] を参照してください。
また、フィボナッチ数の加法定理については、[6] で証明しているため、証明は省略します。
From mathcomp Require Import all_ssreflect.
Require Import FunInd. (* Functional Scheme *)
Require Import Recdef. (* Function *)
Require Import Wf_nat. (* wf *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* Set Print All. *)
Section Fib3.
フィボナッチ数の定義と定理
Function fib (n : nat) : nat :=
match n with
| 0 => 0
| 1 => 1
| (m.+1 as pn).+1 => fib m + fib pn (* fib n.-2 + fib n.-1 *)
end.
1個分のフィボナッチ数の計算
Lemma fib_n n : fib n.+2 = fib n + fib n.+1.
Proof.
done.
Qed.
隣り合ったフィボナッチ数は互いに素である。
Lemma fib_coprime (n : nat) : coprime (fib n) (fib n.+1).
Proof.
rewrite /coprime.
elim: n => [//= | n IHn].
rewrite fib_n.
by rewrite gcdnDr gcdnC.
Qed.
フィボナッチ数列の加法定理
Lemma fib_addition n m :
1 <= m -> fib (n + m) = fib m * fib n.+1 + fib m.-1 * fib n.
Proof.
(* see. ssr_fib_2.v *)
Admitted. (* OK *)
GCDの定義と定理
Function を使って定義します。
Function gcd (m n : nat) {wf lt m} : nat :=
match m with
| 0 => n
| _ => gcd (n %% m) m
end.
Proof.
- move=> m n m0 _.
apply/ltP.
by rewrite ltn_mod.
- by apply: lt_wf.
Qed.
MathComp の gcdn を同じであることを証明する。
Lemma gcdE m n : gcdn m n = gcd m n.
Proof.
functional induction (gcd m n).
- by rewrite gcd0n.
- rewrite -IHn0.
by rewrite gcdnC gcdn_modl.
Qed.
GCDの可換性
Check gcdnC : forall m n, gcdn m n = gcdn n m.
Lemma gcdC m n : gcd m n = gcd n m.
Proof.
by rewrite -2!gcdE gcdnC.
Qed.
GCDの簡単な性質
Lemma gcd0m m : gcd 0 m = m.
Proof.
by rewrite gcd_equation. (* gcd の定義で展開する。 *)
Qed.
Lemma gcdmm m : gcd m m = m.
Proof.
case: m => [| m].
- by rewrite gcd_equation.
- by rewrite gcd_equation modnn gcd0m.
Qed.
Lemma gcdnn_gcd0n n : gcd n n = gcd 0 n.
Proof.
by rewrite gcdmm gcd0m.
Qed.
Check gcdnMDl : forall k m n : nat, gcdn m (k * m + n) = gcdn m n.
Lemma gcdMDl (k m n : nat) : gcd m (k * m + n) = gcd m n.
Proof.
by rewrite -2!gcdE gcdnMDl.
Qed.
Check Gauss_gcdl : forall p m n : nat, coprime p n -> gcdn p (m * n) = gcdn p m.
Lemma Gauss_gcdl' p m n : coprime p n -> gcd p (m * n) = gcd p m.
Proof.
rewrite -2!gcdE.
by apply: Gauss_gcdl.
Qed.
フィボナッチ数のGCD
GKPの解答にある、m > n ならば gcd (fib m) (fib n) = gcd (fib (m - n)) (fib n)と同じものを証明するが、そのために m を 0 と非0で振り分ける。
Lemma fib_lemma_gkp' m n :
1 <= m -> gcd (fib (n + m)) (fib n) = gcd (fib m) (fib n).
Proof.
move=> H.
rewrite fib_addition //.
rewrite gcdC addnC gcdMDl.
rewrite Gauss_gcdl'.
- by rewrite gcdC.
- by apply: fib_coprime.
Qed.
Lemma fib_lemma_gkp m n :
gcd (fib (n + m)) (fib n) = gcd (fib m) (fib n).
Proof.
case: m => [| m].
- rewrite addn0 /=.
by apply: gcdnn_gcd0n.
- rewrite fib_lemma_gkp' //=.
Qed.
gcdnMDl のフィボナッチ数版
Check gcdnMDl : forall k m n : nat, gcdn m (k * m + n) = gcdn m n.
Lemma fib_gcdMDl n q r :
gcd (fib (q * n + r)) (fib n) = gcd (fib n) (fib r).
Proof.
elim: q => [| q IHq].
- rewrite mul0n add0n.
rewrite gcdC.
done.
- Search _ (_.+1 * _).
rewrite mulSn -addnA.
rewrite [LHS]fib_lemma_gkp.
done.
Qed.
gcdn_modr のフィボナッチ数版
Check gcdn_modr : forall m n : nat, gcdn m (n %% m) = gcdn m n.
Lemma fin_gcd_modr m n :
gcd (fib m) (fib n) = gcd (fib n) (fib (m %% n)).
Proof.
move: (fib_gcdMDl n (m %/ n) (m %% n)).
rewrite -divn_eq.
done.
Qed.
証明したいもの
$ F_0 = 0 $ や $ F_1 = 1 $ でも成り立つことを確認しておく。
Compute gcdn 0 0. (* 0 *)
Compute gcdn 1 0. (* 1 *)
Compute gcdn 0 1. (* 1 *)
Compute gcdn 1 1. (* 1 *)
Goal gcd (fib 1) (fib 0) = fib (gcd 1 0).
Proof.
rewrite gcd_equation //=.
by rewrite gcd_equation.
Qed.
functional induction を使って証明します。
Theorem gcd_fib__fib_gcd (m n : nat) : gcd (fib m) (fib n) = fib (gcd m n).
Proof.
rewrite gcdC.
functional induction (gcd m n).
- rewrite gcdC.
rewrite gcd_equation.
done.
(*
IHn0 : gcd (fib m) (fib (n %% m)) = fib (gcd (n %% m) m)
============================
gcd (fib n) (fib m) = fib (gcd (n %% m) m)
*)
- rewrite fin_gcd_modr.
done.
Qed.
End Fib3.
Section Fib3_2.
おまけ
Coq Tokyo 終了後に教えてもらった GCD の帰納法
Lemma my_gcdn_ind (P : nat -> nat -> nat -> Prop) :
(forall n, P 0 n n) ->
(forall m n, P (n %% m) m (gcdn (n %% m) m) -> P m n (gcdn m n)) ->
forall m n, P m n (gcdn m n).
Proof.
move => H0 Hmod.
elim/ltn_ind => [[| m ]] // H n.
- have -> : gcdn 0 n = n by elim: n.
done.
- apply : Hmod.
exact : H (ltn_mod _ _) _.
Qed.
これを使うと functional induction を使わずに証明できます。
[7] を参照してください。
End Fib3_2.
文献
[1] Graham, Knuth, Patashnik "Concrete Mathematics", Second Edition
[1'] 有澤、安村、萩野、石畑訳、「コンピュータの数学」共立出版
[2] D.E.Knuth, "The Art of Computer Programming: Vol.1: Fundamental Algorithms (3rd ed.) "
[3] "GCD of Fibonacci Numbers"、https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers
[4] ぱるち、「フィボナッチ数列で互除法っぽいこと」、https://mathlog.info/articles/278
[5] 名古屋大学 2021年度秋・数理解析・計算機数学 IV (同 概論IV) "Mathcomp, 自己反映と数論の証明"、https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2021_AW/ssrcoq5.pdf
[6] https://github.com/suharahiromichi/coq/blob/master/math/ssr_fib_2.v
[7] https://github.com/suharahiromichi/coq/blob/master/math/ssr_fib_3_2.v