数学ガールの「数学的帰納法」の問題

@suharahiromichi

2020/06/21

結城浩さんの「数学ガールの秘密ノート」に数学的帰納法の話題があります（文献 [1][2]）。
数学ガールシリーズにしてはめずらしく、入試問題を題材にしています（文献 [3]）。なので、解答にチャレンジしたかたもいるのではないかとおもいます。これを Coq/MathComp （文献 [4]）で解いてみようと思います。
ひとつ前の値を使う数学的帰納法は、Coqのような定理証明器（定理証明支援システム）が得意とすることのはずなのですが、案外と大変でした。

• 与えられた漸化式をCoqの関数で定義しようとすると、停止性の証明が必要となる。

• 自然数をインデックスとする数列の一般項を求める問題だが、数列の値は有理数（自然数を分母子とする分数）である。

• 一般項を求める過程で、有理数環の補題の証明が必要となる。

• その補題を適用するときに、分子が零ではないことを示す必要があり、数列の項が > 0 であることを（一般項を使わずに）証明する必要があった。このとき、完全帰納法 (complete induction, strengthening induction) が必要になった。

• 高校数学なので、1からの自然数を使っているが、Coqでは自然数は0以上としなければならない。

このファイルは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/math/ssr_ind_of_math_girl_2.v
証明スクリプトは模範回答ではなく、一例として参考程度にしてください。

FrommathcompRequireImportall_ssreflect.FrommathcompRequireImportall_algebra.RequireImportssromega.(* ssromega タクティク *)RequireImportRecdef.(* Function コマンド *)SetImplicitArguments.UnsetStrictImplicit.UnsetPrintingImplicitDefensive.ImportGRing.Theory.(* mulrA などを使えるようにする。 *)ImportNum.Theory.(* unitf_gt0 などを使えるようにする。 *)ImportintZmod.(* addz など *)ImportintRing.(* mulz など *)OpenScopering_scope.(* 環の四則演算を使えるようにする。 *)SectionLemmas.

補題

最初に、0でない(1を越える)有理数 p と q に対して、
$$ \frac{p}{\frac{p}{q}} = q $$

であることを証明します。分母を払うためのものですが、この補題を Coq/MathComp のルールにしたがって、divKq と命名します。有理数(q)の割算(div)で、もとに戻る(K, cancel) の意味です。
ここで証明した補題の段階では、0 < p と 0 < q の前提が残ることに注意してください。

divKq を直接証明してもよいのですが、
divqA と mulKq の別の補題を証明して使っています。その証明には、MathComp の環 (ring) の補題を使っています（文献 [6]）。

LemmadivqA(pqr:rat):0<q->0<r->p/(q/r)=(p*r)/q.Proof.move=>HqHr.rewriteinvrM.(* p * (r^-1^-1 / q) = p * r / q *)-rewriteinvrK.(* p * (r / q) = p * r / q *)rewrite-div1r.(* p * (r * (1 / q)) = p * r * (1 / q) *)byrewrite!mulrA.-byapply:unitf_gt0.(* q \is a GRing.unit *)-rewrite-invr_gt0inHr.(* r^-1 \is a GRing.unit *)byapply:unitf_gt0.Qed.LemmamulKq(pq:rat):0<p->(p*q)/p=q.Proof.move=>Hp.rewrite[p*q]mulrC.(* q * p / p = q *)(* rewrite -div1r. *)rewrite-mulrA.(* q * (p / p) = q *)(* rewrite div1r. *)rewritedivrr.(* q * 1 = q *)-byrewritemulr1.-byrewriteunitf_gt0.(* p \is a GRing.unit *)Qed.LemmadivKq(pq:rat):0<p->0<q->p/(p/q)=q.Proof.move=>HpHq.rewritedivqA;lastdone;lastdone.rewritemulKq;lastdone.done.Qed.EndLemmas.

試験問題

本題の試験問題（文献 [3]）を解いていきます。大筋では、数学ガール（文献 [1][2]）と同じです。ですが、少し異なるとこともあります。

• 数列 a の漸化式を Coq の再帰関数として定義する。ただし、a_0 を起点とするため、試験問題や数学ガールの記事と比べると、インデックスがひとつづづずれる。

a_0 = 3\\
a_1 = 3\\
a_2 = 3\\
a_{k+3} = \frac{a_k + a_{k+1}}{a_{k+2}}

• 数列 b と 数列 c を 数列 a から定義する。ただし、試験問題や数学ガールの記事と逆に、b_k を a_2k （偶数番）、c_k を a_2k+1 （奇数番）とする。

