64 Mathematical Components 1969 Curry-Howard (statement) INRIA Mathematical Components RSA Mathematical Components Mathematical Components M

64

解 説

Mathematical Components

入門

アフェルト・レナルド

コンピュータのプログラムと数学の証明の間に密な関係があることはよく知られている．1969 年に発見された Curry-Howard 同型対応により，プログラムの型を言明 (statement) として見れば，プログラム自体はその言明の 証明として見られる．これにより，数学の証明の検査はプログラムの型付けに帰着する．この発想に基づいて，定理 証明支援系という検証ツールの開発が行われてきた．近年，定理証明支援系を用いて，ようやく現実的なプログラム と証明の検証が可能となっている． 現実的な証明の一例として，2005 年から 2012 年までマイクロソフト・INRIA の共同研究組織で形式化された 奇数位数定理が挙げられる．奇数位数定理は膨大な証明により示された重要な群論の定理であるため，その形式化は 大きなマイルストーンとなっている．加えて，その形式化の基盤である Mathematical Components もまた，形式 数学におけるライブラリとして重要な成果である． 我々のデジタル社会を支える基本的なコンピュータプログラムである RSA 暗号や楕円曲線暗号や符号などは， 整数論や群論や線形代数などの数学に基づいているが，Mathematical Components を用いることで，これらのプ ログラムの厳密な仕様の記述ができるようになった．しかし，Mathematical Components のような大規模なライ ブラリの利用には専門知識が不可欠である． 本解説では，Mathematical Components による形式化を紹介する．群論のラグランジュ定理を用いて，そのラ イブラリの基本的な使い方を説明する．

Since 1969 and the Curry-Howard isomorphism, we know that there is a strong relation between computer programs and mathematical proofs: concretely, if we look at the type of a program as a mathematical statement, then the program itself can be regarded as a proof. As a consequence, proof-checking can be performed by type-checking. Based on this theoretical idea, verification tools have been developed that are now mature enough to tackle non-trivial formal verification tasks.

The formal verification of the odd order theorem, conducted from 2005 to 2012 by Microsoft Research-INRIA, is an example of realistic formal verification. It became a milestone because this theorem is an important result of group theory whose proof is particularly large. But in fact, the formal libraries known as the Mathematical Components that form the basis of this formalization are an equally important output of this experiment.

Indeed, using the Mathematical Components, it becomes possible to carry out rigorous verifications of computer programs that rely on non-trivial mathematics. Such programs are actually important parts of our digitial society. One can think for example of RSA encryption or elliptic-curve cryptography, that are based on number theory, group theory, linear algebra, etc.

Still, the Mathematical Components form a huge library whose usage requires specific expertise. In this introductory paper, we explain the basics of the Mathematical Components, using as a running example the Lagrange theorem.

Introduction to Mathematical Components.

Reynald Affeldt, 産業技術総合研究所情報技術研究部 門, Information Technology Research Institute, Na-tional Institute of Advanced Industrial Science and Technology. コンピュータソフトウェア, Vol.34, No.2 (2017), pp.64–74. [解説論文] 2016 年 7 月 12 日受付.

1 はじめに

Mathematical Componentsプロジェクトは，最初 の目標として奇数位数定理の形式化に取り組んだ．奇 数位数定理は有限群論の重要な定理で，ファイトとト ンプソンによって1963年にその証明が発表された．

Vol. 34 No. 2 May 2017 65 長い証明であったため，単純化されたが，なお紙上の 証明は250頁程度であった．そのため，その形式化 はチャレンジとして見られていた．7年間の作業を経 て，2012年にGonthierらが奇数位数定理の形式化 を発表した[6]． 本解説の目的は，Mathematical Componentsの紹

介である． Mathematical Componentsは，Coq[5]

という定理証明支援系で開発された数学の形式化の ためのライブラリである．奇数位数定理の形式化に必

要な数学(有限群，代数，体，指標等)は様々であり，

Mathematical Componentsの規模はCoqのライブ

ラリとしては珍しく大きい．具体的には， Mathemat-ical Componentsのライブラリは，約4千の形式定 義と1万3千の形式定理を含む15万行のCoqスク リプトとなり，奇数位数定理の250頁の証明は約4万 行となる．Coqスクリプトの長さを抑えるためには， Coqの拡張が不可欠だった．その拡張は専用タクティ ク群_SSReflectと呼ばれる．今回，Mathematical Componentsの包括的な説明は省略する代わりに，有 限群論に関する部分を集中的に紹介する．具体的な 例としてラグランジュ定理を用いて，Mathematical

Componentsと_SSReflectを説明する．Coqの紹

