Coq/SSReflectで型クラスを定義する

# はじめに
本記事では、Coq/SSReflectで型クラスに相当するレコードを定義する方法を紹介します。

また、型クラスの継承や合流するときの書き方についても記述していきます。

ソースコードは[こちら](https://github.com/nekonistyle/type-class-example-in-coq/blob/main/monoid.v)にあります。


# 基本となる型クラスを定義する

まず、他の型クラスを継承しないベースとなるような型クラスを定義します。

例として、モノイドの型を定義してみます。

## 定義の全体像

定義の全体像としては以下のようになります。

```coq
Module Monoid.
  Section ClassDef.
    Record class_of (G:Type) :=
      Class {
          op : G -> G -> G;
          id : G;
          _: associative op;
          _: left_id id op;
          _: right_id id op
        }.

    Structure type := Pack {sort; _: class_of sort}.
    Variable (cT : type).
    Definition class :=
      let: Pack _ c := cT return class_of (sort cT) in c.
  End ClassDef.

  Module Exports.
    Coercion sort : type >-> Sortclass.

    Notation monoidType := type.
    Definition opg G := op (class G).
    Definition idg G := id (class G).
  End Exports.
End Monoid.
Import Monoid.Exports.
```

まず、原則として`Monoid`モジュールを作ります。
これがセクションでないのは、他の型クラスを定義するときにも内部で同名の関数を定義したいからです。つまり、`Module`なら内部関数をモジュールの外からそのままの名前で呼び出せないため、外部で同名の関数を定義できますが、`Section`だとそのまま使えてしまうため、名前を変えなければ外部で定義できなくなります。
特に、`Section ClassDef`はある程度どの型クラスでも使い回せるのと、モジュール名だけ変えて同じ名前の関数が使えた方が統一感があるので、`Module`で定義しておいた方が無難です。


## `class_of`を定義する

まず、`class_of`という名前のレコードを、型引数`G:Type`をとるように定義します。
これに対して、演算やそれらが満たす性質を定義します。
このとき、性質に関してはあとで定理として証明するので、ここで名前を付ける必要はないです。

今回、定義したいのはモノイドなので、モノイド上の演算`op`と、単位元`id`、そして、それらが満たすべき公理、すなわち結合則`associative op`と左単位元則`left_id id op`、右単位元則`right_id id op`を定義します。

```coq
    Record class_of (G:Type) :=
      Class {
          op : G -> G -> G;
          id : G;
          _: associative op;
          _: left_id id op;
          _: right_id id op
        }.
```

特に`class_of`は`Type -> Type`型を持ちます。

## `type`を記述する

上で定義した`class_of`に対して、それを満たす型変数`T`とその証明`class_of T`をパックしたレコード`type`を定義します。

```coq
    Structure type := Pack {sort; _: class_of sort}.
    Variable (cT : type).
    Definition class :=
      let: Pack _ c := cT return class_of (sort cT) in c.
```

これにより、`G:type`を仮定すると、`sort G`によってモノイドの型を呼び出せるようになります。
また、`class : forall cT:type, class_of (sort cT)`を定義しておくとのちに役に立ちます。

## 外部で使用する型クラス名と`Coersion`を定義する

最後に、外部で使用する定義をまとめる`Exports`モジュールを作ります。

```coq
  Module Exports.
    Coercion sort : type >-> Sortclass.

    Notation monoidType := type.
    Definition opg G := op (class G).
    Definition idg G := id (class G).
  End Exports.
```

まず`Coersion : sort : type >-> Sortclass`によって、`type`を`Sortclass`、すなわち型の型として扱えるようにします。
つまり、本来はレコードである`G:type`に対し、`x:G`のように型として呼び出すと、暗黙のうちに`x:sort G`として扱ってくれるということです。

また、`type`に外部で使用する名前(ここでは`monoidType`)を付けます。
命名規則ですが、Coqでは慣習的に`eqType`や`zmodType`などの小文字から始まる`〇〇Type`とつけることが多いです。

`class_of`で演算が定義されている場合はそれにも名前を付けます。
具体的には、引数`G:type`をもらった時の`sort G:Type`上の演算として定義します。
つまりこの例だと、コアーションを含め、`opg : forall G:monoidType, G -> G -> G`になるように定義するということです。
この定義には`ClassDef`内で定義した`class`が役に立ちます。


最後に、一番外のモジュール`Monoid`の外で`Exports`だけを`Import`します。

```coq
Import Monoid.Exports.
```

これにより、`Exports`内で定義したものだけが、そのまま外で使えるようになります。
これで型クラスの定義が完了です。


## 公理が成り立つことを証明する

型クラスを定義しただけでは、それが自身の公理が満たすことを証明するためにレコードの定義を解く必要があり、そのまま使うのが少々面倒です。
したがって、まずはこれらを補題として証明しておきます。

```coq
Section MonoidTheory.
  Variable (G:monoidType).

  Lemma opgA : associative (@opg G).
  Proof. by case : G =>[s []]. Qed.

  Lemma op0g : left_id (idg G) (@opg _).
  Proof. by case : G =>[s []]. Qed.

  Lemma opg0 : right_id (idg G) (@opg _).
  Proof. by case : G =>[s []]. Qed.
```

また、先ほど記述したように、実際はレコードである`G:monoidType`はコアーションのおかげで以下の`e:G`ように型としても扱えます。

```coq
  Lemma idg_uniquel (e:G) : left_id e (@opg _) -> e = idg G.
  Proof.
    move =>/(_ (idg _)). by rewrite opg0.
  Qed.
End MonoidTheory.
```

## 具体的な型に対して型クラスの公理を満たすことを証明する。

例として、`nat`が具体的に`monoidType`として扱えることを示します。
型クラスは実際にはレコードであるので、`Monoid.class_of nat`をコンストラクタ`Monoid.Class`を使って定義し、それを`Monoid.Pack`してしまえばいいです。

```coq
Definition nat_monoid_class_of : Monoid.class_of nat :=
  Monoid.Class addnA add0n addn0.
Canonical nat_monoid : monoidType :=
  @Monoid.Pack nat nat_monoid_class_of.
```

このとき`nat_monoid`を`Canonical`で定義することにより、`monoidType`上の演算や補題を`nat`上でも使えるようになります。

```coq
Lemma my_addn0 : forall n : nat, n + 0 = n.
Proof. exact : opg0. Qed.
```


# 型クラスを継承する

型クラスを継承する場合は以下のように記述します。

## 定義の全体像

例えば、型クラス`monoidType`を継承した可換モノイドの型クラス`comoidType`を定義したい場合は以下のように記述します。

```coq
Module Comoid.
  Record mixin_of (G:monoidType) :=
    Mixin {
        _: commutative (@opg G)
      }.

  Section ClassDef.
    Record class_of (G:Type) :=
      Class {
          base : Monoid.class_of G;
          mixin : mixin_of (Monoid.Pack base)
        }.
    Structure type := Pack {sort; _: class_of sort}.
    Variable (cT : type).
    Definition class :=
      let: Pack _ c := cT return class_of (sort cT) in c.

    Definition monoidType := Monoid.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Monoid.class_of.
    Coercion mixin : class_of >-> mixin_of.

    Coercion sort : type >-> Sortclass.

    Coercion monoidType : type >-> Monoid.type.
    Canonical monoidType.

    Notation comoidType := type.
  End Exports.
End Comoid.
Import Comoid.Exports.
```

ポイントとなるのは３点、`mixin_of`と`class_of`、それに`Coercion : monoidType : type >-> Monoid.type`です。


## `mixin_of`を定義する

継承する型クラスに新たに追加したい公理は`mixin_of`に記述します。

具体的には、継承する型クラスの引数`G:monoidType`を取るレコードとして定義し、その上に追加したい演算や性質を記述します。

```coq
  Record mixin_of (G:monoidType) :=
    Mixin {
        _: commutative (@opg G)
      }.
```

今回はモノイド`G`上の演算`@opg G`における可換則`commutative (@opg G)`を仮定しています。

## `class_of`を定義する

先ほど定義した`mixin_of`を使って、`monoidType`のときのように、単なる型引数`G:Type`をとるようなレコード`class_of`を定義します。


```coq
    Record class_of (G:Type) :=
      Class {
          base : Monoid.class_of G;
          mixin : mixin_of (Monoid.Pack base)
        }.
```

`class_of`によって型引数`G:Type`が継承したい性質のクラスを満たすことの証明`base : Monoid.class_of G`と、その証明によって作られた`(Monoid.Pack base) : Monoid.type`が追加する公理である`mixin_of`を満たすことの証明をまとめます。

このように定義することにより、各型クラスの`class_of`はそれぞれ`Type -> Type`型を持つことで統一できます。


## 継承元への変換関数を定義する

また、継承した型クラスへのコアーションを定義するために、`type`から`Monoid.type`への自然に定義される関数`monoidType`を定義しておきます。

```coq
    Definition monoidType := Monoid.Pack (base class).
```

## `Exports`内での追加

`Exports`モジュールで、いくつかのコアーションを追加します。
具体的には、`class_of`から`base`を使った継承元の`class_of`へのコアーションと`mixin`による`mixin_of`へのコアーション、あとは先ほど定義した`type`から継承元の`type`への`Coercion`と`Canonical`です。

```coq
  Module Exports.
    Coercion base : class_of >-> Monoid.class_of.
    Coercion mixin : class_of >-> mixin_of.

    Coercion sort : type >-> Sortclass.

    Coercion monoidType : type >-> Monoid.type.
    Canonical monoidType.

    Notation comoidType := type.
  End Exports.
```

`class_of`からのコアーションはこの型クラスをさらに継承する型クラスを定義するときに使います。
`type`から`Monoid.type`へのコアーションとカノニカルによって、`comoidType`は`monoidType`としても使え、その上で定義される関数や補題が適用できるようになります。


## 公理が成り立つことを証明する

追加した公理が成り立つことの証明は、`mixin_of`の定義を分解すれば示せます。

```coq
Section ComoidTheory.
  Variable (G:comoidType).

  Lemma opgC : commutative (@opg G).
  Proof. by case : G =>[s [b []]]. Qed.
End ComoidTheory.
```


# 2つに分岐して継承した型クラスを合流する

2つに分岐した型クラスを合流するような型クラスを定義します。

本記事では、まず`monoidType`を継承する群を表す型クラス`groupType`を定義して、
`comoidType`と合流して可換群を表す型クラス`comgroupType`を定義します。

まず群`groupType`を以下に定義します。

```coq
Module Group.
  Record mixin_of (G:monoidType) :=
    Mixin {
        inv : G -> G;
        _: left_inverse (idg G) inv (@opg _)
      }.

  Section ClassDef.
    Record class_of (G:Type) :=
      Class {
          base : Monoid.class_of G;
          mixin : mixin_of (Monoid.Pack base)
        }.
    Structure type := Pack {sort; _: class_of sort}.
    Variable (cT : type).
    Definition class :=
      let: Pack _ c := cT return class_of (sort cT) in c.

    Definition monoidType := Monoid.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Monoid.class_of.
    Coercion mixin : class_of >-> mixin_of.

    Coercion sort : type >-> Sortclass.

    Coercion monoidType : type >-> Monoid.type.
    Canonical monoidType.

    Notation groupType := type.
    Definition invg G := inv (class G).
  End Exports.
End Group.
Import Group.Exports.
```

## 定義の全体像

これに対して、可換群`comGroupType`は以下のように定義します。


```coq
Module ComGroup.
  Section ClassDef.
    Record class_of (G:Type) :=
      Class {
          base : Group.class_of G;
          mixin : Comoid.mixin_of (Monoid.Pack base)
        }.
    Definition base2 G (class:class_of G) : Comoid.class_of G :=
      Comoid.Class (mixin class).

    Structure type := Pack {sort; _: class_of sort}.
    Variable (cT : type).
    Definition class :=
      let: Pack _ c := cT return class_of (sort cT) in c.

    Definition monoidType := Monoid.Pack (base class).
    Definition groupType := Group.Pack (base class).
    Definition comoidType := Comoid.Pack (base2 class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Group.class_of.
    Coercion base2 : class_of >-> Comoid.class_of.

    Coercion sort : type >-> Sortclass.

    Coercion monoidType : type >-> Monoid.type.
    Canonical monoidType.
    Coercion groupType : type >-> Group.type.
    Canonical groupType.    
    Coercion comoidType : type >-> Comoid.type.
    Canonical comoidType.

    Notation comGroupType := type.
  End Exports.
End ComGroup.
Import ComGroup.Exports.
```

## `class_of`を定義する

まず`class_of G`において、継承する片方の`class_of`、すなわちここでは`Group.class_of G`を`base`という名前で仮定します。
それに対し、もう一つの型クラスの`mixin_of`をこの`base`から作っていきます。
今回の例では、もう一つの型クラスが`comoidType`であり、その`mixin_of`の引数`monoidType`を`base`から作ればいいです。
今、`base : Group.class_of G`から`Monoid.class_of`へのコアーションがあるのでこれを`Monoid.Pack`してやればOKです。

```coq
    Record class_of (G:Type) :=
      Class {
          base : Group.class_of G;
          mixin : Comoid.mixin_of (Monoid.Pack base)
        }.
```

のちに`class_of`から`mixin_of`で継承した型クラスの`class_of`へのコアーションを定義するための関数も用意します。

```coq
    Definition base2 G (class:class_of G) : Comoid.class_of G :=
      Comoid.Class (mixin class).
```

あとは1つの型クラスを継承するときと同じように記述すれば大丈夫です。


# まとめ

Coq/SSReflectで型クラスを定義する方法について記述しました。参考にしていただければ幸いです。