読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqで型クラスで群論

群論に関する定義をするのであれば、型クラスを使うのが一番うまくいくと思います。

Class Group G :=
  {
    gunit : G;
    gadd : G -> G -> G;
    ginv : G -> G;
    gadd_unit_l : forall g : G, gadd gunit g = g;
    gadd_unit_r : forall g : G, gadd g gunit = g;
    gadd_assoc : forall a b c : G, gadd (gadd a b) c = gadd a (gadd b c);
    gadd_inv : forall g : G, gadd g (ginv g) = gunit /\ gadd (ginv g) g = gunit
  }.

Infix "<+>" := gadd (at level 40, left associativity).

何より、このgaddを演算子にできるのが便利です。他の方法で、例えば

Definition is_group (G : Type) (gadd : G -> G -> G) (gunit : G) ...

としても、gaddは単なる束縛変数なので、別な名前を付けることはできません。

群の定義だけして終わるのもつまらないので、簡単な定理を証明してみましょう。

単位元の一意性。

Theorem group_unit_unique:
  forall (G : Type) (Grp : Group G),
  forall u : G,
    (forall g : G, g <+> u = g /\ u <+> g = g)
    -> u = gunit.
Proof.
  intros G Grp u H.
  specialize (H gunit).
  destruct H.
  rewrite -> gadd_unit_l in H.
  assumption.
Qed.

逆元の一意性。

Theorem ginv_unique:
  forall (G : Type) (Grp : Group G) (g h : G),
    g <+> h = gunit /\ h <+> g = gunit
    -> h = ginv g.
Proof.
  intros G Grp g h H.
  destruct H.
  assert (Hinv := gadd_inv).
  specialize (Hinv g).
  destruct Hinv.
  rewrite <- H1 in H.
  assert (H3: ginv g <+> (g <+> h) = ginv g <+> (g <+> ginv g)).
  {
    rewrite -> H. reflexivity.
  }
  rewrite <- gadd_assoc in H3.
  rewrite -> H2 in H3.
  rewrite <- gadd_assoc in H3.
  rewrite -> H2 in H3.
  rewrite -> gadd_unit_l in H3.
  rewrite -> gadd_unit_l in H3.
  assumption.
Qed.

自明な群は任意の群の部分集合

Definition hom {G H : Type} {Grp : Group G} {Hrp : Group H} (f : G -> H) :=
  forall a b : G, f (a <+> b) = f a <+> f b.

Definition mono {A B : Type} (f : A -> B) :=
  forall a b : A, f a = f b -> a = b.

Definition subgroup (H G : Type) {Grp : Group G} {Hrp : Group H} (f : H -> G) :=
  mono f /\ hom f.

Inductive trivial : Type := T.

Instance trivial_group : Group trivial :=
  {
    gunit := T;
    gadd := fun _ _ => T;
    ginv := fun _ => T
  }.
Proof.
  (* gadd_unit_l *)
  intros g.
  destruct g.
  reflexivity.
  (* gadd_unit_r *)
  intros g.
  destruct g.
  reflexivity.
  (* gadd_assoc *)
  intros.
  reflexivity.
  (* gadd_inv *)
  intros.
  split.
  reflexivity.
  reflexivity.
Qed.

Definition trivial_to_grp {G : Type} {Grp : Group G} (z : trivial) : G := gunit.

Theorem trivial_subgroup:
  forall (G : Type) (Grp : Group G),
  exists f : trivial -> G,
    subgroup trivial G f.
Proof.
  intros G Grp.
  exists trivial_to_grp.
  unfold subgroup.
  split.
  - (* mono f *)
    unfold mono.
    intros a b H.
    destruct a.
    destruct b.
    reflexivity.
  - (* hom f *)
    unfold hom.
    intros a b.
    destruct a.
    destruct b.
    unfold trivial_to_grp.
    rewrite -> gadd_unit_l.
    reflexivity.
Qed.

Coqだと「部分群」などの概念をうまく記述できないので、より圏論的な同等の定義(monoな射の存在とか)で代替したほうがうまく書けるものが多い気がします。