Coq で環

coq_ring.md

title	tags	author	slide
Coq で環	Coq	mathink	false

まとめ

• Coq で Setoid ベースの環を定義した。
• Z が環だよって言った。
• ring とかの話ではない。
• 何か tactic 定義したりとかもしてない。
• 証明付きのスクリプトはここ。

環を定義する

環は加法について可換な群、乗法についてモノイドとなる代数系です。

環を定義するため、以下の順番で必要な道具を構成していき、最後に環を定義します。

• Setoid とその間の射 Map
• 二項演算 Binop
• モノイド
• 群
• 環

二項演算に関する性質は、それを必要とする構造を定義する直前で記述します。

とりあえず、以下のような設定をしておきます。

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable All Variables.

Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.

また、以降のスクリプトにおける

• Existing Instance
• Coercion
• Class の中の :>

は、書かないと超面倒なことになるので、忘れずに記述しておいてください。

Setoid & Map

Setoid と Map の定義は、基本的にこれまで私が書いてきたものをそのまま使い回しています。 記事を書く時にライブラリ化していないのは、こういう時は丸ごと書いてある方がわかりやすいかな、と考えているためです。

Setoid は、同値関係を等価性と見做した型。

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" := (equal x y) (at level 70, no associativity).
Notation "x == y :> S" := (equal (s:=S) x y)
  (at level 70, y at next level, no associativity).

Map は、Setoid の間のモルフィズムです。 等価性を保存するという性質を持ちます。

Class isMap (X Y: Setoid)(f: X -> Y) :=
  map_subst:> Proper ((==) ==> (==)) f.

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

    prf_Map:> isMap 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 ] ']'").

Proper は、関係を保存する演算などに使う既成の型クラスです。 これを使うと証明で rewrite が使えるのでとても便利です。 詳しくは A Gentle Introduction to Type Classes and Relations in Coq. を読んでください。 わかりやすいのでおすすめです。

二項演算

次に定義するのが二項演算です。モノイドも群も環も、全てマグマですから、二項演算がなければ話が始まりません。 Map を使って二項演算を構成できなくもないのですが、非常にめんどくさい見た目になるので、ここでは新たに Binop 型を構成します。

Map と同様に、等価性、すなわち同値関係を保存するという性質を持ちます。

Class isBinop (X: Setoid)(op: X -> X -> X) :=
  binop_subst:> Proper ((==) ==> (==) ==> (==)) op.

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

ここでも Proper を利用しています。ビノップ。

モノイド

モノイドは二項演算を持つ Setoid で、その二項演算が

• 結合律を満たす
• 単位元を持つ

という性質を持つものです。 これらの性質を表す命題は、二項演算に関する型クラスとして記述します。

Class Associative `(op: Binop X): Prop :=
  associative:>
    forall (x y z: X), op x (op y z) == op (op x y) z.

Class LIdentical `(op: Binop X)(e: X): Prop :=
  left_identical:> forall x: X, op e x == x.

Class RIdentical `(op: Binop X)(e: X): Prop :=
  right_identical:> forall x: X, op x e == x.

Class Identical `(op: Binop X)(e: X): Prop :=
  {
    identical_l:> LIdentical op e;
    identical_r:> RIdentical op e
  }.
Existing Instance identical_l.
Existing Instance identical_r.
Coercion identical_l: Identical >-> LIdentical.
Coercion identical_r: Identical >-> RIdentical.

そして、モノイドの規則をそのまま書き下して Monoid 型を定義します。 Class と Structure と Module の使い方は、読めばなんとなくわかります(一日ぶり二度目)。

Module Monoid.
  Class spec (M: Setoid)(op: Binop M)(e: M) :=
    proof {
        associative:> Associative op;
        identical:> Identical op e
      }.

  Structure type :=
    make {
        carrier: Setoid;
        op: Binop carrier;
        e: carrier;

        prf: spec op e
      }.

  Module Ex.
    Existing Instance associative.
    Existing Instance identical.
    Existing Instance prf.

    Notation isMonoid := spec.
    Notation Monoid := type.

    Coercion associative: isMonoid >-> Associative.
    Coercion identical: isMonoid >-> Identical.
    Coercion carrier: Monoid >-> Setoid.
    Coercion prf: Monoid >-> isMonoid.

    Delimit Scope monoid_scope with monoid.
    Notation "x * y" := (op _ x y) (at level 40, left associativity): monoid_scope.
    Notation "'1'" := (e _): monoid_scope.
  End Ex.