介については[2]を参照されたい． 1. 1 ラグランジュ定理の言明 ラグランジュ定理は群論を勉強する際，最初に習う 定理である． ラグランジュ定理の言明に必要な群論 の定義を復習する．群は基本的な代数的構造である． 群Gは集合Gと二項演算⋆ : G× G → Gの組であ る．ただし，次の3つの条件を満たす: (1) Gの任意の元a，b，cに対して，(a ⋆ b) ⋆ c = a ⋆ (b ⋆ c) (結合法則)， (2) Gの元1が存在し，任意のGの元aに対して， a ⋆ 1 = 1 ⋆ a = a (単位元の存在)， (3) Gの任意の元aに対して，Gの元a′が存在し， a ⋆ a′= a′⋆ a = 1 (逆元の存在)． 集合Gの濃度が有限のとき，Gは有限群という．二 項演算⋆を部分集合H ⊆ Gに制限するとき，もし Hは群であれば，Hは部分群という． ラグランジュ定理の言明は次のようになる． Gは有限群とし，HをGの部分群とする．こ のとき，Hの濃度は，Gの濃度を割り切る． この商を部分群の指数といい，[G : H]と書く．つま り，_{|G| = [G : H] × |H|}が成り立つ(ラグランジュ 定理の形式的な言明は9節を参照)． 1. 2 ラグランジュ定理の意義 ラグランジュ定理を用いて，群の様々な性質を証明 できる．例えば，RSA暗号で応用されているフェル マーの小定理はラグランジュ定理の系である．また， 暗号で使う素数判定アルゴリズムもフェルマーの小定 理に基づいている． 数学でラグランジュ定理は，群を分類するための重 要な定理である．説明のため，群の元の位数と巡回 群を定義する．g∈ Gの位数をgn_{= 1を満たす最小} のnとする． 巡回群Cnを{1, g, g2, . . . , gn−1}のよ うに記述できる有限群とする．g∈ Gの位数はnで あるとき，H ={1, g, g2, . . . , gn−1}は部分群であり， ラグランジュ定理により，nは|G|を割り切ることが 分かる．更に，|G|が素数でかつg̸= 1の場合，Gは {1, g, g2 , . . . , gn−1}になると分かる．つまり，Gは濃 度nの巡回群Cnである． また，ラグランジュ定理を用いて，群の分類がで きる．例えば，_{|G| = 4}の場合，g ∈ Gの位数は1 または2または4になる． 位数4のgがあれば， G ={1, g, g2, g3}と分かる． 位数4のgがなければ， 1以外の元は位数2を持つことが分かる．更に，Gの 元は1，g0，g1，g2と書くと，g1⋆ g0= g2と分かる (そうでなければ，g1= 1またはg0= 1; g1⋆ g0= 1 であれば，g1 = g0となる)．つまり，Gの演算は次 の表となる: 1 g0 g1 g2 1 1 g0 g1 g2 g0 g0 1 g2 g1 g1 g1 g2 1 g0 g2 g2 g1 g0 1 上記の表は_Z2× Z2のKlein群(四元群)と同じ表に なることが分かる：

66 (0, 0) (0, 1) (1, 0) (1, 1) (0, 0) (0, 0) (0, 1) (1, 0) (1, 1) (0, 1) (0, 1) (0, 0) (1, 1) (1, 0) (1, 0) (1, 0) (1, 1) (0, 0) (0, 1) (1, 1) (1, 1) (1, 0) (0, 1) (0, 0) つまり，ラグランジュ定理を用いて，濃度4の群は C4またはC2× C2であることが分かった． 1. 3 ラグランジュ定理の証明の概要と 本解説の流れ ラグランジュ定理を次のように証明できる．まず， g∈ Gに対するHの左剰余類を_{{g ⋆ h | h ∈ H}}と定 義する．[G : H]はHの剰余類の数として定義する． Hの剰余類はGを分割し，それぞれの剰余類はHと 同じ濃度があるため，ラグランジュ定理が成り立つ． 上記の証明は，Mathematical Componentsにおい て見つけることができる．様々な形式定義や補題を使 うので，そのまま再現すると説明は長くなる．本解説 では，直接的な証明を行う．その証明は，紙上で，1 頁もかからない([4]の定理V.3.1の系1)． 具体的には，ラグランジュ定理を次のように一般化 する． Gを有限群とし，HとKをK ⊊ Hを満 たすGの部分群とするとき，[G : K] = [G : H]× [H : K]． これの形式化は8節に説明する．この定理を示すた め，濃度[G : K]の集合(具体的には，左剰余類の 集合(G/K)l)と濃度[G : H]× [H : K]の集合の 間の全単射を用意する．その全単射の基本的な部品は 7節で構築する．準備として，6節で左剰余類の性質 を示す．その際，_SSReflectの専用タクティクを紹 介する．4節と5節で，Mathematical Components による有限集合と有限群を紹介する．

2 定理証明支援系 Coq の基本

定理証明支援系Coqは，数学またはソフトウェア の形式検証のためツールである．1984年からフラン スのINRIAが開発している[5]．ツールの基本的な 部分は型付き関数型言語Gallinaである．ユーザは Gallinaの型 を用いて，形式言明を書く．証明はその 型を持つGallinaのプログラム となる．この発想は Curry-Howard同型対応に基づく．具体的に，Coqで の補題の証明は次のように記述する: L e m m a 補題名 : Gallina の型 . P r o o f. Gallina のプログラム Qed. 上記のとおり，形式証明として直接Gallinaのプロ グラムを与えることもできるが，一般的に困難であ る．通常は，形式証明の記述を部分的に徐々に行う． そのため，タクティクという基本的な論法を使う． Coqは様々なタクティクを提供するが，本解説は，

