Coq でモジュラー束

この記事は LL/ML Advent Calendar の 23 日目です。

「タイトルに "LL" もしくは "ML" を含むこと」という謎ルールに従い、「群の正規部分群の全体がモジュラー束 (Modular Lattices) をなすこと」を Coq により証明してみました。なお、完全なコードは http://gist.github.com/4359976 に置いてあります。

モジュラー束を表す型クラス

数学的な定義をいちいち説明するのもアレなので wikipedia:束_(代数学) を参照。モジュラー束は分配束の条件を若干緩めたもので、今回の例は「分配性を満たさないがモジュラー性なら満たす」ような例になっています。問題はどうやって Coq で書くかですが、ちょうど Coq で群を扱う記事 Group on Setoid を見かけたので、今回はこの方を真似して「型クラス + Setoid」で書いてみました。

まずモジュラー性を要求しない、通常の束はこんな感じ。Wikipedia の表現で言えば、sup が「結び」、inf が「交わり」ですね。台となる型 L は同値関係 eq によって Setoid にする予定なので、well-definedness (L_sup_mor、L_inf_mor) も忘れずに入れておきます。ちなみに POSet は部分順序集合の型クラスです。

Class Lattice (L : Type) (eq : L -> L -> Prop)
              (le : L -> L -> Prop)
              (sup : L -> L -> L) (inf : L -> L -> L) := {
    L_POSset :>
        POSet L eq le;
    L_sup_mor :
        forall x x' : L, eq x x' ->
        forall y y' : L, eq y y' ->
        eq (sup x y) (sup x' y');
    L_inf_mor :
        forall x x' : L, eq x x' ->
        forall y y' : L, eq y y' ->
        eq (inf x y) (inf x' y');
    L_sup_l :
        forall x y : L,
        le x (sup x y);
    L_sup_r :
        forall x y : L,
        le y (sup x y);
    L_sup_min :
        forall x y z : L,
        le x z -> le y z -> le (sup x y) z;
    L_inf_l :
        forall x y : L,
        le (inf x y) x;
    L_inf_r :
        forall x y : L,
        le (inf x y) y;
    L_inf_max :
        forall x y z : L,
        le z x -> le z y -> le z (inf x y)
}.

さらにそのサブクラスとしてモジュラー束を定義します。

Class ModularLattice (L : Type) (eq : L -> L -> Prop)
                     (le : L -> L -> Prop)
                     (sup : L -> L -> L) (inf : L -> L -> L) := {
    ML_Lattice :>
        Lattice L eq le sup inf;
    ML_mod :
        forall x y z : L,
        le x z -> eq (sup x (inf y z)) (inf (sup x y) z)
}.

これで、示したい結論は「群の正規部分群の全体は、型クラス ModularLattice のインスタンスとなること」と表現できました。さて、次の問題は「正規部分群」をどう書くか、です。

正規部分群を表す型クラス

まず前提として、G を群の型クラス Group のインスタンスにしておきます。台 G の上に同値関係 Geq が入っていて、Gop、Gunit、Ginv がそれぞれ群としての演算、単位元、逆元になっています。

Variable G : Type.
Variable Geq : G -> G -> Prop.
Variable Gop : G -> G -> G.
Variable Gunit : G.
Variable Ginv : G -> G.
Hypothesis G_Group : Group G Geq Gop Gunit Ginv.

さらにここで忘れちゃいけないのが、Gop、Ginv が Setoid としての Morphism になるということを Add Prametric Morphism で Coq に教えておくこと。面倒ですが、これをやっておかないと Setoid に対して rewrite タクティクが機能しません。

埋め込みによる方法

真っ先に思いつくのは、G の部分群 H を「群 H と H から G への単射準同型の組」として定義する方法です。しかし、最終的には G の正規部分群たちに同値関係を入れて Setoid にする必要があったことを思い出しましょう。この埋め込みによる方法では、「二つの部分群が等しい」と書きたいときにハマる予感がします。という訳でこの方針は却下。

特性関数による方法

そこで今回は、集合を型として直接扱うのではなく、それを表現する論理式と同一視して扱う方針を取ってみました。つまり、「G の元 x が正規部分群 N に属する」という述語 G -> Prop たちの全体にモジュラー束としての構造を入れます。

以下が対応する型クラスです。G が Setoid なので、同値関係 Geq に対する well-definedness (SS_mor) も忘れずに要求しておきます。正規部分群の定義については wikipedia:正規部分群 あたりをよろしく。

Class Subsetoid {X : Type} {eq : X -> X -> Prop}
                (S : X -> Prop) := {
    SS_mor :
        forall x x' : X,
        eq x x' -> (S x <-> S x')
}.

Class Subgroup {G : Type} {eq : G -> G -> Prop}
               {op : G -> G -> G} {unit : G} {inv : G -> G}
               (H : G -> Prop) := {
    SG_outer_Group :>
        Group G eq op unit inv;
    SG_Subsetoid :>
        @Subsetoid G eq H; 
    SG_unit_in :
        H unit;
    SG_op_clo :
        forall x y : G,
        H x -> H y -> H (op x y);
    SG_inv_clo :
        forall x : G,
        H x -> H (inv x)
}.

Class NormalSubgroup  {G : Type} {eq : G -> G -> Prop}
                      {op : G -> G -> G} {unit : G} {inv : G -> G}
                      (H : G -> Prop) := {
    NSG_Subgroup :>
        @Subgroup G eq op unit inv H;
    NSG_normal :
        forall x y : G,
        H x -> H (op (op y x) (inv y))
}.

ちなみに今回の証明には幸い登場しませんが、「x は N に属さない」という主張が必要になるとこの方針では詰むかもしれません。

束としての構造

さて、とりあえず準備はできました。最終的な台集合となる G の正規部分集合の全体 NSG を、依存積を使って書いておきます。

Definition CF : Type := G -> Prop.

Definition NSG : Type :=
    {N : CF | @NormalSubgroup G Geq Gop Gunit Ginv N}.

NSG 上の順序 NSGle は集合としての包含関係、交わり NSGinf は共通部分をとればよいのですが、注意が必要なのは結び NSGsup の定義。前述の Wikipedia には書いてありませんが、今回欲しかった「モジュラー束だが分配束にならない」例を作るためには、以下を用いて結びを定義する必要があります。

Definition CFprod (S1 S2 : CF) : CF :=
    fun x => exists s1 : G, exists s2 : G,
             S1 s1 /\ S2 s2 /\ x |=| s1 |*| s2.

直感的に言えば、「S1 の元と S2 の元の積の全体」が CFprod S2 S2 ですね。これに正規性の証明を付け加えたものが NSGsup になります。正規部分群の結びが再び正規部分群になる、という部分が今回の証明中で最も重い部分でしょうか。難しいわけではないのですが、書き換えが多くて手数が掛かります。

後は証明するだけ。やっていることは基本的に正規部分群としての性質を使った書き換えのみです。先にも触れましたが、最終的な結論はコードの一番最後で登場する以下の一文です。

Instance NSG_ModularLattice : ModularLattice NSG NSGeq NSGle
                                             NSGsup NSGinf.

その他補足

我ながら駆け足過ぎますね。しかしまあ Advent Calendar 担当者としての義務は果たしたのでよしとしましょう。もしよかったら実際のコードも覗いてやって下さい。

ちなみに題材自体に特に深い意味はなく、頭文字が ML になるからというだけの話です。当初は、分配束の型クラスを作って「分配束ならばモジュラー束」を証明するというプランもあったのですが、今考えるとそっちの方がよかったかもしれません。

また、束に関する面白い性質として、今回のような順序による定義の他、結びと交わりを先に与えることによっても結果的に同じものを定義することができます。この点についても Coq で書いた証明があるのですが、それはまた別の話。