b_k = a_{2k}\\
c_k = a_{2k+1}

• 試験問題（と数学ガールの記事）の誘導問題に従い、b_k+2 と c_k+1 の式を求める(lemma_1 と lemma_2)。

• 0 < a_k であることを証明する。このとき、帰納法の仮定として、k0 < k であるすべてのk0で 0 < a_k0 が成り立つものとして、
  0 < a_k であることを証明する（完全帰納法を使う）。

• 0 < a_k から 0 < b_k と 0 < c_k を導く。

• b_k = b_k+1 であること(lemma_3)を、k についての数学的帰納法で証明する。このとき、 補題 divKq を使う。そして、divKq の前提を消すために、a_k, b_k, c_k のそれぞれが > 0 であることを使う。

• 最終的に、bの一般項 b_k が 3 であることを証明することは同じである。
  $$ b_k = 3 $$

SectionQuestion.

数列 a_k の漸化式

数列 a_k の漸化式 を Coq の関数で定義します。自然数 k を引数とする再帰関数として定義することになりますが、Coq はこの関数が、任意の自然数 k に対して計算できること、すなわち、再帰が止まって値が求まること（計算の停止性）を自動判定できない、というエラーを出力します。
そこで、定義に際して、再帰の毎に k の値が減ることを明示してやります（Function コマンドを使う。文献 [9]）。
すると、Function コマンドは、k.+2 < k.+3 と k.+1 < k.+3 と k < k.+3を証明することを求めてきます（証明責務ですね）。FunctionコマンドはStarndard Coqのコマンドなので、StandardCoqの不等式 (例：(k.+2 < k.+3)%coq_nat) を出力します。これは apply/ltP を使って、MathCompの不等式（例：(k.+2 < k.+3)%N）に変換できます。Coqの自然数 %coq_nat が MathCompの自然数 %N に変わっています。
そして、ssromega タクティク（文献 [7]）を使って証明します。なお、ここでは文献[7]のうちの sssromega の定義の部分だけを取り出して、最初に Require Import ssromega で読み込んでいます。

(* 【２】の式 (a_k の定義) *)Functiona(k:nat){measureidk}:rat:=matchkwith|0=>ratz3(* fracq (3%:Z, 1%:Z) *)|1=>ratz3(* fracq (3%:Z, 1%:Z) *)|2=>ratz3(* fracq (3%:Z, 1%:Z) *)|k'.+3=>(ak'+ak'.+1)/ak'.+2end.-move=>k3k2k1kHk1Hk2Hk3.apply/ltP.byssromega.-move=>k3k2k1kHk1Hk2Hk3.apply/ltP.byssromega.-move=>k3k2k1kHk1Hk2Hk3.apply/ltP.byssromega.Defined.(* 実際に計算できるように、Defined で終える。 *)

関数をその定義で展開するときには、rewrite /a (Standard Coq の unfold タクティク)は使用できず。a_equation による書き換えを使わなければいけません（文献 [9]）。
これは、Function コマンドで定義した関数 a には、その定義に余計な証明が付随するからです。

数列 b_k と c_k

a_k の定義を使います。

Definitionb(k:nat):rat:=ak.*2.(* a_k の偶数番 *)Definitionc(k:nat):rat:=ak.*2.+1.(* a_k の奇数番 *)

実際に計算してみます。正しそうですね。

Computea0.(* b_0 = 3 *)Computea1.(* c_0 = 3 *)Computea2.(* b_1 = 3 *)Computea3.(* c_1 = 2 *)Computea4.(* b_2 = 3 *)Computea5.(* c_2 = 5/3 *)Computea6.(* b_3 = 3 *)Computea7.(* c_3 = 14/9 *)

b_k+2 と c_k+1 の式

数学ガールの記事にあるとおり、誘導問題に従い、b_k+2 と c_k+1 の式を求めます。
a_k の漸化式（の関数）の定義を展開するときは、a_equation を使っています。
補題 doubleS は 2 * (n + 1) と 2 * n + 2 との間の書き換えをします。

CheckdoubleS:foralln:nat,(n.+1).*2=n.*2.+2.Lemmalemma_1(k:nat):(* 計算で得た式(1) *)bk.+2=(ck+bk.+1)/ck.+1.Proof.rewrite/b!doubleSa_equation.rewrite/cdoubleS.done.Qed.Lemmalemma_2(k:nat):(* 計算で得た式(2) *)ck.+1=(bk+ck)/bk.+1.Proof.rewrite/c!doubleSa_equation.rewrite/bdoubleS.done.Qed.