Mathematical Componentsが導入した_SSReflect の専用タクティクのみを扱う． Coqの標準ライブラリでは論理積/\(中置記法)が2 つのパラメーターを持つ型として定義されている†1_． 例えば，/\の可換性は次のように言明として表現でき る: L e m m a a n d C : f o r a l l P Q : Prop, P /\ Q - > Q /\ P . P r o o f. forallを 用 い て ，変 数P, Q を 束 縛 す る ．Prop は Gallinaが提供する命題の型である．P Q : Propは (P : Prop) (Q : Prop)の略である．->は関数の型であ るが，Curry-Howard同型対応によって含意関係とし て読むことができる． 上記のandC補題の型が関数型であるため，その証 明はGallinaの関数になると分かる．その関数はタク ティクを用いて次のように構築できる: m o v e= > P Q . by c a s e. Qed. move=> P Q.タクティクは束縛変数PとQを固定する． caseタクティクは論理積P /\ Qの消去を行う．消去 の結果，PとQの証明が明確になり，論理積Q /\ Pの 構成が容易になるため，Coqによる自動証明が可能に なる．byタクティカルを用いて，証明の完成を求める (moveとcaseタクティクの詳細な説明は6節を参照)． †1 論理積は帰納的に定義されている．論理積を構成する ため，conj という構成子がある．

Vol. 34 No. 2 May 2017 67

Qed命令でスクリプトを完成する前に，Show Proof命

令を用いてCoqが構築した関数を表示できるが，そ の可読性は低い． 一方，Coqではデータ構造も定義できる．特に， Mathematical Componentsではブール型が重要な役 割を果たす．Coqの標準ライブラリではブール型を 帰納的型として定義している: I n d u c t i v e b o o l : Set : = | t r u e : b o o l | f a l s e : b o o l . SetはGallinaが提供するデータ構造の型である．上

記の定義により，boolが構成子trueまたはfalseを

用いて構成する型であると分かる． Coqで形式検証を行う際，命題の型として，Prop の 代 わ りboolを 用 い る こ と も あ る ．例 え ば ，先 ほ ど Prop に 対 し て 証 明 し た 論 理 積 の 可 換 性 を ブ ー ル 型 に 対 し て 表 現 す る と ，次 の よ う に な る: L e m m a a n d b C :

f o r a l l P Q : bool , andb P Q = true - > a n d b Q P = t r u e . P r o o f. 今回，命題PとQはbool型となる．/\の代わりに andbというブール関数を用いる． 上記のandbC補題の証明は次のようにできる: c a s e. - by c a s e. - by c a s e. Qed. 最初のcaseタクティクを用いて，ブール変数Pの場 合分けを行う．その結果，2つのサブゴールができる: 1番目のサブゴールではPはtrueとなり，2番目の サブゴールではPはfalseとなる．それぞれのサブ ゴールを明確にするために，-を用いて箇条書きにす る．今回，それぞれのサブゴールに対するスクリプト は同じである．caseタクティクを用いてブール変数Q の場合分けを行うと，各サブゴールはandb関数によ る真理値表の確認で証明できる．byタクティカルに よる自動化で，Coqが証明を完成する． 上記の両方の証明を比較すると，andCの場合，命 題P /\ Qの証明を消去し，新たな命題(Q /\ P)の証 明を構成した．andbCの場合，命題PとQを場合分 けし，ブール関数andbの計算によって，証明を簡単 にした．Mathematical Componentsでは，できるだ けboolを使うように証明が構成されている．bool型 の計算力に頼ると，膨大な形式証明が簡単になると Mathematical Componentsの作成者が経験したた めである．bool型の計算力だけでなく，bool型の性 質もPropの性質より良い場合がある．例えば，bool 型は外延性を満たすが，Prop型は満たさない．さら に，bool型のおかげで，書き換えを使える機会が増

える(P /\ Qと異なり，andb P Q = trueはrewriteタ

クティクの対象になる; 6節を参照)．一方，Gallina

の含意関係->またはCoqが生成する帰納法は通常に

Prop型を用いて使う．Mathematical Componentsで

は，boolの利点を活かすようにPropとboolの間を，

行ったり来たりできるようになっている．その機能は，

small-scale reflectionと呼ばれ，Mathematical Com-ponentsの主な特徴である．Small-scale reflectionを

実現しているのは，Mathematical Componentsの専 用タクティク群_SSReflectである．次にラグラン ジュ定理の形式化でMathematical Componentsと SSReflectを説明する(具体的な_SSReflectの例 は6節を参照)．

3 本解説に関わる

Mathematical Components のファイル

現時点では，Mathematical Componentsライブラ リのファイルは約130個†2_{あるが，本解説で扱う有} 限群論の範囲で必要な次のファイルのみを紹介する: • ssreflect.ml4：OCaml言語で書かれた定理証明

支援系Coqの拡張．Mathematical Components

の開発において，Coqのタクティクを改善する 必要があり，その成果であるタクティク群を SS-Reflectと呼ぶ．そのタクティクの一部を紹介 する(例えば，6節のmove/)． • ssrbool.v: ブール型に関する補題等．2節で説明 したように，Mathematical Componentsでは， bool型を効率的に扱えるように，様々な工夫が なされている．これから紹介するリフレクション 補題の仕組みはこのファイルで設計されている †2 テストと旧ファイルを除いた 2016 年 9 月の開発版: https://github.com/math-comp/math-comp．