End Monoid.
Export Monoid.Ex.

注意すべきは Module Ex. 内における二項演算のために定義した記法です。 モノイドは二項演算を持ちますが、それをどう表記するかは場合によって変わります。 一種類のモノイドのみを考えているときは気にしなくてもよいかもしれませんが、例えば半環を考えるときは二種類のモノイド(加法と乗法)を同時に考えることになります。 そうすると、一つの記法ではまかないきれなくなってしまいます。

そういった事態を回避するため、monoid_scope に於いてのみ適用できるように記法を定義しています。

以降、群や環を定義するときも同様の規約に則ります、

群

群は、任意の元が逆元を持つモノイドでした。

そのため、まずは「逆元を持つ」ということを表す型クラスを記述します。 ここでは「逆元を持つ」という言明を「逆元を与える Map が存在する」に読み替えています。

Class LInvertible `{Identical X op e}(inv: Map X X): Prop :=
  left_invertible:>
    forall (x: X), op (inv x) x == e.

Class RInvertible `{Identical X op e}(inv: Map X X): Prop :=
  right_invertible:>
    forall (x: X), op x (inv x) == e.

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

逆元には左逆元と右逆元が存在し、それらが一致するときにのみ「逆元」と省略して呼ぶのでした。 上述の定義もその形式に倣って定義しています。 まとめて定義しても、左と右の区別をする予定がないのであれば問題はありません。好みの問題です。

さて、以上の道具を使い群の型 Group を定義します。 流れは Monoid の時と同じです。

Module Group.
  Class spec (G: Setoid)(op: Binop G)(e: G)(inv: Map G G) :=
    proof {
        is_monoid:> isMonoid op e;
        invertible: Invertible inv
      }.

  Structure type :=
    make {
        carrier: Setoid;
        op: Binop carrier;
        e: carrier;
        inv: Map carrier carrier;
        
        prf: spec op e inv
      }.

  Module Ex.
    Existing Instance is_monoid.
    Existing Instance invertible.
    Existing Instance prf.

    Notation isGroup := spec.
    Notation Group := type.

    Coercion is_monoid: isGroup >-> isMonoid.
    Coercion invertible: isGroup >-> Invertible.
    Coercion carrier: Group >-> Setoid.
    Coercion prf: Group >-> isGroup.

    Delimit Scope group_scope with group.

    Notation "x * y" := (op _ x y) (at level 40, left associativity): group_scope.
    Notation "'1'" := (e _): group_scope.
    Notation "x ^-1" := (inv _ x) (at level 20, left associativity): group_scope.
  End Ex.
Export Group.Ex.

これで群の定義まで終わりましたので、環の定義に臨むことができるようになりました。

環

環は、加法について可換な群であり、乗法についてモノイドとなる代数系です。 更に、加法と乗法の間には分配律が成立します。

まずは、可換律と分配律を表す型クラスを記述します。

