Coqで定理を記述してみる、型クラスとか使って - 檜山正幸のキマイラ飼育記 (はてなBlog)

Coqの証明スキルが全然身につきません。ダメです。それで、証明はともかくとして、定理の記述方法を試行錯誤してました。短くて抽象度が高くて読みやすい記述はどんなものだろう？と。型クラスを使うのがよろしいようです。

内容：

例題：ミート半束と順序集合
ミート半束を定義する、マグマだけ
ノーテーション定義で読み書きを楽にする
ミート半束を定義する、満たすべき法則も
順序集合を定義する
ミート半束から順序集合を作り出す
ソースコード

例題：ミート半束と順序集合

今回の例題は、「ミート半束は（最大元付きの）順序集合とみなせる」という主張です。

[追記]このエントリーを最初に書いたとき、最大元と最小元を取り違えていました。最大元（トップ）とすべき所を最小元（ボトム）としていたのです。直しました。[/追記]

ミート半束というのは、ミート演算∧を備えた集合です。ミート演算には単位元があるのでそれをι（ギリシャ文字イオタ）とします -- イチに形が似ているので。ミート半束をちゃんと定義しましょう。Mが集合、∧が M×M→M という写像、ι∈M だとして、次が成立するとき、三つ組 (M, ∧, ι) をミート半束（meet semilattice）といいます。

ミートの結合律： x∧(y∧z) = (x∧y)∧z;
ミートの左単位律：ι∧x = x;
ミートの右単位律：x∧ι = x;
ミートの可換律： x∧y = y∧x;
ミートのベキ等律：x∧x = x

ここで、x, y, zは集合Mの要素と仮定しています。ミート半束は、可換モノイドに演算のベキ等性を加えたものですね。

次に順序集合。ここでは、最大元を持つ順序集合を単に順序集合と呼ぶことにします。Qが集合、≦がQ上の二項関係、T∈Q として、次が成立するとき、三つ組 (Q, ≦, T) を（最大元を持つ）順序集合（ordered set with {greatest element, maximum, top}）といいます。

順序の反射律： x≦x;
順序の推移律： x≦y かつ y≦z ならば x≦z;
順序の反対称律： x≦y かつ y≦x ならば x = y;
順序の最大元（トップ）： x≦T

ミート半束 (M, ∧, ι) があるとき、

台集合QはMと同じ
x ≦ y とは x∧y = x であること
Tはιのこと

と定義すると、(M, ∧, ι) から (Q, ≦, T) が作れて、この (Q, ≦, T) は最大元を持つ順序集合となります。この事実の証明は人間にとっては簡単だと思います。で、Coqにやらせようと思ったわけです。

ミート半束を定義する、マグマだけ

ミート半束のような代数構造をどう定義するのが良いのか、あんまり分かってないのですが、まーまー使える方法を紹介します。この方法には課題があることを注意しておきます。今回の目的ではうまくいきますが、より大規模な記述にはもっと効率的な方法が必要かも知れません。

とりあえずは、満たすべき法則（結合律、左単位律、右単位律、可換律、ベキ等律）は後回しにして、集合の上に二項演算が載っているだけの構造を考えます。

集合とその上の二項演算の組はマグマと呼ばれます。二項演算に何の法則性も要求しません。マグマという言葉を少し拡張解釈して、法則性を持たない素材だけの構造を一般にマグマと呼ぶことにします。素材とは、集合、演算、特定の要素、関係などです。

ミート半束から法則を除いたミートマグマの場合は、「台集合、二項演算、特定の要素」がその構成要素です。このことをCoqの型クラスを使って次のように表現してみました。

Class MeetMagma := 
  {
    meet_carrier: Set;
    meet_operation: meet_carrier -> meet_carrier -> meet_carrier;
    meet_unit: meet_carrier
  }.