68 (例えば，6節のlcosetsP)． • finset.v: 有限集合の形式化．4節は有限集合の ライブラリの概要を説明する． • fingroup.v: 有限群の形式化．有限集合の形式化 に基づく．5節と6節で有限群の基本を紹介する． 10節で他のMathematical Componentsライブラ リも簡単に説明する．

4 有限集合の概要

Mathematical Componentsの有限群は有限集合を 用いて定義されている．本節では本解説で使う有限集 合の基本を説明する． Mathematical Componentsの元の目的は有限群論 であったため，有限集合のライブラリが充実している． そのライブラリで構成できる有限集合の要素の型は finType型に制限されている．finType型は，限られ た数の要素しか持たない型である．実際に数学の形式 化の際，finType型に当たるものが多い(例えば，行 列の指数)ため，Mathematical Componentsでは特 別扱いしている．例えば，bool型を持つ要素はtrue とfalseのみであり，finTypeとして使える．一方で， どう定義しても，自然数は無限であるため，finType 型にならない．finTypeの詳しい定義については，そ れを理解していなくてもMathematical Components を充分使えるので，本解説では省略する． T型を持つ要素の有限集合S0とS1は次のように 宣言できる: V a r i a b l e T : f i n T y p e . V a r i a b l e s S0 S1 : {set T} .

Variable/Variablesは仮定の宣言のためのCoqの命 令である．_{setT}はMathematical Componentsが 提供する記法である．ここでは詳しい定義を省略す る．一言で説明すると，TはfinType型であるので， {setT}は指示関数として考えれば良い． 有限集合を構成するため，Mathematical Compo-nentsは様々な定義を提供している．本解説では次の 定義を用いる: • 空集合はset0と書く．要素の型はコンテキスト から推論される． • 共通部分S0∩ S1はS0 : &: S1と書く．S0とS1 の要素の型は同じであることが求められている． • 写像fによる集合S0 の像(つまり，f (S0))は f @: S0と書く．fの型がT -> T’ならば，f @: S0 の型は_{setT’}となる． • 直 積 集 合 S0 × S1 は setX S0 S1 と 書 く．S0 とS1の型がそれぞれ{setT}と{setT’} なら ば，setX S0 S1は型{setT∗ T’}となる(ここで， T∗ T’はペアの型である)． 有限集合の基本的な性質は次の述語で記述できる： • S0の濃度は#|S0|と書く．自然数である． • 帰属関係a∈ S0はa \in S0と書く． • 真部分集合S0⊊ S1はS0 \proper S1と書く． • 部分集合S0⊆ S1はS0 \subset S1と書く． 以上の記法はLA_{TEXに似ているため覚えやすい．因} みに，2節で説明したように，Mathematical Com-ponentsでは，優先的にbool型を使うため，上記の 属する述語や部分集合述語などはProp型ではなく， bool型を持つ．

5 有限群の概要

本節では，Mathematical Componentsによる有限 群の基本的な宣言方法を説明する．6節，7節，8節 で，有限群に関する補題を用いて，ラグランジュ定理 の証明に必要な補題を証明する． 有限群は次のように宣言する: V a r i a b l e gT : f i n G r o u p T y p e . V a r i a b l e G : { group gT } . gTは群の元の型となる．finGroupTypeに属する型は 群の基本的な性質の一部を持つ．具体的に，二項演算 と単位元と逆元が定義して，結合法則と逆元の性質 を持つ(下記に記法を紹介する)．有限群そのものは {group gT}という型を持つ．基本的に，Gは単位元を 含む二項演算で閉じた有限集合である．以上の有限群 の二段階の定義は重要であるが，難しいので詳細を省 略する． 上記の宣言をすれば，群の定義に当たる基本的な要 素を確認できる: • 二項演算は関数mulgまたはそれに当たる∗記法 となる(ペアの型と同じ_∗記法であるが，型推論 により，多重定義による曖昧性は生じない)．例

Vol. 34 No. 2 May 2017 69 えば，gとhがGの元とする: V a r i a b l e s g h : gT . H y p o t h e s e s ( gG : g \in G ) ( hG : h \in G ) . (Hypothesesは述語のためのVariables命令であ る．伝統的に，述語の場合，Hypothesesを使う.) そうすると，g∗ hは型gTを持つ．Check命令で 確認できる: C h e c k g ∗ h : gT . g∗ hはGの元であることは補題groupMから得る: C h e c k g r o u p M gG hG : g ∗ h \in G . • 二項演算の結合法則は次の補題になる: L e m m a m u l g A : a s s o c i a t i v e m u l g .

