自然数(エンコーディングは問わず)の加算の可換法則、結合法則、分配法則を証明。

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。

まず、自然数全体の型 nat を定義する。

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

次にこの自然数上での足し算を計算する plus 関数を定義する。

Fixpoint plus x y :=
  match x with
  | O => y
  | S x => S (plus x y)
  end
where "x + y" := (plus x y).

まず一番簡単な足し算の結合則を証明する。

Proposition p01_plus_assoc :
  forall x y z, x + (y + z) = (x + y) + z.
Proof.
intros x y z; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

次に足し算の可換性を証明しようと思うが、そのために次の2つの補題を証明しておく。
ちなみに O+x = x と S x + y = S (x + y) は定義より明らかに成り立つことなので、あえて補題を用意することはしない。

Lemma plus_O : forall x, x + O = x.
Proof.
intro x; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

Lemma plus_Sy : forall x y, x + S y = S (x + y).
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

そして、足し算の可換性。

Proposition p01_plus_comm :
  forall x y, x + y = y + x.
Proof.
intros x y; induction x; simpl.
 rewrite plus_O in |- *; reflexivity.
 rewrite IHx in |- *; rewrite plus_Sy in |- *.
 reflexivity.
Qed.

あとは分配法則だが、これには掛け算が必要なので掛け算を定義する。

Fixpoint mult x y :=
  match x with
  | O => O
  | S x => y + mult x y
  end
where "x * y" := (mult x y).

左からの分配法則は簡単である。上で証明した足し算の結合則や可換性をバリバリ使っているのがわかるだろう。

Proposition p01_distr_l :
  forall x y k, k * (x + y) = k * x + k * y.
Proof.
intros x y k; induction k; simpl in |- *.
 reflexivity.
 
 rewrite IHk in |- *.
 rewrite <- (p01_plus_assoc x y _) in |- *.
 rewrite (p01_plus_assoc y (k * x) (k * y)) in |- *.
 rewrite (p01_plus_comm y (k * x)) in |- *.
 rewrite <- (p01_plus_assoc (k * x) y (k * y)) in |- *.
 rewrite (p01_plus_assoc x (k * x) _) in |- *.
 reflexivity.
Qed.

掛け算の可換性があれば右からの分配法則も示せるので、掛け算の可換性を証明。足し算の可換性と同様にいくつかの補題を証明して使った。

Lemma mult_O :
  forall x, x * O = O.
Proof.
intros x; induction x; simpl in |- *.
 reflexivity.
 apply IHx.
Qed.

Lemma mult_Sy :
  forall x y, x * S y = x + x * y.
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 
 rewrite IHx in |- *.
 rewrite (p01_plus_assoc y x (x * y)) in |- *.
 rewrite (p01_plus_comm y x) in |- *.
 rewrite <- (p01_plus_assoc x y (x * y)) in |- *.
 reflexivity.
Qed.

Lemma mult_comm :
  forall x y, x * y = y * x.
Proof.
intros x y; induction x; simpl in |- *.
 rewrite mult_O in |- *; reflexivity.
 
 rewrite mult_Sy in |- *.
 rewrite IHx in |- *.
 reflexivity.
Qed.

右からの分配法則。

Proposition p01_distr_r :
  forall x y k, (x + y) * k = x * k + y * k.
Proof.
intros x y k.
rewrite (mult_comm (x + y) k) in |- *.
rewrite (mult_comm x k) in |- *.
rewrite (mult_comm y k) in |- *.
apply p01_distr_l.
Qed.