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

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

(1 + 2 + ... + n) = n*(n+1) / 2の証明

この問題はCoqの自然数ライブラリを使った。まず\sum^{n}_{k=1}kを計算するsum関数を定義した。

Require Import Arith.

Fixpoint sum n :=
  match n with
  | O => O
  | S n => S n + sum n
  end.

自然数では割り算が難しいので、全体に2を掛けた次の形をまず証明する。

Lemma p02_aux : forall n, 2 * sum n = n * (n + 1).
Proof.
intro n; induction n.
 reflexivity.
 
 unfold sum in |- *; fold sum in |- *.
 rewrite mult_plus_distr_l in |- *.
 rewrite IHn in |- *.
 ring.
Qed.

自然数では割り算が自由にできないが、次のdiv2 という関数が標準ライブラリにあったのでそれを使った。

Require Import Div2.

Proposition p02 : forall n, sum n = div2 (n * (n + 1)).
Proof.
intros.
rewrite <- p02_aux in |- *.
rewrite div2_double in |- *; reflexivity.
Qed.

今回は自然数の範囲で証明したが、有理数上で証明した方がきれいだったかもしれない。Coqの標準ライブラリにはQArithというのがあり、有理数も標準的に扱うことができる。