associativeはMathematical Componentsで定 義された一般的な結合法則の定義である． • 単位元はoneg gTまたはそれに当たる1%g記法 となる．逆元はinvg gまたはそれに当たるgˆ-1 記法となる．単位元と逆元に関する補題を表1に 示す．8節で，その補題を具体例に用いる． Mathematical Componentsでは，有限群は有限集 合から定義され，4節で説明した述語をそのまま使え る．そのため，部分群の宣言は簡単になる．例えば， 上記のGの部分群Hは次のように宣言する: V a r i a b l e H : { group gT } . H y p o t h e s i s HG : H \subset G . 5. 1 剰余類 本解説では具体的な例として，ラグランジュ定理の 証明を行う．ラグランジュ定理は剰余類に関する定理 であり，Mathematical Componentsが提供する剰余 類を紹介する． Gを有限群とし，Hを部分集合とする．このとき， g∈ Gに対する左剰余類gH ={g ⋆ h | h ∈ H}に当 たる形式定義はlcoset H gまたはg ∗: Hと書く． 左剰余類の集合(G/H)lはlcosets H Gと書く．

6 左剰余類の共通の元はないこと

本節では有限群の簡単な補題を紹介する．具体的 に，剰余類は互いに共通の元をもたないことを示す． その際，Mathematical Componentsの基本的な専用 タクティクを紹介する． Gを 有 限 群 と し ，H を 部 分 群 と す る(宣 言 の や り 方 は5節 を 参 照)．L0と L1を2つ の 左 剰 余 類 と す る ．つ ま り，L0 \in lcosets H Gと 仮 定 す る (L1 も 同 様)．そ の 際 ，L0と L1 の 共 通 の 元 が あ れ ば(つ ま り，L0∩L1 ̸= ∅ の と き)，L0=L1が 成 り 立 つ ．以 上 の 言 明 を 次 の よ う に 記 述 で き る: L e m m a c o s e t _ d i s j o i n t L0 L1 : L0 \in l c o s e t s H G - > L1 \in l c o s e t s H G - > L0 : & : L1 ! = set0 - > L0 = L1 . 上記の補題の証明を次のタクティクで開始できる: c a s e/ l c o s e t s P = > g0 g0G - >{L0 } . 上記のスクリプトはMathematical Componentsの 専用タクティクで書いている．コンパクトな記述で あるため，説明のため細かく分けて説明する．実際 に，次のスクリプトは上記のタクティクと同じ意味を 持つ: 1 m o v e/ l c o s e t s P . 2 c a s e. 3 m o v e= > g0 . 4 m o v e= > g0G . 5 m o v e= > TMP . 6 r e w r i t e TMP . 7 r e w r i t e { TMP } . 8 r e w r i t e {L0 } . 専用タクティクで，スクリプトを短く記述できること はMathematical Componentsの1つの特徴である． 次に上記の長いスクリプトを説明する．図1は1と2 行目のタクティクの効果を表している． 1番目のタクティクはMathematical Components の専用タクティクmove/である．move/の右側は特別 な形を持つ補題でなければならない．許されている形 の1つはリフレクション補題と言う．リフレクション 補題の言明はreflect P bという形となる．reflect はMathematical Componentsで広く使われている 述語である．PはProp型を持ち，bはbool型を持つ． reflect P bは2節で説明したPとbの等価性を表す． 例えば，1番目で使われているlcosetsPはリフレク ション補題の一例である: l c o s e t s P : r e f l e c t

70 = = = = = = = = = = = = = = = = = = = =(ゴール 0) L0 \in l c o s e t s H G - > L1 \in l c o s e t s H G - > L0 : & : L1 ! = set0 - > L0 = L1 . move/lcosetsP.(1番目のタクティク) = = = = = = = = = = = = = = = = = = = =(ゴール 1) ( e x i s t s 2 g , g \in G & L0 = g ∗ : H ) -> L1 \in l c o s e t s H G - > L0 : & : L1 ! = set0 - > L0 = L1 . case. (2番目のタクティク) = = = = = = = = = = = = = = = = = = = =(ゴール 2) f o r a l l g , g \in G - > L0 = g ∗ : H -> L1 \in l c o s e t s H G - > L0 : & : L1 ! = set0 - > L0 = L1 . 図 1 左剰余類の共通の元はないこと： 形式証明の最初のステップ ( e x i s t s 2 g , g \in G & C = g ∗ : H ) ( C \in l c o s e t s H G ) move/lcosetsPの効果は図1で分かる．====の直下 にある仮定に対して，lcosetsPが表す等価性を適

用すると bool命題L0 \in lcosets H GはProp命題

exists2 g, g \in G & L0 = g ∗: Hに変わる．

Mathematical Componentsの専用タクティクはパ ラメータがなければ，====の直下にある仮定に適用さ れる．====の直下にある仮定をトップ仮定と呼ぶ． 2行目のタクティクはcaseである．トップ仮定が 帰納的型であるとき，場合分けを行う．例えば，図1 のゴール1のトップ仮定は(exists2 g, P g & Q g)の形 である．この仮定は帰納的型として定義されているた め，caseタクティクは場合分けを行う．その結果，P とQを満たす元gを取り出すことができ，gはゴール 2でforallで束縛される． 3行目から5行目までのmove=> ...タクティクは， トップ仮定に名前を付け，====の上(ローカルコンテ キストと言う)に保管する: g0 : gT g0G : g0 \in G TMP : L0 = g0 ∗ : H = = = = = = = = = = = = = = = = = = = = = = = = = = = = L1 \in l c o s e t s H G - > L0 : & : L1 ! = set0 - > L0 = L1 6と7行目のrewriteTMP.rewrite{TMP}.タクティ クは書き換えを行い，仮定を消す． 以上のような仮定の簡単な操作がよくあるが，深い 意味があるとは言えない．このような簡単な操作につ いては短く記述できるように，Mathematical Com-ponentsの専用タクティクが調整された．その結果， 本節の最初に出てきたcase/lcosetsP =>g0 g0G ->{L0} でまとめられる． 補題coset_disjointの完全な証明は[1]を参照され たい．この補題は7節での単射性の証明で用いる．