Class Commute `(op: Binop X): Prop :=
  commute:>
    forall a b, op a b == op b a.

Class Distributive (X: Setoid)(add mul: Binop X) :=
  {
    distributive_l:>
      forall a b c, mul a (add b c) = add (mul a b) (mul a c);

    distributive_r:>
      forall a b c, mul (add a b) c = add (mul a c) (mul b c)
  }.

分配律は、二つの二項演算に関する性質だということに注意してください。 また、ここでは逆元の時と違い、二つの性質を一つの型クラスに収めています。 これも分けて書いてもかまいません。証明時のサブゴールの生成のされ方が少し変わるだけです。

性質の記述が済んだので、環の型 Ring を定義します。

Module Ring.
  Class spec (R: Setoid)(add: Binop R)(z: R)(inv: Map R R)(mul: Binop R)(e: R) :=
    proof {
        add_group: isGroup add z inv;
        add_commute: Commute add;
        mul_monoid: isMonoid mul e;

        distributive: Distributive add mul
      }.

  Structure type :=
    make {
        carrier: Setoid;

        add: Binop carrier;
        z: carrier;
        inv: Map carrier carrier;

        mul: Binop carrier;
        e: carrier;

        prf: spec add z inv mul e
      }.

  Module Ex.
    Existing Instance add_group.
    Existing Instance add_commute.
    Existing Instance mul_monoid.
    Existing Instance distributive.
    Existing Instance prf.

    Notation isRing := spec.
    Notation Ring := type.

    Coercion add_group: isRing >-> isGroup.
    Coercion add_commute: isRing >-> Commute.
    Coercion mul_monoid: isRing >-> isMonoid.
    Coercion distributive: isRing >-> Distributive.
    Coercion carrier: Ring >-> Setoid.
    Coercion prf: Ring >-> isRing.

    Delimit Scope ring_scope with rng.

    Notation "x + y" := (add _ x y): ring_scope.
    Notation "x * y" := (mul _ x y): ring_scope.
    Notation "'0'" := (z _): ring_scope.
    Notation "x ^-1" := (inv _ x) (at level 20, left associativity): ring_scope.
    Notation "'1'" := (e _): ring_scope.
  End Ex.
  Import Ex.

  Definition add_id_l {R: Ring}(x: R) := (@left_identical R (add R) (z R) (add_group (spec:=R)) x).
  Definition add_id_r {R: Ring}(x: R) := (@right_identical R (add R) (z R) (add_group (spec:=R)) x).
  Definition add_inv_l {R: Ring}(x: R) := (@left_invertible R (add R) (z R) (add_group (spec:=R)) (inv R) (add_group (spec:=R)) x).
  Definition add_inv_r {R: Ring}(x: R) := (@right_invertible R (add R) (z R) (add_group (spec:=R)) (inv R) (add_group (spec:=R)) x).
  Definition mul_id_l {R: Ring}(x: R) := (@left_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
  Definition mul_id_r {R: Ring}(x: R) := (@right_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
End Ring.
Export Ring.Ex.
Coercion Ring.group: Ring >-> Group.
Coercion Ring.monoid: Ring >-> Monoid.

さて、先程までの例と違うのは Module Ex. の後に、幾つかの定義が行われていることです。

これらは、演算の単位元などに関する性質についての曖昧性を除去するためのものです。 加法と乗法のどちらもモノイドですから、両者共に単位元を持ち、単位元についての性質、例えば $e * x == x$ が成り立ちます。

しかし、何もせずに証明においてこの性質を利用しようとすると、単位元律がどちらの演算に対してのものなのか Coq には判断が付かないという問題が生じてしまいます。 これを回避するために Module Ring. の中であらかじめそれぞれの性質に個別の名前を割り当てておき、後々利用する際に Ring.add_id_l という曖昧さのない形式で使えるようにしているのです。

というわけで、環の型を定義するところまでが終わりました。 残りは Coq であらかじめ定義されている Z がここでの Ring であることを示して終わりとします。

Z は環

下準備

まずはライブラリ ZArith をインポートして Z_scope を開いておきます。 そうしないと数字列を Z 型の数と認識してくれません。

Require Import ZArith.
Open Scope Z_scope.

また、Coq の Z は positive 型を使って定義されているのでした。

Print Z.
(* Inductive Z : Set :=  Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z *)

(* For Zpos: Argument scope is [positive_scope] *)
(* For Zneg: Argument scope is [positive_scope] *)

そのため、以降では少しだけ positive が顔を覗かせます。 なお、それに限らず全ての証明は省略します。 完全なスクリプトの URL は上述してありますのでよろしくお願いします。

まずは positive と Z を eq による Setoid としておきます。

Canonical Structure positive_setoid := Setoid_of (@eq positive).
Canonical Structure Z_setoid := Setoid_of (@eq Z).

次に行うのは、 Z のコンストラクタである Zneg と Zpos が上記の二つの Setoid 間の等価性を保存していることの保証です。 そうしないと Zneg p の p に関する rewrite による代入などが出来ないからです。

Instance Zneg_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zneg.

Instance Zpos_Proper : Proper ((==:>positive_setoid) ==> ((==:>Z_setoid))) Zpos.

Map になっていることを示してもよいのですが、　Proper でさえあれば代入に支障はないので、簡単のため、これだけにしておきます。

加法について可換な群

次に、加法について群となることを示します。 可換性についてもここで示しておきましょう。

手順は

1. Zplus が Binop であることを示す。
2. Zplus と 0 が Monoid であることを示す。
3. Zopp が Z_setoid から Z_setoid への Map であることを示す。
4. Zplus,Zopp,0 が群であることを示す。
5. Zplus の可換性を示す。

となっています。

(* Group of '+' *)
Program Instance Zplus_is_binop: isBinop (X:=Z_setoid) Zplus.
Canonical Structure Zplus_binop := Build_Binop Zplus_is_binop.

Program Instance Zplus_is_monoid: isMonoid Zplus_binop 0.
Canonical Structure Zplus_monoid := Monoid.make Zplus_is_monoid.

Program Instance Zinv_is_map: isMap (X:=Z_setoid) Zopp.
Canonical Structure Zinv_map: Map Z_setoid Z_setoid := Build_Map Zinv_is_map.

Program Instance Zplus_is_group: isGroup Zplus_binop 0 Zinv_map.
Canonical Structure Zgroup_monoid := Group.make Zplus_is_group.

Program Instance Zplus_commute: Commute Zplus_binop.

乗法についてモノイド

加法と同様に乗法についてもモノイドとなることを示します。 先程よりは大分単純です。

1. Zmult が Binop であることを示す。
2. Zmult と 1 が Monoid を構成することを示す。

という順番で行っています。

(* Monoid of '*' *)
Instance Zmult_is_binop: isBinop (X:=Z_setoid) Zmult.
Canonical Structure Zmult_binop := Build_Binop Zmult_is_binop.

Program Instance Zmult_is_monoid: isMonoid Zmult_binop 1.
Canonical Structure Zmult_monoid := Monoid.make Zmult_is_monoid.

Z は環になる

最後に、以上の道具を使って Z が Ring であることを示します。 可換性は証明してあるので、残りは分配律の証明だけとなります(省略していますが)。

(* Ring of '+' & '*' *)
Program Instance Z_is_ring: isRing Zplus_binop 0 Zinv_map Zmult_binop 1.
Canonical Structure Z_ring := Ring.make Z_is_ring.

というわけで、最後はかなり単純な作業でしたが、為すべきは為しました。 あとは、少しだけ計算の例をやってみましょう。

試す

ということで Z が環だと示せましたから、実際に計算してみましょう。 計算した結果は Z_ring になって

Compute (1 * 2 + 3).
     (* = 5 *)
     (* : Z *)

ませんね。

どうしてでしょう。

答えは簡単、+ とか * は元から Z のための記法としても用意されているから、そっちが使われちゃったんだ！まいったね！

とか言っても仕方がないのでちゃんとやりましょう。 まずは ring_scope を開きます。そもそも Ring 用の記法はここでしか通用しないはずなので、スコープを開いてない状態じゃ上手くいくはずもありませんでした。

Open Scope ring_scope.

さて、準備は終わったので同じ見た目の計算をしてみると、

Compute (1 * 2 + 3).
     (* = 5 *)
     (* : Z_ring *)

はい、正しい結果になりました。 返り値が Z_ring ということは、今回定義した環、 Ring の上での計算として扱われたということです。

よかったよかった。

ちなみに、 Unset Printing Notations. した上でそれぞれの式を Check すると

Check (1 * 2 + 3).
(* Z.add (Z.mul (Zpos xH) (Zpos (xO xH))) (Zpos (xI xH)) *)
(*      : Z *)

と

Check (1 * 2 + 3).
(* (Ring.add Z_ring) ((Ring.mul Z_ring) (Ring.e Z_ring) (Zpos (xO xH))) *)
(*   (Zpos (xI xH)) *)
(*      : Z_ring *)

になり、実際に項の形で以てその事実を確かめることができます。

冒頭のリンクから証明付きスクリプトを得られるので、気になる方はそれをコピペして色々計算してみてください。