[Coq] Group on Setoid

@cocoatomo さんの blog に Python で群論をという記事があったので、同じことを Coq でやってみました。

証明を含む実際のコードは https://github.com/tmiya/coq/blob/master/group/setoid_group.v にあります。以下は解説です。
将来的に剰余群みたいなものを定義することを考え、集合の上の等号を自分で定義出来る様にします。つまり同値関係を定義し、setoid の上に群を定義することになります。

まず setoid の定義に必要なライブラリと、サンプルを証明するのに必要なライブラリを Import します。

Require Import Relation_Definitions Setoid Morphisms.
Require Import Arith Omega.

次いでサンプルとして、$\mathbb{Z}' := \{(a,b)\; | \; a,b \in \mathbb{N}\}$ として自然数の組を使って整数を表す例を考えます。同値関係は $(a,b) \sim (a',b') \Leftrightarrow a+b' = a'+b$ と定義し、$z=(a,b)$ に対して $z^{-1}= (b,a)$, $(a,b) \ast (a',b') = (a+a',b+b')$ と定義すると、整数 $\mathbb{Z}'$ 上の加法に関する群を構成出来ます --- ということを後から示します。まずは $\mathbb{Z}'$ とその上の演算を定義します。

Inductive Z' : Set :=
| mkZ' : nat -> nat -> Z'.

Definition eq'(z1 z2:Z') : Prop :=
  match z1,z2 with
  | (mkZ' p1 n1),(mkZ' p2 n2) => (p1+n2 = p2+n1)
  end.

Definition minus'(z:Z') :=
  match z with
  | mkZ' a b => mkZ' b a
  end.

Definition plus'(z1 z2:Z') :=
  match z1,z2 with
  | (mkZ' a1 b1),(mkZ' a2 b2) => (mkZ' (a1+a2) (b1+b2))
  end.

さて eq' が Z' の同値関係になっていることを示す必要があります。 以下の様に示します。Add Paramereic Relation 云々は setoid であることを Coq に登録する手続きです。

Lemma refl_eq' : reflexive _ eq'.
Lemma sym_eq' : symmetric _ eq'.
Lemma trans_eq' : transitive _ eq'.

Add Parametric Relation : Z' eq'
  reflexivity proved by refl_eq'
  symmetry proved by sym_eq'
  transitivity proved by trans_eq' as Z'_setoid.

次いで、minus', plus' が well-defined であることを示す必要があります。どういうことかというと、$z, z' \in \mathbb{Z}'$ について、$z \sim z'$ ならば $z^{-1} \sim z'^{-1}$ などを示す必要があるということです。これも以下の様に示します。

Add Parametric Morphism : 
  minus' with signature (eq' ==> eq') as minus'_mor.

Add Parametric Morphism :
  plus' with signature (eq' ==> eq' ==> eq') as plus'_mor.

ここまできたら、群の定義をします。同値関係の話は通常の数学では自明として述べないと思いますが、後々の証明で使いたい公理なので群の定義の他に含めて書くことにします。

Class Group {S:Set}(eq:S->S->Prop)
  (e:S)(inv:S->S)(op:S->S->S) := {
  equiv : Equivalence eq ;
  equiv_dec : 
    forall x y:S, {eq x y} + {~(eq x y)} ;
  inv_mor : 
    forall x y:S, eq x y -> eq (inv x) (inv y) ;
  op_mor :
    forall x1 y1 x2 y2:S, eq x1 y1 -> eq x2 y2 ->
    eq (op x1 x2) (op y1 y2) ;
  op_assoc :
    forall x y z:S, eq (op (op x y) z) (op x (op y z)) ;
  left_unit :
    forall x:S, eq (op e x) x ;
  right_unit :
    forall x:S, eq (op x e) x ;
  left_inv :
    forall x:S, eq (op (inv x) x) e ;
  right_inv :
    forall x:S, eq (op x (inv x)) e
}.

最後に先ほど作った $\mathbb{Z}'$ が群であることを示します。

Instance Z'_group : Group eq' (mkZ' O O) minus' plus'.