7 終域 (G/H)l

の単射

本節ではラグランジュ定理の証明で使う特別な関 数の単射性を証明する．その関数は，8節の部分群の 指数の推移関係の証明で重要な役割を果たす．その関 数はαと表記し，その終域を左剰余類の集合(G/H)l とする．定義域をGと表記し，群Gの部分集合とす る．関数αの定義は次のように記述する: α : G → (G/H)l : g7→ gH 関数αの定義域Gを集合(G/H)lの像として定義 する．そのため，Mathematical Componentsが用意 するrepr関数を使う．repr Xは集合Xの代表的な要 素を返す．従って，定義域_Gは次のように定義できる: D e f i n i t i o n r e p r s : = repr @ : l c o s e t s H G . (@:は4節で定義した像である.) 関数αは次の図で描 ける: repr L0 repr L1 repr Li L0 L1 Li reprs (紙上の記法: G) lcosets H G (紙上の記法: (G/H)l) 関数αの単射性の言明のため，Mathematical

Com-Vol. 34 No. 2 May 2017 71

ponentsの既存の定義を使う．関数f の単射性は injective fと書く．injectiveは5節のassociative

のようにMathematical Componentsが提供する一 般的な定義である．定義域を制限するため，記法

{in ... &, ...}を使う:

L e m m a i n j e c t i v e _ c o s e t : {in reprs & , i n j e c t i v e (fun x = > x ∗ : H ) } . Mathematical Componentsの定義を使うため，上記 の言明の記法に慣れていないと正確性を判断できな い．確認のため，証明を開始する．move=> /= g g’タク ティクを実行すると，ゴールは次のように展開される: g , g ’ : gT = = = = = = = = = = = = = = = = = = = = = = = = = = = = g \in r e p r s - > g ’ \in r e p r s - > g ∗ : H = g ’ ∗ : H -> g = g ’ 上記の/=記号はSSReflectのフラグと言い，move タクティクと組み合わせることができる．このフラグ によって，Gallinaの項のβ-簡約が求められる．ここ では必須ではないが，β-簡約によって型の表示が読み やすくなる．これで，確かに単射性の話をしているこ とが分かる． 次に証明のアイデアを説明する．上記のゴールのg とg’はreprsに属し，それぞれLとKの左剰余類の 代表的な要素である．L = Kを示すだけで，g = g’と 分かる．具体的なLとKを取り出すために，集合の 像に関するimsetPリフレクション補題を使う． その 補題はreflect述語を用いて集合の像の要素とその元 の関係を表す: y∈ f(D) ↔ ∃x, x ∈ D ∧ y = f(x)†3． ここでは，g \in reprsに適用すると，gに当たる元 の左剰余類を取り出せる．具体的には，次のタクティ クの実行により， m o v e/ imsetP = > / = . c a s e. m o v e= > L LHG gL . ゴールは次のように変わる: g , g ’ : gT L : {set gT} LHG : L \in l c o s e t s H G gL : g = repr L = = = = = = = = = = = = = = = = = = = = = = = = = = = = g ’ \in r e p r s - > †3 形式言明は 6 節の lcosetsP に近い． g ∗ : H = g ’ ∗ : H -> g = g ’ 証明を書き始めたが，定義を展開しただけなので，短 いスクリプトにまとめたい．6節と同じようなまとめ 方ができる: m o v e= > / = g g ’ / imsetP [ ] / = L LHG gL . 本解説では省略するが，左剰余類の性質(特に既に 6節で使ったリフレクション補題lcosetsP)とrepr関 数の性質を用いて，関数αの単射性の証明を完成で きる．更に，関数αは全射であることも証明できる ([1]を参照)．従って，Gと(G/H)l集合は同じ濃度 であることが分かる．

8 部分群の指数の推移関係

本節ではラグランジュ定理の主な補題を証明する． その補題は部分群の指数の推移関係という([4]の定 理V.3.1)．この証明には，7節で定義した関数αを 使う． 部分群の指数の推移関係は次の言明となる．G を有限群とし，HとKをGの部分群とする．但し， K⊊ H．そのとき，[G : K] = [G : H]×[H : K]． 部分群の指数の推移関係の言明の形式化は次のよ うに記述される: V a r i a b l e gT : f i n G r o u p T y p e . V a r i a b l e s G H K : { group gT } . H y p o t h e s e s ( HG : H \subset G ) ( KG : K \subset G ) ( HK : K \proper H ) . L e m m a i n d e x _ t r a n s : #| G : K | = #| G : H | ∗ #| H : K | . 形式証明を説明する前に，証明のアイデアを説明 する．まず，GとHを用いて，7節の関数αを用意 する．次に，HとKを用いて，同様の関数βを用意 する: β : H → (H/K)l : h7→ hK 7節で証明したように，αとβは全単射である．指数 の推移関係を証明するには，次の関数の全単射を証明 すれば充分である: ϕ : G × H → (G/K)l : (g, h)7→ (g ⋆ h)K 形式証明は上記のϕ関数の定義で始まる．関数ϕは