ミート二項演算（meet_operation）は、台集合（meet_carrier）上の二項演算なので、meet_carrier × meet_carrier → meet_carrier という写像ですが、カリー化して、meet_carrier → (meet_carrier → meet_carrier) にしています。カリー化をベースにした関数型言語では普通の記述です。

meet_carrier, meet_operation, meet_unit という名前とその型の組合せは、指標（signature）だと考えられます。ミートマグマは、ミート指標を持つ構造（指標のモデル）です。まだ法則性はない状態です。それらミートマグマの全体からなるクラス（構造の集まり）がミートマグマ・クラスであり、Class MeetMagma として宣言されています。

ミートマグマ・クラスのインスタンスを一つ作ってみます。trueとfalseからなる集合boolはCoqで事前に定義されていますが、これがミートマグマの具体例になります。

Instance boolMeetMagma : MeetMagma :=
  {
    meet_carrier := bool;
    meet_operation := andb;
    meet_unit := true
  }.

このインスタンス定義の内容は：

台集合はboolとする。（bool = {true, false}）
ミート演算は andb: bool -> bool -> bool とするる。andbはブール値のAND演算。
ミート演算の単位はtrueとする。

こうやって作った特定のミートマグマにboolMeetMagmaという名前を付けているわけです。当たり前ですが、boolMeetMagmaはMeetMagmaクラスのインスタンスです、そう宣言したのですからね。この当たり前は、Coqによって保証されます。クラスのインスタンスとして不適切な定義をするとハネられます。

例えば、次の定義では「1」が間違っています。

Instance boolMeetMagma : MeetMagma :=
  {
    meet_carrier := bool;
    meet_operation := andb;
    meet_unit := 1
  }.

次のように言われます。

Error: The term "1" has type "nat" while it is expected to have type "bool".

まだ法則性は要求されてないので、次のインスタンス定義は大丈夫（ハネられない）です。

Instance natMeetMagma : MeetMagma :=
  {
    meet_carrier := nat;
    meet_operation := plus;
    meet_unit := 0
  }.

nat（自然数）の足し算はベキ等律を満たしませんが、まだベキ等律は定義してません。

ノーテーション定義で読み書きを楽にする

Coqには、簡潔で見慣れた記法をサポートするためにノーテーション定義の機能があります。名前に別名を与えたり、関数適用を中置記法／後置記法で書けるようにします。

Notation M := meet_carrier.
Notation "x ∧ y" := (meet_operation x y) (at level 40, left associativity).
Notation ι := meet_unit.

このように定義すると、Mはmeet_carrierの別名に、ιはmeet_unitの別名に、そして中置記法 x ∧ y は (meet_operation x y) に展開されます。レベル（優先度）の数値は https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Notations.html を参考に決めました。meet_carrierの別名にMという一文字を使うのはリスキーですが、分かりやすいので使いました。他にも（後で）一文字の別名を使っていますが、おすすめできる行為ではありません。

Coqのノーテーションは、実行中にパーザーをカスタマイズできる機能であって、それ以上のものではありません。構文的マクロとしてはなかなかに賢いのですが、意味的処理は何もしてません。

ノーテーションの解釈・展開を、特定の文脈（スコープ）に限定できるようですが（やったことない）、スコープを指定しないと大域的にどこでも展開されます。Coq自身が使っている重要な記号をノーテーション定義で上書きすると酷いことになります。実は、リストのconsを意味する「::」を「;」（セミコロン）にしたことがあって、パーザーが壊れてしまったような挙動になりました。

というわけで、ノーテーション機能は純粋にシンタックスシュガー用途ですが、うまく使うと読み書きが劇的に楽になります。

ミート半束を定義する、満たすべき法則も

ミート半束の法則は、ミートマグマとは別なクラスとして定義してみます。

Class MeetSemiLattice (MM: MeetMagma) :=
  {
    meet_associative: forall(x y z: M), x∧(y∧z) = (x∧y)∧z;
    meet_unit_left: forall(x: M), ι∧x = x;
    meet_unit_right: forall(x: M), x∧ι = x;
    meet_commutative: forall(x y: M), x∧y = y∧x;
    meet_idempotent: forall(x: M), x∧x = x
  }.

ノーテーション定義により、ほとんど普通の書き方で記述できます。キーワードforallを∀で置き換えることもできますが、今回はやっていません((Require Import Utf8_core. すると、∀もλも使えるようになります。しかし、Utf8_coreでは、∧が命題の論理ANDに割り当てられているので、Notation "x ∧ y" := (meet_operation x y) (at level 40, left associativity). すると、エラーになります。))。

さて、普通の書き方で法則を書き並べると、それでミート半束が定義されるのか？どうやら定義されているようなのです。概念としてのミート半束が、このMeetSemiLatticeクラスで表現されたと言っていいでしょう。

ミート半束のインスタンスを生成してみます。概念としてのミート半束クラスではなくて、具体例な実物としてのミート半束を作るのです。次のようにします。

Instance boolMeetSemiLattice : MeetSemiLattice boolMeetMagma.

ミート半束インスタンスは、先ほど定義したミートマグマのインスタンであるboolMeetMagmaを土台に作ります。MeetSemiLatticeクラスに、ミートマグマのインスタンスを実引数として渡すと土台の具体化は完了します。土台だけではミート半束ではありません。5つの法則も具体化が必要です。

法則の具体化とは何でしょうか。これは、法則の証明なんですよ。Coqのなかでは、証明は証明オブジェクトと呼ばれる具体的データ（pCic項）なんです。法則、例えば結合律の記述である命題は型でした。だから、型の制約を満たして具体値を割り当てることが、命題の証明オブジェクトを指定することになるわけです。

よって、ミート半束インスタンスの構成には次のステップを踏むことになります。

土台となる具体的なミートマグマの提供
そのミートマグマがミート半束としての法則を満たしていることの証明の提供

土台となる具体的なミートマグマは既にboolMeetMagmaとして作っておいたのでいいのですが、Instance boolMeetSemiLattice : MeetSemiLattice boolMeetMagma. の段階で、Coqが証明編集モードに入って、「はよ証明せい」と言います（言ってるような気がします）。

僕は心の準備が出来てなかったので、いったん証明モードを中断して（Abortコマンド）、状況を再確認。SearchAbout bool. で調べると、初期状態ではboolに関する定理があまり準備されてないようです。Require Import Bool.すると、いくつかの定理が追加されます。

andb_assoc, andb_true_l, andb_true_r, andb_comm がそれぞれ、andb演算の結合律、左単位律、右単位律、可換律です（https://coq.inria.fr/library/Coq.Bool.Bool.html）。ベキ等律だけは自前で証明することにします。

Require Import Bool.

Lemma andb_idempotent: forall(x: bool), x && x = x.
Proof.
 intros.
 induction x.
 trivial.
 trivial.
Qed.

boolMeetMagmaに対して証明すべき命題は、これで定理として準備できました。それらを列挙しておくと：

andb_assoc: forall(x y z: bool), x && (y && z) = (x && y) && z
andb_true_l: forall(x: bool), true && x = x
andb_true_r: forall(x: bool), x && true = x
andb_comm: forall(x y: bool), x && y = y && x
andb_idempotent: forall(x: bool), x && x = x

今度は「はよ証明せい」と言われても大丈夫です。

Instance boolMeetSemiLattice : MeetSemiLattice boolMeetMagma.
Proof.
 split.
 intros; apply andb_assoc.
 intros; apply andb_true_l.
 intros; apply andb_true_r.
 intros; apply andb_comm.
 intros; apply andb_idempotent.
Qed.

「マグマを定義するクラス」と「法則だけを記述するクラス」に分けるやり方は、インスティチューションを意識しています。Σを指標とするとき、インスティチューションではモデル圏Mod[Σ]を定義しますが、Coqの型クラスとしてのΣマグマクラスは、モデル圏 Mod[Σ]の対象類 |Mod[Σ]| = Obj(Mod[Σ]) に対応します。

指標Σの論理式の集合Sen[Σ]の部分集合Aを公理として特定したとき、Aを満たすモデルの全体は|Mod[Σ]|の部分類を定義します。公理系Aを記述したCoqの型クラスが、構造の法則クラスです。法則クラスは、マグマクラスで定義した対象（モデル圏の対象）を絞り込む目的で使うので、|Mod[Σ]|上の述語の形をしています。

順序集合を定義する

順序集合の定義も、ミート半束の場合と同じです。次の手順に従います。

順序集合のマグマ版OrderMagmaを定義する。
記述の簡略化のためにノーテーション（Q、≦、T）を定義する。
順序集合が満たすべき法則を記述したクラスOrderを定義する。

以下のようになります。

Class OrderMagma :=
  {
    order_carrier: Set;
    order_relation: order_carrier -> order_carrier -> Prop;
    order_top: order_carrier
  }.

Instance boolOrderMagma : OrderMagma :=
  {
    order_carrier := bool;
    order_relation := leb;
    order_top := true
  }.

Notation Q := order_carrier.
Notation "x ≦ y" := (order_relation x y) (at level 70, no associativity).
Notation T := order_top.

Class Order (OM: OrderMagma) :=
  {
    order_reflexive: forall(x: Q), x≦x;
    order_transitive: forall(x y z: Q), x≦y -> y≦z -> x≦z;
    order_antisymmetry: forall(x y: Q), x≦y -> y≦x -> x = y;
    order_minimum: forall(x: Q), x≦T
  }.

OrderMagmaクラスのインスタンスであるboolOrderMagmaも作りました。この具体的なマグマを、法則を記述したクラスOrderに渡してインスタンス化すれば、Orederクラスのインスタンス（つまり、具体的な順序集合）が出来るはずです。

Instance boolOrder : Order boolOrderMagma.

この段階で次の命題を証明しなくてはなりません。

bool_reflexive: forall(x: bool), leb x x;
bool_transitive: forall(x y z: bool), leb x y -> leb y z -> leb x z;
bool_antisymmetry: forall(x y: bool), leb x y -> leb y x -> x = y;
bool_minimum: forall(x: bool), leb false x

また中断して、補題（定理）を準備します。

Lemma bool_reflexive: forall(x: bool), (leb x x).
Proof.
 intros.
 induction x.
 apply leb_implb.
 compute.
 trivial.
 apply leb_implb.
 compute.
 trivial.
Qed.

なんかめんどくさいな。場合分けして調べればいいはずだけど、bool_transitiveとか場合が多い。これは後回しにして先に進もう、と。

ミート半束から順序集合を作り出す

最初の例題に戻って、今、具体的なミート半束 (M, ∧, ι) が与えられたとして、次の手順で（最大元を持つ）順序集合 (Q, ≦, T) が作れるのでした。

台集合QはMと同じ
x ≦ y とは x∧y = x であること
Tはιのこと

この構成法には、ミート半束／順序集合の法則は無関係で、マグマのレベルの操作です。つまり、与えられたミートマグマから順序集合マグマを構成すればいいので、MeetMagma → OrderMagma という関数を定義すればいいことになります。

その関数MeetToOrderは次のように定義します。

Definition MeetToOrder (MM: MeetMagma) : OrderMagma :=
  {|
    order_carrier := M;
    order_relation := fun(x y: M)=> (x∧y = x);
    order_top := ι
  |}.

Eval compute in MeetToOrder boolMeetMagma. で評価してみると、評価結果は次のようになります：

     = {|
       order_carrier := bool;
       order_relation := fun x y : bool => (if x then y else false) = x;
       order_top := true |}
     : OrderMagma

MeetToOrder関数を使うと、「ミート半束は（最大元付きの）順序集合とみなせる」ことは次のように言えます。