0 < a_k の証明

• 0 < a_k であることを証明するには、a_k-1, a_k-2, a_k-3 の値が > 0 であることが必要になります。
  そこで、帰納法の仮定 k' < k の k' に対して a_k' < 0 が成り立つとして、
  k' < k+1 の k' に対して a_k' < 0 が成り立つことを示す完全帰納法 (complete induction) を使って証明します。
  k についての完全帰納法を使うとき、MathComp の場合は、elim: k {-2}k (leqnn k)というイデオムを使います（文献 [8]、および、[5] の 3.2.4 Application: strengthening induction）。

• [| [| [| k']]] はパズルのようですが、a_k' の k' について条件分け（0か1以上か）を3回繰り返すことで、a_k'+3 を取り出すためのものです。

• 補題 divr_gt0 と addr_gt0 を適用することで、0 < (a k' + a k'.+1) / a k'.+2 を
  0 < a k' と 0 < a k'.+1 と 0 < a k'.+2 に分解します。

• 最後に、それぞれに対して（完全）帰納法の仮定を適用することで得られた不等式は、ssromgaで片付けています。

Lemmaak_gt_0k:0<ak.Proof.elim:k{-2}k(leqnnk)=>[k|kIHk].(* 完全帰納法のイデオム *)-byrewriteleqn0=>/eqP->.-case=>[|[|[|k']]]Hk//.(* 条件分けで a k'+3 を取り出す。 *)rewritea_equation.rewritedivr_gt0//.+rewriteaddr_gt0//.*apply:IHk.byssromega.*apply:IHk.byssromega.+apply:IHk.byssromega.Qed.

0 < b_k と 0 < c_k の証明

0 < a_k を使います。

Lemmabk_gt_0k:0<bk.Proof.rewrite/b.byapply:ak_gt_0.Qed.Lemmack_gt_0k:0<ck.Proof.rewrite/c.byapply:ak_gt_0.Qed.

b_k = b_k+1

k についての数学的帰納法を使い、帰納法の仮定 b_k = b_k+1 が成り立つとして、b_k+1 = b_k+2 を示すことで証明します。先に証明した、lemma_1とlemma_2と、帰納法の仮定を使って書き換えることで得られた、
b_k = (c_k + b_k) / ((c_k + b_k) / b_k) から、divKq で書き換えることで、(c_k + b_k) を消し（分母を払い）ます。
このとき分母 (c_k + b_k) が > 0 である条件を示すために、前節の補題を使います。

Lemmalemma_3(k:nat):bk=bk.+1.Proof.elim:k=>[|kIHk]//.rewritelemma_1.rewritelemma_2.rewrite-[inRHS]IHk.rewrite-[inLHS]IHk.rewrite[bk+ck]addqC.rewrite[RHS]divKq;firstbyrewriteIHk.-apply:addr_gt0.+byapply:ck_gt_0.+byapply:bk_gt_0.-byapply:bk_gt_0.Qed.

求めたかったもの : b_k の一般項 b_k = 3

Theorembk_3(k:nat):bk=ratz3.(* b の一般項 *)Proof.elim:k=>[|kIHk]//.byrewrite-lemma_3.Qed.EndQuestion.

文献

[1] 結城浩、数学ガールの秘密ノート - センター試験の数学的帰納法、Cakes

• 第13回 (前編) https://cakes.mu/posts/1095

• 第14回 (後編) https://cakes.mu/posts/1157

[2] 結城浩、数学ガールの秘密ノート/整数で遊ぼう、SBクリエイティブ

[3] 2013年大学入試センター試験 数学II・数学B 第3問、
https://school.js88.com/sd_article/dai/dai_center_data/pdf/2013sugaku2B_q.pdf

[4] 萩原学 アフェルト・レナルド、「Coq/SSReflect/MathCompによる定理証明」、森北出版

[5] Mathematical Components Book、
https://math-comp.github.io/mcb/

[6] MathComp, ssralg.v,
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v

[7] Affeldt Reynald, Library ssrnat_ext,
https://staff.aist.go.jp/reynald.affeldt/coqdev/ssrnat_ext.html

[8] Coq/SSReflectでたった1行のコマンドで完全帰納法を適用する方法
https://qiita.com/nekonibox/items/514da8edfc6107b57254

[9] Advanced recursive functions
https://coq.inria.fr/refman/language/gallina-extensions.html#advanced-recursive-functions