72 表 1 有限群に関する補題例 (G : {group gT}) 補題名 言明 mul1g 1 ∗ x = x mulg1 x ∗ 1 = x mulgA x ∗ (y ∗ z) = x ∗ y ∗ z mulgV x ∗ xˆ-1 = 1 mulVg xˆ-1∗ x = 1 invgK xˆ-1ˆ-1 = x

invMg (x∗ y)ˆ-1 = yˆ-1 ∗ xˆ-1 group1 1 \in G

groupV (xˆ-1 \in G) = (x \in G)

groupM x \in G -> y \in G -> x∗ y \in G

型gT∗ gTを持つペアghを受け取る(ここの_∗は直積 型である)．let: ... : = ... in構文を用いて，ペアgh それぞれの射影gとhを取り出し，集合(g∗ h) ∗: K を構成する(ここの_∗は群の二項演算である)．タク ティックposeでphiを定義する: p o s e phi : = fun gh : gT ∗ gT => let: ( g , h ) : = gh in ( g ∗ h ) ∗ : K . phi の 単 射 性 は 今 回 の 補 題 の 重 要 な ス テップ で あ る た め ，ス ク リ プ ト で 明 確 に す れ ば 良 い ．関 数αとβ の定義域_G と_{H (Coq} でcalG とcalH)

は既にあるとする．Mathematical Componentsの

専 用 タ ク ティックhave で 次 の サ ブ ゴ ー ル を 開 く: h a v e p h i _ i n j e c t i v e :

{in setX calG calH & , injective phi } .

(setXは4節の直積集合である．) ここからの証明の流れはテクニカルなので，最初の ステップだけを解説する．最初に，7節のように，単 射性の定義を展開し，G ×Hに属する(g, h)と(g′, h′) を得る．集合(g ⋆ h)Kと(g′⋆ h′)Kの等しさから (g′−1⋆ g ⋆ h)K = h′Kを証明する: = = = = = = = = = = = = = = = = = = = = = = = = = = = = ( g ∗ h ) ∗ : K = ( g ’ ∗ h ’ ) ∗ : K -> ( g ’ ˆ - 1 ∗ g ∗ h ) ∗ : K = h ’ ∗ : K つまり，トップ仮定の両方側に関数λX.g′−1Xを適 用 す る ．こ の た め に ，Mathematical Components で よ く 使 わ れ る イ ディオ ム が あ る ．タ ク ティック move/(congr1 ...)に適切な関数を渡す: m o v e/ ( congr1 (fun X = > g ’ ˆ - 1 ∗ : X ) ) . ここでのmove/タクティクは6節と同じである．但し， 今回リフレクション補題の代わりに通常の補題を使 い，トップ仮定を特化する． その結果，ゴールは次のように変わる: = = = = = = = = = = = = = = = = = = = = = = = = = = = = g ’ ˆ - 1 ∗ : ( ( g ∗ h ) ∗ : K ) = g ’ ˆ - 1 ∗ : ( ( g ’ ∗ h ’ ) ∗ : K ) -> ( g ’ ˆ - 1 ∗ g ∗ h ) ∗ : K = h ’ ∗ : K 今度，トップ仮定での ... ∗: (... ∗: ...) を (... ∗ ...) ∗: ... に 書 き 換 え る ．Mathematical Componentsで適 切 な 補 題 が あ りそ う な ので ，適 切なパターンを用いて検索を行う: S e a r c h _ ( _ ∗ : ( _ ∗ : _ ) ) . 検索の結果，補題lcosetMが見つかる: l c o s e t M : f o r a l l ( gT : f i n G r o u p T y p e ) ( A : {set gT}) ( x y : gT ) , ( x ∗ y ) ∗ : A = x ∗ : ( y ∗ : A ) 今回，補題lcosetMを用いて書き換えを右から左へ 2回行う．そのため，書き換えタクティクに逆向きの -フラグと2回繰り返しの2!フラグを設定する: r e w r i t e - 2 ! l c o s e t M . その書き換えの結果，ゴールは次のように変わる: = = = = = = = = = = = = = = = = = = = = = = = = = = = = ( g ’ ˆ - 1 ∗ ( g ∗ h ) ) ∗ : K = ( g ’ ˆ - 1 ∗ ( g ’ ∗ h ’ ) ) ∗ : K -> ( g ’ ˆ - 1 ∗ g ∗ h ) ∗ : K = h ’ ∗ : K 今度，g’ˆ-1∗ (g’ ∗ h’)をh’に書き換える．そのため， 表1の補題を使う．群の結合法則，逆元と単位元の性 質の書き換えを次のように行う:

r e w r i t e 2 ! mulgA mulVg mul1g .

その結果，ゴールは次のようになる: = = = = = = = = = = = = = = = = = = = = = = = = = = = = ( g ’ ˆ - 1 ∗ g ∗ h ) ∗ : K = h ’ ∗ : K -> ( g ’ ˆ - 1 ∗ g ∗ h ) ∗ : K = h ’ ∗ : K これは，自動的に証明できる．実際には，上記の2 つの書き換えタクティクを1行でまとめることがで きる:

by r e w r i t e - 2 ! l c o s e t M ! mulgA mulVg mul1g .

Vol. 34 No. 2 May 2017 73 ステップは短く記述できる．

9 ラグランジュ定理の形式証明

以上の準備を用いて，ラグランジュ定理の証明を記 述できるようになった．紙上のラグランジュ定理の言 明を1. 1節で述べた．その形式記述を，以上で説明 したMathematical Componentsのライブラリを用 いて，次のように記述する: V a r i a b l e gT : f i n G r o u p T y p e . V a r i a b l e s G H : { group gT } . H y p o t h e s i s HG : H \subset G . T h e o r e m L a g r a n g e : #| G | = #| H | ∗ #| G : H | . ラグランジュ定理は部分群の指数の推移関係の系で ある．{1} ⊊ Hの場合，8節の部分群の指数の推移 関係の部分群Kを群{1}にすると，ラグランジュ定 理の証明ができる．H ={1}の場合，左剰余類は単 集合となり，_{|G| = |(G/H)}l|である．従って，ラグ ランジュ定理が成り立つ． 以上のリーズニングの形 式化に関しては文献[1]を参照されたい．

10 その他の Mathematical Components

ライブラリの紹介

本解説では，有限群に関するライブラリを紹介した が，Mathematical Componentsの一部だけである． 今回紹介できなかったが，数学の形式化の際，よく使 われるライブラリの中には次のものもある: • tuple.v: 固定長のリストの形式化． • finfun.v: 有限の定義域を持つ関数．固定長の リストから得る．グラフとして考えられるので， Coqの関数と異なり，外延性を満たすので，数学 で使われている関数に近い．実際に，有限集合の 基になる: 4節の指示関数は有限の定義域を持つ． • bigop.v:

∑

や

∏

等の一般的な反復演算子の形 式化である．奇数位数定理の成功に不可欠だっ た．組合せ論の形式化に必要である． また，Mathematical Componentsには代数の基本 が揃っている: • ssralg.v: 代数的構造(環や体等)のヒエラルキー の形式化． • poly.v/polydiv.v: 多項式の形式化．多項式は ssralg.vで定義されている環の構造を持つ． • matrix.v: 行列の形式化．有限の定義域を持つ 関数として定義されている．行列の環構造は ssralg.vから導ける．線形代数の基礎になる． 奇数位数定理の実験ファイルはまだ別にある[6]．

11 結論

本解説で数学の形式化のためのライブラリ Mathe-matical Componentsを紹介した．具体的な例として ラグランジュ定理の形式化を行った．その際，

Mathe-matical Componentsの専用タクティク_SSReflect を紹介した．省いた詳細は全体の証明スクリプトで確 認できる[1]． Mathematical Componentsのおかげで，数学の 形式化の研究が大きく進んだ．現在，様々な研究が Mathematical Componentsに基づいている．例え ば，著者は情報理論と符号理論の形式化のプロジェ クトに参加している[3]．Mathematical Components の専用タクティク_SSReflectも形式証明の記述に 大きな影響を与えた．数学の形式化だけでなく，ソフ トウェアの検証でも使われ，HOL Lightという定理 証明支援系にも移植されている． 謝辞 多くのコメントをいただいた才川隆文さん， 磯部祥尚さん，匿名の査読者に感謝します． 参 考 文 献

[ 1 ] Affeldt, R.: Mathematical Components を 用 い た ラ グ ラ ン ジュ定 理 の 形 式 化. 証 明 ス ク リ プ ト, https://github.com/affeldt/mathcomp-intro [ 2 ] アフェルト レナルド: 定理証明支援系に基づく形

式検証—近年の実例の紹介と Coq 入門—, 情報処理, Vol. 55 (2014), pp. 482-491.

[ 3 ] Affeldt, R., Garrigue, J.: Formalization of Error-correcting Codes: from Hamming to Modern Cod-ing Theory, in Proc. ITP 2015, LNCS, Vol. 9236, Springer, pp. 17–33.

[ 4 ] Arnaudi`es, J. M. and Fraysse, H.: Cours de math´ematiques 1, Alg`ebre, Dunod Universit´e, 1987. [ 5 ] The Coq Proof-assistant, http://coq.inria.fr.

IN-RIA, 1984–2016.

[ 6 ] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Ould Biha, S., Pasca, P., Rideau, L.,

74

Solovyev, A., Tassi, E. and Th´ery, L.: A Machine-Checked Proof of the Odd Order Theorem, in Proc.

ITP 2013, LNCS, Vol. 7998, Springer, pp. 163–179.

AFFELDT Reynald 2004年東京大学大学院情報理工科 学研究科・コンピュータ科学専攻博 士課程修了．現在，産業技術総合研 究所・情報技術研究部門・サイバー フィジカルウェア研究グループ主任研究員．定理証明 支援系Coqを用いて，安全なソフトウェアの構築方 法を研究している．セキュリティプロトコルや情報・ 符号理論やロボット工学への応用を目標として，アセ ンブリやC言語などの低レベルのプログラムの形式 検証と安全性用の数学の形式化を研究している．