More than 5 years have passed since last update.
(Coqで)カタラン数を語らん
2020/06/28
はじめに
Coq/MathComp には binomial.v というパッケージがあって、二項係数（順列・組合せの「組合せ」）の定義と基本的ないくつかの補題が証明されています。これを使ってなにか証明してみましょう。
このファイルは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/math/ssr_catalan.v
また、
https://github.com/suharahiromichi/coq/blob/master/common/ssromega.v
も必要です。
MathCompの階層としては、有理数や環を導入する前なので、自然数の割算と剰余を使って証明を進めます。
二項係数を使って定義される、カタラン数 (Catalan Number) というものがあります（文献[1]）。nが自然数のとき、以下で定義されます。
c_n =\frac{1}{n + 1}\dbinom{2 n}{n}
これの意味については、「カタラン数を語らん」としているサイト（文献[2]）に譲ります。
ここでは、n番めのカタラン数について、
c_n = \dbinom{2 n}{n} - \dbinom{2 n}{n - 1}、ただし 0 \lt n
が成り立つことを証明したい思います。実際には、上記ふたつの式を整理した、
n \dbinom{2 n}{n} = (n + 1) \dbinom{2 n}{n - 1}、ただし 0 \lt n
を証明します。
以下では、n、m を（0以上の）自然数とします。また、MathCompの表記にあわせて、二項係数 $\dbinom{n}{m}$ を C(n, m) で、また、「m は n で割り切れる」をn | m で示します（除数 | 被除数）。
FrommathcompRequireImportall_ssreflect.RequireImportssromega.SetImplicitArguments.UnsetStrictImplicit.UnsetPrintingImplicitDefensive.補題
SectionLEMMAS.
n! = n (n - 1)! 、ただし 0 < n
階乗の定義から自明ですが、MathComp では (n + 1) = (n + 1) * n!でしか証明されていないので、証明しておきます。
Lemmafact_predn:0<n->n`!=n*n.-1`!.Proof.move=>Hn.haveH:=factSn.-1.rewriteprednKinH;lastdone.done.Qed.
(n! m!) | (n + m)!
階乗の積と和の剰余についての補題を証明します。
「ふたつの数の和の階乗は、それぞれの数の階乗の積で割り切れる」という、ちょっと直観に反する補題ですが、二項係数の定義から導くことができます。
Lemmadivn_fact_mul_add_fact(nmp:nat):n+m=p->(n`!*m`!)%|p`!.Proof.move=><-.have<-:'C(n+m,m)*(n`!*m`!)=(n+m)`!.-rewrite-(@bin_fact(n+m)m);lastbyrewriteleq_addl.rewrite-[n+m-m]addnBA;lastbyrewriteleqnn.byrewritesubnnaddn0[m`!*n`!]mulnC.-rewrite-{1}[n`!*m`!]mul1n.byapply:dvdn_mul.Qed.次のふたつは、先の階乗の積と和の剰余の応用ですが、少し長くなるので、別に証明しておきます。
Lemmadivn_n2_ln:0<n->(n*n.-1`!*n`!)%|n.*2`!.Proof.move=>H.rewrite-[n*n.-1`!]fact_pred;lastdone.apply:divn_fact_mul_add_fact.rewrite-addnn.done.Qed.Lemmadivn_n2_rn:0<n->(n.+1*n`!*n.-1`!)%|n.*2`!.Proof.move=>H.rewrite-[n.+1*n`!]fact_pred;lastdone.apply:divn_fact_mul_add_fact.rewrite-addnn.byssromega.Qed.EndLEMMAS.SectionTH.定理
証明の概略を示します。
(1) C(n, m) = n! / (m! (n - m)!) を使って、二項係数を階乗の式に変換する。整理すると、
\begin{eqnarray}
n \frac{(2n)!}{n! (2n-n)!} &=& (n+1) \frac{(2n)!}{(n-1)! (2n-(n-1))!}\\
n \frac{(2n)!}{n! n!} &=& (n+1) \frac{(2n)!}{(n-1)! (n+1)!}\\
n \frac{(2n)!}{n (n-1)! n!} &=& (n+1) \frac{(2n)!}{(n+1) n! (n-1)!}
\end{eqnarray}
が得られる。
Checkmuln_divA:foralldmn:nat,d%|n->m*(n%/d)=(m*n)%/d.(2) 補題muln_divAを使い、左辺は (n * □) / (n * ■) に変換する。また、右辺は ((n+1) * ○) / ((n+1) * ●) に変換する。このとき、先に証明した階乗の積と和の補題を使います。
\frac{n (2n)!}{n (n-1)! n!} = \frac{(n+1)(2n)!}{(n+1) n! (n-1)!}
CheckdivnMl:forallpmd:nat,0<p->(p*m)%/(p*d)=m%/d.(3) 補題divnMlを使い、左辺から n、右辺から n+1を消す。
\frac{(2n)!}{(n-1)! n!} = \frac{(2n)!}{n! (n-1)!}\\
左辺 = 右辺 で証明が終わりです。
Theoremcatalan_reln:0<n->n*'C(n.*2,n)=n.+1*'C(n.*2,n.+1).Proof.move=>Hn.(* LHS *)(* (1) *)rewritebin_factd;lastbyrewritedouble_gt0.have->:n.*2-n=nbyrewrite-addnn;ssromega.rewrite{1}[inn`!*n`!]fact_pred;lastdone.(* (2) *)rewritemuln_divA;lastbyrewritedivn_n2_l.(* (3) *)rewrite-mulnAdivnMl;lastdone.rewrite[(n.-1)`!*n`!]mulnC.(* RHS *)(* (1) *)rewritebin_factd;lastbyrewritedouble_gt0.have->:n.*2-n.+1=n.-1byrewrite-addnn;ssromega.rewrite[n.+1`!]factS.(* (2) *)rewritemuln_divA;lastbyrewritedivn_n2_r.(* (3) *)rewrite-mulnAdivnMl;lastdone.done.Qed.EndTH.おまけ
カタラン数には、漸化式を使った表現もあります。これが一致することを証明できるでしょうか。
SectionDEFINE.Definitioncatalann:='C(n.*2,n)%/n.+1.Computecatalan0.(* 1 *)Computecatalan1.(* 1 *)Computecatalan2.(* 2 *)Computecatalan3.(* 5 *)Fixpointcatalan_recn{structn}:=matchnwith|0=>1|n'.+1=>\sum_(0<=i<n'.+1)(catalan_rec(n'-(i+n'))*catalan_rec(n'-i))end.停止性が判定できるように、i でよいところを n' - (i + n') としています。。。。
Computecatalan_rec0.Computecatalan_rec1.Computecatalan_rec2.EndDEFINE.文献
[1] https://ja.wikipedia.org/wiki/カタラン数
[2] https://www.google.com/search?&q=カタラン数を語らん
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme