代数的構造と Coq:序

「『タイトルは可能な限り誇張するといいよ』って言われました」だそうです。

1 この記事は、

  1. Theorem Prover Advent Calendar 2014 の 20 日目の記事です。
  2. Coq の Structure とか Class を使って、群を定義していきます。
  3. 二通りの構成法を扱い、後にそれらの間の関係も示します。
  4. 準同型はあとで。
  5. 載っているコードはそのまま coqc 出来ます。コードを抽出したものは こちら
  6. Coq のことを少し知っていればなんとなくわかるかもしれません。

1.2 流れとか

Coq の Structure とか Class の使い方の一例を示す、という建前で Setoid から話を広げて群を作ることにしました。 Wikipedia の Magma のページ の六角形がかっこよかったので、マグマから始めて二通りの方法で群を構成します。

以降の流れは、

  1. マグマを定義(Structure)
  2. マグマの性質を記述(Class)
  3. 群を作るその1
  4. 群を作るその2
  5. 同じものだよと述べる

となっております。

2 マグマ

集合 \(M\) と二項演算子 \(\bullet: M\times M \rightarrow M\) の組 \(\langle M,\bullet \rangle\) を、 マグマとか亜群(groupoid)とか呼びます。

二項演算子に色々な性質を付加した代数構造は多々ありますが、その大元になっている構造です。

ここでは、 Setoid と Setoid 上の二項演算子で以ってマグマを定義します。

2.1 準備

引数の暗黙性を設定したりクォートを自由に使えるようにしたりしています。 Generalizable All Variables コマンドについては ここ を参照のこと。 ざっくり言うと、シングルクォートで囲まれた中では可能なら初出でも変数名の型を推論するよ、というもの。 大抵、推論の対象になる変数名をあらかじめ指定しておきますが、 All を付けて全ての変数を対象にすることも可能。

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable All Variables.

Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.

前回とか前々回で Setoid とか Map を定義しました。 それをインポートしてもいいんですが、コード量が少なかったのでここに挿入しておきます。 ですので、今回のコードはそのまますぐに使えるよ。

Structure Setoid :=
  {
    carrier:> Type;
    equal: relation carrier;

    prf_Setoid:> Equivalence equal
  }.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).

Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y :> S" := (equal (s:=S) x y)
  (at level 70, y at next level, no associativity).
Notation "x == y" := (x == y :> _) (at level 70, no associativity).

Structure Map (X Y: Setoid) :=
  {
    map_body:> X -> Y;

    prf_Map:> Proper ((==) ==> (==)) map_body
  }.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'").

2.2 Magma 型の定義

Structure Binop (X: Setoid) :=
{
  binop:> X -> X -> X;
  prf_Binop:> Proper ((==) ==> (==) ==> (==)) binop
}.
Existing Instance prf_Binop.

Structure Magma :=
  {
    magma_setoid:> Setoid;
    magma_binop: Binop magma_setoid
  }.
Arguments magma_binop {m}.
Notation "x \dot y" := (magma_binop (m:=_) x y)
			(at level 60, right associativity,
			format "x  \dot   y").

prf_Binop の型は \[ \forall x,x',y,y' \in X.\; x == x' \wedge y == y' \Rightarrow x \bullet y == x'\bullet y' \] を意味しています(Properrespectful の定義を解けばわかります)。

台集合ならぬ台 Setoid の上の「関数」であるためには同値関係を保存する必要がありますね。

今回は magma_binop の well-definedness を直接記述していますが。 それをせずに Map として記述することもできます。 具体的には、 Map が Setoid になるので X: Setoid から Map X X: Setoid への Map を作ればよいわけです。

ただ、この方法はわかりにくいので、今回は採用しませんでした。 圏論とかやるなら、豊穣性とかと絡む話なので悪くはないんですけどね。

3 性質たち

マグマは単純な構造で、特にこれといった性質を持っていません。 何かを論ずるときはマグマの演算に性質を付加したうえで行われます。

ここではマグマから群を作るにあたって関係のある四つの性質を、 Class を使って定義していきます。

3.1 結合性(Associativity)

マグマ \(\langle M, \bullet \rangle\) が 結合的(associative) であるとは \[ \forall x,y,z\in M.\; (x \bullet y)\bullet z = x \bullet (y \bullet z) \] が成り立つことです。

これを Coq で書くと

Class Associative (m: Magma): Prop :=
  associative:
    forall (x y z: m), (x \dot y) \dot z == x \dot (y \dot z).

こうなります。 Class は基本的にレコードなのですが、このように括弧を付けずにたった一つのフィールドだけを与えて定義した場合、クラス名はそのフィールドの型の別名となります。

Associative = 
fun m : Magma => forall x y z : m, m (m x y) z == m x (m y z)
     : Magma -> Prop

こんな具合ですね。レコードではないので、 Associative m がゴールのときは split タクティクが失敗します。

3.2 単位性(Identity)

マグマ \(\langle M, \bullet \rangle\) が 単位的(identical) であるとはある元 \(e \in M\) があって \[ \forall x\in M.\; e \bullet x = x \bullet e = x \] が成り立つことです。この \(e\) を単位元と呼びます。

さて、単位元はこのように二つの等式を満すのですが、 この二つは左単位元律と右単位元律を意味しています。

演算の可換性は仮定されていないので、それぞれの単位元が同一のものであるとは限らず、一般に \(e\) が単位元と呼ばれる場合、それは \(e\) が左単位元であり右単位元でもあることを意味しています。

Coq における単位元律の定義もこの流儀に倣うこととします。

Class LIdentical (m: Magma)(e: m): Prop :=
  left_identical: forall x: m, e \dot x == x.

Class RIdentical (m: Magma)(e: m): Prop :=
  right_identical: forall x: m, x \dot e == x.

Class Identical (m: Magma)(e: m): Prop :=
  {
    identical_l:> LIdentical e;
    identical_r:> RIdentical e
  }.
Existing Instance identical_l.
Existing Instance identical_r.

二つの述語的クラスを定義して、それらを併せ持つクラスを定義するという流れです。

ここでちょっと重要なのは「性質」を記述するクラスのフィールドには、 可能な限り命題のみを書くようにした方が良い、ということです。

例えば、単位的というのは 単位元の存在 を意味していますが、 単位元そのものはクラスの構成要素に含まれていません。 マグマのとある元に対して その元が単位元であるとはどういうことか を意味するクラスを構成しています。左単位元と右単位元についても同様です。

仮に左単位元と右単位元をクラスの定義に含めていたとすると、 単位元律の定義をする際、二つの元の同一性を述べなければいけません。

今回は Setoid の要素ですから同値関係で記述できなくはないですが、 同一性を述べる対象が例えば群だったり体だったり、付加的な構造やら性質やらを大量に持っていると、同一性の記述だけで大変です。

もっと根本的な問題もあります。 今回のようにクラスの型を Prop にしてしまうと、 その中に含まれるフィールドの具体的構成を利用することができません。 単位元があることはわかっても、単位元の具体的な定義を参照できないということになります。 この状況は、証明だけを行うのであればある程度はなんとかなるかもしれませんが、 実際に計算を行うとなったら途端に破綻してしまいますね。

ということで、性質を記述する際にクラスを利用するならそのフィールドには命題のみを与えよう、となります。 exists を使ったらその要素の存在性は利用できても具体的構成は利用できない、 というのと同じ話です。

3.3 可逆性(Invertibility)

マグマ \(\langle M, \bullet \rangle\) が単位元 \(e \in M\) を持つとします。元 \(x \in M\) が 可逆(invertible) であるとは、 ある元 \(x^{-1} \in M\) が存在し、 \[ x^{-1} \bullet x = x \bullet x^{-1} = e \] となることです。この \(x^{-1}\) を \(x\) の逆元と呼びます。

そして \(M\) の任意の元が可逆であるとき、 \(\langle M, \bullet, e \rangle\) が 可逆(invertible) であるといいます。

さて、実際に定義する可逆性は、これと少し異なる形をしています。

Class LInvertible `{Identical m e}(inv: Map m m): Prop :=
  left_invertible:
    forall (x: m), (inv x) \dot x == e.

Class RInvertible `{Identical m e}(inv: Map m m): Prop :=
  right_invertible:
    forall (x: m), x \dot (inv x) == e.

Class Invertible `{Identical m e}(inv: Map m m): Prop :=
  {
    invertible_l:> LInvertible inv;
    invertible_r:> RInvertible inv
  }.

逆元にも左逆元とか右逆元とかありますので、その辺りの雰囲気は単位性と同じ流れです。

ポイントは、逆元を与える写像 inv を明示しているところです。 結合性の仮定されていない状況下では逆元の唯一性を言えませんので、 inv は逆元のうちの一つを与える写像ということになります。

「全ての元が可逆である」という言明を「逆元を与える写像が存在する」と言い換えているわけですね。

3.4 可除性(Divisibility)

マグマ \(\langle M, \bullet \rangle\) が 可除(divisible) であるとは任意の二元 \(a,b\in M\) について、一方が一方の「約数」となっていることを言います。 具体的には \[ \forall a,b \in M.\; \exists x,y\in M.\; x \bullet a = b \wedge a \bullet y = b \] が成り立つことです。

任意の二元について左側と右側の両方で「割り算」が出来ると思えばよいですね。 Coq での定義は以下のようになります。

Class Divisible (m: Magma)(divL: Binop m)(divR: Binop m): Prop :=
  {
    divisible_l:
      forall (a b: m), (divL a b) \dot a == b;
    divisible_r:
      forall (a b: m), a \dot (divR a b) == b
  }.

divLdivR はそれぞれ左側での割り算と右側での割り算です。 今回は左可除とか右可除とかを経由せずに定義しています。

複数の等式が命題に存在する場合は、「且つ」を使わずにそれぞれをフィールドとしたクラスを用意するなどして、簡単に rewrite タクティクを使えるようにしておくと便利です。

4 群を作る

それでは、以上の性質たちを組み合せ、マグマから群を作ります。 Wikipedia にのってる六角形 の左側です。

こちらは、多くの方にはあまり馴染みのない構成方法かもしれません。 私もよく知りませんでした。

4.1 準群(Quasigroup)

可除なマグマを 準群(quasigroup) といいます。

Structure Quasigroup :=
  {
    qg_magma:> Magma;
    qg_divL: Binop qg_magma;
    qg_divR: Binop qg_magma;
    prf_Quasigroup:> Divisible qg_divL qg_divR
  }.
Existing Instance prf_Quasigroup.

可除であるとは、左右両方での割り算ができることでしたので、 それぞれの「割り算」は Structure の構成要素となります。

そのため「準群であること」はそれらの割り算が Divisible であることと同値になります。

4.2 擬群(Loop)

単位元を持つ準群を 擬群(loop) と言います。 なんで loop っていうんでしょうね?

Structure Loop :=
  {
    loop_qg:> Quasigroup;
    loop_unit: loop_qg;

    prf_Loop:> Identical loop_unit
  }.
Existing Instance prf_Loop.

4.3 群(Group)

そして、結合律を満たす擬群を 群(group) といいます。 おそらく、この流れでの群の定義は馴染みのないものだと思います。

後に、群の公理に基づくものと同じであることを論じます。

Structure Group_1 :=
  {
    group_loop:> Loop;
    prf_Group_1:> Associative group_loop
  }.
Existing Instance prf_Group_1.

ということで、説明すべきことを性質の記述で説明してしまったのであっさりと通り過ぎてしまいました。

言い換えれば、個々の性質をしっかりと記述しておけば、それを組み合せる作業はとても簡単だ、ということです。

こんな感じでもう一つの構成の仕方も追っていきます。

5 群を作る

次は群の公理に則った流れで、マグマから群を構成していきます。 Wikipedia にのってる六角形 の右側です。

5.1 半群(Semigroup)

結合的なマグマを 半群(semigroup) と言います。

Structure Semigroup :=
  {
    sg_magma:> Magma;
    prf_Semigroup:> Associative sg_magma
  }.
Existing Instance prf_Semigroup.

5.2 単系(Monoid)

単位的な半群を モノイド(monoid) と言います。 単系って日本語訳、使ってるところを見たことがないです。

Structure Monoid :=
  {
    monoid_sg:> Semigroup;
    monoid_unit: monoid_sg;

    prf_Monoid:> Identical monoid_unit
  }.
Existing Instance prf_Monoid.

モノイドは計算機科学では非常に出番が多い代数構造の一つですが、 今回は深く追求しません。

そういえば モナドは自己函手の圏のモノイド対象 らしいですね。 この MonoidSetoid のなす圏のモノイド対象(になっているはず)です。

5.3 群(Group)

可逆なモノイドが群です。

Structure Group_2 :=
  {
    group_monoid:> Monoid;
    group_inv: let m := group_monoid in Map m m;
    prf_Group_2:> Invertible group_inv
  }.
Existing Instance prf_Group_2.

これまでの定義の流れは

  • 結合的であり、
  • 単位元を持ち、
  • 逆元も持つ。

となっています。これらは群の公理と対応していますね。

さきほどの Group_1 と違い、こちらの方は馴染みがあってわかりやすいのではないかと思います。

6 群は群

二通りの構成法でマグマから群を構成しました。 次に気になるのは、これらが本当に同じ「群」を与えているのかということです。

今回はこの疑問に対し、互いが互いを構成するという形で答えることにします。 それぞれの構成は、上で定義した流れに則る形になります。

6.1 Group_1 から Group_2 を構成する。

Group_1 から Group_2 を構成するにあたって

  • 結合性
  • 単位性
  • 可逆性

の三つの性質が言えればよいのですが、単位性と結合性は Group_1 でも直接的に述べられていますので、可逆性さえ言えれば OK です。

そして、可逆性は「逆元を与える写像が存在すること」でしたので、 必要なのはこの写像を構成することと、それが所与の等式を満たすことを示すことになります。

  1. 可逆性の証明

    まずはその写像の定義を与えます。

    Program Definition inv_Group_1 (g: Group_1): Map g g :=
      [ x :-> qg_divL g x (loop_unit g) ].
    

    \(a,b\in M\) について \((divL\ a\ b) \bullet a = b\) という等式が成り立ちますので、 単位元 \(e \in M\) に対しては \(divL\ a\ e \bullet a = e\) が成立し、 このことから \(divL\ a\ e\) が \(a\in M\) の左逆元であることがわかります。

    可逆であれば左逆元は逆元そのものですので、このような定義となります。

    残ったゴールは写像の well-definedness です。

    inv_Group_1 has type-checked, generating 1 obligation(s)
    Solving obligations automatically...
    1 obligation remaining
    Obligation 1 of inv_Group_1:
    forall g : Group_1,
    Proper ((==) ==> (==)) (fun x : g => (qg_divL g) x (loop_unit g)).
    

    それほど難しくはありませんので、

    Next Obligation.
      intros x y Heq; simpl; rewrite Heq; reflexivity.
    Qed.
    

    ちゃちゃっと証明終了です。 qg_divL 自身が適切な「写像」になっているので、特に何も気にすることなく rewrite タクティクが使えました。

    それでは、これが実際に可逆性をもたらす写像であることの証明を行います。 Invertible クラスのインスタンスを構成することになります。

    Instance inv_Group_1_Invertible (g: Group_1)
    : Invertible (inv_Group_1 g).
    Proof.
    
    1 subgoals, subgoal 1 (ID 203)
      
      g : Group_1
      ============================
       Invertible (inv_Group_1 g)
    
    
    (dependent evars:)
    

    Invertible クラスは左可逆性と右可逆性の二つから構成されているので split します。

    split.
    
    2 subgoals, subgoal 1 (ID 205)
      
      g : Group_1
      ============================
       LInvertible (inv_Group_1 g)
    
    subgoal 2 (ID 206) is:
     RInvertible (inv_Group_1 g)
    
    (dependent evars:)
    

    まずは左可逆性の証明になります。

    intros x; simpl.
    
    subgoal 1 (ID 209) is:
      
      g : Group_1
      x : g
      ============================
       (qg_divL g) x (loop_unit g) \dot  x == loop_unit g
    

    intro して simpl したゴールはこのようになっています。 これは可除性そのものなので

    apply divisible_l.
    

    として証明終了です。次の右可逆性にいきましょう。

    1 subgoals, subgoal 1 (ID 206)
      
      g : Group_1
      ============================
       RInvertible (inv_Group_1 g)
    
    
    (dependent evars:)
    

    こちらも同様に intro して simpl すると

    intros x; simpl.
    
    1 subgoals, subgoal 1 (ID 216)
      
      g : Group_1
      x : g
      ============================
       x \dot  (qg_divL g) x (loop_unit g) == loop_unit g
    
    
    (dependent evars:)
    

    というゴールが得られます。一見すると右可除性なのですが、 qg_divR であってほしいところが qg_divL になっています。

    というわけで、次の補題を示すことにしましょう。

    Lemma qg_div_LR (g: Group_1):
      forall x: g,
        qg_divL g x (loop_unit g) == qg_divR g x (loop_unit g).
    

    この等式は、結合的で単位元を持つ可除なマグマ、つまり群で成り立つ等式です。

    Proof.
      intros x; simpl.
    
    1 subgoals, subgoal 1 (ID 221)
      
      g : Group_1
      x : g
      ============================
       (qg_divL g) x (loop_unit g) == (qg_divR g) x (loop_unit g)
    
    
    (dependent evars:)
    

    単位元律を使って一時的に両辺を膨らませます。

    rewrite <- right_identical at 1.
    rewrite <- (left_identical (qg_divR g x (loop_unit g))).
    
    1 subgoals, subgoal 1 (ID 288)
      
      g : Group_1
      x : g
      ============================
       (qg_divL g) x (loop_unit g) \dot  loop_unit g ==
       loop_unit g \dot  (qg_divR g) x (loop_unit g)
    
    
    (dependent evars:)
    

    そして左辺の右側の単位元、右辺の左側の単位元をそれぞれ可除律で書き換えると、

    rewrite <- (divisible_r x (loop_unit g)) at 2.
    rewrite <- (divisible_l x (loop_unit g)) at 3.
    
    1 subgoals, subgoal 1 (ID 458)
      
      g : Group_1
      x : g
      ============================
       (qg_divL g) x (loop_unit g) \dot  x \dot  (qg_divR g) x (loop_unit g) ==
       ((qg_divL g) x (loop_unit g) \dot  x) \dot  (qg_divR g) x (loop_unit g)
    
    
    (dependent evars:)
    

    結合の順序は違えど、同じ元が得られ、

      rewrite associative.
      reflexivity.
    Qed.
    

    証明終了です。

    そして元々のゴールは

    1 subgoals, subgoal 1 (ID 216)
      
      g : Group_1
      x : g
      ============================
       x \dot  (qg_divL g) x (loop_unit g) == loop_unit g
    
    
    (dependent evars:)
    

    です。補題 qg_div_LRrewrite すれば右可除性そのものですので、

        rewrite qg_div_LR; apply divisible_r.
    Qed.
    

    証明終了です。可逆性を示すことができました。

  2. 構成

    可逆性さえ示してしまえば、あとの作業はルーチンワークです。 Strucutre の実体を与えるとき、省略されたフィールドについては推論してくれるので、記述すらも容易です。

    半群は

    Definition sg_Group_1 (g: Group_1): Semigroup :=
      {|
        sg_magma := g
      |}.
    

    と与えることができ、モノイドもこの半群を使って

    Definition monoid_Group_1 (g: Group_1): Monoid :=
      {|
        monoid_sg := sg_Group_1 g
      |}.
    

    とすれば構成できます。

    そして、先程定義した逆元写像 inv_Group_1 を使えば、 Group_2 の実体も

    Definition group_Group_1 (g: Group_1): Group_2 :=
      {|
        group_monoid := monoid_Group_1 g;
        group_inv := inv_Group_1 g
      |}.
    

    のように簡単に定義することができます。 証明すべきものは既に証明し終えているので、 これ以上特にやることはありません。

    これで以って Group_1 から Group_2 が構成できることを示せました。

6.2 Group_2 から Group_1 を構成する。

Group_2 から Group_1 を構成するにあたっては、 可除性が言えれば十分です。

さきほどは除法と単位元を利用して逆元を構成しましたので、 今回は逆元と単位元から除法を定義することになります。

  1. 逆元と単位元を使って除法

    まずは簡単に等式で以って説明します。 左側の「割り算」は \(a,b\in M\) に対して \[ x \bullet a = b \] なる \(x\in M\) を与えることでした。 \(M\) が群であれば \(x := b \bullet a^{-1}\) とすればよいですね。

    それを Coq で書くと次のようになります。

    Program Definition divL_Group_2 (g: Group_2): Binop g :=
      {| 
        binop x y := y \dot group_inv g x
     |}.
    Next Obligation.
      intros x x' Heqx y y' Heqy; simpl in *.
      rewrite Heqx, Heqy; reflexivity.
    Qed.
    

    Program コマンドを使って Binop の実体を定義しています。 証明しているのは well-definedness ですので、説明は割愛します。

    同様に考えると、右側の「割り算」は \(a,b\in M\) に対して \(y := a^{-1} \bullet b\) とすることで \(a \bullet y = b\) となりますので、

    Program Definition divR_Group_2 (g: Group_2): Binop g :=
      {| 
        binop x y := group_inv g x \dot y
     |}.
    Next Obligation.
      intros x x' Heqx y y' Heqy; simpl in *.
      rewrite Heqx, Heqy; reflexivity.
    Qed.
    

    として Coq での定義も終了です。証明部分がさきほどと全く同じですね。

    以上で二つの除法が定義できましたので、それらの可除性を示しましょう。

    Instance div_Group_2_Divisible (g: Group_2)
    : Divisible (divL_Group_2 g) (divR_Group_2 g).
    Proof.
      split; intros x y; simpl.
    

    少々タクティクを適用していますが、今のゴールは

    2 subgoals, subgoal 1 (ID 1041)
      
      g : Group_2
      x : g
      y : g
      ============================
       (y \dot  (group_inv g) x) \dot  x == y
    
    subgoal 2 (ID 1042) is:
     x \dot  (group_inv g) x \dot  y == y
    
    (dependent evars:)
    

    となっています。 それぞれの等式は結合律、可逆性、単位元律を利用して直ちに証明できます。

      now rewrite associative, left_invertible, right_identical.
      now rewrite <- associative, right_invertible, left_identical.
    Qed.
    
  2. 構成

    ここまでくればあとは先程と同様に、 Structure の実体をちまちまと書いていけば終りです。

    上で定義した除法たちを使えば準群が構成でき、

    Definition qg_Group_2 (g: Group_2): Quasigroup :=
      {|
        qg_magma := g ;
        qg_divL := divL_Group_2 g;
        qg_divR := divR_Group_2 g
      |}.
    

    それを利用して擬群が作れます。

    Definition loop_Group_2 (g: Group_2): Loop :=
      {|
        loop_qg := qg_Group_2 g;
        loop_unit := monoid_unit g
      |}.
    

    単位元はそのまま使えますね。

    そしてその擬群で以って Group_1 の実体が構成できます。

    Definition group_Group_2 (g: Group_2): Group_1 :=
      {|
        group_loop := loop_Group_2 g
      |}.
    

    これにて Group_2 からの Group_1 の構成は終了です。

7 まとめ

以上で、二つの異なる方法で作られた構造が、互いに互いを与えるという意味で「等価」であることを示せました。

二通りの構成が終わりましたので、最後に振り返りましょう。

Group_1 から Group_2 を構成したことで

group_Group_1
     : Group_1 -> Group_2

という関数が定義されたことになります。 同様に、 Group_2 から Group_1 を構成したことで

group_Group_2
     : Group_2 -> Group_1

という関数が定義されました。

すると、これらを合成した関数は Group_1Group_2 の上の自己関数となります。

より本格的に「等価性」の議論を行なうのであれば、各々の代数構造の間の準同型を定義し、その意味での同型性を証明することになると思います。 先の自己関数と恒等関数との「等価性」も示しておかなければなりませんね。

今回の記事ではさすがにそこまでは扱いませんが、気が向いたらやるかもしれません。 なんだか圏論っぽい香りがとてもしてきましたので、どうせそちらの文脈で手を出すことになるだろうとは思います。

というわけで、本記事は以上となります。 Coq の Structure とか Class は上手いこと使い分けるといいよ! を言いたいだけの事例紹介記事でした。

Coq で代数的構造を扱おうとか、 Structure とか Class とか使ってみたいなぁと思っている方々の参考になれば幸いです。

8 おまけ:構造をネストさせない

今回は「マグマから始めて性質を順々に付与していき群を構成する」という形を取りましたので、群の定義が

「結合的な「単位元を持つ「可除なマグマ」」」

か、あるいは

「可逆な「単位元を持つ「結合的なマグマ」」」

という形になっています。

しかし、群の公理で群を定義した場合、

「結合的で単位元を持つ可逆なマグマ」

という形になります。

これらの間に違いがあるわけではないのですが、 Coq で代数構造を定義するときには気にしておくとよいかもしれません。 例えば群を定義したいとき、一々半群やら準群やらから始めるのは億劫ですので、群に必要なものをまとめて与えられると便利です。

具体的には、次のような「群の公理」に該当するクラスを定義することになります。

Class isGroup (m: Magma)(e: m)(inv: Map m m) :=
  {
    group_identical:> Identical e;
    group_invertible:> Invertible inv;
    group_associative:> Associative m
  }.

各フィールドが群の公理の各々に対応しています。 もちろんマグマの定義から解いて二項演算子の well-definedness まで isGroup のフィールドとすることもできます。 どこまでの粒度で記述するかは、扱いたい命題の粒度との相談でしょうか。

この isGroup を使えば、群の定義は

Structure Group :=
  {
    group_magma:> Magma;
    group_unit: group_magma;
    group_inverse: Map group_magma group_magma;

    prf_Group:> isGroup group_unit group_inverse
  }.

となります。

その上で例えば

Notation make_Group m e inv := (@Build_Group m e inv _).

といった記法を定義すれば、 SetoidMap のように Program コマンドや refine タクティクと併用した定義が可能です。

代数構造がネストしている場合でもこの記法は定義できなくもないですが、 個人的にはこちらのスタイルの方が好きですね。

「群である」という命題はそれ自身で完結している方がしっくりきます。

Author: mathink

Created: 2015-06-28 Sun 02:42

Validate