MMは任意に与えられたミートマグマ（のインスタンス）だとする。
もし、ミートマグマMMがミート半束であるならば、
MMをMeetToOrder関数で変換した結果 (MeetToOrder MM) は、
単なる順序集合マグマではなくて実際に順序集合である。

この記述をそのままCoqの定理にすると：

Theorem meetSemiLattice_is_order: 
  forall(MM: MeetMagma), 
    (MeetSemiLattice MM) -> Order (MeetToOrder MM).

たぶんこれが「ミート半束は（最大元付きの）順序集合とみなせる」の機械可読形式になっていると思います。えっ？証明。もう力尽きました。

ソースコード

(* -*- coding: utf-8 -*- *)

Class MeetMagma := 
  {
    meet_carrier: Set;
    meet_operation: meet_carrier -> meet_carrier -> meet_carrier;
    meet_unit: meet_carrier
  }.

SearchAbout bool.

Instance boolMeetMagma : MeetMagma :=
  {
    meet_carrier := bool;
    meet_operation := andb;
    meet_unit := true
  }.

Instance natMeetMagma : MeetMagma :=
  {
    meet_carrier := nat;
    meet_operation := plus;
    meet_unit := 0
  }.


(* 参考： https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Notations.html *)
Notation M := meet_carrier.
Notation "x ∧ y" := (meet_operation x y) (at level 40, left associativity).
Notation ι := meet_unit.

Class MeetSemiLattice (MM: MeetMagma) :=
  {
    meet_associative: forall(x y z: M), x∧(y∧z) = (x∧y)∧z;
    meet_unit_left: forall(x: M), ι∧x = x;
    meet_unit_right: forall(x: M), x∧ι = x;
    meet_commutative: forall(x y: M), x∧y = y∧x;
    meet_idempotent: forall(x: M), x∧x = x
  }.

Require Import Bool.
(* 参考： https://coq.inria.fr/library/Coq.Bool.Bool.html 
  andb_assoc
  andb_true_l 
  andb_true_r
  andb_comm 
*)

Lemma andb_idempotent: forall(x: bool), x && x = x.
Proof.
 intros.
 induction x.
 trivial.
 trivial.
Qed.

Instance boolMeetSemiLattice : MeetSemiLattice boolMeetMagma.
Proof.
 split.
 intros; apply andb_assoc.
 intros; apply andb_true_l.
 intros; apply andb_true_r.
 intros; apply andb_comm.
 intros; apply andb_idempotent.
Qed.

Class OrderMagma :=
  {
    order_carrier: Set;
    order_relation: order_carrier -> order_carrier -> Prop;
    order_top: order_carrier
  }.

Instance boolOrderMagma : OrderMagma :=
  {
    order_carrier := bool;
    order_relation := leb;
    order_top := true
  }.

Notation Q := order_carrier.
Notation "x ≦ y" := (order_relation x y) (at level 70, no associativity).
Notation T := order_top.

Class Order (OM: OrderMagma) :=
  {
    order_reflexive: forall(x: Q), x≦x;
    order_transitive: forall(x y z: Q), x≦y -> y≦z -> x≦z;
    order_antisymmetry: forall(x y: Q), x≦y -> y≦x -> x = y;
    order_minimum: forall(x: Q), x≦T
  }.

Lemma bool_reflexive: forall(x: bool), (leb x x).
Proof.
 intros.
 induction x.
 apply leb_implb.
 compute.
 trivial.
 apply leb_implb.
 compute.
 trivial.
Qed.

Instance boolOrder : Order boolOrderMagma.
Abort.

Definition MeetToOrder (MM: MeetMagma) : OrderMagma :=
  {|
    order_carrier := M;
    order_relation := fun(x y: M)=> (x∧y = x);
    order_top := ι
  |}.

Eval compute in MeetToOrder boolMeetMagma.

Theorem meetSemiLattice_is_order: 
  forall(MM: MeetMagma), 
    (MeetSemiLattice MM) -> (Order (MeetToOrder MM)).
Abort.