目的

代数入門―群と加群 を読んでいたら自然数が加法,乗法について可換モノイドだと書いてあった気がするので、それを Coq/SSReflect で示します。 (実際はSoftware Foundations の第一章を SSReflect 使って解いただけ。)

可換モノイド

S が可換モノイドとは

  • 結合律 $$ \forall x, y, z \in S, (x \cdot y) \cdot z = x \cdot (y \cdot z) $$
  • 単位元の存在 $$ \exists e \in S, \forall x \in S , e \cdot x = x \cdot e = x $$
  • 可換 $$ \forall x, y \in S, x \cdot y = y \cdot x $$

を満たすことである。

  • 逆元の存在 $$ \forall x \in S, \exists x’ \in S, x \cdot x’ = x’ \cdot x = e $$

を加えると可換群になる。

自然数は加法と乗法について可換モノイドであるが可換群ではない。

準備

ssreflect を import する。

From mathcomp
     Require Import ssreflect.

Section addition.
  (* 自然数は加法に関して可換モノイド *)

  (* ここにコードを書く *)

End addition.

Section multiplication.
  (* 自然数は乗法に関して可換モノイド *)

  (* ここにコードを書く *)

End multiplication.

加法

結合律

Theorem plus_assoc:
  forall n m l : nat, (n + m) + l = n + (m + l).
Proof.
  move => n m l.
  elim n => [//= | n' H /=].
  rewrite H => //=.
Qed.
  • move => n m l.はintros n m l.と同じ。
  • elim n => X.はelim n; move => X.と同じ。
  • elim n.はinduction n.と同じ。
  • [//= | n' H /=]の部分は、それぞれの subgoal に対してmove =>で実行する。
  • move => //=.はreflexivity.と同じ。move => /=.はsimpl.と同じ。
  • rewrite H => //=はrewrite H; move => //=.と同じ。

同じことを ssreflect を使わずに書くと、

Theorem plus_assoc':
  forall n m l : nat, (n + m) + l = n + (m + l).
Proof.
  intros n m l.
  induction n as [|n'].
    reflexivity.
    simpl. rewrite IHn'. reflexivity.
Qed.

となる。

単位元の存在

0 が加法の単位元である。

Theorem plus_iden1:
  forall n : nat, 0 + n = n.
Proof.
  move=> //=.
Qed.

Theorem plus_iden2:
  forall n : nat, n + 0 = n.
Proof.
  move => n.
  elim n => [//= | n' H /=].
  rewrite H => //=.
Qed.

可換

ここで必要になる補題

Lemma plus_n_Sm:
  forall n m: nat, S (n + m) = n + S m.
Proof.
  move => n m.
  elim n => [//= | n' H /=].
  rewrite H => //=.
Qed.

これを用いて示す。

Theorem plus_comm:
  forall n m : nat, n + m = m + n.
Proof.
  move => n m.
  elim n => [//= | n' H /=].
  rewrite H plus_n_Sm => //.
Qed.

乗法

右分配法則

Lemma mult_plus_distr_r:
  forall n m l : nat, (n + m) * l = n * l + m * l.
Proof.
  move => n m l.
  elim n => [//= | n' H /=].
  rewrite H plus_assoc => //.
Qed.

結合則

Theorem mult_assoc:
  forall n m l : nat, (n * m) * l = n * (m * l).
Proof.
  move => n m l.
  elim n => [//= | n' H /=].
  rewrite -H mult_plus_distr_r => //.
Qed.

単位元の存在

1 が乗法の単位元である。

Theorem mult_iden1:
  forall n : nat, 1 * n = n.
Proof.
  move => n.
  elim n => [//= | n' H /=].
  rewrite plus_iden2 => //=.
Qed.

Theorem mult_iden2:
  forall n : nat, n * 1 = n.
Proof.
  move => n.
  elim n => [//= | n' H /=].
  rewrite H => //=.
Qed.

可換

ここで必要になる補題

Lemma mult_Sn:
  forall n m : nat, n + n * m = n * S m.
Proof.
  move => n m.
  elim n => [//= | n' H /=].
  rewrite -H -2!plus_assoc (plus_comm n' m) => //.
Qed.

これを用いて示す。

Theorem mult_comm:
  forall n m : nat, n * m = m * n.
Proof.
  move => n m.
  elim n => [//= | n' H /=].
  rewrite H mult_Sn => //.
Qed.

左分配法則

おまけ

Lemma mult_plus_distr_l:
  forall n m l : nat, n * (m + l) = n * m + n * l.
Proof.
  move => n m l.
  rewrite (mult_comm n (m + l)) (mult_comm n m) (mult_comm n l) mult_plus_distr_r => //.
Qed.

感想